Secrecy by typing in security protocols.
We develop principles and rules for achieving secrecy properties in security protocols. Our approach is based on traditional classification techniques, and extends those techniques to handle concurrent processes that use shared-key cryptography. The rules have the form of typing rules for a basic concurrent language with cryptographic primitives, the spi calculus. They guarantee that, if a protocol typechecks, then it does not leak its secret inputs.
Introduction
Security is an elusive cocktail with many rare ingredients. For any given security
protocol, one may want properties of integrity, confidentiality, availability, various
forms of anonymity and non-repudiation, and more. Seldom does a protocol
achieve all the properties that its designers intended. Moreover, even when a
protocol is sound, it is often delicate to define all its important properties, and
difficult to prove them.
The tasks of protocol design and analysis can be simplified by having principles
that make it easier to achieve particular security objectives, in isolation,
and rules that help recognize when these objectives have been achieved. For ex-
ample, if we wish to obtain some availability properties and are concerned about
denial of service attacks, we may design our protocols in such a way that there
is an obvious, small bound on the amount of work that any principal will do in
response to any message. One could relax this bound for messages from trusted,
authenticated principals; but trust and authentication are not always correct, so
letting availability depend on them should not be done lightly.
In this paper, we develop informal principles and formal rules for achieving
secrecy properties in security protocols. These principles and rules are based
on traditional concepts of classification and information flow [Den82,Gas88], extended
to deal with concurrent processes that use shared-key cryptography. In
particular, in analyzing a protocol, we label each piece of data and each communication
channel as either secret or public. Secret data should not be sent on
public channels, and secret channels should not be made available indiscriminately

In our approach, encryption keys are pieces of data, and as such they are
labelled. Secret data can be made public-declassified-by encryption under a
secret key. However, this declassification cannot be done without some additional
precautions. For example, given a secret bit b and a secret key K, we cannot
simply publish b under K if we may also publish 0 or 1 under K: an attacker
could deduce the value of b by comparing ciphertexts. The rules of this paper
capture a sufficient set of simple precautions that permit this declassification.
The rules have the form of typing rules for a basic concurrent language, the
calculus [AG97a]; this calculus is an extension of the pi calculus [MPW92]
with shared-key cryptographic primitives. The purpose of these rules is rather
different from those of standard typing rules for related languages (such as those
of Pierce and Sangiorgi [PS96]). The rules guarantee that, if a protocol type-
checks, then it does not leak its secret inputs. This secrecy is obtained independently
of any other feature (or any flaw) of the protocol. For example, the rules
may guarantee that a protocol does not leak the contents of certain messages,
without concern for whether message replay is possible. The notion of leaking is
formalized in terms of testing equivalence [DH84,BN95]: roughly, a process P (x)
does not leak the input x if a second process Q cannot distinguish running in
parallel with P (M) from running in parallel with P (M 0 ), for every M and M 0 .
These typing rules are helpful, in that following them may lead to designs
that are clearer, more robust, and more likely to be sound. Furthermore, they
enable us to give simple proofs of properties that would be hard to establish from
first principles. However, the secrecy theorems that we obtain should be taken
with a grain of salt: they are dependent on the choice of a particular model, that
of the spi calculus. This model is fairly accurate and expressive, but does not
take into account issues of key length, for example.
The next section explains, informally, our approach for achieving secrecy. Section
3 is a review of the spi calculus. (The spi calculus presented is a generalization
of that defined originally [AG97a]; it includes polyadic constructs [Mil91].)
Section 4 provides the typing rules for the spi calculus, and Section 5 shows that
these rules can be applied to prevent undesirable flows of information. Section 6
illustrates the use of the rules in examples. Finally, Section 7 discusses some
conclusions.
Throughout this paper, we often opt for simplicity over generality, considering
this work only a first exploration of a promising approach. In particular, we take
a binary, Manichaean view of secrecy. According to this view, the world is divided
into system and attacker, and a secret is something that the attacker does not
have. A more sophisticated view of secrecy would distinguish various principals
within the system, and enable us to discuss which of these principals have a given
piece of data. In our binary view, however, we can vary the boundary between
system and attacker, with some of the same benefits.
Some Principles for Secrecy
In the security literature there are well-known methods for controlling flows of
information. Typically, these methods rely on putting objects and subjects into
security classes, and guaranteeing that no data flows from higher classes to lower
classes. In some of these methods, security classes are formalized as types, and
the control of flows of information relies on typing rules (e.g., [VSI96]).
We adapt some of that work to security protocols. This section describes
our approach informally, along with the main difficulties that it addresses. It is
probable that some of the basic observations of this section have already been
made, but they do not seem to be documented in the open literature.
2.1 On Rules in Distributed Systems
In a centralized system, an administrator that controls all the hardware in the
system may hope to control all information flows. If all communication is mediated
by the system hardware, the control of all information flows is plausible
at least in principle. In particular, the administrator may check user programs
before running them, statically, or may apply some dynamic checks.
In a distributed system, on the other hand, no single administration may
control all the hardware. No part of the system may be able to check that the
software of any other part is constructed according to a given set of rules. At best,
each principal can analyze the programs that it receives from other principals,
as well as all other messages.
Therefore, whatever rules we propose, they should be such that an attacker
satisfies them vacuously. We cannot expect to restrict the code that the attacker
runs. Our rules should constrain only the principals that want to protect their
secrets from the attacker.
2.2 Preliminaries on Keys and Channels
As mentioned in the introduction, this paper concerns shared-key protocols.
We write fMgK for the result of encrypting M with K, using a shared-key
cryptosystem such as DES [DES77]. With shared-key cryptography, secrecy can
be achieved by communication on public channels under secret keys.
In addition to public channels, on which anyone may communicate, we consider
channels with some built-in protection. We restrict attention to channels on
which the same principals can send and receive. On a single machine, channel
protection can be provided by an operating system that mediates communication
between user processes; in a distributed system, the protection can be
implemented cryptographically.
The ability to communicate on a channel is often determined by possession of
a capability, such as a password or a key. (In the pi calculus and the spi calculus,
the name for a channel is the capability for the channel.) A public channel is
one for which the capability is public; similarly, a secret channel is one for which
the capability is secret.
2.3 Classifying Data
We consider only three classes of data:
Public data, which can be communicated to anyone,
- Secret data, which should not be leaked,
Any data, that is, arbitrary data.
We use the symbols T and R to range over the classes Secret , Public, and Any .
We refer to Secret , Public, and Any as classes, levels, or types; the difference is
one of emphasis at most. It should be possible to generalize our rules to richer
classification structures, with more than three classes; but such a generalization
is not essential for our immediate purposes.
Encryption keys are data, so our classification scheme applies to them. Several
different levels can be associated with a key:
its level as a piece of data,
- the levels of the data that it is used to encrypt,
- the levels of the resulting ciphertexts.
However, not all combinations are possible, as for example a public key should
not be used to turn secret data into public ciphertexts. It is simplest to retain
only one level for each key. Similarly, we associate a single classification with
each channel. We adopt the following principles:
The result of encrypting data with a public key has the same classification
as the data, while the result of encrypting data with a secret key
may be made public.
Only public data can be sent on public channels, while all kinds of data
may be sent on secret channels.
The relation T !: R holds if T equals R or if R is Any . If a piece of data has
level T and T !: R, then the piece of data has level R as well.
Because a piece of data of level Any could be of level Secret , it should not be
leaked. On the other hand, a piece of data of level Any could be of level Public,
so it cannot be used as a secret. For example, it cannot be used as a secret key
for encrypting secret data. Thus, if all we know about a piece of data is that
it has level Any , then we should protect it as if it had level Secret , but we can
exploit it only as if it had level Public. This piece of data is therefore not very
useful for constructing channel capabilities or encryption keys; we find it cleaner
to forbid these uses altogether.
Furthermore, we focus on the case where the classification Secret is given only
to data created fresh within the system that we are trying to protect. However,
other data can be of class Any , and then it must be protected as though it were
of class Secret .
2.4 Classifying Inputs
Whereas each principal may know the classification of the data that it creates,
the principal may not always know the classification of the data that it acquires
through communication with other principals. Data that arrives in clear on public
channels can be presumed to be public. On the other hand, data that arrives
with some protection may be either secret or public.
The participants of protocols typically know how to handle each of the fields
of the encrypted messages that they receive, as in the following example (inspired
by the Needham-Schroeder protocol [NS78]):
Message
Message 3 A
In this protocol, the principals A and B share keys KSA and KSB with the
server S, respectively. The server provides some confidential information I A to
A and I B to B, in response to a request from A. When A receives a message
from the server, it decrypts it, retrieves I A , and forwards fI B gKSB to B. It is
crucial that A be able to recognize when this action is appropriate. For example,
if a principal X plays the role of A and B in two concurrent runs of the protocol,
it should be able to recognize whether a message is an instance of Message 2 or
an instance of Message 3. If X mistakes an instance fI X gKSX of Message 3 for
an instance Message 2, then X would forward part of I X in clear.
As in this example, it is common for principals to deduce the sensitivity of
inputs from the expected kind of a message or other implicit information. Such
implicit information is often incorrect and often hard to analyze [AN96].
It is clearer to label explicitly each component of a message with a classifi-
cation, avoiding the dependence on implicit context. This labelling is important
only for messages on secret channels or under secret keys, as all other messages
can contain only public information.
Alternatively, we may adopt a standard format for all messages on secret
channels or under secret keys. The format should guarantee that there is a
standard way to attach classifications to parts of each message, avoiding again
the dependence on implicit context. In our rules, we adopt this scheme. Each
message on a secret channel has three components, the first of which has level
Secret , the second Any , and the third Public. Each message under a secret key
has those three components plus a confounder component, as discussed next.
Both of these schemes are implementations of the following principle:
Upon receipt of a message, it should be easy to decide which parts of
the contents are sensitive information, if any. This decision is least error-prone
when it does not depend on implicit context.
2.5 Confounders
As noted in the introduction, given a secret bit b and a secret key K, we cannot
simply publish b under K if we may also publish 0 or 1 under K: an attacker
could deduce the value of b by comparing ciphertexts. On the other hand, we can
create a fresh value n, then publish the concatenation of b and n under K. A value
such as n is sometimes called a confounder. The purpose of n is to guarantee that
the resulting ciphertext differs from all previous ones. The resulting ciphertext
will differ from all future ones too if each ciphertext includes a fresh confounder,
always in the same position. In general (unless one is concerned about encrypting
known plaintext), confounders need not be kept secret.
Confounders are not needed if encryption is history-dependent, so a different
transformation is applied to each message. In particular, confounders are not
needed when encryption is done with a stream cipher or with a block cipher in
an appropriate chaining mode. The remarks of this section are not intended to
apply to protocols built on such algorithms.
Independently of the choice of cipher, confounders are not needed in protocols
where all ciphertexts generated are guaranteed to be different. Unfortunately, it
is not always clear whether this guarantee is offered.
As an example, we consider a simple protocol where a principal A sends
a message M to a principal B under a shared key KAB . Before A sends the
message, B provides a challenge NB , fresh for each message; the challenge serves
as a proof of freshness, and protects against replays.
We may reason that all the ciphertexts from A are different, since each of them
includes a fresh challenge. However, this reasoning is incorrect. An attacker C
could provide a challenge instead of B, and A would reply without noticing that
the challenge did not come from B. The attacker may pick the same challenge NC
twice in a row. In that case, the ciphertexts with which A responds, fM;NC gKAB
and are identical if and only if the cleartexts M and M 0 are
identical. Thus, C can find out whether A is sending two identical cleartexts, even
without knowing the key KAB . Thus, the protocol is leaking some information.
In order to prevent this small leak, A should create a confounder NA for each
encryption. The modified protocol is:
This protocol is analyzed in [AG97c], where it is proved that the protocol guarantees
the secrecy of M .
It is prudent to adopt the following principle:
If each encrypted message of a protocol includes a freshly generated
confounder in a standard position, then the protocol will not generate
the same ciphertext more than once. Confounders should be used unless
it is obvious that they are not needed.
2.6 Implicit Flows
A system may reveal something about one of its parameters even if this parameter
never appears explicitly in a message. For example, the system may send
different cleartext messages depending on the value of the parameter. An attacker
could deduce something about the parameter from patterns of communication.
Such a leak of information is sometimes called an implicit flow.
It is of course important to restrict implicit flows. For this purpose, we may
forbid any comparison that involves pieces of sensitive data and that could be
followed by actions that would reveal the result of the comparison.
It is also important not to push this restriction to uncomfortable extremes.
Many protocols exhibit implicit flows in some form, usually without severe undesirable
effects. As an example, we consider again this protocol:
Message
Message 3 A
An attacker can send an arbitrary message to A, instead of Message 2. On receipt
of this message, A performs a test that involves the secret KSA , and branches
on the result of this test. The reaction of A depends visibly on whether the
message is a ciphertext under KSA . One could regard this as an implicit flow,
but perhaps one of little importance because the chance that an independently
created message will be under KSA is negligible. We can allow this implicit flow;
it is harmless in our model.
Our (tentative) policy on implicit flows is summarized in the following principle

Implicit flows of information should be prevented, except perhaps when
the likelihood of the implicit flow is no greater than the likelihood that
an attacker will guess the information.
2.7 Further Principles
The discussion of this section is not comprehensive. In practice, several additional
warnings and techniques are important. A few of these are:
- It is often hard not to leak the size of a secret. The use of padding in encrypted
messages can help in this respect.
- It is prudent to minimize the benefit that an attacker may derive from discovering
any one secret. In particular, the same key should not be used to
protect a great volume of sensitive traffic, because then even a brute-force
attack on the key may be profitable.
- Weak secrets, such as passwords, should be protected from brute-force attacks
(see for example [Sch96]).
Undoubtedly there are more. However, the discussion of this section suffices as
background for our rules and theorems.
3 The Untyped, Polyadic Spi Calculus
This section defines the version of the spi calculus that serves as the setting for
our formal work. The main novelty with respect to the earlier versions of the spi
calculus is the introduction of polyadic forms: each input, output, encryption,
and decryption operation applies to an arbitrary number of pieces of data, rather
than to a single piece. This novelty is important for the typing rules of the next
section. However, this novelty is not substantial, as in particular it does not
affect the expressiveness of the spi calculus.
Therefore, our presentation is mostly a review. Most of this material is derived
from the earlier presentations of the spi calculus [AG97b]; it includes ideas
common in the pi-calculus literature.
3.1
We assume an infinite set of names and an infinite set of variables. We let m,
range over names, and let w, x, y, and z range over variables. We
for the outcome of replacing each free occurrence of x in P with
M , and identify expressions up to renaming of bound variables and names.
The set of terms is defined by the grammar:
name
suc(M) successor
x variable
The set of processes is defined by the grammar:
composition
(-n)P restriction
replication
[M is N ] P match
let in P pair splitting
case M of case
case L of fx
(The name n and the variables x, y, x 1 , . , x k are bound in these processes.)
Most of these constructs should be familiar from earlier process algebras;
see [AG97a] for a review, and see below for an operational semantics. The informal
semantics of some of the constructs is as follows.
- The term fM represents the ciphertext obtained by encrypting
under the key N .
- The process case L of fx attempts to decrypt L with
the if L has the form fM then the process behaves
as and otherwise the process is stuck.
- The process let (x; in P behaves as P [N=x][L=y] if M is a pair
(N; L), and it is stuck if M is not a pair.
- The process case M of is 0, as Q[N=x]
if M is suc(N) for some N , and otherwise is stuck.
- The process [M is N ] P behaves as P if M and N are equal, and otherwise
is stuck.
- The process MhN on M and then behaves
as P ; the output happens only if M is a name and there is another process
ready to receive k inputs on M . We use MhN as an abbreviation for
is a process that may output
on M and then stop.
- The process M(x is ready to receive k inputs N
and then to behave as P [N 1
- The process !P behaves as infinitely many copies of P running in parallel.
- The process (-n)P makes a new name n and then behaves as P .
The polyadic notations (input, output, encryption, decryption for k 6= 1)
are not necessary for expressiveness. They are definable from the corresponding
unary notations; for example, we can set:
case L of fx
case L of fygN in
let
where variable y is fresh. However, as mentioned above, the polyadic constructs
are useful for typing. They also introduce a typing difficulty, when arities do
not match, as in case fM in P . This typing difficulty
could be overcome with an appropriate system of sorts.
In addition to the polyadic notations, we use the following standard abbreviations
for any k - 2:
let
let
where variable y is fresh.
We write fn(M) and fn(P ) for the sets of names free in term M and process
respectively, and write fv (M) and fv (P ) for the sets of variables free in M
and P respectively. A term or process is closed if it has no free variables.
3.2 Commitment
As an operational semantics, we rely on a commitment relation. The definition of
commitment depends on some new syntactic forms, abstractions and concretions.
An abstraction is an expression of the form
x k are bound variables, and P is a process. A concretion is an expression of the
are terms, P
is a process, and the names m 1 , . , m l are bound in M 1 , . , M k and P . An
agent is an abstraction, a process, or a concretion. We use the metavariables A
and B to stand for arbitrary agents.
We extend the restriction and composition operators to abstractions:
assuming that x fv(R), and to concretions:
(-m)(-~n)h ~
assuming that m 62 f~ng and f~ng " We define the dual composition
A j R symmetrically. (The definition of (-m)(-~n)h ~
MiQ is slightly different from
the original one [AG97b]. The change is crucial for Lemma 9, below.)
If F is the abstraction and C is the concretion (-n
we define the processes F@C and
C@F as follows:
The reduction relation ? is the least relation on closed processes that satisfies
the following axioms:
(Red Repl)
(Red Match)
(Red Let)
let
(Red Zero)
case 0 of
(Red Suc)
case suc(M) of
(Red Decrypt)
case
A barb is a name m (representing input) or a co-name m (representing out-
put). An action is a barb or the distinguished silent action - . The commitment
relation is written P ff
\Gamma! A, where P is a closed process, ff is an action, and A
is a closed agent. It is defined by the rules:
(Comm Out)
(Comm In)
\Gamma!
(Comm Inter 1)
\Gamma! C
\Gamma! F@C
(Comm Inter 2)
\Gamma!
\Gamma! F
\Gamma! C@F
(Comm Par 1)
\Gamma! A
\Gamma! A j Q
(Comm Par 2)
\Gamma! A
\Gamma!
(Comm Res)
\Gamma! A
(-m)P ff
\Gamma! (-m)A
(Comm Red)
\Gamma! A
\Gamma! A
3.3 Testing Equivalence
A test is a pair (R; fi) consisting of a closed process R and a barb fi. We say
that P passes a test (R; fi) if and only if
\Gamma! Qn fi
\Gamma! A
for some n - 0, some processes Q 1 , . , Qn , and some agent A. We obtain a
testing preorder v and a testing equivalence ' on closed processes:
for any test (R; fi), if P passes (R; fi) then Q passes (R; fi)
A strict barbed simulation is a binary relation S on closed processes such that
(1) for every barb fi, if P fi
\Gamma! A then Q fi
\Gamma! B for some B,
\Gamma! P 0 then there exists Q 0 such that Q -
(These requirements are somewhat stronger than those for barbed simulations
[AG97b].) A strict barbed bisimulation is a relation S such that both S and S \Gamma1
are strict barbed simulations.
The following lemma provides a method for proving testing equivalence:
Lemma 1. If for every closed process R there exists a strict barbed bisimulation
S such that (P j R) S (Q j R), then P ' Q.
Proof. The lemma is a consequence of earlier results [AG97b], but we give a
simple direct proof, since there is one. We argue that if P passes a test (R; fi)
then so does Q, assuming that there exists a strict barbed bisimulation S such
that (Symmetrically, if Q passes a test (R; fi) then so does P .)
If P passes (R; fi), then
\Gamma! Rn fi
\Gamma! A
for some agent A and processes R 1 , . , Rn , for some n - 0. By the definition
of strict barbed simulation, there exist R 0
n and A 0 such that R i
\Gamma! A 0
Therefore, Q passes (R; fi). 2
4 The Typing System
This section describes our rules for controlling information flow in the spi cal-
culus. They are based on the ideas of Section 2. While there are several ways of
formalizing those ideas, we embody them in a typing system for the spi calculus.
This typing system is simple enough that it could be enforced statically. Our
main results for this typing system are in Section 5.
The typing system gives rules for three kinds of assertions (or judgments):
means that environment E is well-formed.
means that term M is of class T in E.
means that process P typechecks in E.
4.1 Environments
An environment is a list of distinct names and variables with associated levels.
In addition, each name n has an associated term, of the form fM
for some k - 0. Intuitively, this association means that the name n may be used
as a confounder only in the term fM We
x with level T , and level T and term
We as a shorthand for arbitrarily,
when n is not needed as a confounder.
The set of names and variables declared in an environment E are its domain;
we write it dom(E).
The rules for environments are:
(Environment Empty)
well-formed
(Environment Variable)
well-formed
(Environment Name)
well-formed
Collectively, these rules enable us to form environments as lists of variables
and names with associated levels, and in addition with terms attached to the
names. The empty list is written ; in the rule (Environment Empty).
In the rule (Environment Name), the hypotheses
are included so that, if any variable occurs in M 1 , . , M k , then it is declared
in E. This restriction is important because, without proper care, a variable
could be instantiated in two different ways, so that the same confounder could
be used for two different messages; this double use would defeat the purpose of
confounders.
4.2 Terms
The rules for terms are:
(Level Subsumption)
(Level Variable)
(Level Name)
(Level Zero)
well-formed
(Level Successor)
(Level Pair)
(Level Encryption Public)
(Level Encryption Secret)
The rule (Level Subsumption) says that a term of level Public or Secret has
level Any as well.
The rules (Level Variable) and (Level Name) enable us to extract the levels
of names and variables from an environment.
The rules (Level Zero) says that 0 is of level Public. The rule (Level Successor)
says that adding one preserves the level of a piece of data. Therefore, the terms
0, suc(0), suc(suc(0)), . are all of level Public. However, a term of the form
suc(x) may be of level Secret .
The rule (Level Pair) says that the level of a pair is the level of its components.
Both components must have the same level; when we pair a term of level Public
and one of level Secret , we need to regard them both as having level Any . Thus,
the rule (Level Pair) loses a little bit of typing information; it would be interesting
to explore a richer, more "structural" typing system that would avoid this loss.
The rule (Level Encryption Public) says that k pieces of data of the same level
T can be encrypted under a key of level Public, with a resulting ciphertext of level
T . The rule (Level Encryption Secret) imposes more restrictions for encryption
under keys of level Secret , because the resulting ciphertext is declassified to level
Public. These restrictions enforce a particular format for the levels of the contents
and the use of a confounder, as explained in Section 2. One could relax this rule
somewhat, considering also the case where the resulting ciphertext is given a
level other than Public; the present rule strikes a reasonable balance between
simplicity and flexibility. Finally, note that there is no rule for encryption for
the case where N is a term of level Any . If N is a term of level Any , and it is
not known whether it is of level Public or Secret , then N cannot be used as a
key.
4.3 Processes
The rules for processes are:
(Level Output Public)
(Level Output Secret)
(Level Input Public)
(Level Input Secret)
(Level Nil)
well-formed
(Level Parallel)
(Level Replication)
(Level Restriction)
(Level Match) for T
(Level Pair Splitting) for T 2 fPublic; Secretg
(Level Integer Case) for T 2 fPublic; Secretg
case M of
(Level Decryption Public) for T 2 fPublic; Secretg
case L of fx
(Level Decryption Secret) for T 2 fPublic; Secretg
case L of fx
There are two rules for output and two rules for input. The rule (Level
Output Public) says that terms of level Public may be sent on a channel of
level Public. The rule (Level Output Secret) says that terms of all levels may be
sent on a channel of level Secret-provided this is done according to the format
described in Section 2. The two rules for input, (Level Input Public) and (Level
Input match these rules for output. In (Level Input Public) all inputs
are assumed to be of level Public, while in (Level Input Secret) the levels of the
inputs are deduced from their position, as allowed by the format of messages on
channels of level Secret . If M is a term of level Any , and it is not known whether
it is of level Public or Secret , then M cannot be used as a channel.
The rules for nil, for parallel composition, for replication, and for restriction
are routine. In the rule (Level Restriction), the name n being bound is associated
with an arbitrary term L for which it can be used as a confounder.
The rule (Level Match) enables us to compare any two terms of levels Public
or Secret . Terms of level Any are excluded in order to prevent implicit flows, as
discussed in Section 2. It may be a little surprising that terms of level Secret are
allowed in this rule, because this may seem to permit an implicit flow. However,
the generality of the rule (Level Match) does not present an obstacle to our
results.
The rule (Level Pair Splitting) enables us to try to break a term of level
Public or Secret into two components, each assumed to be of the same level as
the original term. The case where the original term is known only to be of level
Any is disallowed; if it were allowed, this rule would permit leaking whether the
term is in fact a pair.
Similarly, the rule (Level Integer Case) enables to examine whether a term
is 0 or a successor term, and to branch on the result. In the successor case,
the variable x represents the predecessor of the term being examined, which
is assumed to be of the same level as the term. As in (Level Pair Splitting),
the term should not be of level Any , but it may be of level Secret . If names
were numbers, then repeated applications of the rule (Level Integer Case) would
enable us to publish a secret key in unary. Formally, this leak cannot happen
because names are not numbers. The practical meaning of this small formal
miracle is debatable; it may suggest that a model more concrete than the spi
calculus would be worth investigating.
Finally, there are two rules for decryption. The rule (Level Decryption Public)
handles the case where the decryption key is of level Public, while the rule (Level
Decryption Secret) handles the case where the decryption key is of level Secret .
These rules are analogous to the corresponding rules for input. There is no rule
for the case of a key of level Any .
5 What Typing Guarantees
The goal of this section is to prove that if a process typechecks then it does not
leak the values of parameters of level Any . More precisely, our main theorem
says that if only variables of level Any and only names of level Public are in the
domain of the environment E, if oe and oe 0 are two substitutions of values for the
variables in E, and if P typechecks (that is, can be proved), then P oe
and P oe 0 are testing equivalent. This conclusion means that an observer cannot
distinguish P oe and P oe 0 , so it cannot detect the difference in the values for the
variables.
In order to prove this result, we develop a number of propositions and lemmas
that analyze the typing system and characterize the possible behaviors of
processes that typecheck.
5.1 Typing for Concretions and Abstractions
The first step in our proofs is to extend the typing rules to concretions and
abstractions:
(Level Concretion Public)
(Level Concretion Secret)
(Level Abstraction Public)
(Level Abstraction Secret)
These rules should be reminiscent of corresponding rules for output and input.
5.2 Auxiliary Propositions
Next we obtain several auxiliary results. The first of them, Proposition 2, is a
formal counterpart of the discussion of Section 2.1: this proposition shows that,
given a suitable environment, a closed process P that we may construe as an
attacker always typechecks.
Proposition 2. Assume that ' E well-formed, that dom(E) does not contain
any variables, and that all the names in dom(E) are of level Public.
If M is a closed term and fn(M) ' dom(E), then
If P is a closed process and fn(P
Proof. We prove a more general property, allowing variables to occur in E, M ,
and P . We consider an environment E such that ' E well-formed, where the
levels of names and variables are all Public. We prove that:
If M is a term with fn(M) [ fv(M) ' dom(E), then
If P is a process with
The former of these facts is obtained by a direct induction on the structure of
(using (Level Encryption Public) for terms of the form fM
latter of these facts is then obtained by a direct induction on the structure of
(using (Level Output Public), (Level Input Public), and (Level Decryption
Proposition 3 is fairly standard; it says that anything that can be proved
in a given environment can also be proved after adding assumptions to the
environment.
Proposition 3. Assume that '
Proof. This property is proved by induction on the derivations of
and
Proposition 4 enables to reorder an environment, moving the declaration of
a name past the declarations of some variables.
Proposition 4. Let E 1 be
Proof. The proof is by induction on the derivations of '
Note that the converse of this proposition cannot be true because, under the
hypotheses of the converse, L could contain free occurrences of x 1 , . , x k .
The next proposition says that the levels Secret and Public are mutually
exclusive.
Proposition 5. If then it is not the case that
Proof. We assume that both hold, and derive
a contradiction, by induction on the size of the two derivations of
Public. The only interesting case is that where M has the form
. The term fM could have levels Secret and Public
at once only if N did as well (and by application of the two rules for encryption);
the induction hypothesis yields the expected contradiction. 2
The remaining auxiliary results all concern substitutions. The first of them
is a standard substitution lemma.
Proposition 6. Assume that E
well-formed then '
Proof. The proof is by a joint induction on the derivations of the judgments
In
the case of the rule (Level Encryption Secret), it is important to note that if the
confounder n appears in E then x cannot occur in the term being formed. 2
In general, a substitution is a partial function from the set of variables to the
set of terms. We write dom(oe) for the domain of the substitution oe.
Proposition 7. Given an environment E, suppose that only variables of level
Any in E are in dom(oe), and that either E
- If Loe is a variable then L is the same variable.
- If Loe is a name then L is the same name.
- If Loe is of the form (M; N) then L is of the same form.
- If Loe is 0 then L is 0.
- If Loe is of the form suc(M) then L is of the same form.
- If Loe is of the form fM then L is of the same form.
Proof. This follows from the fact that L cannot be a variable in dom(oe), since
this domain consists of variables of level Any . 2
Proposition 8. Given an environment E, suppose that only variables of level
Any in E are in dom(oe). Suppose further that
Proof. The proof is by induction on the derivation of . The rule (Level
Subsumption) can be applied only trivially as the last rule of this derivation
since T 2 fPublic; Secretg. There is one case for each of the remaining rules for
typechecking terms.
- If the last rule of the derivation of
M is a variable, but not one in dom(oe) since dom(oe) consists of variables
of level Any , so M Therefore, M oe = N oe implies that
Proposition 7.
- If the last rule of the derivation of (Level Name) or (Level
then M is a name or 0, so M Therefore, M oe = N oe implies
that by Proposition 7.
- The cases of (Level Successor) and (Level Pair) are by easy applications of
Proposition 7 and the induction hypothesis.
- The two remaining cases are for M of the form fM We have
depending on whether the derivation
of finishes with an application of (Level Encryption Public) or
an application of (Level Encryption Secret). In both cases, Proposition 7
implies that N has the form fN
, with
depending on whether the derivation of
finishes with an application of (Level Encryption Public) or an
application of (Level Encryption Secret). By induction hypothesis, we obtain
. By Proposition 5, the derivations of
finish with applications of the same rule.
ffl If this rule is (Level Encryption Public), then we have
. ,
to the applications of the rule. Since M oe = N oe, we have M 1
oe. By induction hypothesis, we obtain M
ffl If this rule is (Level Encryption Secret), then 4 is a name
in E for some level T 0 , and N 4 is a name n with
a name may be declared in an environment at most once, we conclude
that .5.3 Lemmas on Commitment and Simulation
The main lemma of this section relates the typing system with the commitment
relation. We write E ' oe when, for every x 2 dom(E), oe(x) is a closed term
such that fn(oe(x)) ' dom(E).
Lemma 9. Assume that:
(3) all variables in dom(E) are of level Any.
Then:
then there is a process Q such that
then there is a process Q such that
\Gamma! A 0 then either there is a
concretion A such that
OkCSecret (depending on whether
\Gamma! A 0 then either there is an
abstraction A such that
OkASecret (depending on whether
Proof. The argument for this lemma is quite long, but not surprising, given
the auxiliary propositions. It consists of one case for each of the axioms for the
reduction relation and one case for each of the rules for the commitment relation.
We therefore omit the details of this argument. 2
Lemma 10. Given an environment E, suppose that all the variables in dom(E)
are of level Any. Suppose further that E ' oe and E ' oe 0 . Then the relation
is a strict barbed bisimulation.
Proof. First we consider any commitment P oe ff
\Gamma! A 0 , where ff is a barb. By
Lemma 9, there is an agent A such that P oe 0 ff
\Gamma! Aoe 0 .
Next, we consider any commitment P oe -
\Gamma! Q 0 . By Lemma 9, there is a
process Q such that
\Gamma! Qoe 0 . Thus, any - step
of P oe may be matched by P oe 0 .
Therefore, the relation f(P oe; P oe 0 is a strict barbed simula-
tion. By symmetry, it is a strict barbed bisimulation. 2
5.4 Main Theorem
Finally, we obtain the theorem described at the start of Section 5:
Theorem 11. Given an environment E, suppose that only variables of level
Any and only names of level Public are in dom(E). Suppose further that E ' oe
Proof. According to Lemma 1, it suffices to show that for every closed process Q
there exists a strict barbed bisimulation that relates P oe j Q and P oe 0 j Q. Since
We construct an extension of E with the names that appear free in Q but
are not in dom(E). For each such name n, we us call
the resulting environment. By Propositions 2 and 3, we obtain E
Also by Proposition 3, we obtain E   ' Combining these two results,
rule (Level Parallel) yields E   ' (P
Finally, Lemma 10 yields the desired result. 2
Note that this theorem would not hold if P could have free occurrences of names
of level Secret . Such occurrences are ruled out by the hypotheses that only names
of level Public are in E and that
6 Examples
In order to illustrate the use of our typing rules, we consider as examples two
protocols for key exchange and secure communication.
In both cases, we can typecheck the protocols. As corollaries, we obtain that
the secrecy of certain messages is protected. These corollaries should not be
surprising. However, they would be much harder to prove in the spi calculus
without the rules developed in this paper, from first principles.
Analogues of our corollaries might be provable in other formal systems. Sur-
prisingly, there do not seem to be any formal proofs of this sort in the literature.
In some methods, one may be able to show that the messages in question are
not among the terms that the attacker obtains when the protocol runs. However,
this result is only an approximation to the corollaries, as it does not rule out
that the attacker could at least deduce whether the messages are even numbers
or odd numbers, for example. The corollaries exclude this possibility.
Analogues of our corollaries can perhaps be established in informal but rigorous
models (see for example [BR95]). These models are rather accurate, as in
particular they can take into account issues of probability and complexity. Unfor-
tunately, proofs in these models remain much more difficult than typechecking.
6.1 A First Example
The first protocol is similar in structure to the Wide Mouthed Frog protocol
[BAN89]. Informally, this protocol is:
on c S
Message
Message 3 A
Message
Message
Message 7 A
A gKAB on c B
In this protocol, A and B are two clients and S is a server. The channels c S , c A ,
and dB are public. The keys KAS and KSB are secret keys for communication
with the server, while KAB is a new key for communication from A to B. The
message M is intended to be secret. Both NS and NB are nonces (used to prove
timeliness);   is an arbitrary message of appropriate level (not necessarily the
same for all occurrences of  ); and CA , C 0
A , and CS are confounders. In Messages
1 and 2, A requests and receives a nonce challenge from S. In Messages 4 and
requests and receives a nonce challenge from B. In Message 3, A provides
the key KAB to S, which passes it on to B in Message 6. In Message 7, A uses
KAB for sending M . On receipt of this message from A, the recipient B outputs
the names of A and B on a public channel dB , in Message 8. It is not important
to specify who receives this last message, which we include only in order to
illustrate that B is allowed to react.
We can express this protocol in the spi calculus, much as in the earlier work
on the spi calculus [AG97a] but with attention to the requirements of typing.
The definition is for a given set of messages M 1 , . , Mm with source addresses
These addresses
are natural numbers in the range 1::n; they indicate who plays the role of A
and who plays the role of B in each run of the protocol. In addition, S is an
address. For each address i, there are channels c i and d i . We write i for the term
representing i, and simply write S for the term representing S. In the definition
of Send i;j , the variable z corresponds to the message M ; we write Send i;j (M)
for Send i;j [M=z].
nonce
nonce
A gK i)
i21::n [x A is i] (-NS )(c i hNS
case x cipher of fx
let (y A ; z A ; xB ; x nonce
j21::n [y A is i] [z A is i] [x B is j] [x nonce is NS
nonce
nonce
case y cipher of fx
let nonce
i21::n [x S is S] [x A is i] [x B is j] [y nonce is NB
case z cipher of fz s ; z a ; z
x key
in
Sys \Delta
The next proposition says that this protocol typechecks.
Proposition 12. Let E be the environment
be any fixed numbers in 1::n, for k 2 1::m. Let M k be z k , for
Proof. In order to indicate how the process Sys typechecks, we annotate its
bound names and variables with their levels, as they are introduced; we also
annotate confounders with the terms in which they are used. For
nonce
A gK i)
i21::n [x A is
case x cipher of fx key
nonce
j21::n [y A is i] [z A is i] [x B is j] [x nonce is NS
nonce
case y cipher of fx
let
i21::n [x S is S] [x A is i] [x B is j] [y nonce is NB
case z cipher of fz s
in
Finally, in the given environment E, we set:
Sys \Delta
writing
As a consequence of the typechecking, we obtain that the protocol does not
reveal the message M from A. This conclusion is stated in the following corollary,
where for simplicity we restrict attention to the case where M is a numeral.
numeral is one of the terms 0, suc(0), suc(suc(0)), .)
Corollary 13. Let i k and j k be any fixed numbers in 1::n, for k 2 1::m. Let Sys1
and Sys2 be two versions of Sys where the terms M k are arbitrary numerals, for
Proof. This is an immediate consequence of Proposition 12 and Theorem 11. 2
6.2 A Second Example
In the second example, the principal A transmits the secret message M under a
generated by the server S. This example is interesting because it brings up
an issue of trust: A trusts S to provide a key appropriate for the transmission
of M .
Message
Message
S gKSB on c B
Message 5 A
Again, A and B are two clients and S is a server, and c S , c A , c B , and dB are
public channels. The keys KSA and KSB are secret keys for communication from
the server to A and B, while KAB is the new key for communication between A
and B. Both NA and NB are nonces, and CS , C 0
S , and CA are confounders.
We write this example in the spi calculus in much the same style as the first
example. The definition is for a given set of messages M 1 , . , Mm with source
case x cipher of fx
let
[x A is i] [y B is j] [x nonce is NA
nonce
i21::n [x A is i]
nonce
nonce
i21::n [x A is i]
case y cipher of fx
let nonce
[x A is i] [y B is j] [y nonce is NB
case z cipher of fz s ; z a ; z
in
Sys \Delta
The next proposition and corollary are the analogues of Proposition 12 and
Corollary 13, respectively. We omit their proofs.
Proposition 14. Let E be the environment
be any fixed numbers in 1::n, for k 2 1::m. Let M k be z k , for
Corollary 15. Let i k and j k be any fixed numbers in 1::n, for k 2 1::m. Let Sys1
and Sys2 be two versions of Sys where the terms M k are arbitrary numerals, for
Conclusions
Perhaps in part because of advances in programming languages, the idea of static
checking of security properties seems to be reviving. The Java bytecode verifier
is a recent static checker with security objectives [LY96]. In the last couple of
years, more sophisticated security checks have been based on self-certification
and on information-flow techniques (see for example [Nec97,VSI96]).
This work can be seen as part of that revival. It develops a method for static
checking of secrecy properties of programs written in a minimal but expressive
programming language, the spi calculus. These programs can be concurrent, and
can use cryptography. The method is embodied in a set of typing rules.
The principles and rules developed in this paper are neither necessary nor
sufficient for security. They are not necessary because, like most practical static
typechecking disciplines, ours is incomplete. They are not sufficient because they
ignore all security issues other than secrecy, and because they do not account for
how to implement the spi calculus while preserving secrecy properties. However,
these principles and rules provide some useful guidelines. Furthermore, the rules
are tractable and precise; so we have been able to study them in detail and to
prove secrecy properties, establishing the correctness of the informal principles
within a formal model.

Acknowledgments

Butler Lampson suggested studying authentication protocols through classification
techniques, several years ago. That suggestion was the starting point for
this work.
This work took place in the context of collaboration with Andrew Gordon on
the spi calculus, so the themes and techniques of this paper owe much to him;
Andrew Gordon also commented on a draft of this paper.
Conversations with Mike Burrows, Steve Kent, and Ted Wobber were helpful
during the writing of this paper.



--R

A calculus for cryptographic protocols: The spi calculus.
A calculus for cryptographic protocols: The spi calculus.
Reasoning about cryptographic protocols in the spi calculus.
Prudent engineering practice for cryptographic protocols.
A logic of authentication.
Testing equivalence for mobile processes.
Provably secure session key distribution: The three party case.
Cryptography and Data security.
Data encryption standard.
Testing equivalences for processes.
Building a Secure Computer System.
The Java Virtual Machine Specification.
The polyadic
A calculus of mobile processes

Using encryption for authentication in large networks of computers.
Typing and subtyping for mobile processes.
Applied Cryptography: Protocols
A sound type system for secure flow analysis.
--TR
Building a secure computer system
A calculus of mobile processes, I
A calculus of mobile processes, II
A lesson on authentication protocol design
Testing equivalence for mobile processes
Applied cryptography (2nd ed.)
Provably secure session key distribution
Prudent Engineering Practice for Cryptographic Protocols
Linearity and the pi-calculus
Proof-carrying code
A calculus for cryptographic protocols
A decentralized model for information flow control
From system F to typed assembly language
Secure information flow in a multi-threaded imperative language
The SLam calculus
A typed language for distributed mobile processes (extended abstract)
The Compositional Security Checker
A probabilistic poly-time framework for protocol analysis
A calculus for cryptographic protocols
A sound type system for secure flow analysis
The inductive approach to verifying cryptographic protocols
Using encryption for authentication in large networks of computers
Cryptography and Data Security
Handbook of Applied Cryptography
Java Virtual Machine Specification
A bisimulation method for cryptographic protocols
Protection in Programming-Language Translations
Reasoning about Cryptographic Protocols in the Spi Calculus
Control Flow Analysis for the pi-calculus
The Polyadic Pi-calculus (Abstract)
Robustness Principles for Public Key Protocols
Mobile Ambients
Secure Implementation of Channel Abstractions
Strategies against Replay Attacks
Proving Trust in Systems of 2nd-Order Processes
Limitations on Design Principles for Public Key Protocols

--CTR
Martn Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, ACM SIGPLAN Notices, v.37 n.1, p.33-44, Jan. 2002
Riccardo Focardi , Sabina Rossi, Information flow security in dynamic contexts, Journal of Computer Security, v.14 n.1, p.65-110, January 2006
Shahabuddin Muhammad , Zeeshan Furqan , Ratan K. Guha, Understanding the intruder through attacks on cryptographic protocols, Proceedings of the 44th annual southeast regional conference, March 10-12, 2006, Melbourne, Florida
Antonio Brogi , Carlos Canal , Ernesto Pimentel, Component adaptation through flexible subservicing, Science of Computer Programming, v.63 n.1, p.39-56, November 2006
Roberto Zunino , Pierpaolo Degano, Weakening the perfect encryption assumption in Dolev-Yao adversaries, Theoretical Computer Science, v.340 n.1, p.154-178, 13 June 2005
Michael Backes , Peeter Laud, Computationally sound secrecy proofs by mechanized flow analysis, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
Pankaj Kakkar , Carl A. Gunter , Martn Abadi, Reasoning about secrecy for active networks, Journal of Computer Security, v.11 n.2, p.245-287, May
Luca Cardelli , Giorgio Ghelli , Andrew D. Gordon, Types for the ambient calculus, Information and Computation, v.177 n.2, p.160-194, 15 September 2002
C. Bodei , P. Degano , F. Nielson , H. Riis Nielson, Flow logic for Dolev-Yao secrecy in cryptographic processes, Future Generation Computer Systems, v.18 n.6, p.747-756, May 2002
Grard Boudol , Ilaria Castellani, Noninterference for concurrent programs and thread systems, Theoretical Computer Science, v.281 n.1-2, p.109-130, June 3 2002
Fabio Martinelli, Analysis of security protocols as open systems, Theoretical Computer Science, v.290 n.1, p.1057-1106, 1 January
Eijiro Sumii , Benjamin C. Pierce, Logical relation for encryption, Journal of Computer Security, v.11 n.4, p.521-554, 01/01/2004
Luca Cardelli , Giorgio Ghelli , Andrew D. Gordon, Secrecy and group creation, Information and Computation, v.196 n.2, p.127-155, January 29, 2005
dependent types for higher-order mobile processes, ACM SIGPLAN Notices, v.39 n.1, p.147-160, January 2004
Benjamin C. Pierce, Type systems, Programming methodology, Springer-Verlag New York, Inc., New York, NY,
Andrew D. Gordon , Alan Jeffrey, Authenticity by typing for security protocols, Journal of Computer Security, v.11 n.4, p.451-519, 01/01/2004
Phan Minh Dung , Phan Minh Thang, Stepwise development of security protocols: a speech act-oriented approach, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA
Chiara Bodei , Pierpaolo Degano , Riccardo Focardi , Corrado Priami, Primitives for authentication in process algebras, Theoretical Computer Science, v.283 n.2, p.271-304, June 14, 2002
Martn Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM (JACM), v.52 n.1, p.102-146, January 2005
Peeter Laud, Secrecy types for a simulatable cryptographic library, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA
Martn Abadi , Bruno Blanchet, Secrecy types for asymmetric communication, Theoretical Computer Science, v.298 n.3, p.387-415, 11 April
Annalisa Bossi , Damiano Macedonio , Carla Piazza , Sabina Rossi, Information flow in secure contexts, Journal of Computer Security, v.13 n.3, p.391-422, 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
Christian Haack , Alan Jeffrey, Pattern-matching spi-calculus, Information and Computation, v.204 n.8, p.1195-1263, August 2006
David Monniaux, Abstracting cryptographic protocols with tree automata, Science of Computer Programming, v.47 n.2-3, p.177-202, May
Avik Chaudhuri , Martn Abadi, Formal security analysis of basic network-attached storage, Proceedings of the 2005 ACM workshop on Formal methods in security engineering, November 11-11, 2005, Fairfax, VA, USA
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
Giampaolo Bella , Stefano Bistarelli, Soft constraint programming to analysing security protocols, Theory and Practice of Logic Programming, v.4 n.5-6, p.545-572, September 2004
Martn Abadi , Cdric Fournet, Mobile values, new names, and secure communication, ACM SIGPLAN Notices, v.36 n.3, p.104-115, March 2001
Gilles Barthe , Tamara Rezk , Amitabh Basu, Security types preserving compilation, Computer Languages, Systems and Structures, v.33 n.2, p.35-59, July, 2007
cryptographic protocols;process calculi;secrecy properties