Using a Declarative Process Language for P2P Protocols

Andrés A. Aristizábal, Hugo A. López, Camilo Rueda
Universidad Javeriana Cali
Colombia

Editor: Frank Valencia


Download PDF Version of this Article.


Abstract:

Peer-to-Peer (P2P) systems can be seen as highly dynamic distributed systems designed for very specific purposes, such as resources sharing in collaborative settings. Because of their ubiquity, it is fundamental to provide techniques for formally proving properties of the communication protocols underlying those systems. In this paper we present a formal model of MUTE, a protocol for P2P systems, in the SPL; a specification language with a striking resemblance to Concurrent Constraint Programming. Furthermore, we use the SPL reasoning techniques to show the protocol enjoys a secrecy property againts outsider attacks. By formally modeling and analyzing a popular (albeit never specified) protocol, we bear witness to the applicability of SPL as a formalism to model and reason about security protocols as well as flexibility of the its reasoning techniques.

Introduction

Peer-to-Peer (P2P) protocols are widely used for communication in distributed systems, providing an accurate and efficient way to perform certain important tasks, including information retrieval and routing. Protocols for P2P systems are then used to share private information between peers, which usually involves security risks. Currently these systems are dramatically receiving attention in research, development and investment. They had become a major force in the nowadays computing world because of its huge amount of benefits, such as its architecture cost, scalability, viability, and resource aggregation of distributed management resources. Essentially this kind of systems are used to obtain the major benefit from distributed resources to perform a function in a real decentralised manner. In this way, these systems are scalable since they avoid dependencies on centralised points, and they also have a low cost infrastructure, since they enable direct communication between the participants of these systems.

The P2P protocols used in various tools have to maintain a certain amount of important properties to guarantee its well functioning. One class of the most relevant P2P protocols are those concerned to security. Properties like secrecy, anonymity and non-traceability have been studied in the literature in order to overcome security risks [9]. Anonymity itself, is considered of the essence of any peer to peer protocol, since the participants on the network wish to establish communications and share resources without revealing their identity. Similarly, secrecy is considered crucial, since messages transmitted and managed between the distributed components in the network shall be kept as a secret for an entity outside the peer to peer group.

Despite the popularity of this kind of protocols, the importance of maintaining security matters within them and the existence of different calculi to reason about protocols, to the best of our knowledge, little has been done in modelling P2P protocols using process languages.

MUTE is a P2P tool for sharing and transmitting resources in a highly dynamic distributed network [12]. It is based on its particular searching protocol, which claims to guarantee an anonymous way of communicating data, in a secure way, through all the P2P network. In spite of being a very well known peer to peer protocol, MUTE has only been informally described.

We shall use SPL, a specification language for security protocols developed by Winskel and Crazzolara to give MUTE a formal specification for the first time. We then use SPL reasoning techniques to verify a secrecy property againts attacks of an outsider.

SPL has strong a similarity with Concurrent Constraint Programming (CCP) [13]. Just like CCP, SPL is operationally defined in terms of configurations containing items of information (messages) which can only increase during evolution. Such a monotonic evolution of information is akin to the notion of monotonic store central to CCP and a source of its simplicity.

One contribution of this paper is to give, to our knowledge, the first formal model of MUTE which abstracts away from details not concerned with secrecy issues. Another contribution is to bear witness of the applicability of SPL and its proof techniques for modelling and reasoning about protocols. The work in the present paper represent our first approach towards the use of SPL as formalism for specifying and verifying P2P protocols. The current work has been submitted to a workshop in P2P systems.

We shall proceed as follows: We extract a formal model directly from the implementation code. Then, using the SPL formalism along with its compositional power, we establish the formal specification of the MUTE protocol searching phase, modeling its components as a set of processes which work together to achieve the main goal of the protocol. Finally we use the proof techniques of SPL to prove a secrecy property for the messages in the network, taking into account an outsider malicious entity.

The paper is structured as follows. In the next section we present a brief summary of preliminaries, including a short introduction of the SPL calculus. In section 3, we explain the MUTE protocol, presenting an intuitive representation, as well as its formalisation on SPL. In the following section, we follow the SPL proof techniques scheme to verify the secrecy property for messages behind a passive outsider in the MUTE protocol. In section 5 we discuss some related work and in the last chapter we give out some concluding remarks, as well as future work.


Preliminaries

This section presents a brief overview of SPL (Security Protocol language), a process calculus for security protocols proposed by Winskel and Crazzolara in [3]. The full coverage of the calculus is given in [2].

SPL

SPL is a process calculus designed to model protocols and prove their security properties by means of transitions and event-based semantics. SPL is based on the Dolev-Yao Model [4], which states that cryptography is unbreakable and the spy is an active intruder capable of intercept, modify, replay and suppress messages. The calculus is operationally defined in terms of configurations containing items of information (messages) which can only increase during evolution, modelling the fact that, in an open network an intruder can see and remember any message that was ever in transit.

SPL Syntax

The syntactic entities SPL are described below:

\begin{figure*}\begin{center}
\subfigure[SPL Syntax]
{
{\footnotesize
\begin...
...e } p'_i = p_i $\ \\ \hline
\par
\end{tabular} }
}
\end{center}
\end{figure*}

The rest of the elements of SPL syntactic set are defined in Table 1(a), where Pub(v), Priv(v),  and $ Key(\vec{v})$ denote the generation of public, private and shared keys respectively. We use the vector notation $ \vec{s}$ to denote a list of elements, possibly empty, s1, s2, ..., sn.

Intuitive Description and Conventions

Let us now give some intuition and conventions for SPL processes.

The output process $ out \, new(\vec{x}) \, M.p$ generates a set of fresh distinct names (nonces) $ \vec{n}=n_1,n_2,\ldots ,n_m$ for the variables $ \vec{x}=x_1,x_2\ldots x_m.$ Then it outputs the message $ M[\vec{n}/\vec{x}]$ (i.e., $ M$ with each xi replaced with ni) in the store and resumes as the process $ p[\vec{n}/\vec{x}]$. The output process binds the occurrence of the variables $ \vec{x}$ in $ M$ and p. As an example of a typical output, $ p_A=out \, new(\vec{x}) \, \{x,A\}_{Pub(B)}.p$ can be viewed as an agent $ A$ posting a message with a nonce n and its own identifier $ A$ encrypted with the public key of an agent $ B$. We shall write $ out \, new(\vec{x}) \, M.p$ simply as $ out \, M.p$ if the $ \vec{x}$ is empty.

The input process $ in \, pat \, \vec{x} \vec{\chi} \vec{\psi} \,M.p$ waits for a message in the store that matches (the pattern) the message $ M$ for some instantiation of its variables $ \vec x$, $ \vec \chi$ and $ \vec \psi$. The process resumes as p with the chosen instantiation. The input process $ in \, pat \, \vec{x} \vec{\chi} \vec{\psi} \,M.p$ is the other binder in SPL binding the occurrences of $ \vec{x} \vec{\chi} \vec{\psi}$ in $ M$ and p. As an example of a typical input, $ p_B= in \, pat \, x,Z \,\{x,Z\}_{Pub(B)}.p$ can be seen as an agent $ B$ waiting for a message of the form $ \{x,Z\}$ encrypted with its public key $ B$: If the message of pA above is in the store, the chosen instantiation for matching the pattern could be $ n$ for $ x$ and $ A$ for $ Z$. When no confusion arises we will sometimes abbreviate $ in \, pat \, \vec{x} \vec{\chi} \vec{\psi} \,M.p$ as $ in \,M.p$.

Finally, $ \parallel _{i \in I}P_i$ denotes the parallel composition of all $ P_i$. For example in $ \parallel _{i \in \{A,B\}}P_i$ the processes $ P_A$ and $ P_B$ above run in parallel so they can communicate. We shall use $ !P = \parallel _{i \in \omega}P$ to denote an infinite number of copies of $ P$ in parallel. We sometimes write $ P_1 \parallel P_2 \parallel \ldots \parallel P_n$ to mean $ \parallel _{i \in \{1,2,\ldots n\}}P_i.$

The syntactic notions of free variables and closed process/message are defined in the obvious way. A variable is free in a process/message is has a non-bound occurrence in that process/message. A process/message is said to be closed if it has no free variables.

Transition Semantics

SPL has a transition semantics over configurations that represents the evolution of processes. A configuration is defined as $ \langle p,s,t\rangle$ where p is a closed process term (the process currently executing), s a subset of names $ \mathbf{N}$ (the set of nonces so-far generated), and $ t$ is a subset of variable-free messages (i.e., the store of output messages).

The transitions between configurations are labelled by actions which can be input/output and maybe tagged with an index i indicating the parallel component performing the action. Actions are thus given by the syntax $ \alpha ::= out \, new(\vec n)\, M ~\vert~ in \, M ~\vert~ i:\alpha.$ where $ \vec n$ is as a set of names, i as an index and $ M$ a closed message.

Intuitively a transition   says that by executing $ \alpha$ the process p with s and t evolves into p' with s' and t'. The new set of messages t' contains those in t since output messages are meant to be read but not removed by the input processes. The rules in Table 1(b) define the transitions between configurations. The rules are easily seen to realize the intuitive behaviour of processes given in the previous section.

Nevertheless, SPL also provides an event based semantics, where events of the protocol and their dependencies are made more explicit. This is advantageous because events and their pre and post-conditions form a Petri-net, so-called SPL nets.

Event-Based Semantics

Although transition semantics provide an appropriate method to show the behaviour of configurations, these are not enough to show dependencies between events, or to support typical proof techniques based on maintenance of invariants along the trace of the protocols. To do so, SPL presents an additional semantics based in events that allow to explicit protocol events and their dependencies in a concrete way.

SPL event-based semantics are strictly related to persistent Petri nets, so called SPL-nets [2] defining events in the way they affect conditions. The reader may find full details about Petri Nets and all the elements of a SPL-Nets in AppendixA [Editor Note: the appendix is available in the PDF version of this document] and [2], below we just recall some basic notions.

Description of Events in SPL

In the event-based semantics of SPL, conditions take an important place as they represent some form of local state. There are three kinds of conditions: control, output and name conditions (denoted by $ C$, $ O$ and $ N$, respectively). $ C$-conditions includes input and output processes, possibly tagged by an index. $ O$-conditions are the only persistent conditions in SPL-nets and consists of closed messages output on network. Finally, $ N$-conditions denotes basically the set of names $ \mathbf{N}$ being used for a transition. In order to denote pre and post conditions between events, let $ ^.e = \{^ce,^oe,^ne\}$ denote the set of control, name and output preconditions, and $ e^. =\{e^c,e^o,e^n\}$ the equivalent set of postconditions. An SPL event e is a tuple $ e = (^.e,e^.)$ of the preconditions and postconditions of e and each event e is associated with a unique action $ act(e)$. Figure 1 gives the general form of an SPL event. In the Appendix we will give the events for the protocol MUTE according to the SPL Event-Semantics. The exact definition of each element of the semantics can be can be found in [2]. For space limitations,here we shall recall some and illustrate others.

To illustrate the elements of the event semantics, consider a simple output event $ e=(\mathbf{Out}\left( out\, new \vec{x} M \right) ;\vec n)$, where $ \vec n = n_1 \dots n_t$ are distinct names to match with the variables $ \vec x = x_1 \dots x_t$. The action $ act(e)$ corresponding to this event is the ouput action $ out\, new \vec{n} M[\vec{n}/\vec{x}].$ Conditions related with this event are:


$ ^ce =\langle out \, new(\vec x).M.p , a\rangle$ $ ^oe=\emptyset$ $ ^ne= \emptyset $
$ e^c = \langle Ic( p[\vec n/ \vec x] ) \rangle$ $ e^o=\left\lbrace M[\vec n/\vec x]\right\rbrace$ $ e^n=\left\lbrace n_1, \dots n_t \right\rbrace$

Where $ Ic(p)$ stands for the initial control conditions of a closed process p: The set $ Ic(p)$ is defined inductively as $ Ic(X)=\{ X \}$ is $ X$ is an input or an output process, otherwise $ Ic (\parallel _{i \in I}P_i)=\bigcup_{i\in I}\{ i:c \ \vert \ c \in Ic(P_i)\}$

Figure 1: Events and transitions of SPL event based semantics. pi and qi denote control conditions, ni and mi name conditions and Ni, Mi output conditions. Double circled conditions denote persistent events.

Relating Transition and Event Based Semantics

Transition and event based semantics are strongly related in SPL by the following theorem from [2]. The reduction   where e is an event and $ M$ and $ M'$ are markings in the SPL-net is defined in the Appendix following the token game in Persistent Petri Nets (see Appendix A [Editor note: appendix available in the PDF version of the document]).

Theorem 2.1  
i)
If $ \langle p,s,t\rangle \stackrel{\alpha}{\longrightarrow} \langle p',s',t'\rangle$, then for some event e with $ act(e) = \alpha$,    formula in the SPL-net.
ii)
If $ Ic(p) \cup s \cup t \stackrel{e}{\longrightarrow}
\emph{M'}$ in the SPL-net, then for some closed process term p' for some $ s' \subseteq N$ and $ t'$ $ \in O$,   and M' $ = Ic(p') \cup s' \cup t'.$

Justified in the theorem above, the following notation will be used: Let e be an event, p be a closed process, $ s \subseteq N,$ and t $ \subseteq O.$ We write   iff $ Ic(p)
\cup s \cup t \stackrel{e}{\longrightarrow} Ic(p') \cup s' \cup t'$ in the SPL-net.

Events of a Process

Each process has its own related events, and for a particular closed process term p, the set of its related events Ev(p) is defined by induction on size, in the following way:

$ Ev(out \, new \, \vec{x} M.p)$ = $ \{$ Out $ (out \, new \, \vec{x} M.p; \, \vec{n}) \}$
$ \cup \bigcup \{Ev(p[\vec{n}/\vec{x}]) \}$
Where $ \vec{n}$ are distinct names
$ Ev(in \, pat \, \vec{x} \vec{\chi} \vec{\psi} M.p)$ = $ \{\textbf{In}(in \, pat \, \vec{x} \vec{\chi} \vec{\psi}
M.p; \, \vec{n},\vec{k},\vec{L}) \} \cup$
$ \bigcup
\{Ev(p[\vec{n}/\vec{x},\vec{k}/\vec{\chi},\vec{L}/\vec{\psi}]) \}$
Where $ \vec{n}$ names, $ \vec{k}$ are keys, and $ \vec{L}$ are closed messages
$ Ev(\Vert _{i \in I} p_i)$ = $ \bigcup _{i \in I} i : Ev(p_i)$

where, if $ E$ is a set, $ i:E$ denotes the set $ \{ i:e \ \vert \ e \in E\}.$

The MUTE protocol

The MUTE protocol works in a P2p network as a tool to communicate requests of keywords through the net, so that an specific file can be found and then received [12]. This protocol is composed of two main phases, the searching and the routing part. We will focus directly in its first phase, since it is the most related to the security concerns proposed in our work.

This protocol aims to provide an easy and effective search while protecting the privacy of the participants involved. It is inspired in the behaviour of ants in the search for food. The analogy is accomplished representing each ant as a node of a network, files requested as food, and pheromones as traces. In this way, one of the key properties of this model is the inherent anonymity of the protocol, because, like the ants that do not know the shortest path between the food and the anthill, peers are unaware of the overall environment layout and MUTE messages must be directed through the network using only local hints.1

Since the MUTE protocol claims to have anonymous users, none of the nodes in the P2P network knows where to find a particular recipient. Each node in the MUTE network contains direct connections to other nodes in the network in order to achieve its desired search. This nodes are called "neighbours" and through these, messages are secretly passed, either as a request or as an answer, in such a way that no agent outside the peer to peer network could manage to understand any of these data. Despite anonymity being essential on this protocol, secrecy is also one its main goals, since transmitted messages along the network involve information only concerned to the ones sharing the resources and must not be revealed to the outside world.


Dolev Yao Representation for the MUTE protocol

In spite of being already implemented and used as a tool for downloading and sharing files, to our knowledge MUTE has not yet been formally specified. Part of our work consists in abstracting from the code elements that have an impact in security.

We shall represent a P2P network as an undirected graph $ G$ whose nodes represent the peers and whose edges represent the direct connections among peers. We use $ \it {Peers}(G)$ to denote the set of all nodes in $ G$. Given a node $ X \in \it {Peers}(G)$, Let $ {\it ngb}(X)$ be the set of immediate neighbours of $ X$. We use the Dolev Yoe notation $ X \longrightarrow Y : M$ stating that $ X$ sends a message $ M$ to $ Y.$ For Example, consider a P2P network $ G$ with peers $ A,B$. Suppose that $ A$ is the initiator of the protocol and $ B$ is the responder. In this case, $ B$ can be any node inside the network, with the desired file on its store. So, $ A$ requests a particular file he wishes to download. For this purpose he sends the request to the network, by broadcasting it to his neighbours. This request includes a keyword $ kw \in Keywords$ which will match the desired file. Along the searching path an unknown amount of peers will forward the request until it reaches $ B$, a peer which has the correct file, st $ \exists f \in Files(B)$ and $ kw \in f$, where $ Files$ means the set of all files in the network, $ Files(A)$ means the set of files of the Agent or peer $ A$ in the network, $ Keywords$ the set of keywords associated to the files $ Files$, and $ Keywords(A)$ the keywords associated to the peer $ A$. Then, $ B$ sends its response by means of the header of the file, again by means of a broadcast through a series of forward steps, until it reaches the actual sender $ A$. Figure 2 give a representation of the above description using Dolev Yao notation [4].

Figure 2: Dolev Yao Model of the MUTE protocol
\begin{figure}\begin{center}
{\footnotesize
\begin{tabular}{lll}
$A \longrighta...
... & $(\{N,RES,M\}_{key(Z',A)},Z',A)$\ &
\end{tabular}}\end{center}\end{figure}

Here X, Y are variables which represent the forwarder peers along the path that goes from the Initiator to the responder node. This intermediate process may continue, until the target is reached. In the same way, these two variables will represent the peers which will forward the answer from the responder to the initiator. This process may be repeated several times as well.

Figure 3 illustrates a particular P2P network example in which $ A$ is the initiator, $ F_1,F_2,F_3$ are the peers involved in the forwarding process and $ B$ is the receptor that sends its answer via the same three forwarders.

Figure 3: A typical MUTE network topology

MUTE Specification on SPL

We use the core of the MUTE protocol in order to establish some security properties. The phases that we shall consider are the ones that involve the transmission of the keyword, the response message and the keys, leaving behind the phases of connection, and the submessages that include plaintext. We assume that $ key(A,B) = key(B,A).$ The formal model in Figure 4.

Figure 4: MUTE specification on SPL
\begin{figure}\par
{\footnotesize
\hspace{-0.3cm}
\begin{tabular}{lll}
{$Init...
...& $\equiv$\ & $\Vert _{A \in Peers(G)} Forward(A)$
\end{tabular}}\end{figure}

Intuitive description of the specification

We assume that the topology of the net has already been established. The agent starts searching for an own keyword. This agent broadcasts the desired keyword to all its neighbours. Its neighbours receive the message and see if the keyword matches one of their files, if at least one of the neighbours have the requested keyword, it will broadcast a response message, such that eventually the one searching for the keyword will get it and understand it as an answer to its request. The message will be forwarded by all the agents until it reaches its destiny. Otherwise, if the keyword does not match any file of the agent, then it will broadcast it to its neighbours asking them for the same keyword. The choice of having or not the right file is modeled in a non-deterministic way. This model abstracts way from issues such as the search for the best path, since it has no impact in secrecy.

MUTE Secrecy Proofs for a Passive Outsider

Here we will establish the secrecy of MUTE for a Spy outside the P2P network.

Definition of the Spy

We use the definition of a powerful spy used in SPL [2] to model the ways of intrusion and attack that an agent can do.
Figure 5: SPL spy model
\begin{figure}{\footnotesize
\begin{enumerate}
\item Compose different messages...
...y \equiv \Vert _{i \in \{1 \dots 9\}} Spy_i$
\par
\end{enumerate}}\end{figure}

In this way, the complete protocol includes the specification of MUTE, $ SecureMute$ in Figure 4, in parallel with the Spy:

$\displaystyle MUTE \equiv SecureMUTE \Vert !Spy$ (1)

Let us recall some elements. Let $ Headers$ be the set of headers of files, which is associated to $ Files$, $ Headers(A)$ the set directly related to $ Files(A)$, such that each header which belongs to $ Headers(A)$ will be associated to a unique file belonging to $ Files(A)$ (See section 3.1).

To analyze secrecy of a given protocol in SPL, one considers arbirtrary runs of the protocol.

Definition 3.1 (Run of a Protcol)   A run of a process p = p0 is a sequence

$\displaystyle \langle p_0,s_0,t_0 \rangle \stackrel{e_1}{\longrightarrow} \dots...
...ghtarrow} \langle p_w,s_w,t_w \rangle \stackrel{e_{w+1}}{\longrightarrow} \dots$    

We shall use in the theorems a binary relation $ \sqsubset$ between messages. Intuitively $ M \sqsubset M'$ means message $ M$ is a subexpression of message $ M'.$ (See Appendix B for the exact definition)

Secrecy Properties

In the following theorems we shall refer to the events of MUTE which for the sake of space are explicitely given in Appendix C.

The first secrecy theorem for the MUTE protocol concerns the shared keys of neighbours. If this shared keys are not corrupted from the start and the peers behave as the protocol states then the keys will not be leaked during a protocol run. If we assume that $ key(X,Y)$ $ \not \sqsubseteq$ t0, where $ X,Y$ $ \in$ $ Peers$, then at the initial state of the run there is no danger of corruption. This will help us to prove some other security properties for MUTE.

Theorem 3.2   Given a run of MUTE $ \langle \textrm{MUTE}\xspace ,s_0,t_0 \rangle \stackrel{e_1}{\longrightarrow} ...
...tarrow} \langle p_v,s_v,t_v \rangle
\stackrel{e_{v+1}}{\longrightarrow} \dots
$ and $ A_0,B_0 \in Peers(G)$, if $ key(A_0,B_0) \not \sqsubseteq
t_0$ then for each $ w \geq 0$ in the run $ key(A_0,B_0) \not \sqsubseteq t_w$

Proof. Outline Following the proof technique given in [2] the proof proceeds by stating a property associated with shared keys not appearing as a cleartext in the protocol. Then we assume a run which contains an event which violates the property stated before, and using dependencies among events within the protocol, we derive a contradiction. (The complete proof can be found in Appendix D1). By proving that shared keys never appear in the cleartext during a run of the protocol, we can guarantee that a Spy outside the P2P network cannot have access to them. Later on we will see the importance of this property for ensuring security in the protocol. $ \qedsymbol$

The following theorem concerns the secrecy property for the request. It states that the keyword asked by the initiator and broadcasted through the network will never be visible for a Spy outside the peer to peer group.

Theorem 3.3   Given a run of MUTE $ \langle \textrm{MUTE}\xspace ,s_0,t_0 \rangle \stackrel{e_1}{\longrightarrow} ...
...tarrow} \langle p_v,s_v,t_v \rangle
\stackrel{e_{v+1}}{\longrightarrow} \dots
$ , $ A_0 \in Peers(G)$ and $ kw_0 \in Keywords(A_0)$, if for all $ A$,$ B$ $ \in$ $ Peers(G)$, $ key(A,B)
\not \sqsubseteq t_0$, where $ B \in ngb(A)$ and the run contains the $ Init$ event a1 labelled with action
$ act(a_1) = Init : (A_0) : i_0 : B_0 :$
$ out \, new (n_0) (\{n_0,kw_0\}_{key(A_0,B_0)},A_0,B_0)$
where i0 is an index, $ B_0$ is an index which belongs to the set $ ngb(A_0)$, and n0 is a name, then for every $ w \geq 0$ in the run $ kw_0 \notin
t_w$

Proof. Outline Following the proof technique given in [2] the proof proceeds by stating that the shared keys are never leaked during a run of the protocol (Theorem 3.2). We state a stronger property $ Q$ which holds for all keywords not appearing as a cleartext during a run of the protocol. Then we assume an event which violates property $ Q,$ and using dependencies among events within the protocol we derive a contradiction. (The complete proof can be found in Appendix D2).

By proving that the keyword sent by the initiator peer as a request never appears in the cleartext during a run of the protocol, we can affirm that a Spy outside of the network will never know that keyword, so he will never recognise the file a sender is requesting. $ \qedsymbol$

The next theorem states that the message sent as an answer by the responder will never appear as a cleartext during a run of the MUTE protocol, and in this way nobody outside the peer to peer boundaries will understand it.

Theorem 3.4   Given a run of MUTE $ \langle \textrm{MUTE}\xspace ,s_0,t_0 \rangle \stackrel{e_1}{\longrightarrow} ...
...tarrow} \langle p_v,s_v,t_v \rangle
\stackrel{e_{v+1}}{\longrightarrow} \dots
$ and $ A_0 \in Peers(G)$ and $ res_0 \in Headers(B_0)$, if for all $ A$,$ B$ $ \in$ $ Peers(G)$, $ key(A,B)
\not \sqsubseteq t_0$, where $ B \in ngb(A)$ and if the run contains a $ Resp$ event $ b_2$ labelled with action

$ act(b_2) = Resp : (A_0) : i_0 : B_0 :$
$ out \, new (m_0) (\{n_0,res_0,m_0\}_{key(A_0,B_0)},A_0,B_0)$
where i0 is an index, $ B_0$ is an index which belongs to the set $ ngb(A_0)$ and n0, m0 are names, then for every $ w \geq 0$ $ res_0 \not \in t_w$

Proof. Outline The proof is analogous to that of Theorem 3.2 (The complete proof can be found in Appendix D3).

If we prove that the answer header sent by the receiver, never appears in the cleartext during a run of the protocol we can manage to guarantee that a Spy outside the peer to peer network will never know or access the file. $ \qedsymbol$

Related Work

To our knowledge, little work has been done in formalisation of P2P protocols using Process Calculi. In particular, the project Pepito [5] has started efforts in verification of properties using CCS variants in static versions of P2P protocols [1], in particular, correctness properties. Other analysis has been made for specific P2P functionalities, like [14] and [15]. However, to our knowledge, this is the first formal attempt using process calculi to model and reason about security properties in P2P protocols.

Concluding Remarks and Future Work

The use of process calculi allows us to formalise communication protocols leaving aside technical details, transforming complex distributed algorithms into abstract models syntactically close to their descriptions in pseudo-code. In particular, the use of SPL calculus lets us model several processes involved in the protocol without losing dependencies among them, in order to verify security properties along all the protocol path. In this way, these properties essential to communication (P2P) protocols can be easily verified. We demonstrate the above by giving the first formal description MUTE and by showing secrecy properties for messages wrt a passive outsider in the MUTE protocol. This bears witness of the specification power of SPL and its reasoning techniques.

We have proved the secrecy property for a passive outsider in the MUTE protocol. It will be interesting to explore security properties for threats inside the P2P network or an outsider who can masquerade as a trusted peer. Our future work will be the verification of the secrecy property for an insider in the MUTE protocol. In the same way, we shall explore the SPL expressiveness in order to model new cutting-edge protocols, using its own reasoning techniques, or extending it in order to verify other important security properties like non-traceability and non-malleability.

Bibliography

1
J. Borgstrôm, U. Nestmann, L. O. Alima, and D. Gurov.
Verifying a structured peer-to-peer overlay network: The static case.
In TBD, editor, Proc. Global Computing 2004, Lecture Notes in Computer Science, page TBD. Springer, 2004.

2
F. Crazzolara.
Language, semantics, and methods for security protocols.
Doctoral Dissertation DS-03-4, brics, daimi, May 2003.
PhD thesis. xii+160.

3
F. Crazzolara and G. Winskel.
Events in security protocols.
In ACM Conference on Computer and Communications Security, pages 96-105, 2001.

4
D. Dolev and A. C. Yao.
On the security of public key protocols.
Technical report, Dept. of Computer Science, Stanford University, Stanford, CA, USA, 1981.

5
S. Haridi and T. Sjôland.
Pepito - peer-to-peer: Implementation and theory, 2002.

6
G. Lowe.
An attack on the needham-schroeder public-key authentication protocol.
Inf. Process. Lett., 56(3):131-133, 1995.

7
G. Milicia.
$ \chi$-Spaces: Programming Security Protocols.
In Proceedings of the 14th Nordic Workshop on Programming Theory (NWPT'02), November 2002.

8
R. Milner.
Communicating and Mobile systems. The Pi Calculus.
Cambridge University Press, 1999.

9
D. S. Milojicic, V. Kalogeraki, R. Lukose, K. Nagaraja, J. Pruyne, B. Richard, S. Rollins, and Z. Xu.
Peer-to-peer computing.
Technical Report HPL-2002-57, HP Labs, March 2002.

10
C. Perkins.
IP Mobility Support - RFC2002.
IETF RFC Publication, 1996.

11
J. L. Peterson.
Petri nets.
ACM Comput. Surv., 9(3):223-252, 1977.

12
J. Rohrer and M. Roth.
Mute: Simple, anonymous file sharing, 2005.
Available at http://mute-net.sourceforge.net/howAnts.shtml.

13
V. Saraswat.
Concurrent Constraint Programming.
The MIT Press, Cambridge, MA, 1993.

14
M. Srivatsa and L. Liu.
Vulnerabilities and security threats in structured peer-to-peer systems: A quantitative analysis.

15
H. J. Wang, Y.-C. Hu, C. Yuan, Z. Zhang, and Y.-M. Wang.
Friends troubleshooting network: Towards privacy-preserving, automatic troubleshooting.
In G. M. Voelker and S. Shenker, editors, IPTPS, volume 3279 of Lecture Notes in Computer Science, pages 184-194. Springer, 2004.


Footnotes

... hints.1
Abstracting from the MUTE website, available at [12]