Primitives for authentication in process algebras.
We extend the &pgr;-calculus and the spi-calculus with two primitives that guarantee authentication. They enable us to abstract from various implementations/specifications of authentication, and to obtain idealized protocols which are "secure by construction". The main underlying idea, originally proposed in Focardi (Proc. Sixth Italian Conf. on Theoretical Computer Science, November 1998) for entity authentication, is to use the locations of processes in order to check who is sending a message (authentication of a party) and who originated a message (message authentication). The theory of local names, developed in Bodei et al. (Theoret. Comput. Sci. 253(2) (2001) 155) for the &pgr;-calculus, gives us almost for free both the partner authentication and the message authentication primitives.
Introduction
Authentication is one of the main issues in security and it can have different purposes depending on the
specific application considered. For example, entity authentication is related to the verification of an entity's
claimed identity [18], while message authentication should make it possible for the receiver of a message
to ascertain its origin [30]. In recent years there have been some formalizations of these different aspects of
authentication (see, e.g., [3, 7, 13, 16, 17, 22, 29]). These formalizations are crucial for proofs of authentication
properties, that sometimes have been automatized (see, e.g. [12, 15, 20, 21, 25]). A typical approach
presented in the literature is the following. First, a protocol is specified in a certain formal model. Then
An earlier version of Sections 7-9 appeared in [8]. This work has been partially supported by MURST Progetto TOSCA and
Progetto "Certificazione automatica di programmi mediante interpretazione astratta".
the protocol is shown to enjoy the desired properties, regardless of its operating environment, that can be
unreliable, and can even harbour a hostile intruder.
We use here basic calculi for modelling concurrent and mobile agents and we give then certain kinds
of semantics, offering built-in mechanisms that guarantee authentication. This is the main contribution
of our paper. Our mechanisms enable us to abstract from the various implementations/specifications of
authentication, and to obtain idealized protocols which are "secure by construction". Our protocols, or
rather their specifications can then be seen as a reference for proving the correctness of "real protocols".
The essence of concurrent and mobile computation can be studied in a pure form using the -calculus
[24], a foundational calculus based on the notion of naming. Systems are specified as expressions called
processes. These are obtained by combining, via a few operators (parallel composition, nondeterministic
choice, declarations), the basic actions of sending and of receiving names between processes along channels.
Names represent values, or messages, and also channels. Since processes exchange names in communica-
tions, the interconnection structure of a network can vary dynamically. Recently, Abadi and Gordon [3]
defined the spi-calculus by enriching the -calculus with primitives for encryption and decryption. The
resulting calculus is particularly suited to security issues, among which authentication.
In [6] the -calculus has been equipped with a structural operational semantics which endows each
sequential process P in the whole system with its own local environment, i.e., P has its local space of
names and its local name manager that generates a fresh name, whenever necessary. The basic ingredient of
this proposal is the notion of relative address of a process P with respect to another process Q: it represents
the path between P and Q in (an abstract view of) the network (as defined by the syntax of the calculus).
Note that relative addresses are not available to the users of the -calculus: they are used by the abstract
machine of the calculus only, defined by its semantics.
We propose here to use the ideas underlying this proposal to study authentication, both in the -calculus
and in the spi-calculus. As a matter of fact, this kind of semantics provides us with two built-in authentication
primitives. The key point is that P can use its address relative to Q to uniquely reach (the subterm of the
whole system representing) Q itself. Consequently, relative addresses may be used both to authenticate
the partners of a communication and to authenticate the origin of a message. For the sake of presentation,
we will first introduce our primitive for partner authentication in the -calculus, and the one of message
authentication in the spi-calculus. We can easily combine them, e.g. by introducing the first mechanism in
the spi-calculus so that both kinds of authentication can be enforced.
Partner authentication A variation of the semantics defined in [6] gives us a run-time mechanism that
guarantees each principal to engage an entire run session with the same partners, playing the same roles.
Essentially, we bind sensitive input and output communications to a relative address, i.e. a process P can
accept communications on a certain channel, say c, only if the relative address of its partner is equal to an
a-priori fixed address loc.
In order to achieve this, we index channels with relative addresses, so obtaining input actions on the
form c loc (x) or output actions of the form d loc 0 hMi. While sending a message, our semantics will check if
the address of the sender with respect to the receiver is indeed loc. In particular, assume that P is explicitly
waiting a message from a process reachable following loc, i.e. P performs the input action c loc (x). Then,
no possibly hostile process E having a relative address with respect to P different from loc, can successfully
communicate with P on c. Moreover, E cannot sniff any message M sent by P through the output action
d loc 0 hMi, if the address of E relative to P is different from loc 0 . These "located" I/O primitives enable
processes to have some control on their partners. As an example we can define, in the -calculus syntax, a
protocol that guarantees partner authentication by construction by putting in parallel the following processes:
where loc P represents the address of P relative to Q, chMi stands for sending M along c to every possible
process (the channel c is not indexed by any relative address, formally by the empty one), and c loc P (x) is an
input action located at loc P . The input can only match an output chMi executed by the process reachable
from Q through the relative address loc P . The resulting communication has the effect of binding x to M
within the residual of Q, yielding Q replaces x).
If we consider P , Q and also an intruder E in parallel, (P j Q) j E, the effect is to guarantee to Q
that the communication over c can only be performed with P . Thus, Q is assured that message M has been
indeed received by P . Note that there is no need for c to be a channel private to P and Q.
Although in this paper we focus on authentication primitives, it is interesting to note that located outputs
also guarantee a form of secrecy. As an example consider the following protocol where now P uses a located
output:
where loc Q is the address of Q relative to P . Consider again (P j Q) j E. Now, P is also guaranteed that
the communication over c will be only performed with Q, i.e., E cannot intercept M which will thus remain
secret. Again, the channel c needs not to be private to P and Q. So, we separately model authentication
and secrecy over public channels: our mechanism is thus more concrete than the use of a private channel for
communication.
In every protocol, legitimate processes may play a few different roles, such as sender, server, receiver,
etc. Usually, processes recognize the roles their partners are playing, but seldom they know which are
the partners' relative addresses. So, we shall also index a channel with a variable , to be instantiated
by a relative address, only. Whenever a process P , playing for instance the role of sender or initiator,
has to communicate for the first time with another process S in the role, e.g. of server, it uses a channel
c  . Our semantics rules will take care of instantiating  with the address of P relative to S during the
communication. Roughly, this implements a sort of anonymous communication. Note that the process S
could also be a hostile process pretending to be the server. However, from that point on, P and S will keep
communicating in the same roles for the entire session, using their relative addresses.
We have sketched how our mechanism guarantees that each principal communicates with the same
partners, in the same role, for the entire session. Through it, we also circumvent some problems arising from
mixing up sessions, in particular, those due to replay attacks. Usually, protocols use challenge-response
mechanisms, based e.g. on nonces (typically numbers used once), whose freshness protects from replay
attacks. In our framework, freshness is no longer needed to distinguish the communications of one session
from the communications of another.
Message authentication The semantics in [6] and its extension to the spi-calculus studied in Section 7 (see
also [5]) directly allow to define another authentication mechanism, providing us with a built-in primitive
that enables the receiver of a message to ascertain its origin, i.e. the process that created it. In fact, the
address of a message M relative to a process P , uniquely identifies the originator of M , even after the
message has been maliciously intercepted and forwarded. Indeed, we guarantee the integrity of the message
its receiver gets it as the originator of M made it. If M is a compound message, the receiver can
additionally ascertain the originators of the components of M . We write the primitive for authentication as
is a message and P is a process. 1 Intuitively, the execution of the process Q starts
only when the check [M @
succeeds, and this happens if and only if the relative addresses of M and of
P with respect to Q coincide: in other words, Q is the generator of M . Note again that this check is done
by the interpreter of the calculus, i.e. the semantic rules, not by the user.
A communication protocol that guarantees message authentication by construction is now easy to define,
by using the plain handshaking communication of the -calculus and the spi-calculus, and the primitive
sketched above. Suppose that a process P sends a message M (for simplicity we consider below a name) to
along a public channel c. In the spi-calculus syntax they have the following form:
where the operator (M) declares M to be a fresh name, different from all the others in the whole system.
If we put P , Q and also an intruder E in parallel, (P j Q) j E, the effect is to guarantee that the residual
of Q is indeed Q 0 [M=x]. Note that here Q is not guaranteed to receive the message directly from P , as
for partner authentication. As a matter of fact, the intruder might as well have intercepted the message M
originated by P and forwarded it to Q. This is legal as we are only checking that M has been originated
by P . As we will see, E cannot modify any of the parts of M without changing the relative address of M
itself, because relative addresses are manipulated by the semantics only. Also in this case, there is no need
for c to be a channel private to P and Q.
Our solutions assume that the implementation of the communication primitives has a reliable mechanism to
control and manage relative addresses. In some real cases this is possible, e.g., if the network management
system filters every access of a user to the network as it happens in a LAN or in a virtual private network.
This may not be the case in many other situations. However, relative addresses can be built by storing the
actual address of processes in selected, secure parts of message headers (cf. IPsec [31]). Yet, our solutions
may help checking the correctness of different implementations, e.g. those based on cryptography, as briefly
discussed in the conclusion.
Contents of this paper In Section 2 we survey the -calculus; in Section 3, we recall relative addresses
and in Section 4 the proved version of the -calculus from [6]. Section 5 is devoted to partner authentication.
In Section 6 we survey the spi-calculus and in Section 7 we enrich it with the relative address mechanism.
Sections 8 and 9 are about the message authentication primitive.
2 The -calculus
In this section we briefly recall the monadic -calculus [24], a model of concurrent communicating processes
based on the notion of naming. Our presentation slightly differs from the usual ones and it will make it
easier to introduce later on the spi-calculus The main difference from standard presentation relies in the
introduction of the new syntactic category of terms, where names and variables are distinguished.
Definition 2.1 (syntax) Terms (denoted by (denoted by
are built according to the syntax
1 Actually, we have [M @
is a message from P ; see the formal development for details.
prefix
(m)P restriction
matching
replication
where  may either be M(x) for input or MhNi for output.
Hereafter, the trailing 0 will be omitted. We often write ~  to denote tuples of objects, for instance ~
m for the
vector actually we feel free to consider and to operate on ~
m as if it were a set. Notations are
extended componentwise, e.g. (~n) stands for (n 1 finally,
means that there are no restricted names.
Intuitively, 0 represents the null process which can do nothing. The prefix  is the first atomic action that
the process :P can perform. After the execution of  the process :P behaves like P . The input prefix
M(x) binds the name x in the prefixed process as follows: when a name N is received along the link named
M , all the (free) occurrences of x in the prefixed process P are substituted with M . The output prefix
MhNi does not bind the name N which is sent along M . Summation denotes nondeterministic choice. The
process . The operator j describes parallel composition of processes.
The components of P 1 jP 2 may act independently; also, an output action of P 1 (resp. P 2 ) at any output port
may synchronize with an input action of P . The value sent by P 1 replaces the relevant
occurrences of the placeholder x in P 2 . The operator (m) acts as a static declaration (i.e. a binder for) the
name m in the process P that it prefixes. In other words, m is a unique name in P which is different from
all the external names. The agent (m)P behaves as P except that actions at ports m and m are prohibited.
However communications along link m of components within P are allowed. Matching is an
if-then operator: process P is activated only if . Finally, the process !P behaves as infinitely
many copies of P running in parallel.
We write fn(M) and fn(P ) for the sets of names free in term M and process P , respectively, and fv(M)
and fv(P ) for the sets of variables free in term M and process P , respectively. A closed term or process is a
term or process without free variables.
2.1 Semantics.
The semantics for the -calculus we consider here is a late semantics, based on a reduction relation and on a
commitment relation. Some structural congruence rules are also needed. The commitment relation depends
on the abstraction and concretion constructs:
An abstraction has the form (x)P , where (x) binds x in P .
A concretion has the form ( ~
m)hMiP , where M is a term, P is a process and the names in ~
are
bound by ( ~
m) in M and P .
An agent A or B is an abstraction, a concretion or a process.
If F is the abstraction (x)P and C the concretion ( ~
m)hMiQ and f ~
then the interactions
F@C and C@F are:
m)(P [M=x] j Q)
Congruence. The structural congruence  on processes is defined in the standard way, except for the
treatment of parallel composition that is assumed to be neither commutative nor associative. It is then
defined to be the least congruence satisfying:
if P and Q are -equivalent then P  Q;
is a commutative monoid;
m)hMi(R j Q); and ( ~
m)hMiQ
In the following, we will never distinguish congruent terms.
Reduction relation. The reduction relation > is the least relation on closed processes that is transitive
and closed under all contexts, and that satisfies the following axioms:
Red Repl !P > P j !P
Red Match
Commitment relation. An action is a name m (representing input) or a co-name m (representing output)
or a distinguished silent action  . Note that actions record only the channel on which the input or the output
occurs. The commitment relation is written P  ! A, where P is a closed process,  is an action, and A is
a closed agent. It is defined by the rules in Tab. 1.
3 Relative Addresses and their Composition
We recall here the ideas of [6] that serve as a basis for the authentication mechanisms we are going to
introduce. Consider for a while the binary parallel composition as the main operator of the -calculus
(neither associative nor commutative). Then, build abstract syntax trees of processes as binary trees, called
trees of (sequential) processes, as follows. Given a process P , the nodes of its tree correspond to the
occurrences of the parallel operator in P , and its leaves are the sequential components of P (roughly, those
processes whose top-level operator is a prefix or a summation or a replication). A tree of processes is
depicted in Fig. 1.
Comm Out
Comm In
Comm Sum 1
Comm Sum 2
Comm Par 1
Comm Par 2
Comm Inter 1
Comm Inter 2
Comm Res
Comm Red
Comm Struct

Table

1: The commitment relation.

Figure

1: The tree of (sequential) processes of (P
Assume now that the left (resp. right) branches of a tree of sequential processes denote the left (resp.
right) component of parallel compositions, and label their arcs with tag jj 0 (resp. jj 1 ). Therefore, any
sequential component in a process is uniquely identified by a string # over fjj . The string corresponds
to a path from the root, the top-level j of the whole process, to a leaf. Intuitively, # is the address of the
sequential component relative to the root of the binary tree.
Consider now two different sequential processes, say G and R, in a tree and call the path between them
the address of the process G relative to the process R. This relative address can be decomposed into two
parts according to the minimal common predecessor P of G and R in the tree. The relative address is then a
string written # 0 , made of jj 0 's and jj 1 's, where # represents the path from P to R, 2 and # 0 the path from
P to G. Let G and R respectively be the processes P 3 and P 1 of Fig. 1. The address of P 3 relative to P 1
is then jj 0 jj 1 jj 1 jj 1 jj 0 (read the path upwards from P 1 to the root and reverse, then downwards to P 3 ). So to
speak, the relative address points back from R to G.
Relative addresses can be composed, in order to obtain new relative addresses. For instance, the composition
of the relative address jj 1 jj 0 jj Fig. 1) with the relative address of P 3 w.r.t.
is the relative address jj 0 jj 1 jj 0 of P 3 w.r.t. P 2 .
Below we recall the formal definition of relative addresses and we define their composition. More
intuition, the full definitions and the statements of some of their properties are in [6].
Definition 3.1 (relative addresses)
be the empty string, and let  be the sum modulo 2. Then, the set of relative
addresses, ranged over by l, is
We will sometimes omit  in relative addresses, e.g. we write n for  n.
A relative address l compatible with l, written l
As we said before, we use relative addresses to encode paths between pairs of nodes of binary trees of
processes, like the one in Fig. 1. Note that the condition jj 0 # 0
explicit that
the two components of the relative address describe the two distinct paths going out from the same node in
a binary tree. Also, l both refer to the same path, exchanging its source and target.
2 For technical reasons we take the path from P to R instead of the more natural path from R to P .
Address composition is a partial operation, defined only when relative addresses can indeed be com-
posed. We make sure that this is always the case when we apply it. Fig. 2 depicts all the cases in which this
happens.
Definition 3.2 (address composition) Address composition is defined by the following
three exhaustive cases:
1.
2.
3.
It is immediate to see that ? has a neutral element (i.e. l ? an inverse for each element (i.e.
the inverse of l is l 1 ) and that ? is associative (i.e. (l ? l
G  R  S
(1) (2) (3)

Figure

2: The three possible relative placements of three processes G, S, and R. The result of the composition
of the relative addresses of S w.r.t. R and of G w.r.t. S is represented by the solid arrows.
4 Proved semantics
Relative addresses can be inductively built while deducing transitions, when a proved semantics is used
[9]. In this section, we recall from [10] the proved transition system for the -calculus, in which labels of
transitions encode (a portion of) their deduction tree. The arrows of the proved transition system are labelled
by @#, where  is an action and # is a string of jj used to single out the sub-process that actually
performed . The rules for proved commitment are in Tab. 2. They are essentially those of the standard
transition system except for those involving the parallel operator. Rule Comm Par 1 (respectively, Comm
Par 2) adds in the label of its conclusion the tag jj 0 (respectively, jj 1 ) to register that the left (respectively,
right) component of a parallel composition is moving. The rules defining the congruence and the reduction
relation are indeed the same as before. To recover the standard semantics of the -calculus, we only need to
erase any occurrence of # from the labels of transitions.
Note that the information added to labels can be used to inductively build relative addresses. Indeed, the
tags jj i are sufficient to recover the parallel structure of a process P because they provide an encoding of the
tree of processes of P . For instance, suppose that process :P performs the transition @jj 0 . Then, we know
that the -action was performed by a sequential process on the form :P in parallel with some process Q.
Indeed, the whole system had the form :P jQ. More generally, if a process R performs a transition @#,
the path # in the tree of processes permits to reach the sub-process that performs the  action. Technically,
we indicate the sub-process R as P@#, which is inductively selected through the following operator.
Comm Out
Comm In
Comm Sum 1
Comm Sum 2
Comm Par 1
Comm Par 2
Comm Inter 1
Comm Inter 2
Comm Res
Comm Red
Comm Struct

Table

2: The proved commitment relation.
Definition 4.1 The localization operator @# is defined on processes by induction as follows:
1.
2. ((m)P
3.
4.
This definition will be helpful at the end of Sections 5 and 8.
Back to Fig. 1, if P 3 communicates with P 1 , the whole process
a computation step. The sub-process P 3 performing the output is Sys@jj 1 jj 1 jj 0 and the sub-process P 1
performing the input is Sys@jj 0 jj 1 . By putting together the single paths, we obtain the relative address
5 Partner authentication
We now introduce our first authentication mechanism. At run-time, it will guarantee each principal to engage
an entire run session with the same partners playing the same roles. We heavily exploit the proved semantics
reported in the previous section. We essentially bind sensitive input and output communications to relative
addresses. More precisely, channels may have a relative address as index, and assume the form c l . Now, our
semantics will ensure that P communicates with Q on c l if and only if the relative address of P w.r.t. Q is
indeed l (and that of Q w.r.t. P is l 1 ). Notably, even if another process R 6= Q possesses the channel c l ,
R cannot use it to communicate with P . Consequently, a hostile process can never interfere with P and Q
while they communicate, not even eavesdrop the exchanged messages.
By using these "located" channels, processes may have some control on their partners. But often a
process P is willing to communicate with several processes, usually through one or very few channels. So,
we shall also index a channel with a variable  to be instantiated. Suppose that process P , playing for
instance the role of sender or of initiator, wants to communicate with a process S (e.g. the server), that P
does not know the relative address of S, say l, and finally that the involved channel is c  . Then, during the
first communication of P with S,  will be instantiated within P by l (recall that our proved operational
semantics indeed computes l). Symmetrically for S, if it uses the same channel c (with a different variable
uses c  0 ). In a sense, this is the case of anonymous communication. Note however that S may
as well use an already located channel c l 0 : the communication occurs only if l From that point on,
P and S will keep communicating in the same roles for the entire session, using their, now known, relative
addresses.
Thus, we extend the names that occur in processes by indexing them with a location, defined to be either
a relative address or a variable  to be instantiated by a relative address. Formally,
Definition 5.1 Let  3 ;  be a countable set of (address) variables, and let t.
is the set of located channels.
Usually, the empty location
The rules defining the congruence and the reduction relation are the same as before, apart from the obvious
substitution of located names for names. The rules for the new commitment relation are in Tab. 3, where
we omit the symmetric rules for communication. The rules for parallel composition are in the proved style,
Comm Out
Comm In
Comm Sum 1
Comm Par 1
Comm Inter L 1
l 0
if
(l
Comm Inter
where l
Comm Inter  1
Comm Res
Comm Red
Comm Struct

Table

3: The proved located commitment relation.
recording which component (left or right) of the process is moving. There, some of the arrows are annotated
also with a location. For each I/O action rule, the location t of the channel involved is recorded under the
arrow, and it is preserved by all non communication rules and discarded by communications. This location
t is used in the premises of communication rules, to establish the relative addresses of one process with
respect to the other. In fact, if the first process (the receiver) performs an input m@# and the second process
(the sender) performs the complementary output action m@# 0 , then the relative address of the sender with
respect to the receiver is jj 0 #jj 1 # 0 . (The additional jj 0 and jj 1 record that the two processes are the left and
the right partners in the communication.)
There are three different rules, up to symmetries, for every communication between two processes, say
P and Q. We comment on them, and we intuitively relate them with the three possible situations in which
P and Q may be.
Comm Inter L 1 P wants to receive from a process located at l, and Q wants to send to a process located
at l 0 . For the communication to happen the relative addresses of Q w.r.t. P and of P w.r.t. Q (the path
established by the communication) should coincide with these locations that should be compatible,
i.e. l as the side conditions require. This situation reflects the fact that P and Q "know each
other", possibly because they have previously established their connection and are session partners.
Note that when l and l 0 are , we recover the "non-located" communication of the standard -
calculus.
Comm Inter wants to receive from a process located at l, while Q is willing to send a message to
any process (it sends on a channel with location variable  0 ). The communication is successful only if
l coincides with the path established by the communication, i.e. if l coincides with the relative address
of indeed the process from which P wants to receive. After the communication,  0
will be suitably bound to l 1 (the relative address of P w.r.t. Q) within Q, so that now P and Q "know
each other".
If l is the empty location, then the communication is always successful and  0 will still be replaced by
the relative address of P w.r.t. Q.
Comm Inter  1 P and Q do not "know each other" and are willing to communicate with any partner. So,
they exchange their relative addresses, as established while deducing the premises. Intuitively, P and
are performing their initial synchronization. So their two variables are replaced with the relative
address of Q w.r.t. P and vice-versa (l and l 0 , respectively).
Variables are not located. Consequently, when a located channel c l is communicated, it becomes a "free"
channel: the location l is lost. The index to c becomes  if so it was; otherwise we get c  (with  not
occurring in the process). Formally, we have the following.
Definition 5.2 Let (y)P be a abstraction and l iQ be a concretion. Then, their interaction
is
otherwise (with  not occurring in Q)
Symmetrically for C@F .
Using the above definition for communication makes it easier to use a channel in a multiplexing way. Suppose
that a process P is committed to communicate on a channel c l with a process Q. Also, assume that
sends c l to a third party R, that receives it as c  . The "same" channel c can now be used for further
communications between P and Q (in this case located at l), as well as for communications between R and
some other process (after  has been suitably instantiated).
In the rules for commitment we use the particular kind of substitution fjl=jg @# , called selective routed
substitution. It uses a particular substitution fjl=jg, called routed, to be applied only to the sub-process
located at #. The routed substitution takes into account the parallel structure of the process. For that it
updates the relative addresses l while traversing the tree of processes. For instance, to substitute # 0 for
in P 0 jP 1 requires to substitute jj i  ? # 0 for  in each component P i .
Definition 5.3 The location routed substitution fjl=jg is defined by induction as follows:
1.
l otherwise
2. (m  hMi:P
3. (m  (x):P
4.
5.
7.
There is no case for !P in the above definition, i.e. the routed substitution may be applied only to P , after
that !P has been reduced to P j!P . This amounts to saying that we are also considering processes that
inside have routed substitutions not fully performed. Consequently, the target of the transitions in Tab. 3
may contain expressions on the form !P fjl=jg. In order not to burden too heavily our notation, we shall still
use P and A for processes, abstractions and concretions with substitutions not yet performed.
We use the above definition to implement a selective substitution that works on the sub-process of a
whole term reachable through #.
. Then, the selective routed substitution Pfjl=jg @# is defined by induction
as
The very fact that channels have indexes, which may also be instantiated, guarantees that two partners can
establish a connection that will remain stable along a whole session. Indeed, let
(note that jj 0 jj 1 is the address of R relative to Q). Then, it is immediate verifying that Q
accepts inputs on c only if they come from R; of course this property remains true for all inputs of Q along
. Symmetrically for the process
Example 5.5 We now illustrate our partner authentication mechanism, through some simple examples. First
of all, consider a single message exchange between Alice, A and Bob, B:
where  and  0 are two location variables. After the message exchange, the semantic rule Comm Inter  1
instantiates  and  0 in A 0 and B 0 , respectively, with the address of A relative to B (i.e., jj 1 jj 0 ) and of B
relative to A (i.e., jj 0 jj 1 ), respectively.
Intuitively, the instantiation of a  with an l represents a secure declaration of the identity of a process
through its location l, that cannot be manipulated even by malicious parties. As we will see later on, located
actions also give some security guarantees on the subsequent message exchanges.
Example (cont'd) Consider now the following protocol (recall that d  is simply written as d; we shall
comment below on the use of channel d, which occurs located in A 0 but not in B 0 ).
Here, Bob sends a message to Alice after the reception of MA . Note that Alice is requiring that the second
message comes from the same process to which she sent MA . Since, after the first message exchange, the
variable  is instantiated to the address of B 0 relative to A 0 , our semantics guarantees authentication of the
second communication with respect to the (secure) identity declaration of : Alice is assured that the second
message will be sent from the same process that received the first one. In order to illustrate this important
point we add another process C which tries to communicate over channel d. The
process has the following steps:
Since the address of C 0 relative to A 0 is jj 0 jj 0 jj 1 6= jj 0 jj 1 , then either (the residual of) A 0 receives from and
only from (the residual of) B 0 or B 0 and C 0 communicate. In the first case we have:
In the second case we have:
In the example above, the same channel d is used in two different ways: it is "located" for Alice and Bob;
alternatively, it is "free" for B 0 and C 0 . In Example 5.9, we shall see that the same channel can be even used
in a multiplexing fashion: two pairs of processes can interleave their communications, still presenting the
property of being engaged with the same process along the entire session.
In the next example we consider the situation where the channel d is located and used to output a message
M . This usage of channels also guarantees a sort of secrecy of M .
Example 5.6 We have seen in the previous example that message MB was intercepted by C 0 , thus violating
its secrecy. Consider now the following protocol:
Here, Bob is requiring that the message MB is received by the same user that sent the first message. In this
case Bob obtains a form of secrecy: he is assured that MB will be read by the process identified by  0 , i.e.,
the process that sent message MA . Indeed, any new process C to read MB . We have that
but the address of C 00 relative to B 00 is jj
We have seen that locating inputs and outputs corresponds to guaranteeing authentication and secrecy of the
communication, respectively. We can summarize these two concepts as follows. In a message exchange and
with respect to an address l, a process obtains
Partner authentication whenever it receives the message from the process reachable at l, only.
Secrecy whenever only the process reachable at l will receive the message.
We now state the above more precisely, exploiting Def. 4.1. We need the notion of context with two holes,
Theorem 5.7 (authentication) Let ^
PROOF. By inspection on the rules used to deduce the transition; in particular consider the side conditions of rules
Comm Inter L 1 (where
Theorem 5.8 (secrecy) Let ^
PROOF. Analogous to the previous proof.
The next example illustrates how locating both inputs and outputs guarantees a permanent hooking between
two parties and allows to model multiple sessions quite easily.
Example 5.9 Consider the following processes:
~
~
~
Indeed both Alice and Bob are assured that the second message (and also all the subsequent messages
sent and received on located channels) will be sent/received by the user that interacted in the first message
exchange. Hence, the two users, after the first communication are permanently hooked together. This time
a third user ~
indeed able to take the place of ~
B in the communication but only if it
starts the session with ~
A. Instead, it can never communicate with ~
A after the first message exchange between
~
A and ~
We now model multiple sessions. Consider ~
B, where an unbounded number
of instances of Alice and Bob are present, each with a different fresh message. Consider now two instances
of ~
A sending their first messages to two instances of ~
B, i.e, two parallel sessions:
~
Note that after the first message exchange the partners in each session are permanently hooked: the second
message is always sent to the correct party, the one who initiated the session. As a consequence, no replay
of messages is possible among different sessions, also in the presence of a malicious party.
6 The Spi-Calculus
Syntax. In this section we briefly recall, often also literally, the spi-calculus [3], in its monadic version
from [1]. This calculus is an extension of the -calculus, introduced for the description and the analysis
of cryptographic protocols. A first difference with the -calculus is that the spi-calculus has no summation
operator +. Also, terms can be structured as pairs (M;N ), successors of terms suc(M) and encryptions
. The last term above represents the ciphertext obtained by encrypting
the key N , using a shared-key cryptosystem such as DES [27].
Definition 6.1 Terms and processes are defined according to the following BNF-like grammars.
names
x variables
suc(M) successor
shared key encryption
prefix
(m)P restriction
matching
replication
let in P pair splitting
case M of case
case L of fx in P shared key decryption
where  may either be M(x) or MhNi. 3
Most of the process constructs are the same of -calculus. The new ones decompose terms:
The process let (x; in P behaves as P [M
is not a
The process case M of is 0, as Q[N=x] if
is stuck otherwise;
The process case L of fx in P attempts to decrypt L with the key N ; if L has the form
then the process behaves as P [M 1 =x and otherwise is stuck.
The structural congruence and the operational semantics for commitment are exactly the same of the -
calculus given in Table 1. Some new reductions rules are instead needed.
Red Split let (x;
Red Zero case 0 of
Red Suc case suc(M) of
Red Decrypt case fM N of fx
7 Names of the spi-calculus handled locally
To introduce our second authentication mechanism, we need to further exploit the ideas contained in [6],
where the relative addresses, introduced in Section 3, are used to handle names locally to sequential processes
in an operational manner. The space of names of a whole process is then partitioned into local
environments associated each with its sequential sub-processes.
To avoid global management of names, we have to solve two problems. Names have to be declared
locally and to be brand-new in that local environment. Furthermore, when a name is exported to other local
environments via communications or by applying a reduction rule, we must guarantee that there are no
clashes involving the other names around. A purely mechanical way of doing that is in [6].
For the sake of simplicity, instead of recalling also the mechanism for generating fresh names, here we
assume that a name is fresh, whenever needed, and we shall recall that by a side condition.
As for keeping names distinct, consider two different sequential processes, say G and R, that have two
syntactically equal names, say n. Suppose now that G sends n to R. To distinguish between the two different
instances of n in the local environment of R, the name generated by G will be received enriched with the
address of G relative to R, which points back from R to the local environment of G.
A slightly more complex situation arises when a process receives a name and sends it to another process.
The name must arrive at the new receiver with the address of the generator (not of the sender) relative to the
new receiver. Consider again Fig. 1, where P 1 sends to P 2 a name generated by P 3 . The rules (in Tab.
for communication use address composition to determine the address of P 3 relative to P 2 , by composing the
address of the message (recording the address of P 3 w.r.t. with the relative address of P 1 w.r.t. P 2 .
We carry the localized semantics of the -calculus of [6] on the monadic spi-calculus. First of all, we
introduce the new set of localized names, that are names prefixed with relative addresses.
Although M is an arbitrary term, we only consider it to be a name or a variable (to be instantiated to a name), because these
are the only useful cases (see [3]).
Definition 7.1 Let N be the set of localized names, where N is the set of standard names and
"" is the operator of language concatenation.
For simplicity, we assume possibly indexed, to range over both N 0 and N and, unless necessary,
we do not syntactically distinguish localized terms from terms, i.e. terms prefixed with relative addresses
like from those not prefixed.
As we said above, we do not recall how the mechanism of [6] generates fresh names whenever needed:
here we simply assume them fresh. However, we require that restricted names are always localized, i.e.
they occur in a declaration as (n). Technically, this is achieved by transforming a process P with (n)
into a new process, obtained by replacing each sub-process of P on the form (n)Q with the process
(n)Qfjn=njg s (the substitution fj=jg s is in Def. 7.3).
When a term M is exported from a process, say P , to another, say Q, it is necessary to compose the
relative address prefixing M with the relative address of P w.r.t. Q. This composition is performed by the
term address composition, that extends address composition in Def. 3.2. Applied to a relative address and
to a localized term, it returns an updated localized term.
Definition 7.2 Term address composition ? T is defined as
We say that , is the term # exported to the relative address # 0 .
Names in N , variables and natural numbers are not prefixed with relative addresses and are insensitive to
address composition:
We now explain how our semantics deals with terms. First, note that the operator ? T considers the compound
term M as a whole, as it does not distribute address composition over the sub-terms of M . Now, consider the
encryption term fMgK . It is an atomic entity, and so it is handled as it were a new name, local to the process
that encrypts M , say P . The two localized terms M and K are frozen just like they were at encryption time,
and their own relative addresses are not changed when the encrypted message is sent through the net; again,
these relative addresses cannot be updated. Since fMgK is atomic, its relative address, say #
always point to the process P that made the encryption. (Technically, M and K are frozen like they were
in the process S containing all the restrictions on the names used in the encryption.) In this way, when
decrypting fMgK the semantic rules recover the correct addresses for M and K by simply composing the
actual address of fMgK , # 0 # 1 , with the (frozen) relative addresses of M and K , respectively. The same
management described above is used for successor and pairs. In the first case, the term M is frozen in
suc(M), while the terms M and N are frozen in (M;N).
Also the routed substitution of Def. 5.3 is extended to deal both with terms and with processes in the
spi-calculus; it distributes to each sub-term or sub-process (note that below the term N cannot be a variable).
Definition 7.3 The spi routed substitution fjN=xjg s is defined by induction as follows on
terms
1. rfjN=xjg
2. zfjN=xjg
z x 6= z
3. 0fjN=xjg
4. suc(M)fjN=xjg
5.
processes
1. 0fjN=xjg
2. (rhMi:P )fjN=xjg
3. (r(y):P )fjN=xjg
4.
5.
7. (let (y
8. (case M of
case MfjN=xjg s of
case MfjN=xjg s of
9. (case L of fy in P )fjN=xjg
case LfjN=xjg s of fx MfjN=xjgs in P
case LfjN=xjg s of fx MfjN=xjgs in PfjN=xjg s otherwise.
Now, the selective routed substitution for the spi-calculus is exactly as in Def. 5.4.
Localized Congruence. The rules for the structural congruence require some changes to accommodate
localized names.
1.
2.
3.
4.
Note that no -conversion is needed: each binding occurrence of the name r in P 1 replaced
by which is different from any name s in P 1 because of the properties of
address composition ?.
Localized Reduction Relation. We add the following reduction rules to those for matching and replication

Red Split let (x;
Red Suc case # 0 # 1 suc(M) of
Red Decrypt case # 0 # 1 of fy
When a process decomposes a term, the involved sub-terms are updated. The intuition for the decryption
rule is that we can decrypt a message fMgN only if we use the key which is exactly how
the frozen key N should appear to the receiver of the encrypted message. When K and N , although starting
from different sites, do refer to the same key, the semantic rules decrypt the message and update its relative
address by composing # 0 # 1 and M . The process P then behaves as Pfj# 0
Localized Commitment Relation. Eventually, we present in Tab. 4 the extended commitments rules. The
localized commitment relation is written P @# ! A, where P is a process,  is the action, performed by the
sub-process at #, and A is an agent.
The component # of labels is needed for checking some side conditions of a few rules. Communication
rules are successful only if the complementary actions refer to the same name; while for the restriction rule
it is necessary to check that there are no clashes between the action and the restricted name. The semantic
rules update the messages with the relative addresses of the sender with respect to the receiver. Indeed,
the congruence rules lift relative addresses and restrictions as much as needed. For instance, by applying
we have that the restricted name r in P 1 appears as jj 0 ? r in the process
similarly, by applying the congruence rule the
term M in P 0 appears as Finally, also interactions have to update relative addresses.
Definition 7.4 Let be an abstraction and be a concretion. Then, their localized
interactions are
To see how the localized interactions work, consider F
@C . The restricted names, known as ~
r in P 1 , are
duly updated to jj 0 ? ~
r in the parallel composition of P 0
after the substitution) and P 1 . As for the
message, it appears as M in P 1 and has to be exported at the term address composition ? T is therefore
applied to the relative address jj 1 jj 0 and to M . As an example, consider again the processes in Fig. 1
and suppose that P 0 is willing to send N to the process P 3 . Then, the message will appear as jj 0 jj 0 N in
It will replace, through the routed substitution, the variable x in (P 2 j(P 3 jP 4 ) as jj 1 jj 0 jj 0 N . Note
that it will arrive to P 3 as enriched with the relative address of P 0 w.r.t. P 3 .
8 Message Authentication
We can now intuitively present our authentication primitive [M @
akin to the matching operator. This
"address matching" is passed only if the relative addresses of the two localized terms M and N coincide.
Comm Out
Comm In
Comm Par 1
Comm Par 2
Comm Inter 1
Comm Inter 2
Comm Res
Comm Red
Comm Struct

Table

4: The localized commitment relation.
The intuition is that if we know which process packed N , say P , we can also say that M comes indeed from
authenticating it. More formally, the extensions due to the new primitive consist in a new case for
processes and a new reduction rule.
Definition 8.1 Let M;N be two terms as in Def. 6.1, and l; l 0 2 Loc be two relative addresses. Then
is a process, on which we define the following reduction rule:
Red Address Match [lM @
Note that free names are prefixed with the empty relative address.
Hereafter, we assume an initial start-up phase, in which processes exchange a message and fix their
relative addresses. This can be obtained, e.g., through a preliminary communication between the partners,
from A to B on a restricted shared channel. This start-up phase is indeed an abstraction of the preliminary
secure exchange of secret information (e.g., long term keys) which is necessary in every cryptographic
protocol. We will see an example of this in the next session. This initialization step can be avoided by using
our partner authentication primitive; however, for the sake of presentation, we do not combine here the two
primitives.
Consider the following simple example, where the process B wants to authenticate a message from A
even in the presence of an intruder E. The protocol P is:
E)
(Recall that M is a name that appears as M in A, by assumption; analogously for N in E, below.) Now we
show the role that localized names play, and how they guarantee by construction that B 0 is executed only if
the message bound to x has been originated by A, i.e., if the message received on channel c is indeed M . As
above, the relative address jj 1 jj 0 jj 0 pointing from B to A, encodes the "site" hosting A, thus it gives
the identity of the process from which B is expecting to receive a message on channel c. In order to analyze
the behaviour of the protocol in a hostile environment, we consider a generic intruder E, as powerful as
possible.
We now examine the following two possible message exchanges:
The first message represents the correct exchange of message M from A to B. The second one is an attempt
of E to send a different message N to B. The intruder E could actually be of the following form:
hother bad actionsi:
The names M and N are received by B prefixed by the relative address corresponding to the respective
originators.
Fig. 3 shows the two message exchanges. In particular we see that M is received by B as jj 1 jj 0 jj 0 M
while N becomes jj 0 jj 1 N . It is now immediate to see that only in the first case B will evolve to BfjM=xjg s ,

Figure

3: The process B detects that the message jj 1 jj 0 jj 0 M is authentic while the message jj 0 jj 1 N comes
from the intruder E.
while in the latter it will stop. This is so because only jj 1 jj 0 jj 0 M matches with the address of A. Every
attempt of the intruder of introducing new messages on c is filtered out by the authentication primitive.
A further interesting case arises when the intruder intercepts M and forwards it to B. We will show that
our mechanism accepts the message as authentic. In particular, we reconsider the previous protocol and we
analyze the case of a different intruder that, masquerading as B (written E(B)), intercepts M and forwards
it to B:
does not, actually cannot modify M we would like to accept the message in B even if it has been
forwarded by E. No matter how many times a message is forwarded, address composition maintains its
integrity and the identity of its generator. In detail, E(B) receives M as jj 1 jj 1 jj 0 M . When E forwards it
to B, the message is composed with the address of E relative to B, jj 0 jj 1 , yielding (jj 0
By applying the rule (1) of Def. 3.2 we see that the message is received by B as jj 1 jj 0 jj 0 M , and therefore
it is accepted as authentic. Note also that B can use jj 1 jj 1 jj 0 M as a component of a new message M 0 . The
receiver R of M 0 will get M prefixed by the relative address of A, say #. So R can check that M 0 has been
packed by B 0 , hence the authenticity of M 0 , and even of its components. Indeed the composition of # and
gives the address of the originator of M (i.e. A), relative to R.
We end this section with the following property, in which C[ ] and are contexts with one and
two holes, respectively, and Pfj ~
stands for Pfj ~
Theorem 8.2 (address matching) Let ^
the input on c binds the variable x in the matching. Suppose that
such
1 and
only if l
PROOF. In the first communication the variable x occurring in the matching is instantiated to l
the input binds x (recall that, in Def. 7.3, the substituting term is enriched while going down in the tree of sequential
processes). The sequence of steps leading to Q 00 only change the contexts C and the process P 1 , and it possibly
binds some variables ~
M=xjg. Now the reduction on matching can be performed if and only if [l 00 M @
is at top-level in C 00 , and l is equal to l.
9 Implementing Authentication
In this section we show that our notion of message authentication based on locations helps studying and
analysing cryptographic protocols. The main idea is to observe if a specific authentication protocol is indeed
a good "implementation" of our authentication primitive, i.e., if the cryptographic protocol is as strong in
detecting names with an "incorrect" relative address as our authentication primitive is.
Recall that in the spi-calculus a compound term, such as an encryption M , is considered localized, i.e.
its relative address, say # point to the process P that made the encryption. In this way,
when decrypting fMgK the semantic rules recover the correct addresses for M and K by simply composing
the actual address of fMgK , # 0 # 0 , with the (frozen) relative addresses of M and K , respectively.
We now show an example of a correct run of the Wide Mouthed Frog key exchange protocol. Consider
its simplified version analyzed in [3]. The two processes A and B share keys KAS and KBS with a trusted
server S. In order to establish a secure channel with B, A sends a fresh key KAB encrypted with KAS to
the server S. Then, the server decrypts the key and forwards it to B, this time encrypted with KBS . Now B
has the key KAB and A can send a message M encrypted with KAB to B. The protocol should guarantee
that when B receives M , such a message has been indeed originated by A.
The protocol is composed of the following three messages:
Message
Message 3 A
Its specification in our calculus with localized names (having mechanically replaced restricted names with
their localized counterparts) is:
i:c AB hfMg KAB
(x):case x of fyg jj 1 KAS
in c BS hfyg jj 1 KBS
(x):case x of fyg jj 0 jj 1 KBS
in
c AB (z):case z of frg y in ^
Not surprisingly, the specification is in the style of [3], except for localized restricted names. Fig. 4 shows
how the localized names are handled in a correct execution of the protocol P . Note that KAS and KBS
assume a different relative address in the different processes.
After the reception of message 2, B decrypts the received message

Figure

4: A correct execution of the Wide Mouthed Frog protocol
This means computing
case
of fyg jj 0 jj 1 KBS
in c AB (z):
case z of frg y in ^
B:
The reduction rule Decrypt applies because jj 0 jj 1 . The variable y is then
set to (jj 0 jj 1 that results in jj 1 jj 0 KAB , by the rule (3) of Def. 3.2. This is indeed the
correct reference to the key KAB generated by A and installed in its local environment. In the last message B
receives
, and succeeds in decrypting it with jj 1 jj 0 KAB , obtaining jj 1 jj 0 M . The addresses
of M and of A relative to B are equal, so M is indeed authentic. This characterizes a "correct" execution.
It is well-known that an attack can take place over two sessions of the protocol above. Basically, it
occurs when the intruder replays some messages of the first session in the second one. We follow below
the formalization of [3], where this attack is analyzed. Note that in the single session illustrated above no
problem arises instead, even if an intruder intercepts the message sent by A, then forwarded to B. Indeed
the message received is the right one, as we have just seen above, as no one can alter neither the relative
addresses, nor the encrypted message fMgKAB .
Now, we show that the attack above is immediately detected by an observer that can compare localized
names, e.g. by using our authentication primitive [M @
For the sake of readability, we call A 0 and B 0
the two instances of A and B in the second session where A 0 is trying to send the message M 0 to B 0 using
the session key K 0
Message
hE eavesdrops Message 2i
Message 3 A
hE eavesdrops Message 3i
The intruder eavesdrops the first session and then replays messages 2 and 3 in the second session (messages
The result is that B 0 receives a copy of M instead of one of M 0 .
In order to model two parallel session of the protocol, we consider the following specification:
where the addresses of localized names KAS and KBS are suitably updated in the processes A, B and
S. Note that A generates both M and KAB as fresh names. So each A of A j A originates two different
messages, say M and M 0 , and two different keys, say KAB and K 0
AB . We also modify S so that it can
serve more sessions (for the sake of simplicity we define a server which is just able to handle two sequential
(x):case x of fyg jj 1 KAS
in c BS hfyg jj 1 KBS
i:
c AS (z):case z of fwg jj 1 KAS
in c BS hfwg jj 1 KBS
and we specify the intruder as:
where the names c AB , c AS and c BS are free, and thus known to all the processes of P 0 (unlike KAS and
KBS that are bound).
Now we can observe the attack sequence in Fig. 5. In particular, when the process B 0 decrypts message
which is a message originated from A and not from A 0 , as it
should be. Indeed, the address of A 0 relative to B 0 is jj 1 jj 1 jj 0 jj 1 , and the attack is detected.
We now want to show how the protocol can be done secure by construction through our authentication
primitive. The idea is that the last message should be accepted only if it has been originated by the correct
initiator. In order to do this we need at least a message from the initiator whose address can be compared
with the last message of the protocol. The trick is to add a startup message that securely hooks one initiator
with one responder, by sending a fresh message on a restricted channel. The resulting specification follows
(the modifications are in bold font and the restricted names are not localized, for the sake of readability):
(x):case x of fyg KAS in c BS hfyg KBS i:
c AS (z):case z of fwgKAS in c BS hfwgKBS i
(x):case x of fyg KBS in
c AB (z):case z of frg y in [r @
In P 00 the two B 00 processes receive by the two A 00 two different startup messages, with two different ad-
dresses. It is thus no longer possible for the intruder to carry out a replay attack. In fact, the cheated B 00
will be able to stop before delivering the message to ^
B. By comparing the traces of this protocol correct "by
construction" with the traces of the previous one it is easy to see that they are not equivalent. A potential
attack is thus detected.
K AS
K AS
fMg K AB
AB g d
AS
AB g d
AS

Figure

5: An attack on the Wide Mouthed Frog protocol; where jj k
stands for a sequence of k tags jj i , and
where d
Conclusions and Future Work
We defined two primitives that guarantee partner and message authentication over public channels, based
on the same semantic feature derived form the proved transition systems [9]. Partner authentication is based
on a semantics of the -calculus where names of channels are indexed with the expected relative addresses
of the communicating parties. In particular, any time two processes try to communicate over a common
channel, their relative addresses are checked against the index of the channel used. The communication is
enabled only if the check is passed, i.e. if the relative addresses are compatible with the indexes. Moreover,
the very same channel can be used in a multiplexing fashion: two processes, say P and Q, can go on
exchanging messages on channel c, interleaving their activity with that of another pair of processes, say R
and S, using c as well. It will be never the case that a message for P is read by R or comes from S, unless
this is indeed the intended behaviour of both P and R or both P and S.
Message authentication is based on a semantics of the spi-calculus where each message M is localized,
via a relative address l, to the process P that packed M . The authentication primitive compares the relative
address l with the address l 0 of a process Q, relative to the receiver of M . The check succeeds and
authenticates the message M only if l = l 0 , expressing that it was indeed the process Q that packed M .
Our two primitives are in a sense orthogonal, as they operate on independent features of the calculi con-
sidered. Of course, one may combine them, e.g. by carrying on the spi-calculus the notion of located channel
introduced for the -calculus. Both notions of authentication can then be guaranteed "by construction".
Note that our partner authentication primitive does not transform a public channel into a private one. In-
deed, partner authentication clearly separates the concepts of authentication and secrecy. More importantly,
once two processes communicating on public channels are hooked it is impossible for a third process to
interfere in the communication.
Our notion of message authentication does not need private channels, as well. A message M may be
considered authentic even if it has been intercepted or eavesdropped, i.e., our mechanism does not guarantee
the secrecy of M , but only that M has been generated or packed by the claimed entity. Thus, our primitive
corresponds neither to a private channel in the basic -calculus, nor to a cryptographic one in the spi-
calculus: both appear to be too strong to message authentication alone, as they guarantee also secrecy.
The idea of exploiting locations for the analysis of authentication comes from [14], where however
entities are bound to physical addresses of the net. An approach related is Abadi-Fournet-Gonthier's [2],
in which principals have explicit, fixed names (see also the Join-calculus [19] and SEAL [33]). Here we
relaxed the rigidity of a fixed mapping of sites, by introducing a sort of "identifiers of sites" represented
by relative addresses. As a matter of fact, the actual placement of a process on a site can be recovered by
composing our localized names (akin to the environment function of sequential languages) with allocation
tables (similar to a store). Actually, [14] models a wider notion of authentication, that we plan to investigate
next.
As discussed in the paper, our primitive may be not implementable directly. Indeed, one should have
a low-level, highly reliable mechanism to manage localized names, which is unrealistic in many cases,
but possible for instance in LAN or virtual private networks. A further step could be encrypting relative
addresses within the header of messages, in the style of IPsec [31]. Nevertheless, our proposal can help
reasoning on authentication and security from an abstract point of view. This is indeed the main aim of our
approach and we are presently developing some ideas that we briefly describe in the following.
First, it could be possible to verify the correctness of a cryptographic protocol by showing that its messages
implement partner authentication when needed. As an example, a typical challenge-response technique
requires to send a nonce (random challenge) and to expect it back, encrypted with a secret shared
key. Challenge-response can be proved to implement our located input actions, under some suitable condi-
tions. The proofs that implementations satisfy specifications are often hard, just because private channels
are used to model authenticated channels. Indeed, private channels often seem too far from cryptographic
implementations. So our proposal can help, as we need no private channels.
Moreover, we could verify if a cryptography-based protocol ensures message authentication, by checking
a version of it containing also the primitive [M @
the original formulation and ours should exhibit
the same behaviour. This check of specifications against implementations, is much in the style of the
congruence-based techniques typical of process calculi (see, e.g., [3]).
Finally, we feel confident that our proposal scales up, because some languages for concurrent and reactive
systems, like Facile [32], PICT [28], CML [26], Esterel [4] are built on top of a core process calculus
like the one we use here; also, they have an operational semantics that can easily be turned into a proved
one, as the successful cases of Facile [11] and Esterel [23] show. Of course a great deal of work is still
necessary to make our proposal applicable in real cases.



--R


"Secure Implementation of Channel Abstractions"
"A Calculus for Cryptographic Protocols: The Spi Calculus"
"The Synchronous Programming Language ESTEREL and its Mathematical Semantics"
Security Issues in Process Calculi.
"Names of the -Calculus Agents Handled Locally"
"A Logic of Authentication"
"Authentication via Localized Names"
"Enhanced Operational Semantics: A Tool for Describing and Analysing Concurrent Systems"
"Non Interleaving Semantics for Mobile Processes"
"Causality for debugging mobile agents"
"A Compiler for Analysing Cryptographic Protocols Using Non-Interference"
"Strand Spaces: Why is a Security Protocol Cor- rect?"
"Using Entity Locations for the Analysis of Authentication Protocols"
"Using Non Interference for the Analysis of Security Protocols "
"Non Interference for the Analysis of Cryptographic Proto- cols"
"A Uniform Approach for the Definition of Security Properties"
International Organization for Standardization.

"Three systems for cryptographic protocol analysis"
"Breaking and Fixing the Needham-Schroeder Public-key Protocol using FDR"
"A Hierarchy of Authentication Specification"
"Applying techniques of asynchronous concurrency to synchronous languages"
"A Calculus of Mobile Processes (I and II)"
"Automated Analysis of Cryptographic Protocols Using Mur"
"From CML to its Process Algebra"
"Data Encryption Standard (DES)"
PICT: A programming language based on the pi-calculus
"Verifying authentication protocols in CSP"
Applied Cryptography.
RFC 2411: IP security document roadmap
"Facile Antigua Release Programming Guide"
"Seal: A framework for secure mobile computations"
--TR
A logic of authentication
A calculus of mobile processes, I
From CML to its process algebra
The reflexive CHAM and the join-calculus
Verifying Authentication Protocols in CSP
A calculus for cryptographic protocols
Non-interleaving semantics for mobile processes
Secrecy by typing in security protocols
Applying techniques of asynchronous concurrency to synchronous languages
Pict
Names fo the MYAMPERSANDpgr;-calculus agents handled locally
A compiler for analyzing cryptographic protocols using noninterference
Enhanced operational semantics
Seal
Non Interference for the Analysis of Cryptographic Protocols
Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR
The ESTEREL Synchronous Programming Language and its Mathematical Semantics
A Uniform Approach for the Definition of Security Properties
Secure Implementation of Channel Abstractions
A Hierarchy of Authentication Specifications
Authentication via Localized Names
Automated analysis of cryptographic protocols using Mur/spl phi/

--CTR
C. Bodei , P. Degano , R. Focardi , C. Priami, Authentication primitives for secure protocol specifications, Future Generation Computer Systems, v.21 n.5, p.645-653, May 2005
Chiara Bodei , Mikael Buchholtz , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Static validation of security protocols, Journal of Computer Security, v.13 n.3, p.347-390, May 2005
secrecy;operational semantics;proved transition systems;distributed process algebras;authentication;security