Security Goals: Packet Trajectories and Strand
Spaces

#
Joshua D. Guttman

The MITRE Corporation
Bedford, MA 01730 USA
guttman@mitre.org
Abstract. This material was presented in a series of lectures at fosad,

a summer school on Foundations of Security Analysis and Design, at the
University of Bologna Center at Bertinoro in September 2000. It has two
main purposes.
The first purpose is to explain how to model and analyze two important
security problems, and how to derive systematic solutions to them.
One problem area is the "packet protection problem," concerning how
to use the security services provided by routers---services such as packet
filtering and the IP security protocols---to achieve useful protection in
complex networks. The other problem area, the "Dolev-Yao" problem,
concerns how to determine, given a cryptographic protocol, what authentication
and confidentiality properties it achieves, assuming that the
cryptographic primitives it uses are ideal.
Our secondary purpose is to argue in favor of an overall approach to
modeling and then solving information security problems. We argue in
favor of discovering security goals for specific domains by examining the
threats and enforcement mechanisms available in those domains. Mathematical
modeling allows us to develop algorithms and proof methods to
ensure that the mechanisms achieve particular security goals. This leads
to a systematic approach to trust management, often a more pressing
information security problem than inventing new and improved security
mechanisms.
1 Introduction

We summarize here a series of lectures at fosad, a summer school on Foundations
of Security Analysis and Design, at the University of Bologna Center at
Bertinoro, in September 2000.
1.1 The Purpose of these Lectures

This series of lectures has two main goals. The first goal is to explain how to
model and analyze two important security problems, and how to design reliable
solutions to them, namely:

#

Work reported here was supported by the National Security Agency through US
Army CECOM contract DAAB07-99-C-C201. Work was in collaboration with Amy
L. Herzog, Jonathan C. Herzog, and F. Javier Thayer.

1. How to use the security services provided by routers---services such as packet
filtering and the ip security protocols---to achieve useful protection in complex
networks; and
2. How to determine, given a cryptographic protocol, what authentication and
confidentiality properties it achieves, assuming that the cryptographic primitives
it uses are ideal.
We refer to these two problems as the packet protection problem and the DolevYao
[9] problem respectively.
The second goal is to argue in favor of an overall approach to modeling and
solving information security problems, based around three ideas:
1. There does not exist any single property, which if we achieve it, will provide
the information security we need in every situation.
Instead, in each application area we must analyze the kinds of threat we face.
From this, we can abstract a class of properties that capture the di#erent
meaningful protections in this type of situation. We call each property in the
class a "security goal," and we regard the class itself as defining the range
of security that may need to be provided in this application area.
Di#erent application areas will lead to di#erent classes of security goals,
formulated in terms of di#erent modeling ideas.
2. Security goals need to be expressed using a simple, well-understood vocabulary
of mathematical notions, and we will use the same vocabulary to model
systems, the systems that we want to ensure will meet these security goals.
In this series of lectures, the mathematical vocabulary we use will include
boolean algebras and freely generated algebras of terms, as well as graphs.
The graphs will include directed and undirected graphs, and at various stages
we will need to partition either the nodes or the edges into distinct classes.
Needless to say, this vocabulary is very familiar and very easy to reason
about.
3. These mathematical notions themselves suggest algorithms and proof methods
that are useful for security management. The mathematical notions lead
to flexible and e#cient ways to resolve problems, such as:
(a) Does a given system meet a particular security goal?
(b) Given a system, what security goals does it meet?
(c) Given a security goal, how can we configure (or modify) a system to
meet it?
(d) Given a real-world system, how can we construct the abstraction that
models it?
(e) Given a real-world system, what automated tests (or manual analysis)
will check whether a given abstraction models it faithfully? Whether a
given security goal has been violated?
(f) If two given systems each meet a security goal, does each continue to
meet that security goal if they are combined in a particular way?
These questions are the core of the crucial real-world problem of security
management.
2

1.2 The Structure of these Lectures

We divide the remainder of our report into five sections.

Section 2 Packet Trajectories : Derived from [11, 13]. Coauthors: A. Herzog and
J. Thayer.

Contents : Introduce the packet protection problem. Define a class of security
goals that filtering routers can achieve. Network model. Algorithms to
determine whether given filtering behavior achieves a goal, and to assign
filtering behavior that will achieve a given goal. Abstraction from router
configuration files.

Section 3 Strand Spaces and Protocol Security Goals : Material derived from
[47]. Coauthors: J. Herzog and J. Thayer. Also from [14, 16]. Coauthor:
J. Thayer.

Contents : Cryptographic protocols and the Dolev-Yao problem. Why cryptographic
protocols fail: Unintended services. Powers of the penetrator. Strand
space definitions. Authentication and secrecy goals.

Section 4 Well-Behaved Bundles and Paths through Them: Material derived
from [16]. Coauthor: J. Thayer.

Contents : Bundle equivalence. Redundancies and redundancy elimination.
Paths. The normal form lemma. Rising and falling paths, bridges, e#ciency.
Proof of the secrecy theorem.

Section 5 Authentication Tests : Material derived from [14, 16]. Coauthor:
J. Thayer.
Authentication tests: proving authentication and secrecy. Proofs of the authentication
test results. Application to examples.

Section 6 Protocol Independence via Disjoint Encryption: Material derived
from [15]. Coauthor: J. Thayer.

Contents : Multiprotocol strand spaces, independence. Disjoint encryption.
Applications of protocol independence.
Copies of the papers cited above are available at URL

http://www.ccs.neu.edu/home/guttman/.
Acknowledgements I am grateful to my coauthors Amy L. Herzog, Jonathan
C. Herzog, and F. Javier Thayer. Dan Klain made numerous suggestions. Sylvan
Pinsky and Grant Wagner provided stimulus, support, and discussion.
2 The Packet Protection Problem

In this section, we explore one security mechanism, namely filtering routers (and
firewalls of related kinds). They are widely used to protect enterprises or their
parts from attacks that could be launched from outside them. Wide practical
experience exists as to the types of packets (identified by the ip, tcp and udp

headers) that are most capable of causing harm to their recipients, and firewall
3

administrators configure their enforcement mechanisms to trade the danger of
incoming datagrams o# against the value of the network services that they provide
and the level of trust in those that may have crafted the datagrams. We
will describe a systematic method to ensure that security policies of this kind
are faithfully implemented, despite the topological complexity of the networks.
Most of this material is contained in [11] in a more systematic style, although
the material on abstraction is previously unpublished.
We have carried out a similar study of how to use the ip security protocols
(IPsec) to achieve genuine confidentiality, authentication, and integrity. The ip

security protocols apply cryptographic operations to individual datagrams, and
they may be active either at the end systems (source and destination) exchanging
the datagrams, or else at intermediate routers ("security gateways") that
provide cryptographic services on behalf of nearby end systems. Indeed, IPsec

is currently used predominantly at security gateways, and there are large potential
advantages of management in doing so. A systematic way to be sure of
reaping those benefits is needed. That material is instead available in [13].
We start by considering the security goals that we would like to achieve. From
those, we infer a way of modeling the goals (and the systems that should meet
those goals) using simple mathematical notions. They in turn suggest algorithms
to solve our security management problems.
2.1 Packet Filtering

The purpose of packet filtering is to prevent the delivery of packets that may
harm the recipient, or occasionally to prevent the transmission of packets considered
inappropriate (e.g. http requests to unwholesome servers). The filtering
point must typically decide what action to take without examining the payload;
only the headers are typically examined by the devices we are concerned with.
Thus, aspects of the headers must be used as a clue to which packets ought to
be discarded.
2.2 An Example

For instance, icmp destination unreachable packets may be used to map an organization
's network, to the extent of determining what ip addresses are in use
and which routers are nearby. The attacker sends unsolicited icmp destination
unreachable messages with source ip address s into the organization. If the destination
address d for that message is not in use, then a router r near the network
on which d would lie sends back an outbound icmp destination unreachable

packet, with destination s. The source address for this packet is an ip address

r for the router itself. In this way, the attacker learns which addresses are not
in use (because an icmp packet is returned); the rest are in use. He also learns
which router r serves each missing ip address.
The scheme works because most firewalls permit icmp destination unreachable
 packets to pass, because they are a useful part of the network infrastructure.
4

If an organization would like to prevent this sort of probing, then its administrators
need to configure their routers (or firewall) to prevent it. They would
prefer to allow as many icmp packets as possible to pass around the network,
so long as the attack is prevented. To prevent the attack with the least loss
of service, the administrators would like to select a small number of filtering
routers. Those routers will be the enforcement points. Each path should traverse
an enforcement point, if that path leads from a network area where the attack
might be launched to a network area whose contents should not be disclosed.
The enforcement point could discard inbound icmp probes; indeed, it would
su#ce to discard inbound probes with destination addresses d that are not in
use. The outbound replies are generated only for these addresses, so filtering
these probes will ensure that no information is returned. Of course, this finer
strategy can be used only if this set is known when the router configuration
is chosen. Alternatively, the router could discard the outbound icmp response,
although in this case the packet source address is r, so that we cannot fine-tune
the behavior depending on which addresses are in use.
2.3 Types of Information in our Security Goals

There were two phases to the reasoning we have just described. One was to determine
a potential kind of attack, and to infer from it a kind of packet that should
be discarded, depending where that packet had come from. In the second phase,
we looked for enforcement points, and attempted to assign filtering behavior to
each enforcement point with the consequence that every harmful packet's path
would be disrupted. We try to do so without disrupting the paths of too many
other packets.
The security goal here is to prevent the delivery of certain packets, and the
definition of which packets involves two di#erent types of information. First, it
concerns what the header of the packet says. In our example, we were concerned
with the following ip header fields or protocol-specific header fields:

-- The protocol header field in the ip header, which must indicate icmp for this
concern to be relevant;

-- The icmp-specific fields for message type and message code, which jointly
indicate a destination unreachable message;

-- The ip destination address, in case we wish to filter only inbound probes
destined for addresses not in use.
In other examples, we would be concerned with the ip source address, or other
protocols such as tcp or udp, or with the protocol-specific fields for those protocols,
such as source or destination port number, and the tcp syn and ack bits.
All this information is contained in the datagrams, and available to any router
inspecting it.
The other kind of information concerns the path that the packet has taken
through the network. If the packet has never been on the public Internet, then
we do not have to worry whether it is an attempt to map our networks. That is,
5

assuming that we trust our employees not to attack us, or we acknowledge that
they have other ways to obtain mapping information if they intend to carry out
an attack.
The path information is not contained in the packet itself (certainly not in any
reliable form, given the ways that packets can be spoofed). Indeed, no individual
router can observe the whole path, but di#erent routers observe di#erent small
pieces of the path. The behavior of a router for a packet it receives is sensitive
to which interface the router received it over; and the behavior of a router for
a packet to be transmitted is sensitive to which interface it will be transmitted
over. The access lists governing filtering are specified on an interface-by-interface
basis. Thus, they are sensitive to a portion of the path. The art of achieving the
desired network-wide security therefore requires us to do di#erent filtering at
di#erent points in the network, thereby disrupting the paths that worry us. A
typical example network, containing enough information to represent the paths
of concern to us, may take the form shown in Figure 1.
Allied
Engineering Finance
Periphery
External
db

#

mail

#

mail

#

proxy

#
Fig. 1. Corporate Protection Example
The task of deciding on a security policy is simplified by the fact that information
we care about is a limited portion of the path information: We care
only whether the datagram was previously in a network region we do not trust,
and whether the datagram has reached a region we would like to protect. A
firewall policy can also enforce a confidentiality policy, thereby restricting the
flow of packets from a vulnerable (internal) area to an untrusted (external) area.
The strategy of filtering the outbound return icmp packets in our example is
a case of enforcing confidentiality (with regard to network information) via a
firewall. Naturally, more inclusive kinds of confidentiality are likely to be harder
to enforce reliably using a firewall.
6

2.4 The Logical Form of our Security Goals

From our intuitive analysis, we can now stipulate the logical form of the security
goals we would like to achieve. They integrate information about path with
information about header in a specific way. A security goal always concerns two
network areas a and a # , with one (say, a) traversed earlier and the other a #

traversed later. If a packet has followed any path from a to a # , then its header
fields should have some property #. Thus, a "policy statement" for pair of areas

a, a # is a statement of the form:

If p was in a and later reaches a # ,

then p's header fields satisfy #.

Thus, for our firewall analysis, we have identified a class of security goals. Each
goal describes a class of paths---those that traverse the areas a and a # in that
order---and says which packets, defined in terms of header fields, are permitted
to travel along those paths in the network. These firewall security goals are
characterized by this logical form, namely an implication in which the antecedent
mentions two areas in a particular order, and the consequent gives a constraint
on the packets traversing those areas.
A security policy, in this context, will mean a security goal for every pair of
areas. Given a graph in which the areas belong to a set A, a policy is a function

# : AA

#

B, where B is some suitable collection of sets of packets.
In other contexts, other security goals will be needed. For instance, the security
goals we can achieve using IPsec, as have discussed in [13], may take
di#erent logical forms or require di#erent real world ingredients to be modeled.
2.5 Some Security Goals

We have already mentioned two candidate security goals, each a possible way to
prevent the icmp destination unreachable network mapping attack. First, we may
prevent the attack by pruning the incoming probe. We assume that the attack
is possible only if the probe packet has passed through the External area (in
the terminology of Figure 1), and we assume that we are concerned only about
an attacker mapping our internal networks, labelled Engineering and Financial.
The Periphery network, being more exposed, may well be vulnerable to mapping
in any case. Thus, one security goal would be:

If p was in External and later reaches Engineering,

then p's header fields satisfy #,

where # stipulates

Either p.destination

##

Engineering,

or p.protocol

#=

icmp,

or p.message type

#=

destination unreachable.
7

Another example security goal in this network (assuming that most tcp connections
are proxied at the application level on the Proxy host on the Periphery
network) may be to ensure that no tcp packet travels from External to Engineering
unless it is an smtp packet, and its destination is the email server Eng mail.
In this case, the antecedent of the policy statement is unchanged, since we are
still concerned with what packets reach Engineering from External; the choice
of # is then:

p.destination = Eng mail,

and p.protocol = tcp,

and p.dest port = 25.
2.6 Security Modeling

Our analysis of the security goals we would like to achieve also suggests some
modeling decisions. We must model the paths of packets as they pass from a
network area across an interface to a router and then across another interface
to some other network area. Thus, we may regard the system as forming a
graph. The edges represent the interfaces, and since packets may flow in either
direction over an interface we may regard the edges as undirected. The nodes are
of two di#erent kinds, namely the router at one end of an edge and the network
area at the other end. Thus, we represent the system by a bipartite graph with
undirected edges. A diagram like Figure 1 summarizes this view of the topology
of the system.
Now, at each edge, for each direction, we have a filter that will be used to
discard some packets that would otherwise flow in that direction. The filter divides
all packets into two sets, those that are permitted to flow over the interface
in that direction and those that will be discarded. Since di#erent characteristics
of packet headers will be used to make these decisions, but presumably not
every set of packets will be relevant, we will regard the relevant sets of packets
as forming a boolean algebra, always a vastly smaller boolean algebra than the
boolean algebra of all sets of packet headers.
Since there are thirty-two bits of source address, thirty-two bits of destination
address, and eight bits for selecting protocols, there are at least 2

72

di#erent ip

headers, so at least 2

2

72

di#erent sets of ip headers. For icmp there are sixteen
bits of protocol specific message type and message code; for tcp there are sixteen
bits of source port and sixteen bits of destination ports, and likewise for udp.

Thus, we have many more sets considering these protocol specific header fields.
Naturally, many of these sets are ridiculously ragged, and play no role in any
meaningful network protection. The "practically useful" sets are comparatively
few and far between, and have smoother edges.
In our example above, there are just a few distinctions we need among ip

addresses. The special hosts have ip addresses that must be distinguished from
all others, since filters will need to permit packets through specially, if those
hosts are source or destination. Then the workstations in a particular network
area may need to be distinguished from those in any other area. Finally, for our
8

icmp example, we might want to distinguish the unused ip addresses in the three
internal corporate networks. This leads to a total of twelve relevantly di#erent

ip addresses, far less than the 2

32

di#erent addresses a priori. There is a big
advantage to taking a special-purpose representation of the boolean algebra of
relevant packet sets, rather than using a representation that could express all
the addresses and all the sets of addresses, and all the sets of packet headers.
Thus, our modeling process leads us to two ideas, the idea of a undirected
bipartite graph to represent the network, and the idea of a boolean algebra to
represent the constraints, both the sets permitted at the various filtering points
and also the #s used in the consequents of security goals. Let us see now what
problems we can solve using these two modeling ideas.
2.7 Localization

The core issue with our packet filtering security policies concerns localization. Although
our security properties are global properties about all paths from a to a # ,
even when these areas are distant from each other, our enforcement mechanism
consists of routers each of which must make its own decision. It has only local
information about what interface a packet has been received over, and what
interface it will be transmitted over. Localization is the problem of achieving
global security goals using this local information.
Localization may be used in two di#erent ways. First, we may know what
security goals we want to achieve, and also the filtering that will be applied
on each interface to packets flowing in each direction. Then the problem is to
decide whether each security goal is enforced by those filters. When they are
not satisfied, one would like to exhibit the undesirable packets and the paths by
which they may reach their targets.
Alternatively, we may decide on the security goals, and wish to discover an
assignment of filtering to interfaces that will achieve them. Each of these two
problems is a matter of localization, because the problem is to interrelate security
policies stated in terms of network-wide paths, with an enforcement mechanism
that must act locally at specific interfaces.
We will use the word posture to mean a specification of filtering behavior.
Filtering routers allow a di#erent set of packets to be filtered at each interface,
and in each direction of flow, into the router or out of the router. Thus, a filtering
posture will mean an assignment of a filter to each interface/direction pair. A
filter just means a set of packets, namely those permitted to traverse the interface
in that direction. The sets of packets are the members of some boolean algebra
that will be far smaller than the boolean algebra of all sets of packet headers.
2.8 Two Algorithms

We have mentioned two problems, namely
1. Given a security policy and a filtering posture, to determine whether the
posture faithfully enforces the policy, and if not, to enumerate the counterexamples;
and
9

2. Given a security policy, to construct a filtering posture guaranteed to enforce
the policy.
We will describe an algorithm to resolve each problem, for which we need some
auxiliary notions. Let p =

##

0 , . . . , # n

#

be a path p. Here, each # i is either an
area or a router in a bipartite graph such as the one in Figure 1, and p is a
path only if # i and # i+1 are adjacent for each i from 0 to n

-

1. We will write

p i for the i

th

entry in p; we will write

|p|

for the length of p; and we will write

p

|p|

for the last entry in p. We use p

#

p # to mean the concatenation of p with p # ,
which is well-defined only if p

|p|

= p # 0 , and is the path consisting of p followed
by p # , omitting the second occurrence of the common location at the end of p

and beginning of p # .
We also assume to simplify notation that each router has at most one interface
on any area. Thus, we regard a filtering posture as a function f : RAD

#

B,

where

R is the set of routers;

A is the set of areas;

D is the set containing the two directions in and out, meaning into the router
and out of the router, respectively; and

B is a boolean algebra of sets of packets.
We adopt the convention that f(r, a, d) =

#

when r lacks an interface on a.

Let #(# i , # j ) = f(# i , # j , out) when # i is a router and # j is a network area, and

f(# j , # i , in) otherwise. Thus, in either case it is the set of packets allowed to
traverse the interface from # i to # j .
We define

F(p),

the feasibility set for p, inductively:
1.

F(##)

=

F(##

0

#)

=

#,

the top member of the boolean algebra;
2.

F(p

#

##

i , # i+1

#)

=

F(p) #

#(# i , # i+1 ).
Thus, the feasibility set for a path p is the set of packets that survive all of the
filters that are traversed while following p. Observe that if the range of a filtering
posture f is in the boolean algebra B, then

F(p)

is also in B, for any p. Also,
by the laws of boolean algebra,

F(p

#

p # ) =

F(p) # F(p

# ).
2.9 Posture Checking

Suppose given a posture f and a security policy # : A

A #

B, we would like
to know whether f enforces # . What does this mean?
It means that whatever path a packet may take from area a 0 to an , if that
packet survives every filter it traverses, then it satisfies the policy constraint

F(p) #

#(p 0 , p

|p|

).
Note also that we may ignore any cyclic path p =

##

0 , . . . , # i , . . . , # i , . . . # n

#,

because

F(p)

=

F(##

0 , . . . , # i

#) # F(##

i , . . . , # i

#) # F(##

i , . . . , # n

#)
# F(##

0 , . . . , # i

#) # F(##

i , . . . , # n

#)

=

F(##

0 , . . . , # i

#

#

##

i , . . . , # n

#)

10

So p cannot cause more violations than its cycle-free part

##

0 , . . . , # i

#

#

##

i , . . . , # n

#.

Therefore, to find all violations, we need only enumerate, starting at each
area a, each cycle-free path p leading to another area a # = p

|p|

. We test

F(p) #

#(a, a # ). If this is false, we report as violations all packets in the set-di#erence

F(p) \

#(a, a # ), noting that the path p permits them to pass. If no cycle-free
path starting at any area a leads to violations, then f correctly enforces # .
Doubtless, this algorithm could be made more e#cient in several ways were
it necessary to handle large graphs.
2.10 Posture Generation

Suppose next that we have a security policy # that we want to enforce, and the
task is to construct a filtering posture f that does so. The idea of this algorithm
is this: We start with a simple but useful initial posture f 0 , and we correct it
successively to eliminate all violations.
The correction process enumerates all cycle-free paths p that start and end
at distinct areas a 0 and an . The next-to-last entry in p is a router r, because the
underlying graph is bipartite. Using the current approximation f i , we calculate

F(p).

If

F(p) #

#(a 0 , an ), then f i+1 = f i . Otherwise, we correct the violations

V , which are the packets in the set di#erence V =

F(p)\#(a

0 , an ), those packets
that may feasibly traverse the path p but are not permissible. The corrected
posture f i+1 di#ers from f i only for the arguments (r, an , out), where we have

f i+1 (r, an , out) = f i (r, an , out)

\

V . Observe that this algorithm modifies only
the outbound filters, not the inbound ones.
There are di#erent strategies for constructing the initial posture f 0 . A useful
choice is the following.
1. f 0 (r, an , out) =

#,

the top member of the boolean algebra;
2. For any datagram #, #

#

f 0 (r, a, in) if #.src

#

a, or else if, every a # adjacent
to r, #.src

##

a # .
This choice of f 0 uses the inbound filters to protect against spoofing: If a datagram
 # claims a source in some adjacent area a # , but is observed entering r from
some di#erent adjacent area a, then # must be lying. If it were really from a # ,
it would reach r o# its interface on area a # . This reasoning assumes that the
packet has not been routed along on odd path because some network resources
are currently down, but it matches an assumption that security-attuned network
administrators frequently want to make.
This algorithm is not guaranteed to be ideal. The correction process discards
packets only at the last step, immediately before they would finally cause a
violation. It may be preferable instead, in a particular case, to discard the packet
earlier, as it embarks on a path that will eventually lead to violations. Similarly,
the choice of an anti-spoofing initial posture f 0 may not be ideal. For instance,
a packet arriving at the External/Periphery router in Figure 1, inbound on its
External interface, which claims to be from Finance, is doubtless lying, but our
initial posture f 0 does not discard it. The reason is that Finance is not adjacent to
11

this router. We know something about the way that packets from Finance should
travel, but it would be hard to generalize that knowledge and incorporate it into
our algorithm.
A reasonable implementation, such as the one described in [11] or its successor,
the current Network Policy Tool (npt) software available from the author,
will combine this posture generation algorithm with the posture checking algorithm
described previously. Then a human user can edit the posture output by
the generation algorithm to make local improvements. The checking algorithm
may then be used to ensure that these "improvements" have not in fact introduced
violations. Alternatively, to understand why npt has done something
apparently unnecessarily complex, it is interesting to edit the output to the simpler,
expected form. The checking algorithm will then show what would have
gone wrong.
If one is given a posture f , it is also possible to calculate a security policy
that describes what f permits; it is the policy # f inferred from f . It is defined
by:

# f (a, a # ) =

#

p

F(p)

where the union is taken over all p of the form p =

#a,

. . . , a #

#.

2.11 Implementing Boolean Algebras

Any such piece of software needs to select a suitable data structure to represent
the members of the boolean algebra. Di#erent possibilities may be tried, although
it is natural to regard each packet as a triple, consisting of a source ip address,
a destination ip address, and "the rest."
The rest consists of information about the network service that the packet
provides. It includes the packet's protocol field (possible values being tcp, udp,
icmp, and so on), together with a variety of protocol specific fields. For instance,
for udp and tcp, the source port and destination port are important. If the
destination port is a well-known value like 25, then this packet is headed toward
a server (in this case an smtp server); if its source port is 25, then it is headed
from an smtp server to a client.
For tcp, so are the syn and ack bits that say whether the packet belongs
to the set-up phase of a connection, or to a connection that has already been
negotiated. For icmp, the message type and code are relevant.
Since each packet is characterized by the three dimensions of source, destination,
and service, a boolean algebra of sets of packets may be regarded as
consisting of regions of a three dimensional space. Although it is a large space,
we are in fact interested only in rather coarse regions. For instance, looking at
a diagram such as Figure 1, we can see that the number of relevantly di#erent
addresses is quite low, nine in fact:

-- There are four specific systems mentioned, that will need special treatment in
defining policy and implementing a suitable posture. They are engineering
db, engineering mail, finance mail, and periphery proxy.
12

-- Hosts other than these are treated uniformly according to the area in
which they are located. Thus, we have engineering other, finance other,
periphery other, external any, and allied any.

We also call these "relevantly di#erent" addresses abstract addresses.

A similar consideration of the protocols and services that the network supports,
and of the policy for permitting them from area to area, might lead to a
short list of relevantly di#erent services, for instance,

-- icmp, distinguishing destination unreachable messages from all others;

-- tcp, distinguishing ftp, smtp, and http by their well-known ports;

-- udp, distinguishing messages to a particular port on the engineering db

machine, on which a data base server is listening;

-- all other protocols.
In addition, for the distinguished tcp and udp services, one will want to treat
packets di#erently depending whether the packet is traveling from client to
server or vice versa; this doubles the number of distinguished tcp and udp services.
There is one additional service grouping together all others, the "undistinguished
" services. On our example, we have thirteen relevantly di#erent services:

-- Two icmp services;

-- Seven (= 3



2 + 1) tcp services;

-- Three (= 1



2 + 1) udp services;

-- One for the others.
We also call these relevantly di#erent services abstract services.

All in all, there are 9913 = 1053 relevantly di#erent packets in this example,
leading to 2

1053

sets in the boolean algebra. Naturally, far fewer sets will come up
in any relevant computation. Observe that these "relevantly di#erent packets,"
called "abstract packets" in [11], are the atoms of the boolean algebra, in the
sense that any two atoms have a null intersection, and any set in the algebra is
a union of atoms. Thus, an abstract packet is a triple, consisting of two abstract
addresses (source and destination) together with an abstract service. Examples
of these abstract packets, shown as triples of abstract source, destination, and
service, would be:

(external any, engineering any, ICMP dest unreachable)
(engineering db, allied any, UDP db from server)
(engineering mail, external any, TCP smtp to server)

Each of these represents a set of possible concrete (real) packets, namely all
those with ip addresses matching the source and destination, and protocol specific
header fields matching the service. It thus represents a cube in the three
dimensional space of real datagrams, being the intersection of the sets of packets
matching each of the three dimensions individually.

1

There are di#erent ways to

1

If there were some natural sense of adjacency for the points on the axes, this would
amount to a finite union of cubes. Since we do not recognize any natural notion of
adjacency, we collect together the matching intervals along any one axis, and regard
the region as a single cube.
13

represent the algebra with these atoms. In npt, we represent any set as a list of
cubes, although we treat the source and destination dimensions specially. The
lists are maintained in a form such that no source destination pair lies in the
projection of two di#erent cubes. For this reason, we described the lists as lists of
colored rectangles, where the source-destination rectangles were always disjoint,
and the permissible services for the packets with those sources and destinations
were regarded as a coloring.
Wool and his colleagues [34] follow [11] in representing sets of packets as
lists of disjoint colored rectangles, although in their work the relevantly di#erent
sources and destinations are not inferred at the start. Instead, they are constructed
by examining real configuration files, and splitting ip addresses into
ranges according to the access list lines contained in the configuration files.
One might alternatively dispense with lists of rectangles and instead represent
the sets more directly, for instance using Binary Decision Diagrams (bdds) [3]. In
our next section, we will instead consider how bdds can be used as an auxiliary
structure to discover the set of atoms that naturally describe existing configuration
files.
2.12 The Abstraction Problem

We have described how to use a boolean algebra in which the atoms are abstract
packets as a way to represent problems about distributed packet filtering. But,
how can we construct a boolean algebra that is faithful to the distinctions made
in a particular set of configuration files? That is, we would like to take the
configuration files for a given set of filtering routers, and deduce from them a
set of abstract addresses and abstract services, such that the filtering posture
determined by these configuration files can be represented in the resulting three
dimensional boolean algebra. Indeed, we would prefer to choose the coarsest such
boolean algebra, so that our abstract addresses and services make the minimum
number of distinctions compatible with the files themselves. This is the problem
addressed in [12], for which the binary decision diagram is an ideal data structure.
An abstract address is a set s of concrete ip addresses such that i, j

#

s implies
that replacing i by j as the source or destination of a packet never transforms
a packet rejected by a filter into a packet accepted by it, or vice versa. A set of

ip addresses is an atom for a filtering posture is this holds for all of the filters
specified by its configuration files.
The problem is the more pressing because the router configurations of real
organizations evolve over time as hosts and routers are added to the network or
removed; as users clamor for additional services or administrators worry about
new attacks; and as sta# comes and goes with an increasingly hazy understanding
of the contributions of their predecessors. Indeed, their decisions are typically
documented only in the configuration file itself, with its low-level, procedural
notation and inflexible syntax.
From our point of view, a configuration file such as for a Cisco router, contains

interface declarations and access lists. An interface declaration may specify a
14

particular access list to apply to packets arriving inbound over the interface or
being transmitted outbound over the interface.
An access list is a list of lines. Each line specifies that certain matching packets
should be accepted ("permitted") or discarded ("denied"). When a packet
traverses the interface in the appropriate direction, the router examines each
line in turn. If the first line that matches is a "deny" line, then the packet is
discarded. If the first line that matches is a "permit" line, then the packet is permitted
to pass. If no line matches, then the default action (with Cisco routers)
is to discard the packet.
For instance, the lines in Figure 2 permit two hosts (at ip addresses 129.83.10.1
and 11.1) to talk to the network 129.83.114.#. They also permit the other hosts
on the networks 129.83.10.# and 129.83.11.# to talk to the network 129.83.115.#.
The asterisks are expressed using a netmask 0.0.0.255, meaning that the last
octet is a wildcard.
! (comments start with !)
!
! keyword num action prot source destination
access-list 101 permit ip host 129.83.10.1 129.83.114.0 0.0.0.255
access-list 101 permit ip host 129.83.11.1 129.83.114.0 0.0.0.255
access-list 101 deny ip host 129.83.10.1 any
access-list 101 deny ip host 129.83.11.1 any
access-list 101 permit ip 129.83.10.0 0.0.0.255 129.83.115.0 0.0.0.255
access-list 101 permit ip 129.83.11.0 0.0.0.255 129.83.115.0 0.0.0.255
Fig. 2. A Cisco-style Access List
2.13 The Logic of Access Lists

Each line of an access list defines a set of sources # s , destinations # d , and service
characteristics # v , and stipulates whether matching packets should be discarded
or passed. A datagram # matches a line if #.src

#

# s

#

#.dst

#

# d

#

#.svc

#

# v .
At any stage in processing, a packet that has not yet been accepted or rejected
is tested against the first remaining line of the list. If the line is a "permit" line,
the packet has two chances to be permitted: it may match the specification for
the first line, or it may be permitted somehow later in the list. If the line is a
"deny" line, the packet has to meet two tests to be permitted: it must not match
the specification for the first line, and it must be permitted somehow later in the
list. Since the default is to deny packets, the empty list corresponds to the null
set of permissible packets. Thus, we have a recursive function # of the access list:

#([ ]) =

#

#((permit, # s , # d , # v ) :: r) = (# s

#

# d

#

# v )

#

#(r)
#((deny, # s , # d , # v ) :: r) = #(r)

\

(# s

#

# d

#

# v )
15

The function # allows us to transform a parser for the individual configuration
file lines (emitting sets describing the matching conditions) into a parser that
emits a set describing the meaning of the whole access list.
2.14 Binary Decision Diagrams

Again we face the question how to implement the boolean algebra of sets in
this context, and for our current purpose of solving the abstraction problem, the
binary decision diagram [3] fits our needs perfectly.
A binary decision diagram (bdd) is a finite directed acyclic graph with two
sinks, labelled true and false. Each interior node has out-degree two, and is
labeled with a propositional (bit-valued) variable. One out-arrow is associated
with the variable taking the value true and the other with the variable taking
the value false. One node is distinguished as the root.
A bdd n represents a propositional function; that is, it yields a truth value as
a function of a number of truth-valued variables: to evaluate it for an assignment
of values to the variables, we start at the root and follow a path determined as
follows:
1. If we have reached a sink, its label is the result.
2. If the current node is labeled with variable v, and the assignment associates

v

##

b, then we traverse the arrow associated with the value b.

Observe that any node n # accessible from a bdd n is itself a bdd. If # is an
assignment of truth values to the variables, then we write #(n) for the truth
value that results from evaluating n at #, i.e. traversing n as described above.
An example is shown in Figure 3, page 18. Each node represents a choice for
the truth value of the variable shown at the right margin. The line marked +
represents the result if that variable is true; the other line represents the result
if that variable is false.
A bdd n is ordered if there exists an ordering

#

on the variables such that

v

#

v # if any traversal starting at n encounters v before v # . A bdd n is reduced

if, whenever n 0 and n 1 are accessible from n and n 0

#=

n 1 , then there is some
variable assignment # such that #(n 0 )

#=

#(n 1 ). Thus, a bdd is reduced if its
nodes obey the extensionality principle that di#erent nodes represent di#erent
propositional functions. Algorithms for maintaining bdds in ordered, reduced
form are found in [2].
In our case, we are interested in using bdds to represent sets of packets. Since
a packet is determined by source address, destination address, and protocolspecific
information, the propositional variables are the thirty-two bits of the
source address (for ip Version 4), the thirty-two bits of the destination address,
and a number of bits representing the protocol-specific information (sixty-four
bits is enough). Thus, any protocol header may be summarized, to the extent we
need to model how filter routers treat it, as a sequence of 128 bits. Any filter (set
of packets) may therefore be represented as a reduced, ordered binary decision
diagram where each internal node is labeled with one of these 128 propositional
variables.
16

An example bdd is shown in Figure 3; in this diagram, we have assumed
that ip addresses are only three bits, and that protocol-specific information may
be summarized in four bits. The nodes are thus labeled s 1 , s 2 , s 3 , d 1 , d 2 , d 3 , and

p 1 , p 2 , p 3 , p 4 . The variables are grouped into three sections representing source
information, destination information, and protocol information.
2.15 Finding Atoms in BDDs

Suppose that we are given a bdd like the one in Figure 3, in which the variables
have been divided into sections. We would like to identify the sets of values
in each section that are treated as atoms. For instance, we will identify the
sets of ip addresses that are treated the same as packet source addresses, so
that if two addresses i, j belong to the same atom, then a packet with source
address i and the identical packet with source address j will necessarily receive
the same treatment from the packet filter. Two concrete addresses belong to
the same abstract addresses if they are treated the same as sources and also as
destinations.
To find the source atoms, we will enumerate the outcomes , meaning those
nodes that are not labeled by source variables, but lie at the end of an arc
starting at a node labeled by a source variable. In our example (Figure 3), one
of these nodes is enclosed in a small box. If two paths lead to the same outcome,
then those paths can make no di#erence: in combination with any assignment
to the remaining variables, either both paths evaluate to true or else both paths
evaluate to false. For instance, let p 1 be the path that assigns T to s 1 and s 2 ,
and F to s 3 ; let p 2 be the path that assigns F to s 1 and s 2 , and T to s 3 . Then
both p 1 and p 2 lead to the boxed outcome. Therefore they must belong to the
same source outcome.
On the other hand, if two paths through the source variables lead to different
outcomes, then because the bdd is in reduced form, there must be at
least one assignment to the remaining variables that leads to di#erent outcomes.
Therefore, the paths do not belong to the same source atom.
This way of thinking suggests some definitions and an algorithm. First, let
us call a sequence of variable/value pairs a path if the variables occur in an order
compatible with

#.

Some examples of paths involving only source variables are:
(s 1 , true), (s 2 , true), (s 3 , false)

(s 1 , false), (s 2 , false), (s 3 , true)

(s 1 , false), (s 3 , true)

We say that a path p leads from n 0 to n k , and write n 0

p

-#

n k , if there is a
sequence of arcs leading from n 0 to n k , and each node n i for i  is labeled by
a variable v i mentioned in p, and the arc from n i to n i+1 is labeled by the truth
value paired with v i in p. There may be several paths leading from n 0 to n k . On
the other hand, a particular path may not lead anywhere in a given bdd: the
third path just mentioned does not lead anywhere in the bdd of Figure 3. In
that bdd, each path involving s 1 and s 3 needs also to specify a value for s 2 .
17

s 1
s 2
s 3
d 1
d 2
d 3
p 1
p 2
p 3
T F

+
+ +
+ +
+
+
+ +
+
+
+
+
+
+ + +
+ +
+
Fig. 3. An example bdd
18

We may interpret each path as a formula in the obvious way, namely as a conjunction
in which each variable in the path occurs negated if the associated value
is false and unnegated if it is true. For convenience, we write the interpretation
of a path p as [[p]]. With this notation, we have the following interpretations for
our example paths:
[[(s 1 , true), (s 2 , true), (s 3 , false)]] = s 1

#

s 2

# s

3

[[(s 1 , false), (s 2 , false), (s 3 , true)]] =

s

1

# s

2

#

s 3

[[(s 1 , false), (s 3 , true)]] =

s

1

#

s 3

If s is a set of paths, we use [[s]] to mean the disjunction

#

p#s

[[p]]. Thus, for
instance, if s contains the three paths mentioned above, then
[[s]] = (s 1

#

s 2

# s

3 )

#

(s 2

# s

3 )

#

(s 1

#

s 3 )
We also say that m is an outcome for n if for some path p, n

p

-#

m, and m

does not lie in the same section as n, but if p # is any proper subpath of p and

n

p #

-#

n # , then n # lies in the same section as n.

We can now see that each atom rooted at n 0 is of the form [[{p : n

p

-#

m}]]

where m is an outcome for n. For if p, p # are two paths such that n

p

-#

m

and n

p #

-#

m, then they surely belong to the same atom. Since they re-join
at m, no assignment to the remaining variables can cause p and p # to lead to
di#erent results. Moreover, if two paths lead to di#erent outcomes, then by the
extensionality principle for reduced bdds, there must be some assignment to the
remaining variables that separates them.
2.16 An Algorithm for Finding Atoms

The analysis we have just carried out motivates an algorithm for finding atoms
in a bdd that has been divided into sections like Figure 3, where the sections
consist of the source address variables, the destination address variables, and the
protocol-specific variables. The two sinks lie below all three sections.
The algorithm maintains a hash table h that associates each outcome with
the paths that lead to it. The algorithm has two phases. Phase one traverses
the bdd rooted at n 0 , and phase two traverses the hash table. In phase one, we
recursively descend the bdd. If the node n at the end of the current path p is
an outcome for n 0 , then:

If h contains an entry s for n, then the new entry for n in h is

{p} #

s;

Otherwise the initial entry for n in h is the singleton

{p}.

If n is not yet an outcome, recursively consider both extensions of the path p.

In phase two, we walk the hash table h. Each entry associates an outcome
node n with the set s of paths leading from n 0 to n. Each entry determines an
atom with value [[s]]. Since every path from n 0 must eventually leave the section,
each path reaches some outcome, which entails that the union of all the atoms is
19

exhaustive. The atoms are mutually exclusive because any path reaches at most
one outcome. Thus, we have derived a partition of the set of source addresses.
As described, this algorithm discovers the source atoms, those sets of source
addresses that are treated the same by a single filter, when appearing as ip packet
sources. The destination atoms may be calculated in the same way, starting from
each outcome n that arose in finding the source atoms. Each outcome n leads
to a list of destination atoms, containing those destination addresses that are
treated the same starting from n. The algorithm is executed once starting for
each source outcome n, each time yielding some destination outcomes. Finally,
service atoms may be discovered starting from each of these destination-atom
outcomes; in calculating the service atoms, the remaining outcomes can only be
the two sinks true and false.
2.17 Source and Destination Addresses, Multiple Filters

So far, we have computed a partition of the set of source addresses; a family
of partitions of the set of destination addresses, starting from various sourceatom
outcomes; and a similar family of partitions of services. This calculation
analyzes a single filter. Several filters may be defined for di#erent interfaces (and
opposite directions of traversal) within the same configuration file, and several
configuration files for di#erent routers may need to be analyzed. How do we put
all of these pieces together? Let us concentrate on constructing the right abstract
addresses, the treatment of abstract services being essentially the same.
In essence, we have a number of partitions

F

i of the ip addresses. Each partition
is a congruence with respect to one condition, such as the source addresses
of packets passing through a particular filter, or the destination addresses, assuming
that the source led to a particular outcome. We call each of these families
a family of pre-atoms. We want to construct a single partition of the ip addresses
which is a congruence with respect to all of the conditions. It will thus be the
coarsest common refinement of the

F

i .
To do so we must split the pre-atoms of

F

i wherever the pre-atoms of

F

j

overlap with them. Let s i

# F

i and s j

# F

j , and define superimpose(s i , s j ) to
be either the tag None or the tag Some applied to a triple of sets:

-- None, if s i

#

s j =

#;

-- Some((s i

#

s j ), (s i

\

s j ), (s j

\

s i )), otherwise.
To add a single pre-atom s i to a list f representing a family of pre-atoms we
recursively apply the following procedure:

-- If f is the empty list [ ], then the result is the singleton list [s i ].

-- Otherwise, f is of the form s j :: rest . If the result of superimposing s i on s j

is None, recursively add s i to rest , obtaining f # , and return s j :: f # .

-- If the result of superimposing s i on s j is Some(c, s # i , s # j ), then recursively add

s # i to rest , obtaining f # , and return c :: s # j :: f # .
Finally, if we have two families, represented as lists f 1 and f 2 , then to combine
them:
20

-- If f 1 is the empty list [ ], then return f 2 .

-- Otherwise, f 1 is of the form s 1 :: rest . Recursively, combine rest with f 2 , and
then add the single pre-atom s 1 to the result (as defined above).
2.18 Atomizer Results

The Atomizer has been implemented as a rather large program written in OCaml,
an implementation of ML developed at inria/Rocquencourt [25]. When run
against a set of three unusually large configuration files in actual use, containing
1380 lines of access lists, it constructs about a hundred atoms. Computation
takes 29 seconds on a 550MHz Pentium iii with 700MB of store. The maximum
process size is 58MB of store. The bulk of the space seems to be devoted to
storing the bdds, so that re-implementing that data structure in C (which is
accessible from OCaml) would probably reduce the space used significantly.
When run against even larger but artificially generated configuration files,
containing 5,575 lines of access lists, it completes in 20.5 seconds, having occupied
45MB of store.
The Atomizer generates abstract addresses and abstract services to be used
in npt, thus providing a method for analyzing actual router configurations to
discover the security goals that they jointly achieve in use.
2.19 Packet Trajectories and Security Management

In this section, we have modeled the trajectories that packets may take through
networks. We regard the networks as bipartite graphs, in which a node is either
a router (used as an enforcement point) or a network area. Edges represent a
router's interface on a network area. The packets that can survive all of the filters
on a particular path form the feasibility set for that path. Given an implementation
for boolean algebras and their fundamental operations, we can calculate
feasibility sets, and use them to answer questions. We described an algorithm to
determine whether a given posture meets a security policy. Another algorithm
constructs a posture that will meet a security policy. We also described an algorithm
that uses binary decision diagrams to determine (from a number of actual
configuration files) the atoms that will be needed in the boolean algebra for these
computations.
Thus, this approach to modeling allows us to answer a number of di#erent

security management questions about our networks. In the introduction, we
enumerated some crucial security management questions. Let us return to that
list, and comment on the extent to which our methods, as described in this
section, give answers to them, in the specific context of packet filtering.
1. Does a given system meet a particular security goal?
If the system is described in terms of the abstract packets passed or discarded
at the di#erent filtering points, then npt answers this question.
21

2. Given a system, what security goals does it meet?
We use the Atomizer to construct a suitable boolean algebra and representations
of the filters. Then, given any two areas a, a # , we can calculate the
union of the feasibility sets

#

p

F(p)

for all p such that p 0 = a and p

|p|

= a # .
This union is the most inclusive security policy enforced by these filters.
3. Given a security goal, how can we configure (or modify) a system to meet
it?
We have described how to use npt to calculate a posture to enforce the
policy. We have not, however, described an algorithm to construct a (procedural,
Cisco-style) configuration file from a list-of-rectangles specification
for a filter, or from a bdd representing it, although work has been done in
this direction.
4. Given a real-world system, how can we construct the abstraction that models
it?
Network mapping tools may be used to construct the bipartite graph for the
system, after which the Atomizer designs the necessary abstractions for the
filters.
5. Given a real-world system, what automated tests (or manual analysis) will
check whether a given abstraction models it faithfully? Whether a given
security goal has been violated?
Our methods can be used to discover what packets are expected to emerge
from a given interface; by sni#ng the network and sampling the headers, we
can raise an alarm if an unexpected packet is found. See also [22], in which
specifications are used to generate test cases systematically.
6. If two given systems each meet a security goal, does each continue to meet
that security goal if they are combined in a particular way?

npt can be used to determine the security consequence of adding direct
network connections between previously distant areas.
Thus, we have illustrated in some breadth how to specify and reason about netwide
security policies for filtering routers, providing an instance of the rigorous
approach to security management.
3 Strand Spaces and Protocol Security Goals
In the remainder of this series of lectures, we will discuss cryptographic protocols.
We would like to define a particular type of failure, and the class of security goals
that rule out these failures. We will explain our modeling for cryptographic
protocols and their security goals in this section, and illustrate how to use the
modeling ideas to detect flaws in protocols that have them. In Section 4 we will
give a more rigorous treatment, leading to a simple method for proving that keys
are not disclosed. Section 5 focuses on how to prove authentication goals. Finally,
in Section 6, we will explain how to determine whether mixing two protocols will
cause interactions that will undermine their (separate) security guarantees.
22

3.1 What is a Cryptographic Protocol?

A cryptographic protocol is a short, convention-bound sequence of messages. It
uses cryptography to aim at security services such as authentication and key
distribution (or key agreement) for session keys.
Despite their simplicity, cryptographic protocols are frequently wrong. Lowe
estimates that about half the protocols published fail to achieve their goals in
some respect [28]. Since this comment concerns only published, peer-reviewed
protocols, one may imagine that the success rate for proprietary protocols would
be lower. However, as a consequence of intense work on this problem, including
apparently hundreds of published papers,

2

the quality of newer protocols such
as ssh [50] and tls [8] seems much better.
The problem is tricky because an attacker ("the penetrator") can be an
active participant on the network itself. The attacker can start sessions with
other principals, or wait for them to start sessions with each other or with
the attacker (not realizing that the attacker is malicious). The penetrator can
encrypt or decrypt using public keys, or legitimately obtained secret keys, or
stolen keys, or keys extracted from messages. The penetrator can prevent the
regular participants from receiving messages, and can substitute messages of his
own.
3.2 The Dolev-Yao Problem

Because of this collection of potential tricks, it is di#cult to see what the penetrator
can accomplish. Indeed, the penetrator can sometimes undermine the
goals of a protocol without any cryptanalysis. The attacks would succeed even
if the protocol was implemented with ideal cryptography. The idea of studying
protocol correctness without regard to cryptographic flaws is due to Dolev and
Yao [9].
The terminology of correctness and flaws is, however, too crude. The question
is really what security goals a cryptographic protocol can achieve. A "flaw" is
a counterexample that shows that a protocol does not achieve some goal that
we thought it should meet. A correct protocol is one that achieves specific goals
that we find useful.
Thus, a more nuanced way to state the Dolev-Yao problem is, to determine,
given a cryptographic protocol, what security goals it achieves, and to find counterexamples
showing why it does not meet other goals. In doing so, one assumes
that the cryptography in use is ideal, meaning that one cannot determine anything
about plaintext from ciphertext, or anything about ciphertext from plaintext,
without possessing the decryption or encryption key (respectively).
The problem is important, because cryptographic protocols are a central
part of the infrastructure for secure communications and networking, and for

2

See [6] for an extensive bibliography through the mid-nineties. Indeed, the present
chapter has 50 citations, despite not citing large numbers of papers in the literature.
For instance, we do not even cite [4], let alone the hordes of papers derived from it.
23

distributed systems and electronic commerce. Their importance applies equally
to military and civil systems. The Dolev-Yao approach of separating cryptographic
issues from structural protocol flaws is valuable for two main reasons.
First, it allows us to discover this class of flaws unencumbered by the complexity
of cryptographic issues. Second, the same protocol can be implemented using a
variety of di#erent cryptographic algorithms; the Dolev-Yao approach tells us
whether even the best adapted implementation can achieve its goals.
3.3 An Example: The Needham-Schroeder Public Key Protocol

The famous Needham-Schroeder article [37] introduced the idea of using cryptographic
protocols to achieve authentication for networked systems. It discusses
both secret-key and public-key protocols, and proposed one of each, both of
which were problematic. Let us examine the public-key protocol. In this protocol
(as presented here) each participant has the other's public key, guaranteed
using some public-key infrastructure assumed reliable. The initiator A constructs
a nonce---a randomly chosen bitstring---N a and transmits it to the recipient B

accompanied by A's name, encrypted in B's public key. B, if willing to have a
conversation with A, replies with a nonce N b of his own construction, accompanied
by N a and encrypted with A's public key. Finally, A replies with N b ,
translated now into B's public key. This is summarized in Figure 4. We write
A {|Na

A|}KB #

{|Na

A|}KB #

B
.


w

#

{|Na

N b

|}

KA #

{|Na

N b

|}

KA

.


w
.


w

{|N

b

|}

KB # {|N

b

|}

KB #

.


w
Fig. 4. The Needham-Schroeder Protocol
{|t|}

K to mean the encryption of t by K, and t t # to mean the concatenation of t

and t # . The protocol is intended to authenticate A and B to each other, and to
assure them that they share the secret values N a and N b . These values may be
combined (for instance, using exclusive-or) for a symmetric session key.
One of the most important parts of Figure 4 is the whitespace that separates
the left side from the right side. The initiator A knows that on a particular
occasion he sent

{|N

a A|} KB and then received

{|N

a N b

|}

KA , but he certainly does
not know that B received the outgoing message and sent the reply. Otherwise,
there would be no need for authentication. On the contrary, A needs to deduce
from the way that the protocol is constructed, that if

{|N

a N b

|}

KA came back,
only B can have sent it, assuming that B's private key, K -1 B , is uncompromised.
Protocol analysis is the art of inferring what others have done, knowing only
what one has done oneself, and the laws of the protocol.
24

Unfortunately, in this protocol, we cannot simply ignore the whitespace.
There is another way that things can fit together, if a malicious penetrator
is present, shown in Figure 5. The attack is due to Lowe [27], and was discovered
a decade and a half after the protocol was published. A has initiated a session
A {|Na

A|}K P

#

P
.


w

{|Na

A|}KB

#

B
.


w
w
w
w
w
w

#
{|Na

N b

|}

KA

.


w
.


w

{|N

b

|}

K P

#

P
.


w

{|N

b

|}

KB

# .


w
w
w
w
w
w
Fig. 5. A Bundle: Penetrated Run of Needham-Schroeder
with a participant P who has decided to misbehave, possibly in response to this
opportunity. As a consequence of A's bad luck, B is duped. B believes that he
shares the confidential values N a , N b with A, whereas messages encrypted with
the resulting session key will come from P .

A is not duped, because A intended to communicate with P and has done
so. B is duped, because B believes that A is sending messages to B using the
resulting session key, whereas P is doing so. Secrecy has failed, because the
nonces and session key are known to P , and authentication has failed, because

A has no run of the protocol intended for B, whereas B has a run apparently
with A. How has this situation come about?
3.4 Unintended Services

The protocol itself imposes an obligation on A, when A starts a run as initiator,
with responder P . A transmits a value N a , and then undertakes to provide
a service. If a value of the form

{|N

a N

|}

KA is presented (for any N ), then A

will perform a translation. A will translate N into the form

{|N |}

KP . Thus, N

is retransmitted in a form that P can read. We call this an unintended service,
because the protocol requires initiators to perform it, despite its being potentially
useful to penetrators.
Indeed, getting N in a readable form is particularly useful to a penetrator,
and the reason for this becomes clear when we consider how the responder B

gets his authentication guarantee. B can get a guarantee that A is executing his
matching run only by receiving some message from B that only A can produce,
and only in a matching run.
If we look at B's behavior, he receives only two messages. The first message
is of the form

{|N

A|} KB . Since KB is public, anyone can create a nonce N ,
25

concatenate it with A's name, and encode it with the public key. Therefore,
from the point of view of its authenticating force, this message is mere junk. It
contributes to no guarantee. Thus, any authenticating force is concentrated in
the last message

{|N

b

|}

KB .
Thus, we may examine a principal's incoming messages to determine which
are junk. Discarding the junk messages, we are left with the other messages,
those capable of providing authenticating force. We then examine the protocol to
see what unintended services it provides, and whether these unintended services
su#ce to counterfeit the non-junk messages. This is a practical recipe for informal
protocol analysis.
3.5 Another Example: An ISO Candidate

The protocol shown in Figure 6 was a candidate considered by an iso committee
as a pure authentication protocol. No shared secret is achieved. It was intended
merely to assure each principal that the expected partner was initiating communications.
In this protocol A uses his private key K -1 A to sign nonces passed to
A
ANa # ANa #

B
.


w

# {|N

b Na A|} K -1 B # {|N

b Na A|} K -1 B

.


w
.


w
w

{|N

# a N b B|} K -1 A # {|N

# a N b B|} K -1 A #

.


w
w
Fig. 6. An iso Candidate Protocol
B, and conversely. Considering how A may authenticate itself to B, clearly the
first, unsigned message is junk. Thus, the last message

{|N

# a N b B|} K -1 A

contains
any authenticating force. Thus, we want to look for unintended services that
would create a value of this form.
The possible services are the two transformations shown in Figure 7. In these
services, any variables originating in incoming messages may be freely renamed.
Those originating on outgoing messages, by contrast, are created by the principal,
and therefore cannot be manipulated by the penetrator. Now if A is active
as a responder, and is presented with the values BN b in the incoming message,
then the target term

{|N

# a N b B|} K -1 A

will be the result.
The resulting attack is shown in Figure 8. Since it was discovered by the
Canadian representatives to the committee, it is sometimes called the Canadian
attack. To discover this attack, we discarded junk messages and focused on the
remaining non-junk target. The unintended services provided by the protocol
then give us a recipe for generating our target message. In fact, it is easy to multiply
examples in which this method of junk messages and unintended services
lead us to attacks.
26

.

ANa

#

B
.

# {|N

b Na A|}

K -1 B # {|N

b Na A|}

K -1 B

.


w
w
w
.


w
w
w

{|N

# a N b B|} K -1 A #

.

Fig. 7. Unintended services in the iso candidate
P
ANp

#

B
P

# {|N

b Np A|} K -1 B

.


w
w
P


w

BN b

#

A
P

# {|Na

N b B|}

K -1 A

.


w
w
P


w
w

{|Na

N b B|} K -1 A #

B


w
w
w
w
w
w
w
w
w
w
w
w
w
w
w
Fig. 8. The Canadian Attack
27

3.6 Types of Unintended Service

There are e#ectively four types of unintended service that a protocol can o#er
to the penetrator.

Signature In a signature service, a protocol entity is required to sign messages
containing an incoming ingredient.
The transformation is N a

## {|

N a

|}

K -1 . The Canadian attack of Section
3.5 is an example.

Encryption In an encryption service, a protocol entity is required to encrypt
messages containing an incoming ingredient.
The transformation is N a

## {|

N a

|}

K . It frequently occurs in protocols
in which the ability to encrypt using a symmetric key is used as an authenticating
characteristic.

Decryption In a decryption service, a protocol entity is required to decrypt
messages containing an incoming ingredient.
The transformation is

{|

N a

|}

K

##

N a . This one does not occur in nature
as far as I know; presumably it is too obviously a problem.

Translation In a translation service, a protocol entity receives encrypted messages
and transmits some ingredients encrypted under a di#erent key.
The transformation is

{|

N a

|}

K

## {|

N a

|}

K # . Lowe's attack on the
Needham-Schroeder protocol is an example.
3.7 The Dolev-Yao Problem Defined

The Dolev-Yao problem is the following challenge. The player is presented with
a cryptographic protocol. The player must then state the secrecy properties and
authentication properties that the protocol achieves. He must also give counterexamples
to any secrecy or authentication properties that he believes it does not
achieve.
In playing this game, the player is allowed to assume that cryptographic
primitives will be chosen to be perfect. The primitives will never have collisions.
The penetrator can infer nothing about plaintext, given a ciphertext, without
using the key. Conversely, the penetrator can infer nothing about ciphertext,
given a plaintext, without using the key. Moreover, the penetrator cannot learn
a key, unless the key is contained in a message that the penetrator can decrypt.
We have already explained how to play the second part of the game, the part
where counter-examples must be given. The next section is devoted to explaining
how to find and prove the secrecy and authentication properties protocols
achieve. The remainder of this section will be devoted to defining our model of
protocol execution, called the strand space model, and to defining what secrecy
and authentication properties mean in this model.
3.8 Strand Space Ideas

We very briefly summarize the ideas behind the strand space model [47, 16]; see
also the definitions given in Section 3.14, which is an appendix to Section 3.
28

A is the set of messages that can be sent between principals. We call elements
of A terms. A is freely generated from two disjoint sets, T (representing texts
such as nonces or names) and K (representing keys) by means of concatenation
and encryption. The concatenation of terms g and h is denoted g h, and the
encryption of h using key K is denoted

{|h|}

K . (See Section 3.14.)
A term t is a subterm of another term t # , written t @ t # , if starting with t we
can reach t # by repeatedly concatenating with arbitrary terms and encrypting
with arbitrary keys. Hence, K

#@ {|t|}

K , except in case K @ t. The subterms of

t are the values that are uttered when t is sent; in

{|t|}

K , K is not uttered but
used. (See Definition 7.)
A strand is a sequence of message transmissions and receptions, where transmission
of a term t is represented as +t and reception of term t is represented
as

-t.

A strand element is called a node. If s is a strand,

#s,

i# is the i

th

node
on s. The relation n

#

n # holds between nodes n and n # if n =

#s,

i# and

n # =

#s,

i + 1#. Hence, n

#

+

n # means that n =

#s,

i# and n # =

#s,

j# for some

j > i. Each column of nodes connected by vertical arrows

#

in Figures 4--8 is a
strand.
The relation n

#

n # represents inter-strand communication; it means that
term(n 1 ) = +t and node term(n 2 ) =

-t.

Inter-strand communication is shown
by horizontal arrows

#

in Figures 5--8.
A strand space # is a set of strands. The two relations

#

and

#

jointly
impose a graph structure on the nodes of #. The vertices of this graph are the
nodes, and the edges are the union of

#

and

#.

We say that a term t originates at a node n =

#s,

i# if the sign of n is positive;

t @ term(n); and t

#@

term(#s, i #

#)

for every i #  i. Thus, n represents a message
transmission that includes t, and it is the first node in s including t. For instance,

A and N p originate at the top left node of Figure 8. If a value originates on only
one node in the strand space, we call it uniquely originating ; uniquely originating
values are desirable as nonces and session keys.
A bundle is a finite, causally well-founded collection of nodes and arrows
of both kinds. In a bundle, when a strand receives a message m, there is a
unique node transmitting m from which the message was immediately received.
By contrast, when a strand transmits a message m, many strands (or none)
may immediately receive m. (See Definition 3.) Figures 5 and 8 are examples of
bundles; those examples happen to be undesirable.
Since a bundle

C

is an acyclic directed graph, the reflexive, transitive closure
of the arrows (# together with

#)

form a partial order

# C

. The statement

m

# C

n means that there is a path from m to n traversing 0 or more arrows,
in which both

#

and

#

may appear. Because

C

is finite,

# C

is a well-ordering,
meaning that every non-empty set of nodes contains a

# C

-minimal element. This
is an induction principle, used extensively in [47].
The height of a strand in a bundle is the number of nodes on the strand that
are in the bundle. Authentication theorems generally assert that a strand has
at least a given height in some bundle, meaning that the principal must have
engaged in at least that many steps of its run.
29

A strand represents the local view of a participant in a run of a protocol.
For a legitimate participant, it represents the messages that participant would
send or receive as part of one particular run of his side of the protocol. We call
a strand representing a legitimate participant a regular strand.
3.9 The Powers of the Penetrator

For the penetrator, the strand represents an atomic deduction. More complex
actions can be formed by connecting several penetrator strands. While regular
principals are represented only by what they say and hear, the behavior of the
penetrator is represented more explicitly, because the values he deduces are
treated as if they had been said publicly.
We partition penetrator strands according to the operations they exemplify.

E-strands encrypt when given a key and a plaintext; D-strands decrypt when
given a decryption key and matching ciphertext; C-strands and S-strands concatenate
and separate terms, respectively; K-strands emit keys from a set of
known keys; and M-strands emit known atomic texts or guesses. A parameter to
the model is the set KP of keys known initially to the penetrator. It represents an
assumption about what keys the penetrator may emit on K-strands, as opposed
to getting them indirectly, for instance by decrypting a message containing a
new session key. (See Definition 9.)
As an example of how the penetrator can hook together several atomic
strands to achieve a harmful compound e#ect, let us consider how the penetrator
carries out his attack in Figure 5. To get from the incoming value

{|N

a A|} KP to
the outgoing value

{|N

a A|} KB , the penetrator must decrypt and then encrypt.
To decrypt

{|N

a A|} KP , the penetrator must apply his (private) decryption key

K -1 P . He obtains this directly, as it is assumed a member of the set KP that he
possesses from the start. In the encryption that produces

{|N

a A|} KB , the penetrator
applies B's public key. We my also assume that it is a member of the set

KP , because it is public knowledge. Thus, we may diagram the penetrator's activity
as shown in Figure 9. The lower column of penetrator activity in Figure 5
may be expanded similarly.
3.10 Representing Protocols

We turn now to the regular participants. Unlike the powers of the penetrator,
which are the same regardless of the protocol, the behavior of the regular principals
is dictated by the protocol. We may assume that we already have a diagram
describing the protocol, in the style of Figure 4. To define a protocol, we take
three steps. We will illustrate these steps starting with the Carlsen protocol [5],
the diagram for which is shown in Figure 10.
Auxiliary Functions A public-key protocol typically requires a function associating
a public key with each principal. A symmetric-key protocol typically
requires a function associating a long-term key, shared with a key server, with
30

D

#
{|Na

A|}K P #

.

K

. K -1

P

#

.


w
w
w
w
E

.


w
w
w

Na A

#

.

K

. KB

#

.


w
w
w
w
.


w

{|Na

A|}KB #

#

Fig. 9. Penetrator Activity in Figure 5
A B S

.

ANa

#

.
.


w

ANa BN b

#

.
.


w

# M3

.


w
.


w
w
w
w
w
w
w
w
w
w
w
w

#

M4

.


w
.


w

{|N

# b

|}

K

#

.


w
M3 =

{|K

N b A|}KB

{|Na

BK|}KA
M4 =

{|Na

BK|}KA

{|Na |}

K N # b
Fig. 10. Carlsen's Protocol
31

each principal. We typically write such functions using subscripts, with KA being
the key associated with A, and refer to it as the "key-of" function. In the
case of the Carlsen protocol, KA represents the long-term key of A, shared with
the key server.
If a protocol uses a key server as Carlsen's protocol does, then we will require
that the session keys it chooses must be disjoint from the range of "key-of"
function.
Occasionally a protocol requires a di#erent function, such as a function associating
a long-term shared secret with each pair of principals.
Parametric Strands Next we define the strands for the protocol. To do this, we
start from the columns shown in the diagram. Each separate column represents
a di#erent role. In the Carlsen protocol, they are initiator, responder, and key
server.
In some cases, there may be message components received a principal that
it cannot check, because they are encrypted using a key that the recipient does
not possess. These terms are simply forwarded to another principal. They will
be represented simply by variables. The component (presumably) of the form

{|N

a BK|}KA cannot be checked when it is received by B. B can only forward
it to A. We will represent this component using the variable H . Other messages
are represented by terms of the obvious form.
By collecting the variables occurring in any term sent or received by that
column, we find the parameters for that role. The parameters for the recipient
are A, B, N a , N b , K,N # b , H , while those for the initiator are A, B, N a , K,N # b . The
initiator never sees N b , and never interprets an encrypted unit as H . The parameters
for the key server are A, B, N a , N b , K, since it never sees N # b and never
interprets an encrypted unit as H . We write:

-- CInit[A, B, N a , K,N # b ] is the set of strands with trace (behavior):
+AN a ,

-{|N

a BK|}KA

{|N

a

|}

K N # b , +{|N # b

|}

K

This means that first a message is sent containing A and N a , and then a
message is received containing the nonce N a again, encrypted in A's longterm
key, and so on.

-- CResp[A, B, N a , N b , K,N # b , H ] is the set of strands with trace

-AN

a , +AN a BN b ,

-{|K

N b A|} KB H, +H

{|N

a

|}

K N # b ,

-{|N

# b

|}

K

-- CServ[A, B, N a , N b , K] is the set of strands with trace

-AN

a BN b , +{|K N b A|} KB

{|N

a BK|}KA

We write

#

in particular argument positions to indicate a union. For instance,
CInit[A, B,

#, #, #]

=

#

Na,K,N # b

CInit[A, B, N a , K,N # b ]
32

is the set of all initiator strands involving A and B, with any nonces and session
keys. We also use

##

to indicate that multiple adjacent arguments have been
projected, writing e.g. CInit[A, B,

##]

for CInit[A, B,

#, #, #].

The regular strands are generated by filling in the parameters with appropriate
values. Instantiations may be limited to subtypes of the message algebra. For
instance, the parameters A and B may be instantiated with any value that names
a principal (perhaps these are ip addresses or X.509 Distinguished Names); N a

may be instantiated with any bitstring of length 128; and so on. We assume
that there is some association D of variables with sets of terms in A. Very often
it is convenient to assume some of these sets are disjoint, for instance the sets

D(N a ), D(K),D(A) of nonces, keys, and names (respectively).
Often, a strand space contains strands belonging to a parametric strand
whenever the instantiation is type-correct. For instance, in the case of a parametric
strand such as CServ[A, B, N a , N b , K], if a

#

D(A), b

#

D(B), n a

#

D(N a ),

n b

#

D(N b ), and k

#

D(K), then CServ[a, b, n a , n b , k] is non-empty. Sometimes
it is convenient to stipulate that variables get distinct instantiations. For
instance, in our formalization of the Needham-Schroeder-Lowe responder's guarantee
(see below, Section 3.12 and [47, 16]) we assume that the responder's nonce

N b is di#erent from the initiator's nonce N a . This may be encoded into the
strand space itself by stipulating that NSLResp[a, b, n a , n b ] is non-empty whenever
 a

#

D(A), b

#

D(B), n a

#

D(N a ), n b

#

D(N b ), and n a

#=

n b .
Restricted Values There are also some additional restrictions on the way that
the values are used. For instance, in the case of the Carlsen protocol, the values

N a , N b , and N # b are nonces. This means that they are intended to originate
uniquely. The session keys K are also intended to originate uniquely, as well as
to be disjoint from the long-term keys. Correctness goals may also depend on
the assumption that the player's long-term keys are not in KP , the penetrator's
initial knowledge, compromised through nefarious means or lucky guessing. This
assumption is unavoidable, in that, when KA

#

KP , the key server and B can
have no assurance that A has done anything, or that session keys destined for

A remain secret.
In this protocol, the assumption that KA

##

KP is also an origination assumption.
It amounts to the assumption that KA will originate nowhere. It entails
that KA does not originate on a penetrator K-strand. No key originates on an
initiator or responder strand in this protocol. And we have assumed that the
session keys originating at the key server are disjoint from the long-term keys.
Origination restrictions are of course implemented using probabilistic mechanisms
in reality, and some work has been done on quantifying the extent to
which a particular implementation is reliable [17].
3.11 Unique Origination and Non-Origination

The value N a originates on the first node of any strand s

#

CInit[#,

#,

N a ,

#, #].

What we mean by this is that a message is sent on that node, and the message
33

contains N a , and that this is the first node on the strand containing N a . By
contrast, N # b does not originate on the third node of any s

#

CInit[##, N # b ],
because although a message is sent on that node and that message contains N # b ,
the previous (receiving) node also contained N # b .
We say that a term t originates uniquely in a bundle

C

if there is exactly
one node n in

C

such that t originates on n. When there is no node on which t

originates, we say that t is non-originating in

C.

In particular, KA does not originate on s

#

CServ[A,

##],

because although a
term encrypted with KA is sent on the second node of s, and KA has not been
used previously, KA is not a subterm of the message. It contributes to how the
term is constructed, but not what the term contains, and this is the intuition
formalized in our definition of subterm (Definition 7).
Assumptions about unique origination and non-origination are a way of restricting
what attacks on a protocol we are willing to worry about. For instance,
in Figure 11 we illustrate an "attack" on the Needham-Schroeder protocol in
which the penetrator simply somehow knows what the responder's nonce N b

is. While this could conceivably happen, it is not a strategy likely to succeed
#

{|Na

N b

|}

KB

#


w
M?! E

.

N b

#

.

K

. KB

#

.


w
w
.


w

{|N

b

|}

KB #

#


w
w
w
w
w
w
w
w
w
w
w
w
w
w
w
Fig. 11. An Improbable Attack: Guessing a Needham-Schroeder Nonce
for the penetrator. Protocol design, therefore, does not need to concern itself
systematically with how to prevent it.
A bundle describes what happens when a protocol runs, and in this we follow
Robert Lowell's maxim, "Why not say what happened?" A bundle may contain
some regular strands and some penetrator strands. The events of sending and receiving
messages are connected in a causally well-founded way. We are concerned
with a particular bundle only if it satisfies some unique origination conditions
and some non-origination assumptions; otherwise, things may go wrong, but it
is too implausible an attack.
3.12 What is an Authentication Goal?

Strands are a suggestive formalism for understanding authentication and authentication
failures. A strand represents one principal's experience of a protocol
34

execution. The strand includes the information that the principal knows directly,
namely that it sent certain messages and received other messages, in a particular
order. Security goals for protocols concern what else must also have happened.
Authentication goals are about what another regular principal must have done.
Secrecy goals are inferences about what the penetrator cannot have done.
Let us return to the Needham-Schroeder protocol to consider what authentication
goals are, in the light of the failure illustrated in Figure 5. One of the
goals of the protocol is to assure the responder B,

For every B-strand (apparently with A),

there is an A-strand (apparently with B),

and they agree on the nonces N a , N b .

3
The attack shows that there can be a B-strand, apparently with A, without any

A-strand apparently with B.

This example is typical. An authentication result justifies a sound inference,
and a counterexample to an authentication property shows that the inference
is unsound. From B's local experience, a conclusion about A's behavior should
follow. Naturally, there are assumptions that must be met for the inference to
hold good, and protocol analysis is informative because it identifies exactly what
the assumptions are.
When we consider the epistemology of authentication protocols, that is, the
theory of knowledge that applies to them, there are four ingredients. First, there
are the facts that a principal knows, which is to say the message sends and
receives belonging to a single strand. Second, there are the conventions of the
protocol, which dictate that the behavior of other regular participants will be
described by the strands of the protocol. Third, there is the model of the penetrator
embodied in Definition 9. Finally, there assumptions about origination:
the unique origination of nonces and session keys, and the non-origination of
long-term secrets.
From these elements, we try to infer what other events have occurred. The
real world (the bundle) must contain events that causally explain what we saw.
To find out what these events could be, we use the causal laws embodied in the
definition of bundle (Definition 3). We may use these principles:

-- What is heard was said, i.e. every negative node has a unique in-arrow in
the bundle

C;

-- Every principal starts at the beginning, i.e. if n

# C,

and m

#

n precedes it
on the same strand, then m

# C;

-- Causality is acyclic, and bundles are finite.

3

It is sometimes said that this was not a goal of the protocol as originally described,
but that the protocol was intended only to establish that A was active. That is, there
should be an A-strand with some partner. The protocol does in fact achieve this.
However, unless the goal of the protocol is the stronger assertion we have given,
and the nonces are intended to become a shared secret between A and B, it is hard
to see why the last message should be the encrypted value

{|N

b

|}

KB . The plaintext
message N b would also achieve the weaker goal.
35

From the last of these, an induction principle follows. Namely, if

# C

is defined as
the reflexive, transitive closure of the union of the two kinds of arrows,

#

and

#,

then every non-empty set S of nodes in

C

has a preceq

C

-minimal member.
If S is a set of nodes at which the penetrator possesses some dangerous value,
then a minimal member of S pinpoints how the penetrator learnt it. The maxim
here, as in Watergate, is, "What did he know and when did he know it?"
To illustrate an authentication goal, let us switch now to a protocol that
achieves its goals, such as the Needham-Schroeder-Lowe protocol [27] as shown
in Figure 12. The only di#erence from the Needham-Schroeder protocol is in the
A {|Na

A|}KB #

{|Na

A|}KB #

B
.


w

#

{|Na

N b B|}KA #

{|Na

N b B|}KA

.


w
.


w

{|N

b

|}

KB # {|N

b

|}

KB #

.


w
Fig. 12. Needham-Schroeder-Lowe Protocol
second message

{|N

a N b B|} KA , in which the responder includes his name. This
prevents the attack shown in Figure 5. We use NSLInit[A, B, N a , N b ] to refer to
the set of all strands having the behavior shown in the left column of Figure 12,
while NSLResp[A, B, N a , N b ] refers to the set of all strands having the behavior
shown in the right column.
In the revised Needham-Schroeder-Lowe, the responder B can in fact be sure
that the initiator A wanted to execute a run with B. This means that in any
bundle

C

containing a responder strand s r

#

NSLResp[A, B, N a , N b ], there is
an initiator strand s i

#

NSLInit[A, B, N a , N b ] contained in

C

(subject to some
origination assumptions). In fact [47], the assumptions needed are

-- N b is uniquely originating in

C

and N b

#=

N a ; and

-- K -1 A is non-originating in

C

(or alternatively, K -1 A

##

KP ).
In the case of the initiator's guarantee, the situation is slightly di#erent. Since the
initiator sends the last message, the initiator can certainly never know whether
the responder receives it. Thus, the only reasonable goal is to show that the first
two nodes of the responder's strand are in the bundle

C.

We express this by
saying that the strand has

C-height

at least 2 (see Definition 4). The initiator's
guarantee states that if

-- N a is uniquely originating in

C;

and

-- K -1 A and K -1 B are non-originating in

C

(or alternatively, K -1 A , K -1 B

##

KP )
and s i

#

NSLInit[A, B, N a , N b ] has

C-height

2,
then some s r

#

NSLResp[A, B, N a , N b ] has

C-height

2.
36

It is an unexpected asymmetry of the Needham-Schroeder-Lowe protocol
that the initiator's guarantee depends on both participants' private keys being
uncompromised, while the responder's guarantee depends only on one private
key being uncompromised.
In some cases, not all data values are authenticated between the principals.
For instance, in the Carlsen protocol (Figure 10), the initiator never sees the
responder's first nonce N b . Thus, the conclusion of the initiator's guarantee can
specify only that s r

#

CResp[A, B, N a ,

#,

K, . . . ].
We can now give the logical form of an authentication goal. Authentication
goals always take the form: for all bundles

C

and all strands s, there exists a
strand s # such that

If some origination assumptions hold,

and s

#

R has

C-height

i,

then s #

#

R # and s # has

C-height

j.

In this, R and R # are role predicates (or "asterisked" unions over role predicates),
such as NSLInit[A, B, N a , N b ] and CResp[A, B, N a ,

#,

K,N # b ,

#].

An origination
assumption always concerns either a parameter X mentioned in R, or else KX

where X is a parameter mentioned in R.

Analyzing the authentication properties of a protocol means finding the right
choices for R and R # , for i and j, and the necessary origination assumptions.
Many di#erent goals can be stated and proved (or refuted) within our framework.
For instance, Gollmann has said that Lowe's attack does not undermine the
claims made by Needham and Schroeder themselves, because they were working
in a context where they assumed that all the principals with whom one
might want to talk are trustworthy. Of course, in a world of open networks and
widespread electronic commerce, this would not be a reasonable assumption, but
such a world was remote in 1978 when their article was published.
Their authentication goal may be stated as follows. Let us say that X is
an interlocutor in a bundle

C

if there exists a strand s

# C

such that s

#

NSInit[#, X,

##]

or s

#

NSResp[X,

##].

Then the intended Needham-Schroeder
authentication result simply has the additional assumption that for every interlocutor
 X , K -1

X is non-originating in

C.

The responder's authentication goal is
sound with this additional assumption.

3.13 What is a Secrecy Goal?

Secrecy goals are loosely dual to authentication goals. While authentication goals
assert that j nodes of some strand s #

#

R # have happened in the bundle

C,

secrecy goals say that nodes of a certain form do not occur in the bundle. Like
authentication goals, they may depend on assumptions about origination. For
instance, in the Needham-Schroeder-Lowe protocol, we want to ensure that there
is no node in the bundle (even a penetrator node) where the message is N a or

N b . The result takes the form: For all bundles

C,

strands s i , s r , and nodes n

# C

If s i

#

NSLInit[A, B, N a , N b ] and s r

#

NSLResp[A, B, N a , N b ] have

C-height

at
least 1 and 2 respectively,
37

and N a and N b are uniquely originating in

C,

and

and K -1 A and K -1 B are non-originating in

C,

then term(n)

#=

N a and term(n)

#=

N b .
Naturally, if we prove that N a and N b are not said in public in any bundle

C,

then it follows that the penetrator cannot derive them from what he sees. If he
could derive them, then there would exist a bundle in which he also (perhaps
imprudently) utters them.
Secrecy goals always take the form: for all bundles

C

and all strands s
If some origination assumptions hold,

and s

#

R has

C-height

i,

then there is no node n

# C

such that term(n) = t.

Again, the origination assumptions concern parameters to R or values KX where

X is a parameter to R. The term t is a parameter to R, or a term constructed
from parameters to R.

We can call the role R in a secrecy or authentication goal the core role
of the goal, since the principal playing role R receives the assurance that the
peer is active, or that the secret has not been disclosed. Thus, the origination
assumptions always concern parameters to the core role.
Summary of this Section In this section, we have studied cryptographic
protocols. We started by explaining the Dolev-Yao problem. We illustrated how
to find flaws in protocols, even assuming that the cryptography by which they are
implemented is perfect. One important insight for finding flaws is that we may
ignore junk messages; the other one is that we want to examine the protocol to
find the unintended services that may allow the penetrator to construct the nonjunk
messages that are intended to provide authenticating force to the regular
principals. We then described how to formalize protocol behaviors using strand
spaces; possible executions are bundles. Finally, we defined the logical forms of
authentication and secrecy goals. We have thus illustrated two of the themes
mentioned in the introduction, namely modeling security problems using simple
mathematical materials, and defining specific classes of security properties to
formalize real-world security goals.
3.14 Appendix: Strand Space Definitions

In this appendix to Section 3, we will define the basic strand space notions.
This material is derived from [47, 16]. The definitions of unique origination and
non-origination (Definition 2, Clause 8) have been relativized to a bundle here,
however. We also stipulate that a strand space has all the penetrator strands
that it can (Definition 9).
38

Strand Spaces Consider a set A, the elements of which are the possible messages
that can be exchanged between principals in a protocol. We will refer to
the elements of A as terms. We assume that a subterm relation is defined on A.

t 0 @ t 1 means t 0 is a subterm of t 1 . We constrain the set A further below in
Section 3.14, and define a subterm relation there.
In a protocol, principals can either send or receive terms. We represent transmission
of a term as the occurrence of that term with positive sign, and reception
of a term as its occurrence with negative sign.

Definition 1. A signed term is a pair

##,

a# with a

#

A and # one of the
symbols +,

-.

We will write a signed term as +t or

-t.

(A) # is the set of
finite sequences of signed terms. We will denote a typical element of (A) # by

# ##

1 , a 1

#,

. . . ,

##

n , an

# #.

A strand space over A is a set # with a trace mapping tr : #

#

(A) # .
By abuse of language, we will still treat signed terms as ordinary terms. For
instance, we shall refer to subterms of signed terms. We will usually represent a
strand space by its underlying set of strands #.

Definition 2. Fix a strand space #.

1. A node is a pair

#s,

i#, with s

#

# and i an integer satisfying 1

#

i

#

length(tr(s)). The set of nodes is denoted by

N

. We will say the node

#s,

i#

belongs to the strand s. Clearly, every node belongs to a unique strand.
2. If n =

#s,

i#

# N

then index(n) = i and strand(n) = s. Define term(n) to be
(tr(s)) i , i.e. the ith signed term in the trace of s. Similarly, uns term(n) is
((tr(s)) i ) 2 , i.e. the unsigned part of the ith signed term in the trace of s.

3. There is an edge n 1

#

n 2 if and only if term(n 1 ) = +a and term(n 2 ) =

-a

for some a

#

A. Intuitively, the edge means that node n 1 sends the message

a, which is received by n 2 , recording a potential causal link between those
strands.
4. When n 1 =

#s,

i# and n 2 =

#s,

i + 1# are members of

N

, there is an edge

n 1

#

n 2 . Intuitively, the edge expresses that n 1 is an immediate causal
predecessor of n 2 on the strand s. We write n #

#

+

n to mean that n #

precedes n (not necessarily immediately) on the same strand.
5. An unsigned term t occurs in n

# N

i# t @ term(n).
6. Suppose I is a set of unsigned terms. The node n

# N

is an entry point for

I i# term(n) = +t for some t

#

I , and whenever n #

#

+

n, term(n # )

##

I .
7. An unsigned term t originates on n

# N

i# n is an entry point for the set

I =

{t

# : t @ t #

}.

8. An unsigned term t is uniquely originating in a set of nodes S

# N

i# there
is a unique n

#

S such that t originates on n.

9. An unsigned term t is non-originating in a set of nodes S

# N

i# there is
no n

#

S such that t originates on n.

If a term t originates uniquely in a suitable set of nodes, then it can play the role
of a nonce or session key, assuming that everything that the penetrator does in
some scenario is in that set of nodes.
39

N

together with both sets of edges n 1

#

n 2 and n 1

#

n 2 is a directed graph

#N

, (#

# #)#.

Bundles and Causal Precedence A bundle is a finite subgraph of

#N

, (#

# #)#,

for which we can regard the edges as expressing the causal dependencies of the
nodes.

Definition 3. Suppose

# C # #;

suppose

# C # #;

and suppose

C

=

#N C

, (#

C

# # C

)# is a subgraph of

#N

, (#

# #)#. C

is a bundle if:
1.

N C

and

# C # # C

are finite.
2. If n 2

# N C

and term(n 2 ) is negative, then there is a unique n 1 such that

n 1

# C

n 2 .
3. If n 2

# N C

and n 1

#

n 2 then n 1

# C

n 2 .
4.

C

is acyclic.
In conditions 2 and 3, it follows that n 1

# N C

, because

C

is a graph.
For our purposes, it does not matter whether communication is regarded as
a synchronizing event or as an asynchronous activity. The definition of bundle
formalizes a process communication model with three properties:

-- A strand (process) may send and receive messages, but not both at the same
time;

-- When a strand receives a message t, there is a unique node transmitting t

from which the message was immediately received;

-- If a strand transmits a message t, many strands may immediately receive t.
Definition 4. A node n is in a bundle

C

=

#N C

,

# C # # C #,

written n

# C,

if

n

# N C

; a strand s is in

C

if all of its nodes are in

N C

.
If

C

is a bundle, then the

C-height

of a strand s is the largest i such that

#s,

i#

# C. C-trace(s)

=

#tr(s)(1),

. . . , tr(s)(m)#, where m =

C-height(s).

We say that s

# C

if the

C-height

of s equals length(s).

Definition 5. If

S

is a set of edges, i.e.

S ## # #,

then

#S

is the transitive
closure of

S,

and

#S

is the reflexive, transitive closure of

S.

The relations

#S

and

#S

are each subsets of

NS NS

, where

NS

is the set of
nodes incident with any edge in

S.

Proposition 6. Suppose

C

is a bundle. Then

# C

is a partial order, i.e. a reflexive,
antisymmetric, transitive relation. Every non-empty subset of the nodes
in

C

has

# C

-minimal members.

We regard

# C

as expressing causal precedence, because n

#S

n # holds only when

n's occurrence causally contributes to the occurrence of n # . When a bundle

C

is
understood, we will simply write

#.

Similarly, "minimal" will mean

# C

-minimal.
40

Terms, Encryption, and Freeness Assumptions We will now specialize the
set of terms A. In particular we will assume given:

-- A set T

#

A of texts (representing the atomic messages).

-- A set K

#

A of cryptographic keys disjoint from T, equipped with a unary
operator inv : K

#

K. We assume that inv is an inverse mapping each
member of a key pair for an asymmetric cryptosystem to the other, and
each symmetric key to itself.

-- Two binary operators encr : K



A

#

A and join : A



A

#

A.

We follow custom and write inv(K) as K -1 , encr(K, m) as

{|m|}

K , and join(a, b)

as a b. If K is a set of keys, K -1 denotes the set of inverses of elements of K. We
assume, like many others (e.g. [29, 32, 39]), that A is freely generated, which is
crucial for the results in this paper.

Axiom 1. A is freely generated from T and K by encr and join.
Definition 7. The subterm relation @ is defined inductively, as the smallest
relation such that a @ a; a @

{|g|}

K if a @ g; and a @ g h if a @ g or a @ h.

By this definition, for K

#

K, we have K @

{|g|}

K only if K @ g already.

Definition 8. 1. If K

#

K, then t 0 @K t if t is in the smallest set containing t 0

and closed under encryption with K

#

K and concatenation with arbitrary
terms t 1 .
2. A term t is simple if it is not of the form g h.

3. A term t 0 is a component of t if t 0 is simple and t 0 @

#

t.
Penetrator Strands The atomic actions available to the penetrator are encoded
in a set of penetrator traces. They summarize his ability to discard messages,
generate well known messages, piece messages together, and apply cryptographic
operations using keys that become available to him. A protocol attack
typically requires hooking together several of these atomic actions.
The actions available to the penetrator are relative to the set of keys that the
penetrator knows initially. We encode this in a parameter, the set of penetrator
keys KP .

Definition 9. A penetrator trace relative to KP is one of the following:

M t Text message:

#+t#

where t

#

T.

KK Key:

#+K#

where K

#

KP .

C g,h Concatenation:

#-g, -h,

+g h#

S g,h Separation:

#-g

h, +g, +h#

E h,K Encryption:

#-K, -h,

+{|h|} K

#.

D h,K Decryption:

#-K

-1 ,

-{|h|}

K , +h#.

P#

is the set of all strands s

#

# such that tr(s) is a penetrator trace.
41

We assume that

P#

contains instances of a penetrator strand type, whenever
the instantiation is type-correct, and (in the case of a K-strand) the key K

#

KP .
A strand s

#

# is a penetrator strand if it belongs to

P#

, and a node is a

penetrator node if the strand it lies on is a penetrator strand. Otherwise we will
call it a non-penetrator or regular strand or node. A node n is M, C, etc. node
if n lies on a penetrator strand with a trace of kind M, C, etc.
4 Paths and Well-Behaved Bundles
In this section we will study the notion of bundle, focusing on a particular
equivalence relation on them, and on the paths that messages and their constituents
take through bundles. In certain "well-behaved" bundles, the paths are
especially predictable, and in fact every bundle has an equivalent well-behaved
bundle. This section will illustrate the advantages of the strand space model over
closely related alternatives [40, 43], at least as a heuristic for discovering results
about cryptographic protocols.
4.1 Bundle Equivalence
Definition 10. Bundles

C, C

# on a strand space # are equivalent i#
1. they have the same regular nodes;
2. for all a, a originates uniquely and on a regular node in

C

if and only if a

originates uniquely and on a regular node in

C

# ;
3. for all a, a is non-originating in

C

i# a is non-originating in

C

# .
A set # of bundles is invariant under bundle equivalences if whenever bundles

C

and

C

# are equivalent,

C #

#

# C

#

#

#.
The penetrator's behavior may di#er arbitrarily between two bundles that are
equivalent in this sense, and the orderings

# C

and

# C

# may also di#er freely.
Authentication goals as defined in Section 3.12 are invariant under bundle
equivalences in this sense (see also [30, 47, 49]). As such, it always concerns what
nodes, representing regular activity of the protocol, must be present in bundles.
Penetrator activity may or may not be present.
Secrecy properties may also be expressed in a form that is invariant under
bundle equivalences. We say (temporarily) that a value t is uncompromised in

C

if for every

C

# equivalent to

C,

there is no node n

# C

# such that term(n) = t.

In this form, a value is uncompromised if the penetrator cannot extract it in
explicit form without further cooperation of regular strands. When stated in
this form, the assertion that a value is uncompromised is invariant under bundle
equivalences.
42

4.2 Redundancies

Some portions of the penetrator behavior in a bundle may be redundant in the
sense that they may be excised locally. Removing them leads to a simpler yet
equivalent bundle. We identify here two kinds of redundancy. First are cased
where the penetrator encrypts a value with a key K, and then decrypts with
the corresponding decryption key K -1 . This is illustrated in the upper portion
of Figure 13, and may be eliminated by omitting nodes and adding the dotted
arrow shown in the lower portion. Something very similar arises if the penetrator
E

#

K

# . D

#

h

# .


w

. #

K -1

#
.


w

{|h|}

K

# .


w
sL

.


w

h

# #

sR
#

K

# .
#

h

# .


w

#

K -1

#
#
.


w

{|h|}

K

#
#
#

h

#

#

Discarded message
Fig. 13. E-D Redundancies, and how to eliminate them
concatenates two values and then promptly separates the concatenated unit
into its two immediate subterms. Since these operations introduce no cycles,
the resulting graph is a bundle. They remove only penetrator nodes, so the
new bundle is equivalent to the original one. Finally, since each bundle is finite,
the process of removing redundancies must finally terminate with an equivalent
bundle containing no redundancies.
As a consequence, we may assume that the penetrator's behavior always
follows a specific pattern:

First take messages apart;

then put messages together;

finally deliver the resulting messages to a regular principal.
In order to formalize this pattern, we introduce the notion of a path.
43

4.3 Paths

m

#

+

n means that m,n are nodes on the same strand with n occuring after

m (Definition 2, Clause 4). The notation m

#-#

n means:

Either m

#

+

n with term(m) negative and term(n) positive,

or else m

#

n.

A path p through

C

is any finite sequence of nodes and edges n 1

#-#

n 2

#-#
   #-#

n k . We refer to the ith node of the path p as p i . The length of p will
be

|p|,

and we will write #(p) to mean p

|p|

, i.e. the last node in p. A penetrator
path is one in which all nodes other than possibly the first or the last node are
penetrator nodes. As an example of a penetrator path, in which the first and last
nodes are in fact regular, consider again the partial bundle shown in Figure 14.
The path # =
D
K

.

K -1 P

# .

#1 {|Na

A|}K P

#

#2


w
E K

#2

#

KB
#1
#3


w
w
w
w
w
w
w
w
w
w

Na A

#

#4


w
w
#5


w
w
w

{|Na

A|}KB

#

#6
Fig. 14. Penetrator Strands for Lowe's Attack on Needham-Schroeder
# 1

#

# 2

#

+

# 3

#

# 4

#

+

# 5

#

# 6

is a path that traverses penetrator nodes, connecting A's first transmission

{|N

a A|} KP to B's first reception

{|N

a A|} KB . In contrast to #, the path # =

# 1

#

# 2

#

+

# 5

#

# 6

starts on a penetrator node and ends on a regular node. Observe that by our
conventions, # 3 and # 4 are well-defined (and equal to # 5 and # 6 respectively).
4.4 Constructive and Destructive Edges, Normal Bundles
Definition 11. A

#

+

-edge is constructive if it is part of a E or C strand. It is

destructive if it is part of a D or if it is part of a S strand.
A penetrator node n is initial if it is a K or M node.
44

Any penetrator path that begins at a regular node contains only constructive
and destructive

#

+

-edges, because initial nodes can occur only at the beginning
of a path.

Proposition 12. In a bundle, a constructive edge immediately followed by a
destructive edge has one of the following two forms:
1. Part of a E h,K immediately followed by part of a D h,K strand for some h, K

2. Part of a C g,h immediately followed by part of a S g,h strand for some g, h.

This result requires the freeness of the message algebra.

Proposition 13. (Penetrator Normal Form Lemma) If the bundle

C

has
no redundancies of type C-S and E-D, then for any penetrator path of

C,

every
destructive edge precedes every constructive edge.
Every bundle is equivalent to a bundle with no redundancies of type C-S and

E-D.

We call a bundle normal if it has no redundancies of type C-S and E-D, by
analogy with Prawitz's normal deductions [42]. Many others have noted related
properties, including [7, 40, 20].
We may also assume another property of the bundle

C.

Definition 14.

C

is directed if for every node n

# C,

there is a regular node

m

# C

such that n

# C

m.

Every bundle

C

is equivalent to some directed bundle

C

# . Define the graph

C

#

to contain those nodes n of

C

such that n

# C

m for some regular node m; the
arrows of

C

# are those arrows of

C

that connect nodes in

C

# .

C

# is easily seen to be
a bundle by enumerating the clauses in Definition 3. Moreover,

C

# is equivalent
to

C,

just by the reflexiveness of

# C

.
4.5 Rising and Falling Paths

We will call a path p rising if term(p i ) @ term(p i+1 ) whenever 1

#

i and

i + 1

# |p|.

This means that each term is a subterm of the next, and ultimately
the first is a subterm of the last. Moving in the other direction, we will call a
path p falling if term(p i+1 ) @ term(p i ) whenever 1

#

i and i + 1

# |p|.

In this
case, each term includes the next, so that the last is a subterm of the first.
A destructive

#-edge

may not be part of a falling path, because the path
may traverse the key edge of a D-strand, as shown in left diagram of Figure 15.

K -1 will typically have no relation to h. As we see in the right side, a E-strand

is similar, since with our definitions, K

#@ {|h|}

K unless by chance K @ h.

However, as long as a path p does not traverse a key edge, it will be falling while
traversing destructive penetrator strands and rising while traversing constructive
penetrator strands.
45

D E

.

K -1

# . .

K

# .
#
{|h|}

K

#

.


w

#

h

#

.


w
.


w

h

# .


w

{|h|}

K

#

Fig. 15. Key Edges into D and E-strands
Falling Paths, Rising Paths, and Subterms Falling paths have a property we
need to explain; rising paths have a dual property. As we follow a falling path,
we traverse a number of S-strands, which select a subterm from a concatenation,
and a number of D-strands which select a plaintext from an encryption. If the
encryption is of the form

{|h|}

K , then the key used on this D-strand is K -1 .
Suppose that p is a falling path and K is a set of keys, and suppose that p

traverses a D-strand only when the key used is of the form K -1 for some K

#

K.

So the ciphertext is always of the form

{|h|}

K with K

#

K. That means that the
term p 1 at the start of p is of the form

   {|   

term(#(p))

   |}

K

  

in the sense that it can be constructed from term(#(p)) by concatenating (with
anything) and encrypting using only keys K

#

K. This is what in Definition 8
we wrote term(#(p)) @K p 1 .
The case of a rising path is similar except that we may omit the inverses.
Suppose that p is a rising path and K is a set of keys, and suppose that p traverses
an E-strand only when the key used is some K

#

K. Then p 1 @K term(#(p)).
4.6 A Catalog of Penetrator Paths

This suggests that we separate penetrator activity into paths which do not traverse
key edges; we end a path p at the node before it traverses a key edge. In
this case, term(#(p)) = K for some key K. The ciphertext is of the form

{|h|}

K

if we stopped before an E-strand, and of the form

{|h|}

K -1

if we stopped before
a D-strand.

In cataloging penetrator paths, we may assume that the bundle is normal,
since otherwise there is an equivalent bundle that is. We may also assume that
the bundle is directed. From this, we may infer that a penetrator path terminates
only when it reaches either a key edge or a regular node.
Thus, the purpose of a penetrator path is always either:

-- To make a key available for a D or E-strand, or

-- To construct some message to deliver to a regular node.
The first type of path terminates before a key edge, and the second terminates
at a regular node.
46

In our catalog of paths p that never traverse a key edge, we will also distinguish
possibilities depending whether p begins on a penetrator node or on a
regular node.
1. p begins on a penetrator node and ends before a key edge. Then term(#(p)) =

K, and since p 1 is an initial penetrator node, it must be a K node with

|p|

= 1.
2. p begins on a regular node and ends before a key edge. So term(#(p)) = K.

Because p never traverses a key edge and ends with an atomic term, p is
falling. So K @ term(p 1 ). In other words, the penetrator has extracted a key
from a message sent by a regular principal. By our remark at the beginning
of Section 4.6, if every occurrence of K in term(p 1 ) is encrypted using some
other key K 1 , then K -1 1 is a key edge joining p at some D-strand. There
must be an earlier path p # furnishing this key K -1 1 .
3. p begins on a penetrator node and ends at a regular node. Then p 1 is either
a K node or a M node, and in either case term(p 1 ) is atomic. Therefore p is
a rising path and term(p 1 ) @ term(#(p)). In this path, the penetrator makes
up a value, and after possibly combining it with other ingredients, delivers
it to a regular participant at #(p).

4. p begins at a positive regular node and ends at a negative regular node. In
this case, p consists of a falling portion followed by a rising portion, either
(or both) of which can be trivial in the sense that it consists of a single node
and no arrows.
Thus, there is a falling path q ending at a positive node #(q), and a rising
path q # beginning at a negative node q # 1 , where term(#(q)) = term(q # 1 ). We
call this common term the path bridge term of p, writing it as pbt(p). The
whole path p is of the form q

#

q # .
We know that pbt(p) @ term(p 1 ), and pbt(p) @ term(#(p)). So the e#ect of
the whole path p is to extract the term pbt(p) via the falling part q, and
compose it with other ingredients in the rising part q # , delivering the result
to a regular participant.
This is a complete listing of what the penetrator can achieve by means of any
path.
4.7 New Components and E#cient Bundles

According to Definition 8, a component of t is a subterm t 0 such that t 0 is either
an atom or an encryption, and such that there are no encryptions hiding t 0 in t.

Thus, given a term t, we generate the set of its components by repeatedly separating
concatenations, stopping whenever we reach an atom or an encryption.
Components are important in cryptographic protocols, because the penetrator
can always undo concatenations and redo them in whatever form is desired. Only
the cryptographic work required to change components can provide authentication
or confidentiality. We write t 0 @ t to mean that t 0 is a component of

t.

A term t 0 is a new component of a node n if t 0 @ term(n), and whenever

m

#

+

n it is not the case that t 0 @ term(m). That is, it should not have been
47

a component of an earlier node on the same strand. We are interested in the
new components of a node, because they summarize what cryptographic work
has been done at that point on the strand.
To simplify reasoning about bundles, it is convenient to assume that when a
penetrator gets a component from the regular participants, he gets it from the
earliest point possible. We call such a bundle e#cient.

Definition 15. A bundle is e#cient if and only if, for every node m and negative
penetrator node n, if every component of n is a component of m, then there is
no regular node m # such that m

#

m #

#

n.

We call a bundle of this kind e#cient because the penetrator does the most with
what he has rather than making use of additional regular nodes.
All of the bundles we have shown in earlier figures are e#cient. Whenever
the penetrator node handles a term, there is no earlier node that has all the
same components, and a regular node has been traversed in between. However,
in the case of the nonsensical variant of the Needham-Schroeder protocol shown
in Figure 16, the edge marked

#

would need to be removed, and replaced with
A {|Na

A|}K P

#

P
.


w
w
w

{|Na

A|}KB

#

B
.


w
w
w
w
w
w
w
w
w

#
{|Na

N b

|}

KA

.


w
.


w

# {|Na

A|}K P

#

n

{
|Na A|

}K P

#
.


w

{|Na

A|}KB

# .


w
w
w
w
w
w
Fig. 16. An Ine#cient Bundle for a Fictitious Protocol
the dashed diagonal. The negative penetrator node n must not receive its term
from the third initiator node, when it can be obtained directly from the first
initiator node.
Every bundle

C

may be replaced by an equivalent e#cient bundle

C

# , and

C

#

will be normal or directed assuming that

C

was.
4.8 Penetrable Keys

We may use the ideas we have developed to give an easy way to determine
whether the secrecy of a key is preserved by a protocol. Let us suppose that

C

is a bundle in which some key K is disclosed, meaning that there exists a node

n

# C

such that K @ term(n). We may assume that

C

is normal, directed,
48

and e#cient. By the bundle induction principle, we may assume that n has been
chosen minimal in the ordering

# C

with component K. We want to determine
when a key is penetrable.
There are only three cases:

-- n may be a K node, in which case K

#

KP ;

-- n may be a regular node, in which case (by minimality), K is a new component
of n;

-- n lies on a penetrator path p at node p i with 1  i. We may assume that p

traverses no key edges.
In the last case, the path

#p

1 , . . . , p i

#

is falling, as it ends with an atomic value,
so p 1 is a regular node. We know from Section 4.5 that K @K term(p 1 ), where

K contains K 1 whenever K -1 1 was used in a D-strand along p.

So a collection of previously penetrable keys, namely the K -1

1 s for K 1

#

K,

su#ce to extract K from some component t 0 @ term(p 1 ). By the e#ciency of

C,

t 0 is a new component of the regular node p 1 .
Letting K =

#,

this also covers the second case. Therefore, for every penetrable
key K, either:
1. K

#

KP , or
2. There is a regular node m

# C

and a new component t 0 of m such that

K @K t 0 , where for every K

#

K, K -1 1 is already penetrable.
So every key that the penetrator learns, he either starts o# knowing in KP , or
else some regular participant puts K into a new component, where it is protected
only by keys that the penetrator can already learn to undo. In this construction,
we are primarily interested in paths of type 2 in our list of possible types of
penetrator path in Section 4.6.
We may therefore define P(C) to be the smallest set of keys such that KP

#

P(C) and closed under Clause 2 as just given. We have just proved that if K =
term(n) for any n

# C,

then K

#

P(C).

Why is this useful? Because we can define a set of safe keys such that it
is very easy to see when a key is safe, and the safe keys are disjoint from the
penetrable keys.
4.9 Safe Keys

Let S 0 (C) be the set of keys K such that:

-- K

##

KP , and

-- for every positive regular node n

# C

and every new component t 0 @

term(n), K

#@

t 0 .
These keys are patently safe. No regular principal will ever utter them in a
component, unless given that component earlier. So, no one is ever the first to
spill the beans.
Let S i+1 (C) be the set of keys K such that:
49

-- K

##

KP , and

-- for every positive regular node n

# C

and every new component t 0 @

term(n), every occurrence of K in t 0 lies within an encryption using some
key K 0 where K -1 0

#

S i (C):

   {|   

K

   |}

K0

  

These keys are derivatively safe, since they can never be penetrated unless the
penetrator gets K -1 0 , which is already known to be safe.
In practice, protocol secrecy goals frequently amount to showing that certain
keys are in either S 0 or S 1 . Larger values of i seem rarely to occur in these
protocols. Showing that a private key or a long-term symmetric key is in S 0 typically
reduces to checking that it is assumed not to be in KP , because protocols
generally avoid emitting terms containing these keys.
For instance, in the Needham-Schroeder protocol, if n is a regular node, then

K

#@

term(n). Hence, S 0 = K

\

KP , which says that any key not initially known
to the penetrator is permanently safe.
Many protocols expect session keys to be generated by a key server, which
sends them encrypted in the long-term keys of two principals, and no principal
ever re-encrypts a session key under a new key. In a particular session, a session
key K may be sent encrypted with long-term keys not in KP (or, if they are
asymmetric, their inverses are not in KP ). If the server never re-sends the same
session key K in a di#erent session, then K

#

S 1 . This method is an easy way
to establish secrecy.
5 Proving Authentication
We focus now on protocols in which a regular participant authenticates its peer
by sending a fresh value a (typically a nonce N ), expecting to receive it back
in a cryptographically altered form. If only the intended peer can perform the
right cryptographic operation, then this pattern will authenticate the peer. The
treatment of authentication tests in this section di#ers from that in [16], and is
indebted to [41].
Consider some arbitrary bundle

C.

5.1 The Outgoing Authentication Test

Let us say that n 0

#

+

n 1 is an outgoing test edge for a if

-- a originates uniquely on n 0 ;

-- There is only one component t 0 =

{|h|}

K @ term(n 0 ) such that a @ t 0 ;

-- t 0

#@

term(n 1 ) but a @ term(n 1 ); and

-- K -1

##

P.
50

Consider the set S =

{m # C

: a @ term(m)

#

t 0

#@

term(m)}. S is non-empty,
because n 1

#

S. So by the bundle induction principle, S has minimal members

m 1 .
We claim that no such m 1 is a penetrator node. Clearly such an m 1 is positive,
since if it were negative, it must receive its message from another node
with the same property. If m 1 is an initial penetrator node, this contradicts the
assumption that a originates uniquely at n 0 . Thus, if it is a penetrator node at
all, m 1 lies on an edge m 0

#

+

m 1 where t 0 @ term(m 0 ) but t 0

#@

term(m 1 ).
Since t 0 =

{|h|}

K , m 0

#

+

m 1 lies on a D-strand, with key edge K -1 . But this
contradicts the assumption that K -1

##

P. Therefore, every minimal member of

S is regular.
Let us call a regular edge m 0

#

+

m 1 a transforming edge for n 0

#

+

n 1 if

t 0 @ term(m 0 ) and m 1 is a minimal member of S.

The outgoing test authentication principle states that if

C

contains an outgoing
test edge, then it also contains a (regular) transforming edge for it.
The meaning of this assertion is illustrated in Figure 17. The two bulleted
nodes in the figure represent m 0 and m 1 .
n0
# a @

{|h|}

K = t K -1

##

P

#

.
n1


w
w
w
w
w
w
w
w
w
w
w
w
w

#

a @ term(n1 ), t

#@

term(n1 )

#

a @ t # t

#@

t #

.


w
w
w
w
w
w
w
w
w
w
w
w
w
.

means this regular node must exist

# a means a originates uniquely here
Fig. 17. Authentication Provided by an Outgoing Test
The Outgoing Test in Needham-Schroeder We may illustrate the outgoing authentication
tests by Needham-Schroeder (see Figure 4). Assume that

C

is a
bundle, and the

C-height

of s r

#

NSResp[A, B, N a , N b ] is 3, which means that
all three nodes of s r belong to

C.

Assume that K -1 A

##

KP . Finally, assume that

N b originates uniquely, and N b

#=

N a (which together mean that N b originates
uniquely at the second node of s r ).
Hence, the edge from the seocnd node of s r to its third node is an outgoing
test edge for N b . By the Outgoing Authentication Test principle, there exist
regular nodes m 0 , m 1

# C

such that m 0

#

+

m 1 is a transforming edge for it. So

{|N

a N b

|}

KA @ (m 0 ). The only negative regular node containing a subterm of this
form is the second node of an initiator strand s i for s i

#

NSInit[A, B # , N a , N b ]
51

and some responder B # . Thus, the transforming edge m 0

#

+

m 1 must be the
edge from the second node of s i to its third node, and s i has

C-height

3.
Unfortunately, we have not proved that s i

#

NSInit[A, B, N a , N b ] for the
expected responder B, rather than some other responder B # . And Figure 5 is a
counterexample in which B # = P

#=

B. Hence we have uncovered a limitation
in the authentication achieved by Needham-Schroeder, first noted by Lowe [26,
27], which led Lowe to amend the protocol to contain the responder's name B

in the second message

{|N

a N b B|} KA .
The Outgoing Test in Needham-Schroeder-Lowe Consider now the corrected
Needham-Schroeder-Lowe protocol as shown in Figure 12. As before, assume
that

C

is a bundle, and the

C-height

of s r

#

NSResp[A, B, N a , N b ] is 3. Assume
again that K -1 A

##

KP ; that N b originates uniquely; and that N b

#=

N a .
We again infer that there exist regular nodes m 0 , m 1

# C

such that m 0

#

+

m 1 is a transforming edge for it. So

{|N

a N b B|} KA @ (m 0 ). The only negative
regular node containing a subterm of this form is the second node of an initiator
strand s i for s i

#

NSInit[A, B, N a , N b ]. Hence, the desired s i has

C-height

3.
5.2 The Incoming Authentication Test

Let us say that n 0

#

+

n 1 is an incoming test edge for a if

-- a originates uniquely on n 0 , and t 1 =

{|h|}

K

#@

term(n 0 );

-- a @ t 1 , and t 1 @ term(n 1 ); and

-- K

##

P.

We call a regular edge m 0

#

+

m 1 a transforming edge for n 0

#

+

n 1 if m 0

contains a as a subterm and m 1 is a minimal node such that t 1 @ term(m 1 ).
As before, only a regular edge can have this property. This assertion is illustrated
in Figure 18 using the same conventions as in Figure 17. Carlsen's
n0
#a @ term(n0)

# #

.
n1


w
w
w
w
w
w
w
w
w

#

a @

{|h|}

K @ term(n1) K

##

P

#

{|h|}

K

.


w
w
w
w
w
w
w
w
w
Fig. 18. Authentication Provided by an Incoming Test
protocol (see Figure 10) is designed around incoming authentication tests. So is
the Neuman-Stubblebine protocol, as we will illustrate in Section 5.4.
52

5.3 The Unsolicited Test

One other authentication test is important especially in the case of a key server,
but in some other instances too. This is the unsolicited test. If

{|h|}

K @ term(n)
and K

##

P, then we may infer that there is a node m such that:

-- m is regular;

--

{|h|}

K originates at m.

This is valid because

{|h|}

K certainly originates at some node m, and m cannot
be a penetrator node: If it were, it would be the positive node of a D-strand. And
then the preceding key node would have the term K, contrary to the assumption

K

##

P.
5.4 Neuman-Stubblebine

The Neuman-Stubblebine protocol [38] contains two sub-protocols. We will call
the first sub-protocol the authentication protocol and the second sub-protocol
the re-authentication protocol. In the authentication sub-protocol, a key disA
S B
.

M1 #

.
.

# M2

.


w
.


w
w
w
w
w
w

#

M3

.


w
.


w

M4 #

.


w
w
w
w
w
w
M1 = ANa
M2 = B

{|A

Na t b

|}

KB N b

M3 =

{|B

Na K t b

|}

KA

{|A

K t b

|}

KB N b

M4 =

{|A

K t b

|}

KB

{|N

b

|}

K
Fig. 19. Neuman-Stubblebine Part I (Authentication)
tribution center generates a session key for an initiator (a network client) and
a responder (a network server); the message exchange is shown in Figure 19.
This session key is embedded in encrypted form in a re-usable ticket of the form

{|A

K T

|}

KB . In the re-authentication protocol the client presents the same ticket
again to the network server to use the same key for another session. The value

T is an expiration date, after which the network server should no longer accept
the ticket, although we will not bother to model this aspect of the behavior.
We consider the authentication protocol alone first. Strands of the form
shown in the columns labelled A, B, and S in Figure 19 will be called
53

-- Init[A, B, N a , N b , t b , K,H ],

-- Resp[A, B, N a , N b , t b , K], and

-- Serv[A, B, N a , N b , t b , K],

respectively.
We define LT to be the set of long-term keys, i.e. the range of the injective
function KA for A

#

Tname . All long-terms keys are symmetrical: K

#

LT

implies K = K -1 .
We likewise assume that the key server generates keys in a reasonable way,
meaning that that Serv[##, K]

# C

=

#

unless:

-- K

##

KP ;

-- K = K -1 ;

-- K is uniquely originating in

C;

-- K

##

LT.

Because of the unique origination assumption, it follows that the cardinality

|Serv[##,

K]

# C| #

1 for every K. We say that

C

has a reasonable server when
these conditions are met.
The overall strategy for showing the responder's guarantee, assuming given
a bundle

C

such that

C

has a reasonable server and

C

contains a strand s r

#

Resp[A, B, N a , N b , t b , K] with KA , KB

##

KP , is the following:
1. Observe that LT

#

S 0

#

KP , as the protocol never transmits a long-term
key. For any key K # , if Serv[A, B,

#, #, #,

K # ]

#= #,

then K # is transmitted
protected by KA and KB , but it will never be transmitted with any di#erent
protection (with a reasonable key server). Since KA , KB

#

S 0 , K #

#

S 1

whenever Serv[A, B,

#, #, #,

K # ]

#= #.

2.

{|A

K t b

|}

KB is an unsolicited test, originating on a regular strand. This can
only be a server strand s s

#

Serv[A, B,

#, #,

t b , K]. Therefore, K

#

S 1 .
3. M 2

#

M 4 is an incoming test for N b in

{|N

b

|}

K . Hence, there is a regular
transforming edge producing

{|N

b

|}

K . This can lie only on the second and
third nodes of an initiator strand s i

#

Init[A # , B # , N # a , N b , t # b , K,

#].

4. The first and second nodes of s i form an incoming test for N # a . Therefore,
there is a regular transforming edge producing

{|B

# N # a K t # b

|}

K A #

. This can
only be s # s

#

Serv[A # , B # ,

#, #,

t # b , K].

5. By the assumption that

C

has a reasonable key server, K is uniquely originating
in

C.

Therefore, s # s = s s , and A # = A, B # = B, t # b = t b . Thus,

s i

#

Init[A, B,

#,

N b , t b , K,

#].

The initiator's guarantee is simpler to establish. The edge M 1

#

M 3 on an
initiator strand is an incoming test for N a in

{|B

N a K t b

|}

KA . It shows there is a
server strand s s

#

Serv[A, B, N a ,

#,

t b , K]. The first node of s s is an unsolicited
test, showing the existence of a responder strand s r

#

Resp[A, B, N a ,

#,

t b ,

#].

In the re-authentication sub-protocol, the key distribution center no longer
needs to be involved; the initiator again presents the same ticket to the responder,
as shown in Figure 20. In this diagram, the first arrow inbound to the initiator
54

A B

{|A

K T

|}

KB #

.
.


w

N # a

{|A

K T

|}

KB #

.
.


w

#

N # b

{|N

# a

|}

K

.


w
.


w

{|N

# b

|}

K

#

.


w
Fig. 20. Neuman-Stubblebine, Part II (Re-authentication)
strand does not represent a real message; it represents the state stored in the
initiator that preserves the ticket for later re-use.
In the presence of this additional sub-protocol, step 3 in the responder's guarantee
can no longer be completed. There must certainly still be a transforming
edge producing

{|N

b

|}

K , but this edge may lie either on an initiator strand for
Part I of the protocol, or on (conceivably) either type of strand for Part II.
By contrast, the initiator's guarantee for Part I is una#ected, because we have
not added any strand with a transforming edge producing a term of the form

{|B

N a K t b

|}

KA .
This example illustrates the need for a systematic way to understand protocol
mixing, as for instance the mixing of part I and part II of Neuman-Stubblebine.
We undertake that task in the next section.
6 Protocol Independence via Disjoint Encryption
Whether a cryptographic protocol achieves a security goal depends on what
cannot happen. To authenticate a regular principal engaging in a protocol run, we
must observe a pattern of messages that can only be constructed by that principal
in that run, regardless of how the penetrator combines his own actions with those
of principals engaging in other runs, as codified in the Dolev-Yao model [9].
When several cryptographic protocols are combined, the penetrator has new
opportunities to obtain the messages which ought to authenticate principals to
their peers. The penetrator has more unintended services to draw on.
Indeed, because protocol mixing has shown itself to be a significant cause
of protocol failure, and makes protocol analysis more di#cult [6, 10, 23, 35, 46,
48], it has been identified [36] as a key problem in applying formal methods to
cryptographic protocols.
Moreover, in practice, di#erent protocols using cryptography are usually combined.
A key distribution protocol is useful only if the session key it delivers is
used for encryption. That later use may involve constructing messages similar
to messages used in the key distribution protocol itself. Does this make replay
attacks possible? Does the use of a key undermine the guarantees provided by
55

the protocol distributing that key? Or conversely, can the penetrator manipulate
messages from the key distribution protocol to spoof the later use of the key?
There are other reasons why protocol mixture is prevalent. Many recent protocols
have large numbers of di#erent options, and therefore have large numbers
of di#erent sub-protocols [33, 18, 8, 35]. Each of these protocols may be easy to
analyze on its own. But the same principal is required to be able to engage in
any sub-protocol. Can the penetrator manipulate this willingness for his own
purposes?
When protocols are mixed together, and we want to appraise whether the
security of one is a#ected by the others, we will refer to the protocol under study
as the primary protocol. We will refer to the others as secondary protocols.
6.1 Avoiding Conflict

Common sense suggests a rule of thumb when protocols are to be mixed together.
This rule is that if the primary protocol uses a particular form of encrypted
message as a test to authenticate a peer [14], then the secondary protocols should
not construct a message of that form. If the primary protocol uses a particular
form of encrypted component to protect some private value, then the secondary
protocol should not receive messages of that form and retransmit their contents
in other (potentially less secure) forms. Putting these two ideas together, the
sets of encrypted messages that the di#erent protocols manipulate should be
disjoint.
In the case of Neuman-Stubblebine, for instance, the ticket

{|A

K T

|}

KB originates
on the primary protocol; it is stored by the initiator for use in the secondary
protocol; and it is then manipulated and transformed by the responder in the
secondary protocol. This violates the disjointness we would like to maintain.
One way to arrange for disjoint encryption is to give each protocol some distinguishing
value, such as a number; that number may then be included as part
of each plaintext before encipherment. Then no principal can mistake a value as
belonging to the wrong protocol; an encrypted value bearing a di#erent protocol
's number must not be transformed. Another way to achieve disjoint encryption
is to ensure that di#erent protocols never use the same key, although this
may be expensive or di#cult to arrange. Although the Abadi-Needham paper
on prudent engineering practice for cryptographic protocols [1] does not discuss
mixing di#erent protocols, this rule---to try to achieve disjoint encryption---is in
the same spirit as those it proposes.
In this section, we will prove that, properly formalized, it su#ces. If two
protocols have disjoint encryption, then the first protocol is independent of the
second. By this we mean that if the primary protocol achieves a security goal
(whether an authentication goal or a secrecy goal as defined in Sections 3.12--
3.13) when the protocol is executed in isolation, then it still achieves the same
security goal when executed in combination with the secondary protocol.
One of the advantages of our approach is that the result works for all secrecy
and authentication goals; in this it continues a trend visible from several
recent papers [31, 21, 45, 44, 19]. We have an additional reason for including this
56

material here: It is a good example of the power of the machinery of paths and
well-behaved bundles developed in Section 4.
6.2 Multiprotocol Strand Spaces

To represent multiple protocols [46], we select some regular strands as being runs
of the primary protocol; we call these strands primary strands.

Definition 16. A multiprotocol strand space is a strand space (#, tr) together
with a distinguished subset of the regular strands # 1

#

#

\ P#

called the set of

primary strands.

# 2 denotes the set of all other regular strands, called secondary strands. A node
is primary or secondary if the strand it lies on is. From the point of view of
a particular analysis, the secondary strands represent runs of other protocols,
di#erent from the primary one under analysis.
The notion of equivalence needed for our purposes in this section concentrates
on primary nodes.

Definition 17. Two bundles

C, C

# in the multiprotocol strand space (#, tr , # 1 )
are equivalent if and only if
1. they have the same primary nodes, meaning

C #

# 1 =

C

#

#

# 1 ;
2. for all a, a originates uniquely and on a primary node in

C

if and only if a

originates uniquely and on a primary node in

C

# ;
3. for all a, a is non-originating in

C

i# a is non-originating in

C

# .
Since this is a more liberal notion of equivalence (it requires fewer nodes and
unique origination facts to be unchanged), any existence assertion about equivalent
bundles from Section 4 remains true in the present context.
We will also jettison the strand space parameter KP for our current purposes,
and express our assumptions about safe keys purely in terms of non-origination.
For our present purposes, this has the advantage of not distinguishing whether
a key is disclosed through a K-strand or through a secondary strand. The e#ect
for us is now the same.
6.3 Linking Paths

From Section 4, we also know that every bundle

C

is equivalent to a directed
bundle

C

# (Definition 14), and this remains true with our new definition of equivalent,
assuming that in the definition of directed bundles we make the same
substitution of "primary" for "regular:"

Definition 18.

C

is directed if for every node n

# C,

there is a primary node

m

# C #

# 1 such that n

# C

m.
57

Suppose we can show that given any bundle

C

involving both protocols, we can
find an equivalent bundle in which no path leads from a secondary node to a
primary node. Then there is also an equivalent

C

# in which there are no secondary
nodes at all. Therefore, if

C

is a counterexample to some authentication goal,

C

#

is a counterexample in which the secondary protocol does not occur at all. This
will establish protocol independence for authentication goals.
Let us say that a penetrator path p is an inbound linking path if p 0

#

# 2

and #(p)

#

# 1 . We thus take the point of view of the primary path, and regard

p as linking the secondary node to a primary node. One of the crucial steps in
showing protocol independence is showing that we can unlink inbound linking
paths.
A penetrator path p is an outbound linking path if p 0

#

# 1 and #(p)

#

# 2 . We
need not unlink these, but we need to ensure that they do not deliver terms to
the secondary protocol from which the secondary protocol will extract a secret.
6.4 Bridges

If

C

is a normal bundle and p is a penetrator path through

C,

then all destructive
edges precede constructive edges in p. The edge that separates the destructive
portion of a path from the constructive portion is of special interest. We call it
a bridge.

Definition 19. A bridge in a bundle

C

is a message transmission edge m

#

n

embedded in a subgraph of one the types shown in Figure 21.
If m

#

n is a bridge, then its bridge term is term(m), which equals term(n).
A bridge is simple i# its bridge term is simple, that is, is not of the form g h.

Any edge between regular nodes is an external bridge. The source m of a bridge

m

#

n is never on a constructive penetrator strand, and the target n is never
on a destructive penetrator strand.
A term is simple if it is an atom or an encryption, not a concatenation (see
Definition 8 in Section 3.14).

Proposition 20. Suppose that

C

is a normal bundle, and p is any penetrator
path in

C.

Then p traverses exactly one bridge.
Any bundle

C

can be replaced by an equivalent bundle

C

# in which the bridge
term for every path is simple. Moreover if

C

is normal or e#cient, so is

C

# .

The proof of the second assertion consists of adding S-strands to separate any
concatenated bridge term g h and C-strands to reconstruct g h after the bridges
of the two new sub-paths.

#

g h

# .
.

#
#

g

# .
.

#
#

h

# .

#
#

.

#
#

g h

# #

58

Destructive Constructive

.
.


w

h

# .
.


Regular Constructive

#

h

# .
.


Destructive Regular

.
.


w

h

# #

Regular Regular

#

h

# #

Fig. 21. Four Types of Bridge: Internal, Entry, Exit, and External Bridges
Since every path p has a unique bridge, we can write pbt(p) for the bridge term
occurring on the bridge.
If a path includes penetrator nodes and regular nodes, then it never traverses
the same component before and after a regular node:

Proposition 21. Suppose that

C

is normal, e#cient, and has simple bridges,
and p is a path through

C

that traverses no key edges. If i  k, p j is a
negative regular node, and p i , p k are penetrator nodes with simple terms, then
term(p i )

#=

term(p k ).

Suppose moreover that p k is the first penetrator node after p j such that p k has
a simple term. Then p j

#

+

p j+1 produces a new component t 0 @ term(p j+1 ),

and term(p k ) = t 0 .

The result follows routinely from e#ciency.
6.5 Disjoint Encryption

The simplest way to state the disjoint encryption assumption would be to require
that the two protocols not use the same ciphertext as a part of any message.
That would mean that if n 1

#

# 1 and n 2

#

# 2 , and if

{|h|}

K @ term(n 1 ), then

{|h|}

K

#@

term(n 2 ).
However, this simple version is unnecessarily restrictive. The secondary protocol
would be unable to accept public-key certificates generated in the primary
protocol, which is intuitively harmless because the contents are public in any
59

case. The secondary protocol would also be unable to re-use symmetric-key tickets
such as those generated by the Kerberos Key Distribution Center [24, 38].
These are also intuitively harmless, so long as the secondary protocol does not
extract private values from within them, or repackage their private contents,
potentially insecurely. Hence, we allow these harmless exceptions to the requirement
that no encrypted term be used by both protocols.

Definition 22.

{|h|}

K is a shared encryption if there exist n 1

#

# 1 and n 2

#

# 2

such that

{|h|}

K @ term(n 1 ) and

{|h|}

K @ term(n 2 ). It is an outbound shared
encryption if this holds with n 1 positive and n 2 negative. It is an inbound shared
encryption if this holds with n 1 negative and n 2 positive.
We want to restrict but not prohibit shared encryptions, and we will do so in
slightly di#erent ways for inbound and outbound shared encryptions.

Definition 23. (Disjoint Outbound Encryption) # has disjoint outbound
encryption if and only if, for every outbound shared encryption

{|h|}

K , for every
atom a @

{|h|}

K , and for every n 2

#

+

n # 2

#

# 2 ,

if n 2 is negative and

{|h|}

K @ term(n 2 ),

and n # 2 is positive and t 0 is a new component of n # 2 ,

then a

#@

t 0 .
That is, no secondary strand manipulates a into a new component.
This definition has the important property that values originating uniquely
on primary nodes cannot "zigzag" to a secondary node, before being disclosed
to the penetrator.

Proposition 24. (No Zigzags) Let # have disjoint outbound encryption, and
let

C

be a normal, e#cient bundle with simple bridges in #. Suppose p is a path
such that term(#(p)) = a (where a

#

K

#

T), a @ term(p i ) for all 1

#

i

# |p|,

and p k

#

# 2 . Then p j

##

# 1 for any j  k.

Proof. Suppose otherwise. We may assume that j, k are chosen so that j is the
largest index such that p j

#

# 1 and there is some later p k

#

# 2 , and k is the
smallest value > j such that p k

#

# 2 . So the path  p = p j

#-#    #-#

p k is a
penetrator path.
If  p traverses a key edge (see Section 4.6) at p i

#

p i+1 , then term(p i ) = a is
a key. Therefore p i

#

p k

#

#(p), contradicting e#ciency.
Therefore  p begins at a positive regular (primary) node, ends at a negative
regular (secondary) node, and never traverses a key edge. It is of type 4 in the
catalog of Section 4.6. Therefore it has a bridge term pbt(p) such that pbt(p) @

term(p j ) and pbt(p) @ term(p k ). Since a @ pbt(p), either a is itself a component
of pbt(p), or else a @

{|h|}

K @ pbt(p). If a is a component of pbt(p), then we
have a contradiction to e#ciency as before.
Otherwise,

{|h|}

K is an outbound shared encryption. By Proposition 21,

p k

#

+

p k+1 produces a new component t 0 , and a @ t 0 . But this contradicts
the definition of outbound disjoint encryption.

##

60

As a consequence, we may infer that there is never a failure of secrecy where
any secondary node touches the secret value.
The condition on inbound shared encryptions is that they should never occur
in new components created on secondary nodes.

Definition 25. (Disjoint Encryption) # has disjoint inbound encryption if,
for every inbound shared encryption

{|h|}

K and n 2

#

+

n # 2

#

# 2 , if t 0 @

term(n # 2 ) is a new component, then

{|h|}

K

#@

t 0 .

# has disjoint encryption if it has both disjoint inbound encryption and
disjoint outbound encryption.
6.6 The Protocol Independence Theorem
Definition 26. # 1 is independent of # 2 if for every bundle

C

in #, there is a
bundle

C

# in # that is equivalent to

C

such that

C

# is disjoint from # 2 .

Proposition 27. (Protocol Independence) If # has disjoint encryption,
then # 1 is independent of # 2 .

Proof. We may assume that

C

is normal, e#cient, and has simple bridges. We
want to show that we can remove any inbound linking paths in

C.

Let p be an inbound linking path. Suppose first that p traverses an atomic
value a

#

T

#

K. This may either be the key edge into a D or E strand, or it
may be the bridge of p. In any case, let a be the first atomic value on p. By
Proposition 24, a does not originate uniquely on a primary node. Therefore,
there is an equivalent bundle

C

# in which a is produced by an initial penetrator
strand (a K-strand or a M-strand).

Suppose next that p never traverses an atomic value. Then in particular it
never traverses a key edge into a D or E strand. Thus, the path bridge term
pbt(p) @ term(p 1 ) and pbt(p) @ term(#(p)). Since pbt(p) is not atomic but it
is simple, it is of the form

{|h|}

K . Therefore, by disjoint inbound encryption, it
does not occur in a new component of p 1 . But by Proposition 21, this contradicts
e#ciency.
Therefore we may remove any inbound linking path p in a normal, e#cient
bundle with simple bridges. It follows that there is a

C

# equivalent to

C

such that

C

#

#

# 2 =

#. ##

An easy consequence of this theorem shows that if the primary and secondary
protocols share no keys whatever, then we have independence.

Corollary 1. For i = 1 and 2, let K i be the set of K such that K @ term(n)
for any n

#

# i or

{|h|}

K @ term(n) for any h and any n

#

# i .
If K 1

#

K 2 =

#,

then # 1 is independent of # 2 .

If # 1 and # 2 involve the activity of di#erent principals, and the keys for the
protocols are chosen in an unpredictable way from a large set, then the keys
they use will in practice never overlap. Therefore, # 1 is independent of # 2 . The
61

same holds when the same principals may participate in both protocols, but they
choose keys independently for each protocol.
Similarly, suppose each ciphertext created in # 1 or # 2 contains a distinguishing
values such as di#erent protocol numbers. If # 1 never accepts a ciphertext
containing # 2 's value, then we have disjoint inbound encryption. If # 2 never extracts
a subterm from a ciphertext containing # 1 's value, then we have disjoint
outbound encryption. Together, they su#ce for protocol independence.
6.7 An Application of Protocol Independence

Let us return to the Neuman-Stubblebine protocol, as described in Section 5.4
and summarized in Figures 19 and 20.
We regard the re-authentication protocol as the secondary protocol; the presence
of the re-authentication protocol should not undermine any security guarantee
o#ered by the primary protocol. However, terms of the form

{|N |}

K are
constructed as new components on secondary strands, and accepted on primary
strands. Hence the corresponding multiprotocol strand space does not have disjoint
inbound encryption. Indeed, the penetrator can use a session of the reauthentication
protocol to complete a responder strand in a bundle with no
initiator [46].
For this reason, we amend (see [46]) the re-authentication protocol to the
form shown in Figure 22. To apply our independence theorem, we check that the
A #

B

{|A

K T

|}

KBS
.


w

N # a

{|A

K T

|}

KBS #

B
.


w

#

{|N

# a N # b

|}

K

.


w
.


w

{|A

N # b

|}

K

#

.


w
Fig. 22. Neuman-Stubblebine, Part II modified (Re-authentication)
corresponding strand space # has disjoint encryption. But that is trivial, because
tickets

{|A

K T

|}

KBS are the only common encrypted subterms of primary and
secondary nodes. The outbound property holds because no private subterm of a
ticket is uttered in a new component of a secondary node. The inbound property
holds because no new component of a secondary node contains a ticket.
Therefore, if

C

is a counterexample to some security property, we may deform

C

into an equivalent standard bundle

C

# , in which there are no secondary nodes.

C

# is still a counterexample, assuming that the security property is invariant
under bundle equivalences, as authentication and secrecy properties are. Thus,
if the primary protocol fails to meet the security goal, that is independent of
62

the presence of the secondary protocol: the corrected Neuman-Stubblebine reauthentication
protocol is entirely guiltless in this a#air.
6.8 Conclusion

In this report, we have focused on two information security problems. One is
the packet protection problem, where we have studied filtering routers and
firewall-oriented security goals that they are capable of achieving. The other
is the Dolev-Yao problem, where we have studied how to achieve authentication
and confidentiality goals in the presence of an active penetrator.
In both areas, we applied essentially the same method. We identified a class
of security goals that capture important real-world security services that people
need to achieve. We introduced simple mathematical modeling notions, such as
directed graphs, boolean algebras, and freely generated algebras. In terms of
this vocabulary, we were able to formalize the security goals and develop proof
techniques and algorithms to determine what postures or protocols achieve the
goals.
We regard these two problems as instances of foundational work in security
 management. Although the phrase sounds prosaic, the problems it covers
are fundamental in a world where many mechanisms and systems cooperate to
achieve our security objectives. Knowing that they jointly achieve something
meaningful is di#cult. Yet the problems have enough structure to repay mathematical
abstraction, and the abstractions tell us, systematically, how to marshal
the mechanisms to achieve practical protection.
References

1. Martn Abadi and Roger Needham. Prudent engineering practice for cryptographic
protocols. In Proceedings, 1994 IEEE Symposium on Research in Security and
Privacy, pages 122--136. ieee, ieee Computer Society Press, 1994.
2. Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. E#cient implementation
of a BDD package. In 27th ACM/IEEE Design Automation Conference, pages
40--45, 1990.
3. Randal E. Bryant. Graph-based algorithms for boolean function manipulation.

IEEE Transactions on Computers, C-35(8):677--691, August 1986.
4. Michael Burrows, Martn Abadi, and Roger Needham. A logic of authentication.

Proceedings of the Royal Society, Series A, 426(1871):233--271, December 1989.
Also appeared as SRC Research Report 39 and, in a shortened form, in ACM
Transactions on Computer Systems 8, 1 (February 1990), 18-36.
5. Ulf Carlsen. Optimal privacy and authentication on a portable communications
system. Operating Systems Review, 28(3):16--23, 1994.
6. John Clark and Jeremy Jacob. A survey of authentication protocol literature:
Version 1.0. University of York, Department of Computer Science, November 1997.
7. Edmund Clarke, Somesh Jha, and Will Marrero. Using state space exploration and
a natural deduction style message derivation engine to verify security protocols.
In Proceedings, IFIP Working Conference on Programming Concepts and Methods
( Procomet), 1998.
63

8. T. Dierks and C. Allen. The TLS protocol. RFC 2246, January 1999.
9. D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions
on Information Theory, 29:198--208, 1983.
10. Li Gong and Paul Syverson. Fail-stop protocols: An approach to designing secure
protocols. In 5th International Working Conference on Dependable Computing for
Critical Applications, pages 44--55, September 1995.
11. Joshua D. Guttman. Filtering postures: Local enforcement for global policies. In

Proceedings, 1997 IEEE Symposium on Security and Privacy, pages 120--29. IEEE
Computer Society Press, May 1997.
12. Joshua D. Guttman. Packet filters and their atoms. Lecture at University of
Pennsylvania, host C. Gunter, April 1999.
13. Joshua D. Guttman, Amy L. Herzog, and F. Javier Thayer. Authentication and
confidentiality via IPsec. In D. Gollman, editor, ESORICS 2000: European Symposium
on Research in Computer Security, LNCS. Springer Verlag, 2000.
14. Joshua D. Guttman and F. Javier Thayer Fabrega. Authentication tests. In Proceedings,
2000 IEEE Symposium on Security and Privacy. May, IEEE Computer
Society Press, 2000.
15. Joshua D. Guttman and F. Javier Thayer Fabrega. Protocol independence
through disjoint encryption. In Proceedings, 13th Computer Security Foundations
Workshop. IEEE Computer Society Press, July 2000.
16. Joshua D. Guttman and F. Javier Thayer Fabrega. Authentication tests and the
structure of bundles. Theoretical Computer Science, 2001. To appear.
17. Joshua D. Guttman, F. Javier Thayer Fabrega, and Lenore D. Zuck.
Faithful to the cryptography. Submitted for publication. Available at

http://cs.nyu.edu/zuck.

18. D. Harkins and D. Carrel. The Internet Key Exchange (IKE). IETF Network
Working Group RFC 2409, November 1998.
19. James Heather, Gavin Lowe, and Steve Schneider. How to prevent type flaw attacks
on security protocols. In Proceedings, 13th Computer Security Foundations
Workshop. IEEE Computer Society Press, July 2000.
20. James Heather and Steve Schneider. Toward automatic verification of authentication
protocols on an unbounded network. In Proceedings, 13th Computer Security
Foundations Workshop. IEEE Computer Society Press, July 2000.
21. Mei Lin Hui and Gavin Lowe. Safe simplifying transformations for security protocols.
In 12th Computer Security Foundations Workshop Proceedings, pages 32--43.
IEEE Computer Society Press, June 1999.
22. Jan Jurjens and Guido Wimmel. Specification-based testing of firewalls. Submitted
for publication, 2001.
23. John Kelsey, Bruce Schneier, and David Wagner. Protocol interactions and the
chosen protocol attack. In Security Protocols, International Workshop April 1997
Proceedings, pages 91--104. Springer-Verlag, 1998.
24. J. Kohl and C. Neuman. The Kerberos network authentication service (v5). RFC
1510, September 1993.
25. Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Remy, and Jerome Vouillon.
 The Objective Caml System. INRIA, http://caml.inria.fr/, 2000. Version
3.00.
26. Gavin Lowe. An attack on the Needham-Schroeder public key authentication protocol.
 Information Processing Letters, 56(3):131--136, November 1995.
27. Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using
FDR. In Proceeedings of tacas, volume 1055 of Lecture Notes in Computer Science,

pages 147--166. Springer Verlag, 1996.
64

28. Gavin Lowe. Some new attacks upon security protocols. In Proceedings of the Computer
Security Foundations Workshop IX. IEEE Computer Society Press, 1996.
29. Gavin Lowe. Casper: A compiler for the analysis of security protocols. In 10th
Computer Security Foundations Workshop Proceedings, pages 18--30. IEEE Computer
Society Press, 1997.
30. Gavin Lowe. A hierarchy of authentication specifications. In 10th Computer Security
Foundations Workshop Proceedings, pages 31--43. IEEE Computer Society
Press, 1997.
31. Gavin Lowe. Toward a completeness result for model checking of security protocols.
In 11th Computer Security Foundations Workshop Proceedings, pages 96--105.
IEEE Computer Society Press, 1998.
32. Will Marrero, Edmund Clarke, and Somesh Jha. A model checker for authentication
protocols. In Cathy Meadows and Hilary Orman, editors, Proceedings of the
DIMACS Workshop on Design and Verification of Security Protocols. DIMACS,
Rutgers University, September 1997.
33. D. Maughan, M. Schertler, M. Schneider, and J. Turner. Internet Security Association
and Key Management Protocol (ISAKMP). IETF Network Working Group
RFC 2408, November 1998.
34. Alain Mayer, Avishai Wool, and Elisha Ziskind. Fang: A firewall analysis engine.
In Proceedings, IEEE Symposium on Security and Privacy, 2000.
35. Catherine Meadows. Analysis of the Internet Key Exchange protocol using the
NRL protocol analyzer. In Proceedings, 1999 IEEE Symposium on Security and
Privacy. IEEE Computer Society Press, May 1999.
36. Catherine Meadows. Open issues in formal methods for cryptographic protocol
analysis. In DISCEX Workshop. DARPA, January 2000.
37. Roger Needham and Michael Schroeder. Using encryption for authentication in
large networks of computers. Communications of the ACM, 21(12), December
1978.
38. B. Cli#ord Neuman and Stuart G. Stubblebine. A note on the use of timestamps
as nonces. Operating Systems Review, 27(2):10--14, April 1993.
39. Lawrence C. Paulson. Proving properties of security protocols by induction. In 10th
IEEE Computer Security Foundations Workshop, pages 70--83. IEEE Computer
Society Press, 1997.
40. Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols.
 Journal of Computer Security, 1998. Also Report 443, Cambridge University
Computer Lab.
41. Adrian Perrig and Dawn Xiaodong Song. Looking for diamonds in the desert:
Extending automatic protocol generation to three-party authentication and key
agreement protocols. In Proceedings of the 13th IEEE Computer Security Foundations
 Workshop. IEEE Computer Society Press, July 2000.
42. Dag Prawitz. Natural Deduction: A Proof-Theoretic Study. Almqvist and Wiksel,
Stockholm, 1965.
43. Steve Schneider. Verifying authentication protocols with CSP. In Proceedings
of the 10th IEEE Computer Security Foundations Workshop, pages 3--17. IEEE
Computer Society Press, 1997.
44. Scott Stoller. A bound on attacks on authentication protocols. Available at
http://www.cs.indiana.edu/stoller/, July 1999.
45. Scott Stoller. A reduction for automated verification of authentication protocols.
In Workshop on Formal Methods and Security Protocols, July 1999. Available at
http://www.cs.indiana.edu/stoller/.
65

46. F. Javier Thayer Fabrega, Jonathan C. Herzog, and Joshua D. Guttman. Mixed
strand spaces. In Proceedings of the 12th IEEE Computer Security Foundations
Workshop. IEEE Computer Society Press, June 1999.
47. F. Javier Thayer Fabrega, Jonathan C. Herzog, and Joshua D. Guttman.
Strand spaces: Proving security protocols correct. Journal of Computer Security,

7(2/3):191--230, 1999.
48. D. Wagner and B. Schneier. Analysis of the SSL 3.0 protocol. In Proceedings,
Second USENIX Workshop on Electronic Commerce, pages 29--40, 1996. Available
at http://www.counterpane.com/ssl.html.
49. Thomas Y. C. Woo and Simon S. Lam. Verifying authentication protocols: Methodology
and example. In Proc. Int. Conference on Network Protocols, October 1993.
50. T. Ylonen, T. Kivinen, and M. Saarinen. SSH prototcol architecture. Internet
draft, November 1997. Also named draft-ietf-secsh-architecture-01.txt.
66

