Semantics and Logic for Security Protocols
Bart Jacobs ∗†Institute for Computing and Information Sciences
Radboud University Nijmegen, The Netherlands
Email: B.Jacobs@cs.ru.nl
URL: http://www.cs.ru.nl/B.Jacobs

Ichiro Hasuo
Institute for Computing and Information Sciences, Radboud University Nijmegen, the Netherlands
and Research Institute for Mathematical Sciences, Kyoto University, Japan
Email: I.Hasuo@cs.ru.nl
URL: http://www.cs.ru.nl/I.Hasuo

June 12, 2007

Abstract
This paper presents a sound BAN-like logic for reasoning about security protocols
with theorem prover support. The logic has formulas for sending and receiving messages (with nonces, public and private encryptions etc.), and has both temporal andepistemic operators (describing the knowledge of participants). The logic’s semantics
is based on strand spaces. Several (secrecy or authentication) formulas are proven ingeneral and are applied to the Needham-Schroeder(-Lowe), bilateral key exchange andthe Otway-Rees protocols, as illustrations.

1 Introduction
Security protocols are difficult to get right, and so a formal understanding of their meaning
with associated reasoning techniques has been an important topic for many years. Roughly
two approaches have emerged, one based on algorithmic techniques using model checkers(such as [22, 3], see also [28]) and one on logical reasoning. This paper fits in the lattertradition. The algorithmic techniques are very good at detecting errors in relatively simple
protocols in a “push button” style, but usually run into problems with the size of state spaces
for more complicated protocols. In contrast, the techniques based on logical reasoning
can in principle handle arbitrarily complex protocols, but may involve considerable userinteraction. Hence, again in broad terms, algorithmic techniques are most useful early on
in design, and logical techniques later on in certification.
This paper describes a formalisation of security protocols, involving a mathematicalmodel in the style of strand spaces [31], on top of which a (sound) logic is defined that
resembles BAN logic [4]. The whole formalisation is represented in the higher order logicof the theorem prover PVS [26], and allows verifications of actual protocols with tool
∗ Corresponding author. Postal address: P.O. Box 9010, 6500 GL Nijmegen, The Netherlands. Tel: +31 24
3652236 Fax: +31 24 3652298† Also part-time at Technical University Eindhoven, the Netherlands.

1

support, like in [27]. Hence, in a sense, it combines the best of these three approaches [31,4, 27].
The following aspects distinguish our formalisation.
• The logic involves both (linear) temporal operators (like henceforth) and epistemic
ones (describing knowledge of participants).
• There is a clear distinction between possession (of messages) and knowledge (oflogical assertions).
• There is a syntactic distinction between “new” nonces (or secret keys1 ) and “used”
nonces, with an associated requirement that “new” nonces (or keys) are globally
fresh.
This paper makes essential use of earlier related work [31, 4, 27, 29, 11] but differs inseveral ways.
• The strand spaces of [31] form a mathematical model consisting of “bundles” of“strands” of incoming and outgoing messages for each participant in a security protocol. Here we formalise essential parts of these strand spaces in the language of atheorem prover and provide it with a logic.
• The virtue of BAN-style logical rules does not confine itself to their use in verification via theorem proving: they also tell a protocol designer how to get a protocol
right, functioning as “rules of thumb”. However, one of the most problematic aspects of the so-called BAN logic [4] is its lack of semantics. Here we approach thematter from a different angle: we do not start with a logic, but with a semantics andformulate logical rules as valid consequences in the formalised model.
Hence, formally speaking we don’t have a logic as a collection of (syntactical) formulas with a derivation relation. Our logic is “shallow” and exists only as provable implications or lemmas about (interpreted) formulas as predicates on the model. Sucha “logic” is most convenient for the verification of concrete protocols in a theorem
prover.
• Within the inductive approach [27] a new model is constructed for each protocolthat is verified, namely as inductively defined set of lists of events. Here instead wehave a semantical infrastructure of strands that is the same for each specific protocol.
This allows us to prove more general logical rules, for instance about the sending or
receiving of public or secret encryptions.
• The aim of the present paper is to formulate a logic to reason about security properties
on top of a strand space semantics. This aim is very similar to the one of [29] (seealso [30, Section 6.2]) and also of [11, 6, 7].
First, the reference [29] only contains a number of definitions for such a logic, without any rules, applications, or formalisations. Thus, one could say, the present paper
achieves what is sketched in [29].
Second, the reference [11] defines a logic on what they call Cord calculus: this is aprocess-algebraic formulation of a variant of strand spaces. The resulting logic looks
quite similar to ours, although the compositionality of logical reasoning is not in our
1 In this paper a key for symmetric encryption is called a secret key. A key pair for asymmetric encryption
consists of a public key and a private key.

2

logic, mainly in order to ease its formalisation in PVS. Compositionality is claimed
to be a feature of the logic in [11] and is utilized in [6, 7] to show security propertiesof compositions of protocols.
The use of a theorem prover in the formalisation of our model is for two reasons.
1. In general, a theorem prover is like a skeptical colleague who patiently checks alldetails. In the present setting this is useful because many proofs (esp. of the logicalrules in Section 5) are complex, highly combinatorial, and involve many different
case distinctions. In such situations humans easily make mistakes.
2. The present formalisation arose via several iterations, in which some subtle properties of the set of messages or of the semantical infrastructure were changed. The
ability to re-run the proofs of existing results after such basic changes is very helpful
to quickly see the consequences, and to maintain overall consistency. It will also beof use for possible future extensions and adaptations of the model.
The fact that we used the theorem prover PVS is not especially relevant for the topic. We
could also have used the higher order logic of the theorem provers Isabelle or COQ. The
presentation in this paper abstracts from the concrete syntax of PVS and uses a more mathematical/logical style. However, readers who wish to see the details of the formalisation [20]will have to read PVS code.
The idea of building a BAN-like logic on top of a strand space model is not reallynew (see for instance [29]). The contribution of this paper is however, that this idea has
been elaborated in full detail, been formalised, and put to use successfully in concrete
examples. Doing so required a subtle balancing of the various possible requirements andformulations—and a non-trivial amount of PVS work!
We analyse three protocols using our toolkit: the Needham-Schroeder(-Lowe), the bilateral key exchange and the Otway-Rees protocols. Security properties of Otway-Rees
are substantially harder to prove compared to the first two, due to the presence of tickets,that is, encrypted units received and forwarded without interpretation. In this paper we first
introduce some simpler secrecy/authentication rules and analyse the first two protocols.
Those rules turn out to be of no use for Otway-Rees because of these tickets. Therefore we
strengthen these rules in a later section.
Below we start in Section 2 with some fundamental results about the well-known
Needham-Schroeder protocol. Their sole role at this stage is to illustrate the style of properties that can be proved. The explanation of the underlying theories starts in Section 3
with the theory of protocol messages, and proceeds with strands and bundles in Section 4,
and with logical rules in Section 5. For the actual application of our theories we choose
to use different protocols than the already much-used Needham-Schroeder protocol. The
bilateral key exchange protocol (from [5, Section 6.6.6]) is analysed in Section 6. In Section 7 the verification challenge in the Otway-Rees protocol is identified and the logicalrules are strengthened accordingly.

2 Results about the Needham-Schroeder public key protocol
Here we consider the well-known Needham-Schroeder public key protocol from [24],which was shown to be flawed in [21]. It can be described via the following three message exchanges between Alice (written as A, with public key KA ) and Bob (B with public
3

key KB ).
A −→ BB −→ AA −→ B:::{ nA , A }KB{ nB , nA }KA{ nB }KB

Here we write nA for a fresh (or new) nonce introduced by A, and similarly nB for a fresh
nonce of B.
What we can prove about this protocol is formulated as follows.
A Sends { newnonce(nA ), name(A) }KB @ i∧A Sees { nonce(nB ), nonce(nA ) }KA @ i + j=⇒HenceForth Secret(A, B)(nonce(nA )) @ i + j

In ordinary words: if Alice sends the first protocol message at stage i and then sees thesecond message at stage i + j, then her nonce nA is a shared secret between her and Bobfrom stage i + j onwards. Notice that Alice’s nonce nA is labeled with ‘new’ in its firstuse, and as a ‘plain’ nonce in subsequent use. Bob’s nonce nB is new when Bob sends it,
but not anymore when Alice sees it.
An analogous result about Bob’s nonce nB is not provable because of Lowe’s attack [21]. It can however be proved for the repaired “Needham-Schroeder-Lowe” protocol:
A −→ BB −→ AA −→ B:::{ nA , A }KB{ nB , nA , B }KA{ nB }KB

Then we can prove for instance the following non-trivial result.
A Sends { newnonce(nA ), name(A) }KB @ i∧A Sees { nonce(nB ), nonce(nA ), name(B) }KA @ i + j∧A Knows B Sees { nonce(nB ) }KB @ i + j + k=⇒A Knows B Knows HenceForth Secret(A, B)(nonce(nB ))@i + j + k

It tells that if Alice first sends and sees the appropriate messages and then knows that Bob
sees the final message, then Alice knows that Bob knows that hisnonce nB is hencefortha shared secret. The knowledge operator satisfies X Knows ϕ ⇒ ϕ so that the conclusion is pretty strong, and implies for instance the secrecy of the nonce. Note that Aliceneeds to know the fact that the final message was seen by Bob—a fact that she cannot directly observe herself—in order to draw conclusions about Bob’s knowledge. This is quite
natural.

In the remainderof this paper we shall explain what formulas like A Sends m @ ior B Knows ϕ mean, and how they can be proved.

3 The theory of messages
The parties involved in the security protocols will be called agents. For the time being weshall assume a (parameter) type AG of agents, without any further structure. Only later on
we shall assume a spy among the agents.
4

Messages are the identities that are exchanged between agents in a protocol. They may
be nonces, keys, names, sequence numbers etc. The type MSG of messages is definedinductively, using the following BNF notation.
m ::=name(a) | number(i) | newnonce(n) | nonce(n) | newseckey(k) |seckey(k) | pubkey(k) | privkey(k) | k{ m } | { m }k | hash(m) | hm, mi

The identifier a in name(a) refers to an agent, where name(−) acts like a tag. The n in
nonce(n) and newnonce(n) belong to an unspecified domain of nonces. Similarly for thedifferent types of keys k, with a tag e.g. pubkey(−) making a key k into a message. The
role of the ‘new’ will be explained later. We use the notation k{ m } for secret (symmetric)
encryption and { m }k for public (asymmetric) encryption. There is an implicit function· that sends a public key k to its associated private one k. The notation h−, −i for tuples
is often used implicitly, for instance in k{ m1 , m2 }. Since messages are freely generated
tupling is not associative: hhm1 , m2 i, m3 i =6 hm1 , hm2 , m3 ii. Signed messages are at thisstage not supported.
The use of an inductively defined set of messages implicitly involves certain idealisations. For instance, hashes are assumed to be perfect, since by construction hash(m1 ) =hash(m2 ) implies m1 = m2 . Also, the explicit use of the datatype’s constructors excludes
type flaw attacks (see e.g. [23, 19]).
A first basic function is n2p : MSG → MSG for “new-to-plain”. It erases ‘new’ recursively, and is defined in the obvious way:n2p(name(a))
n2p(number(i))
n2p(nonce(n))
n2p(newnonce(n))
n2p(seckey(k))
n2p(newseckey(k))

=
=
=
=
=
=

name(a)number(i)nonce(n)nonce(n)seckey(k)seckey(k)n2p(pubkey(k))
n2p(privkey(k))
n2p(k{ m })n2p({ m }k )n2p(hash(m))
n2p(hm1 , m2 i)

=
=
=
=
=
=

pubkey(k)privkey(k)k{ n2p(m) }{ n2p(m) }khash(n2p(m))
hn2p(m1 ), n2p(m2 )i.

It is clear that n2p is idempotent, i.e. satisfies n2p(n2p(m)) = n2p(m). A message m iscalled “plain” if it contains no ‘new’, i.e. if n2p(m) = m.

3.1

Subterms and paths

We use the symbol  for the syntactic subterm relation, that can also be defined inductively. It does not care about encryptions or hashes, so that for instance nonce(n) hash(nonce(n)), but not seckey(k)  k{ m }. It is not hard to see that  is a partial
order. Further results are: m1  m2 implies n2p(m1 )  n2p(m2 ), and: m1  m2 with
m2 plain implies that m1 is also plain; also: if m1  n2p(m2 ) then m′1  m2 for someterm m′1 with n2p(m′1 ) = m1 .
It is useful to extend the subterm relation to subsets U ⊆ MSG of messages: m  Umeans that m  m′ for some m′ ∈ U .
We shall often need a more informative subterm relationship involving “paths”. A pathℓ in ℓ : m1 /o /o / m2 or m1 /o ℓ /o / m2 indicates how a term m1 occurs as a subterm in m2 .
Such a path is a list of labels from the set{se(k), pe(k), ha, π1 , π2 }indicating how the subterm can be reached—where se(k) stands for secret encryption with5

k, etc. The path relation is defined inductively by the following two clauses.
se(k)·ℓ
m1 /o /o /o /o / k{ m2 }
pe(k)·ℓ m1 /o /o /o /o / { m2 }khi/o /o /o / hash(m2 )andm1 /o ℓ /o / m2 =⇒m /o /o / m
m1 /o ha·ℓ


π

o
/
o
/
 m1 1 ·ℓ/o /o / hm2 , m3 i
m1 /o π/o 2 ·ℓ/o /o / hm3 , m2 i

where hi is the empty list, and prefixing an element a to a list ℓ is described by the dot
notation a · ℓ.
Terms with such paths between them form a category 2 , with the empty list as identityℓ ;ℓℓℓmap, and list-append ; as composition: if m1 /o 1 /o / m2 and m2 /o 2 /o / m3 then m1 /o 2/o /o 1 /o / m3 .
Composition works backwards because of the (arbitrary) direction that we have used forpaths.
The relation between paths and subterms is easy:
m1  m 2⇐⇒∃ℓ. m1 /o ℓ /o / m2

Further, with paths we can define the following useful notions.
ℓℓ• Single-occurrence: m1 1 m2 is described as: m1 /o 1 /o / m2 and m1 /o 2 /o / m2 impliesℓ1 = ℓ2 . To be precise, what we define is really at most single occurrence.
• Occurrence under public encryption with key k: m1 pe(k) m2 means that each pathℓ with m1 /o ℓ /o / m2 must contain pe(k).
Similarly one defines occurrence m1 se(k) m2 under secret encryption.
These relations are extended in the obvious way to subsets. We have m pe(k) U
and m se(k) U , where the relation holds for any m′ ∈ U .
Additionally, for a set K of keys, m1 K m2 holds if each path ℓ with m1 /o ℓ /o / m2
contains pe(k) or se(k) with k ∈ K.

3.2

Possessions

We shall refer to “possessions” as the cryptographically accessible parts of messages. For
instance, m is in the possessions of a set U ⊆ MSG if k{ m } ∈ U and seckey(k) ∈ U ,and also if { m }k ∈ U and privkey(k) ∈ U —where the function · maps a public key tothe corresponding private one.
Formally we define possessions as a closure operation P : P(MSG) → P(MSG) via aleast fixed point (see e.g. [8]). It is the analogue of Paulson’s analz [27]. For U ⊆ MSG
we can describe P(U ) ⊆ MSG as the smallest subset with:k{ m }, seckey(k) ∈ P(U ) ∨ { m }k , privkey(k) ∈ P(U ) ∨U ⊆ P(U )and=⇒ m ∈ P(U )′hm, m i ∈ P(U ) ∨ ′
hm , mi ∈ P(U )A basic observation is that m  P(U ) if and only if m  U .

2 It happens more frequently that a partial order can be described in a more refined way leading to morphisms
in a category, for instance in the propositions-as-types view where implications become proofterms.

6

Example 3.1. The set of terms
no
P h { seckey(ks) }kp , ks{ name(a), hash(nonce(n)) } i, privkey(kp)contains name(a) but not nonce(n).
The PVS formalisation [20] contains appropriate rewrite rules that can prove such
inhabitation statements via automatic rewriting. The rewrite rules make several passes
through a list of terms, each time recording the keys that are available and that are stillneeded. The rewriting stops at the end of such a pass when there is no overlap between
these sets of available and needed keys.
Possessions can be described in terms of paths:m ∈ P(U )⇐⇒ ∃m′ ∈ U. ∃ℓ. m /o ℓ /o / m′ ∧ ha 6∈ ℓ ∧∀k. se(k) ∈ ℓ ⇒ seckey(k) ∈ P(U ) ∧∀k. pe(k) ∈ ℓ ⇒ privkey(k) ∈ P(U )This allows us to prove the following two important properties about occurrences underpublic encryptions.
1. If m pe(k) U and m ∈ P(U ) but not m ∈ U , then privkey(k) ∈ P(U ).
2. If m pe(k) U and privkey(k) 6∈ P(U ), then m pe(k) P(U ).
They form a crucial ingredient of the proof of the public encryption rule in Subsection 5.2.

3.3

Communications

Agents use the possessions operator from the previous subsection to decompose incoming
messages. They use a “communications” operator to build up new messages that they cansend out. This operator—comparable to the synth of [27]—is again a closure operator
C : P(MSG) → P(MSG). For U ⊆ MSG we have C(U ) ⊆ MSG as the smallest set
with:U ⊆ C(U )name(a), number(i), newnonce(n), newseckey(k) ∈ C(U )m, seckey(k) ∈ C(U ) =⇒ k{ m } ∈ C(U )m, pubkey(k) ∈ C(U ) =⇒ { m }k ∈ C(U )m ∈ C(U ) =⇒ hash(m) ∈ C(U )m, m′ ∈ C(U ) =⇒ hm, m′ i ∈ C(U ).
The most important point is that ‘new’ nonces and secret keys always belong to the communications. In contrast, ‘plain’ nonces and secret keys only belong to C(U ) if they alreadybelong to U . The restriction that ‘new’ nonces and secret keys must be really new is imposed on a global level, that is, on bundles. This will be explained later in Section 4.2.
Obvious properties are m  U ⇒ m  C(U ), and similarly for pe(k) and se(k)instead of . A less trivial one is:nonce(n) /o ℓ /o / m ∈ C(U ) =⇒∃m′ ∈ U. ∃ℓ1 , ℓ2 . nonce(n) ℓ/o 2 /o / m′ ∧ m′ ℓ/o 1 /o / m ∧ ℓ = ℓ1 ; ℓ2 .
It says: if nonce(n) appears in a message m ∈ C(U ) then we can find a message m′ ∈ Uwhich contains nonce(n) and is contained in m. The same result holds for seckey(k) inplace of nonce(n).
74 Strands and bundles
4.1

Strands

In our formalisation we shall use “strands” as infinite sequences of possible messages. A
strand describes what happens to an individual agent, in terms of the incoming and outgoingmessages (like in [31]). Such a message m at an arbitrary stage i, if any, is either incoming,
written as −m, or outgoing, written as +m. The type of “message” strands is thus defined
as function space:
def
MStr = N −→ 1 + (Sgn × MSG)

where 1 = {⊥} and Sgn = {−, +}. An example of a strand is thus h+m, ⊥, ⊥, −m′ , . . .i
where ⊥ indicates that nothing is sent or received at that stage.
With such a strand of messages we associate a strand of possessions. It contains at eachstage the cryptographically accessible parts of the strand’s messages so far. The type of“possession” strands is:def
PStr = N −→ P(MSG)

Such possession strands are obtained via a function M2P : MStr → PStr defined by induction:
M2P(s)(0)M2P(s)(i + 1)

= U, a given set of initial possessions (terms)
M2P(s)(i)if s(i) = ⊥





 P M2P(s)(i) ∪ {m}if s(i) = −m=
M2P(s)(i)∪{nonce(n) | newnonce(n)  m} ∪if s(i) = +m
{seckey(n) | newseckey(k)  m}

This requires some explanation: the possessions at stage i+1 are the same as at i if nothing
happens in the message strand s, i.e. if s(i) = ⊥. But if there is an incoming message −m
at i, we extract everything we can from what we already have and from m together. For
instance, if the incoming message is a secret encryption m = k{ m′ } and we alreadypossess seckey(k), then we possess m′ at stage i + 1. Finally, if there is an outgoingmessage at stage i, the plain versions of any new nonces or secret keys in the outgoingmessages are added. The reason for this should become clearer in the next subsection.
We note the following two properties.
• The generated possession strand is increasing, or monotone:i≤j=⇒ M2P(s)(i) ⊆ M2P(s)(j).

A disadvantage of this property is that session keys will always be around, and cannot
be “forgotten”.
• Call a subset X of messages P-closed if P(X) = X. Then:=⇒ M2P(s)(i) is P-closed.

M2P(s)(0) is P-closed

We need to cover two more properties for (message) strands. A strand is called wellformed if it satisfies the following two conditions:8

1. The initial possessions in M2P(s)(0) are “primitive”, i.e. of the form name(a),nonce(n), number(i), seckey(k), pubkey(k) or privkey(k). This means in particular that M2P(s)(0) is P-closed—and hence all other M2P(s)(i) as well. Thiscondition excludes tickets or certificates from initial possessions—which, for the examples in this paper, is not a problem.
2. Each outgoing message s(i) = +m satisfies m ∈ C(M2P(s)(i)). This means that it
can be built from the terms that are possessed at that stage.
Next, a strand may be determined by a protocol rule. Here we shall only consider
elementary rules about message initiation and response. We allow for parametrisation by
stages and sets of messages (possessions) in rules, so that the type of rules is:
defRule = N × P(MSG) −→ P MSG + (MSG × MSG)

Like before, + denotes disjoint union. We then say that a strand s ∈ MStr is rule-based
wrt. rule r ∈ Rule if for each s(i) = +m one has either m ∈ r(i, M2P(s)(i)) or i > 0 ands(i − 1) = −m′ with (m′ , m) ∈ r(i, M2P(s)(i)). In the first case the outgoing message+m is an initiative according to rule r, and in the second case it is a reaction determined
by r.

4.2

Bundles

Bundles are collections of strands, parametrised by agents, including a spy. Recall we used
the type AG for agents, in which we now assume a special element spy ∈ AG. We shalldefine two new types: bundles and bundle constraints, and define what it means that abundle satisfies such a constraint. First, the type of bundles:
Bun

def

=

AG −→ MStr

describes for each agent a message strand. A particular bundle can thus be represented in atable:spy
A1
A2· · · ∈ AG
stage 012..
.

−hm1 , m2 i

+hm1 , m2 i

⊥

+m1
..
.

−m1
..
.

−m1
..
.

This describes a scenario where the tuple message hm1 , m2 i sent by agent A1 at stage 0ends up with the spy. At the next stage the spy replays the first part m1 of this tuple, andboth A1 and A2 receive it.
Bundles involve arbitrary sequences. We want them to satisfy certain restrictions, partly
determined by protocol rules. This is realised via the notion of bundle constraint:
def
BunCst = AG −→ P(MSG) × Rule .

Such a bundle constraint tells for each participant what the initial possessions and the rules
are. It thus specifies a protocol.
The next seven points describe what it means that an arbitrary bundle b ∈ Bun satisfies
a bundle constraint bc ∈ BunCst. Intuitively it says that the bundle b is a combined run for
all participants in the protocol specified by bc.
91. For each agent a ∈ AG, b(a) is a well-formed and rule-based strand with initialpossessions given by π1 (bc(a)) and rule by π2 (bc(a)).
2. At each stage i, if there is activity, there must be a sender: if some b(a)(i) 6= ⊥, thenthere must be an a′ ∈ AG with b(a′ )(i) = +m.
3. There is at most one sender at each stage: if b(a)(i) = +m and b(a′ )(i) = +m′ ,then a = a′ (and hence also m = m′ ).
4. Received messages are plain versions of what is sent: if b(a)(i) = +m and b(a′ )(i) =−m′ , then m′ = n2p(m).
5. The spy receives all messages: if b(a)(i) = +m and a 6= spy, then b(spy)(i) =−n2p(m).
6. New nonces are really fresh: if b(a)(i) = +m and newnonce(n)  m, then foreach a′ ∈ AG, not: nonce(n)  M2P(b(a′ ))(i).
7. New secret keys are also fresh: if b(a)(i) = +m and newseckey(k)  m, thenfor each a′ ∈ AG, not: seckey(k)  M2P(b(a′ ))(i) and also not: k{ m′ } 
M2P(b(a′ ))(i), for some term m′ .
The set of all bundles satisfying a particular constraint/protocol form our model of the
protocol. In the remainder of this section we shall investigate some further properties ofsuch models.
First of all, the standard Dolev-Yao attack model [10] is incorporated, like in strand
spaces. The rules for the spy may further refine these capabilities. But in the basic set
up it is guaranteed only that the spy receives any outgoing message. If no-one else does,
one may understand that the spy has deleted the message. But the spy may also replay themessage, or adapt it—subject to cryptographic constraints as described by the possessions
operators from Subsection 3.2.
Next, we are finally in a position to explain the role of the ‘new’ versions newnonce(n)and newseckey(k) of nonces and secret keys. They can always be included in outgoingmessages m ∈ C(M2P(b(a))(i)), according to the definition of the communication operator C from Subsection 3.3. But the last two of the above constraints require that such ‘new’subterms in outgoing messages should be globally fresh. This is how we realise a global
freshness idealisation. Further, by invoking the n2p functions on the incoming messages
the ‘new’ subterms, if any, are turned into ‘plain’ ones, so that ‘new’ really only occurs
in the first use. It is indeed not hard to see that all sets M2P(b(a))(i) of possessions only
contain plain terms.
An important consequence of the distinction between new and plain nonces (and secretkeys) is that if we have a plain nonce nonce(n)  m as subterm of an outgoing messages(a)(i) = +m, then nonce(n) is already in a’s possession at i—this follows from the laststatement in Subsection 3.3—so that it must be a re-use of n, i.e. so that n must alreadyhave been sent before or in a’s initial possession.
To conclude, we list a number of technical properties that hold for an arbitrary bundleb ∈ Bun satisfying a constraint bc ∈ BunCst.
• All sets of possessions M2P(b(a))(i) are P-closed and only contain plain terms.
• New nonces can only be sent once: if there are two outgoing messages b(a1 )(i1 ) =+m1 and b(a2 )(i2 ) = +m2 which both have the same new nonce newnonce(n) 10m1 and newnonce(n)  m2 as subterm, then a1 = a2 and i1 = i2 , and hence also
m1 = m 2 .
Similarly for new secret keys.
• If we have a subterm m  m1 of an incoming message b(a1 )(i1 ) = −m1 , then there
is an agent a2 and earlier stage i2 ≤ i1 with outgoing message b(a2 )(i2 ) = +m2
containing a “source” subterm m′  m2 where m′ ∈ C(M2P(b(a2 ))(i2 )) satisfies
n2p(m′ ) = m.
• More specifically, if we have a secret encryption k{ m }  m1 of an incoming message b(a1 )(i1 ) = −m1 , then there is an agent a2 and earlier stage i2 ≤ i1 where thesecret key seckey(k) ∈ M2P(b(a2 ))(i2 ) is possessed and where there is an outgoing message b(a2 )(i2 ) = +m2 with a secret encryption k{ m′ }  m2 as subterm,
for which m′ ∈ C(M2P(b(a2 ))(i2 )) satisfies n2p(m′ ) = m.
There is an analogous result for public encryptions.
Via such results we can reason backwards about what happens in bundles, much like in thewell-foundedness arguments used in [31].

4.3

Comparison with strand spaces

The notions of strand and bundle as defined above resemble the notions with the samenames in [31]. The basic idea is: behaviour of each agent is described as a strand; a collection of strands communicating with each other form a bundle. A bundle is a whole system
where communication takes place. However there are also some differences between theoriginal notions and ours. We shall explain these differences here.
In general in a system where communication takes place according to a cryptographic
protocol, there are two different kinds of constraints on the participants’ behaviour, namely
a message rule and a cryptographic ability. In our case every agent that wants to senda message needs to be able to construct the message, e.g. by possessing certain keys or
nonces. This is a crucial part of what we call well-formedness. This restriction only applies explicitly to the spy in the original strand space model. There, strands belonging to
the spy must be instantiations of the several kinds of templates—each corresponding to acryptographic operation which the spy can conduct, such as decryption, encryption, providing a possessed key, etc. These templates are independent of specific protocols. The
strands of legitimate (non-spy) agents must be instantiations of message rules. These rules
must incorporate our well-formedness restrictions. The constraints are thus basically thesame in both models, but organised in a slightly different manner. This is summarised in
the following table.
message rule restricts
cryptographic ability restricts

in original strand space semantics
only legitimate agentsonly spyin our semantics
everybody
everybody

Our formalism is a bit more complicated, because we have to keep track of each agents
possessions at each stage. However, the formalism is more uniform and is thus more suitable for expressing various rules, and for proving their soundness. Additionally, we canuse our formalism as basis for other purposes than analysis of authentication protocols. For
example, in the analysis of anonymity protocols (see e.g. [13]) we often need to prove that acertain agent does not possess some given message. It is not possible in the original strand
space formalism, in which we cannot express legitimate participant’s possessions.
11

A
•

spy
{N1 , A}Kspy

/•
O
(∗) 
•



{N1 , A}KB

{N1 , N2 }KA



•o
•

B

{N2 }Kspy

/•


•

/•
O


{N2 }KB◦{N1 , A}Kspy Decryption/••

Possessed key
•

−1
Kspy

where (∗) is

/ •

/ •


N1 , A

Encryption/•

Possessed key
•

KB

/ •

•

{N1 , A}KB



•

/◦

Figure 1: Lowe’s attack in the formalism of [31]
Time
0
1
2
3
4

A’s MStr+{ newnonce(N1 ), A }Kspy⊥−{ N1 , N2 }KA+{ N2 }Kspy⊥

B’s MStr⊥−{ N1 , A }KB+{ N1 , newnonce(N2 ) }KA⊥−{ N2 }KB

spy’s MStr−{ N1 , A }Kspy+{ N1 , A }KB−{ N1 , N2 }KA−{ N2 }Kspy+{ N2 }KB

Figure 2: Lowe’s attack in our formalism
As illustration Lowe’s attack [21] on the Needham-Schroeder protocol (see Section 2)
is presented in the original strand space formalism in Figure 1, and in our formalism inFigure 2. In the latter we have written Ni for nonce(Ni ) in order to save space. Also
we leave the possession strands implicit. Observe that in Figure 1, strands for legitimate
agents embody message rules while those for the spy embody cryptographic operations.
These constraints are implicitly imposed on every agent in Figure 2 as the well-formedness
requirement.
The asynchronous nature of the network—messages can arrive delayed or in a different
order—is obvious in the original strand space formalism since it does not have a global
timing (or stages). In our formalism it is modelled using the spy: for example a delayed
message is first received only by the spy and later sent by the spy to the intended recipient.

5 Logical formulas and rules for protocols
In this section we put a layer of abstraction on the model that was introduced in the previous
section by defining appropriate logical formulas that capture essential aspects of the model.
As we emphasised in the beginning our “logic” is interpreted and consists of a number of12definitions and operations for formulas, together with a suitable collection of implications(rules) between them. We refrain at this stage from formulating a proper syntactic logic
with a derivation relation because: (1) we think that the set of rules is not sufficiently
stable yet, and that further applications of this framework may lead to refinements and/or
additions; and (2) for the verification work in a theorem prover it is unnecessary—eveninconvenient—to have a purely syntactic logic.
The formulas that we shall consider below are atomic formulas of the form:A Possesses m A Sends m A Says m A Receives m
Secret(A)(m) Secret(A, B)(m)and compound formulas of the form:¬ϕ ϕ1 ∧ ϕ2

∀x ∈ X. ϕHenceForth ϕA Knows ϕwhere ϕ, ϕi are formulas.
These formulas, in interpreted form, are special predicates on our model. They take abundle constraint bc ∈ BunCst, a bundle b ∈ Bun satisfying bc, and a number (or stage)i ∈ N to true or false. In order to describe the type of formulas we introduce the notation[bc] for the set of bundles that satisfy the bundle constraint bc. Then:

Y 
def
[bc] × N → bool
Form =
bc∈BunCst

Q

Heredenotes a dependent product. We shall write Greek letters ϕ, ψ, . . . for formulas.
The usual logical operations are extended to such formulas via pointwise definitions, as in:
ϕ1 ∧ ϕ2 (bc, b, i)∀x ∈ X. ϕ(x) (bc, b, i)def=

ϕ1 (bc, b, i) ∧ ϕ2 (bc, b, i)def=∀x ∈ X. ϕ(x)(bc, b, i).

The (linear) temporal operator HenceForth − —sometimes written as —is defined in
the obvious way, namely as:HenceForth ϕ (bc, b, i)def=∀j ≥ i. ϕ(bc, b, j).

The epistemic “knowledge” operator will be described separately in Subsection 5.4. Veryoften the bundle (constraint) arguments bc and b remain the same and there is only variationin the stage argument i. Therefore it makes sense to leave bc and b implicit,
and write ϕ@i
for ϕ(bc, b, i). The temporal operator then says that HenceForth ϕ @ i is ϕ@j for allj ≥ i. This @-notation was already used informally in Section 2.

5.1

Basic formulas and rules

Next we introduce some of the basic formulas about possession, sending, seeing etc. Throughout we shall use variables A ∈ AG and m ∈ MSG for agents and messages.

A Possesses m (bc, b, i)def=m ∈ M2P(b(A))(i)This says that agent A possesses message m if m can be extracted from A’s messages up-toi. Notice that we are careful to talk about “possession” and not “knowledge” of messages,
because “knowledge” is reserved for use with the epistemic operator from Subsection 5.4.

13


As we noted in Section 4, M2P
 is monotone, so the implication A Possesses m ⇒HenceForth A Possesses m holds. Hence the following rule is sound.

A Possesses mHenceForth A Possesses m

Since M2P yields P-closed subsets of terms we also have the following four closure rules.

A Possesses k{ m }A Possesses seckey(k)A Possesses m
A Possesses { m }k
A Possesses privkey(k)A Possesses m
A Possesses hm1 , m2 i
A Possesses hm1 , m2 i
A Possesses m1
A Possesses m2

Our next formulas are about sending.
A Sends m (bc, b, i)A Says m (bc, b, i)def=b(A)(i) = +mdef∃m′ ∈ MSG. m  m′ ∧ A Sends m′ (bc, b, i)∧ m ∈ C(M2P(b(A))(i))=

Agent A thus “says” a message m if m is a subterm of an outgoing message and m itself
can be constructed. Here are some obvious rules.
A Sends mA Says mA Says newnonce(n) @ iA Possess nonce(n) @ i + 1A Says newnonce(n) @ i B Says newnonce(n) @ j
A=B ∧ i=j

There are analogous rules for newseckey(k) in place of newnonce(n).
Now we turn to receiving messages.

A Receives m (bc, b, i)A Sees m (bc, b, i)def=b(A)(i) = −mdef

i > 0 ∧ A Possesses m (bc, b, i)∧¬ A Possesses m (bc, b, i − 1) ∧∃j, m′ . j < i ∧ A Receives m′ (bc, b, j) ∧ m  m′=

The notion is “seeing” is a bit complicated: A sees a message m at stage i if m is a subtermof an earlier incoming message and is only now (i.e. at stage i and not earlier) accessible.
The last line of its definition rules out, for example, that m is a nonce freshly generated by
A at i − 1. Then:
A Possesses seckey(k)A Possesses m
A Possesses mA Sees k{ m } @ i∃B, m′ , j ≤ i. n2p(m′ ) = m ∧ B Says m′ @ j ∧ B Possess seckey(k) @ j
A Sees m
A Sees k{ m }14There are similar rules for public encryptions.
Finally we have secrecy formulas, in twofold, namely in shared form (for two agents)
and un-shared form (for a single agent). We use overloading and give them the same name.
Secret(A)(m) (bc, b, i)defA Possesses m (bc, b, i) ∧∀X, j ≤ i. X Possesses m (bc, b, j) ⇒ X = A
Secret(A, B)(m) (bc, b, i)def= A Possesses m (bc, b, i) ∧ B Possessesm (bc, b, i) ∧∀X, j ≤ i. X Possesses m (bc, b, j) ⇒ X = A ∨ X = B=

The definition can easily be extended to multiple (more than two) agents. Associated rules
appear in Subsection 5.3.

5.2

Rules for authentication

We present some logical rules by which we can draw authentication conclusions: fromwhat an agent A observes, A can be sure that a certain action has been actually done bya specific agent B. Even in the presence of the Dolev-Yao adversary that controls all the
traffic in the network, we can establish authentication with the help of cryptography.
The rules in this section—together with the strengthened ones later in Section 7—are to
our semantics what the authentication tests [16, 9] are to the strand space formalism [31].
Authentication properties often involve the most complex proofs among various security
goals. Since the strand space formalism is independent of specific protocols, it is possible
to establish generic “lemmas” about strand spaces which, via suitable instantiations, help us
to prove authentication properties of various protocols. The proofs of these generic lemmas
are quite complicated, as one observes in [16, 9]. However, the task of proving theselemmas is like giving complicated authentication proofs once for (almost) all protocols.
That is the virtue of having “authentication tests” for the strand space formalism. The
logical rules we shall introduce are useful in the very same sense.
The typical case we wish to consider is when an agent A first sends out a new nonce
under encryption with another agent B’s public key, and then sees its own nonce backin unencrypted form. This forms a so-called outgoing authentication test in [16]. The
desired conclusion is then that B must have seen the nonce, together with whatever was
also included in the encryption, because only B could have decrypted the relevant message.
Making all this precise turns out to be quite subtle.
The rule that we have is too large to fit on one line, so that we describe it with labels as
follows.
“A sends at j” “A sees at i ≥ j”

“A doesn’t say after j” “B’s privkey secret until i”∃j1 . j < j1 ≤ i ∧ “B sees at j1 ” ∧ ∃j2 , C. j1 ≤ j2 ≤ i ∧ “C 6= A sends”
The meaning of the assumptions in this rule will be explained first.
• “A sends at j” means that
 A sends a public-encrypted new nonce as a subterm.
Formally: A Sends m @ j with { newnonce(n), m1 }k  m, together with therequirement that the nonce occurs only once in the outgoing message: nonce(n) 1n2p(m).
• “A sees at i ≥ j” is used as abbreviation for: A Sees m2 @ i where i ≥ j andnot: nonce(n) pe(k) m2 . The latter says that the nonce n has in m2 an occurrence
15which is outside an encryption by k; it requires a subtle addition to exclude a trivial
cases, namely when m2 is the tuple hnonce(n), n2p(m1 )i.
• “A doesn’t say after j” means not: A Says nonce(n) @ j ′ , for any j ′ with j <j ′ ≤ i. Indeed, the nonce n at stake should not be used again by A, so that when it
re-appears it must indeed have been decrypted.
• “B’s privkey secret until i” expresses the crucial assumption that B is the only one
that possesses the private key associated with k, i.e. Secret(B)(privkey(k)) @ i′ forall i′ ≤ i.
The rule’s conclusions then have the following meaning.
• “B sees at j1 ” means B Sees hnonce(n), n2p(m1 )i @ j1 and expresses that B
must have seen the encrypted tuple—because it is the only agent that could havedecrypted the tuple.
• “C 6= A sends” finally means C 6= A ∧ C Sends m3 @ j2 for some message m3
with n2p(m3 ) = m2 . One might have expected that B must also have been the onethat sent the incoming message m2 of A, but that is not guaranteed: B could havepassed the nonce n on to some other agent C who uses it for the message seen by A.
Proving the soundness of this rule is a tour de force, and involves many case distinctions. The main steps are as follows.
1. The incoming term m2 must come from some agent, say C. We know that C is not
A, because A does not “say” n.
2. The nonce n must occur unencrypted in C’s possessions, because of the last property
mentioned in Subsection 3.3.
3. Now we use well-foundedness to find the first stage, say j1 , where an agent, say A′ ,different from A possesses n in unencrypted form.
4. By a non-trivial induction proof we establish that up-to j1 the nonce n can only occur
encrypted under k.
5. Because B is the only agent with the decryption key, we must have A′ = B, using
property 1. mentioned at the end of Subsection 3.2.
There is a similar rule in which nonce(n) and newnonce(n) are replaced by seckey(k)and newseckey(k): a freshly generated secret key can play the role of a nonce as a random
value. But there also is a more useful variation, in which the secret key k does not re-appear
as subterm of the incoming message but as (secret) encryption key in a cipher text k{ m }.
We shall see such an example in Section 6.

5.3

Rules for secrecy

Among the many possible rules for secrecy we shall consider the case where two agents
A1 , A2 only exchange a nonce under each other’s public keys k1 , k2 respectively. In labeledform this rule looks as follows.
“A1 sends new n at j ≤ i”

“A1 , A2 send n only encrypted” “A1 , A2 key secrecy”
B Possess nonce(n) @ i =⇒ B = A1 ∨ B = A2
(1)
The conclusion speaks for itself, so we only explain the three assumptions.
16• “A1 sends new n at j ≤ i” means A1 Says newnonce(n) @ j for j ≤ i.

• “A1 , A2 send n only encrypted” expresses that for j ′ with j ≤ j ′ ≤ i the nonce
n is sent by A1 at j ′ only under A2 ’s public key k2 , and vice-versa. Formally, if
A1 Sends m @ j ′ then nonce(n) pe(k2 ) m, and similarly for A2 .

• “A1 , A2 key secrecy” expresses that agents A1 and A2 both keep their own private
keys secret: Secret(Ap )(privkey(kp )) @ i′ for p ∈ {1, 2} and i′ ≤ i.

There are similar secrecy rules possible where a nonce or secret key is only sent undersecret encryptions, or even under both public and secret encryptions.

5.4

Knowledge of formulas

In order to define knowledge we keep our bundle constraint bc ∈ BunCst fixed, but consider different bundles that satisfy the constraint. Recall that we write [bc] for the set ofA,isuch bundles. We define a collection of equivalence relations ∼ ⊆ [bc] × [bc], for A ∈ AG
and i ∈ N as follows.
A,ib ∼ b′

def=∀j ≤ i. b(A)(j) = b′ (A)(j).

This means that up-to stage i the strands of A are the same in b and b′ . We then define,much like in [29],A Knows ϕ (bc, b, i)

def

=

A,i

∀b′ ∈ [bc]. b ∼ b′ ⇒ ϕ(bc, b′ , i).

The intuition behind this definition is the following. At stage i in bundle b an agent A only
has information about its own incoming and outgoing message so far, i.e. about b(A)(j)for j ≤ i. If ϕ holds in all possible scenarios b′ that agree with b on these incoming
and outgoing messages of A, then ϕ can in fact only depend on these messages (because
everything else may differ in the various scenarios), and so A has all the information toknow ϕ.
Typically in verifications, if we can prove an implication
ϕ1 ∧ · · · ∧ ϕn ⇒ ψ and theassumptions ϕi are of the the form A Sends − , A Sees − or AKnows − , only
involving agent A, then one can prove ϕ1 ∧ · · · ∧ ϕn ⇒ A Knows ψ , since the result ψ
only depends on A’s perspective. The next section contains several such examples.
Because the relations ∼ are equivalence relations we have the familiar associated “S5”modal rules (see e.g. [14, 2]), including for instance:
A Knows ϕ
A Knows ϕ A Knows ψ
A Knows ϕ======================
A Knows ϕ ∧ ψ
A Knows A Knows ϕϕwhere the double line means that the rule may be used in both directions.

6 The bilateral key exchange example
In this section we apply the theories from the previous section to a standard protocol, theso-called bilateral key exchange (BKE), described in [5, §§6.6.6]. Our aim is to establish17

an authentication result in the form of a shared secret key (the K below). The protocol
involves the following steps.
A −→ BB −→ AA −→ B:::A, { nA , A }KB{ K, hash(nA ), nB , B }KA
K{ hash(nB ) }(2)

The protocol is an interesting verification challenge because of 1) the combination of public
and secret encryption (with a fresh session key K), and 2) the hashed versions of nonces
are used as proof of possession of the original nonces. 3
We shall first consider the representation of this protocol in our framework, and thendiscuss some interesting statements about the protocol (and a sketch of their proofs).

6.1

Representation of the BKE protocol

We build a concrete model of bundles that incorporates the BKE protocol. As agents
we take the set/type AG = {A, B, S} for Alice, Bob and the Spy, with corresponding
public keys KA , KB , KS , that are (pairwise) different. We assume three nonce functions
NA , NB , NS , so that at each stage i we have a fresh nonce newnonce(NA (i)) for Alice(and similarly for Bob and the Spy). We assume that:i 6= j ⇒ NA (i) 6= NA (j)NA (i) 6= NB (j)etc.

Further we need a function SK(−) so that Bob can at each stage take a different session
key SK(i).
The initial possessions of our three agents are given as the following sets of messages.
PA
PB
PS

= { pubkey(KA ), privkey(KA ), pubkey(KB ), pubkey(KS ) }= { pubkey(KA ), pubkey(KB ), privkey(KB ), pubkey(KS ) }= { pubkey(KA ), pubkey(KB ), pubkey(KS ), privkey(KS ) }.

Hence at stage 0 they possess their own public and private key, and each others publickeys.
Recall that a rule is a function N × P(MSG) −→ P MSG + (MSG × MSG) that
restricts the sending of messages. For the spy we impose no restrictions via (message)
rules, so that its rule is:rS (i, U )= {z ∈ MSG + (MSG × MSG) | true}.

Hence rule-basedness does not restrict the spy’s strand. Note that, however, well-formedness
does restrict: the spy can send any message, as long as the spy can (cryptographically) construct the message.
The rules for Alice and Bob correspond to the protocol rules (2) from the beginning of thissection. Alice has both an initiator rule (for spontaneously sending A, { nA , A }KB ) and a
responder rule (for the final message K{ hash(nB ) }). We formalise this as follows.
rA (i, U )= {hname(A), { newnonce(NA (i)), name(A) }KX i | X ∈ AG, X 6= A}∪{ ( { seckey(K), hash(nonce(NA (j))), nonce(n), name(X) }KA ,K{ hash(nonce(n)) } )| j < i ∧ X 6= A ∧ nonce(n) 6∈ U ∧ seckey(K) 6∈ U }.

(3)

3 Most probably taking hash values is not necessary to establish security properties. However our aim here isto prove that the original protocol in the literature [5], even if it involves hashes, provides the desired properties.

18

This rule thus says that A may at any stage i send the BKE protocol’s first message
hname(A), { newnonce(NA (i)), name(A) }KX i, in which the newly generated nonce
NA (i) is encrypted with another agent X’s public key. Notice that the protocol description (2) prescribes that the first message should be sent to B, but this is misleading since A
does not know for sure that B can be trusted, i.e. is not the spy. Hence we should leave thisopen by using a variable X. This enables the spy to participate as player in the protocol. In
A’s strand multiple runs of the protocol can be initiated; in each of the runs either B or the
spy can be a responder.
The second part of the rule (after the union ∪) describes the reaction: if A gets a message of the form { seckey(K), hash(nonce(NA (j))), nonce(n), name(X) }KA wherej < i, X 6= A and both nonce(n) and seckey(K) are not already in A’s possession, thenA replies by sending out the message K{ hash(nonce(n)) } that is built from the incoming nonce and key. The condition that neither nonce(n) nor seckey(K) is possessed yet
is included to prevent replays, and is actually used in the proof of security properties. It isneeded because our formalisation does not have an explicit notion of run. A consequenceis that a rule can be applied repeatedly resulting in different continuations. In the BKE protocol for instance, having sent the first message with nonce nA Alice may reply to different
pairs K, nB for this same nonce.
We turn to Bob’s rule. It only involves a reaction:rB (i, U )= { ( hname(X), { nonce(n), name(X) }KB i,{ newseckey(SK(i)), hash(nonce(n)), newnonce(NB (i)), name(B) }KX )| X 6= B ∧ nonce(n) 6∈ U }.
Hence if B receives a message of the form hname(X), { nonce(n), name(X) }KB i where
nonce(n) is not already possessed and X 6= B, then B responds by picking both a fresh
nonce NB (i) and a session key SK(i), and including them in the encrypted response message { newseckey(SK(i)), hash(nonce(n)), newnonce(NB (i)), name(B) }KX , using
the public key of the agent X that occurs in the incoming message.
We see that the representation of the BKE protocol basically follows the informal description (2), but requires that certain implicit assumptions (about the targets of messages
or the freshness of incoming nonces and keys) are made explicit.
It must be noted that in the above representation Alice always plays a role of an initiator
and Bob is always a responder. This design choice is made to ease our PVS formalization
work, although it must be straightforward to allow principals to play multiple roles.
Formally, the above initial possessions and rules form a bundle constraint BKE ∈BunCst, like in Subsection 4.2. The properties that we shall establish below hold foran arbitrary bundle b ∈ Bun satisfying the constraint BKE.

6.2

BKE properties

Once the protocol is represented appropriately, the verification can start. Below we shallsketch some of the secrecy properties that have been proven.
First of all we establish that A and B keep their private keys secret: for each i,
Secret(A)(privkey(KA )) @ i

andSecret(B)(privkey(KB )) @ i

Here we use a secrecy rule that says: if a private key is never sent out then it remains secret.

19

The rule is part of the PVS specification. Next we haveA Sends hname(A), { newnonce(NA (i)), name(A) }KB i @ i∧
X Possess nonce(NA (i)) @ j ∨ X Possess hash(nonce(NA (i))) @ j=⇒
X=A∨X=B
This follows from the secrecy rules in Subsection 5.3. There is a similar implication for B
with his session key:
B Sends { newseckey(SK(i)), hash(nonce(n)),
newnonce(NB (i)),

name(B) }KA @ i∧
X Possess seckey(SK(i)) @ j=⇒
X=A∨X=B
We are not so interested in B’s newnonce NB (i) because it plays a minor role in the protocol. In fact, it could be replaced by a constant.
After these preparatory results, we first concentrate on A’s perspective. Assume for a
moment both:A Sends hname(A), { newnonce(nA ), name(A) }KB i @ i∧A Sees { seckey(K), hash(nonce(nA )), nonce(nB ), name(B) }KA @ i + j

Then we can prove the following results.
1. nA = NA (i) and j > 0.


2. HenceForth Secret(A, B)(nonce(nA )) @ i + j.

3. A Knows − of the previous result, i.e.

A Knows HenceForth Secret(A, B)(nonce(nA )) @ i + j.

4. ∃j ′ . j ′ ≤ j ∧ B Sends { newseckey(K), hash(nonce(nA )), newnonce(nB ),
name(B) }KA @ i + j ′ .

5. A Knows − of the previous result.

6. HenceForth Secret(A, B)(seckey(K)) @ i + j.

7. A Knows − of the previous result.

Next we turn to Bob’s perspective, and assume the following two formulas.


B Sends { newseckey(K), hash(nonce(n)), newnonce(nB ), name(B) }KA @ i∧
B Sees K{ hash(nB ) } @ i + j

Now we can prove:

1. nB = NB (i) and k = SK(i) and j > 0.
20


2. HenceForth Secret(A, B)(seckey(K)) @ i + j.

3. B Knows − of the previous result.

4. ∃j ′ . j ′ ≤ j ∧ A Sends K{ hash(nB ) } @ i + j ′ .

5. B Knows − of the previous result.

6. ∃j ′ . j ′ ≤ j ∧ A Sees { seckey(K), hash(nonce(n)),
nonce(nB ),
′
name(B) }KA @ i + j .

7. B Knows − of the previous result.

The two strongest results we have arise by combining assumptions for A and B, interms of knowledge about what the other agent sends or sees.
A Sends hname(A), { newnonce(nA ), name(A) }KB i @ i∧A Sees { seckey(K), hash(nonce(nA )), nonce(nB ), name(B) }KA @ i + j∧A Knows B Sees K{ hash(nB ) } @ i + j + k=⇒A Knows B Knows HenceForth Secret(A, B)(seckey(K))@i + j + k

In this case it is thus assumed that A knows that B sees the final message. In a dual sense,
if B knows that A sent the initial message, we can also obtain a similarly strong secrecy
result.

B Knows A Sends hname(A), { newnonce(nA ), name(A) }KB i @ i∧B Sends { newseckey(K), hash(nonce(n)), newnonce(nB ), name(B) }KA @ i + j∧B Sees K{ hash(nB ) } @ i + j + k=⇒B Knows A Knows HenceForth Secret(A, B)(seckey(K))@i + j + k

These two conclusions are beginning to look like common knowledge (see e.g. [12]). They
provide a basis for authentication.

7 Logic strengthened for the Otway-Rees
The Otway-Rees key distribution protocol [25] is another well-known target in verification
work. There is a substantial gap between Otway-Rees and, say, Needham-Schroeder or
BKE, with respect to verification: this is due to the presence of tickets. We cope with thisnew challenge by strengthening the logic that we have already introduced. We will see that
this improvement is comparable to the introduction of honest ideals [15] in the strand spaceformalism.
We apply the stronger logical rules to the Otway-Rees protocol to verify its key establishment properties. Additionally, we will observe that an attack presented in [31]—which
can happen in the strand space formalism—is impossible in our formalism. This is due toa difference in nonce management between the two formalisms, exploiting that we keep
track of agents’ possessions.
21

7.1

Verification challenge in the Otway-Rees protocol

The goal of the Otway-Rees protocol is key-distribution: an initiator A and a responder B
aim to establish a session key Ks with the help of a trusted server S. It is assumed thateach of A and B has already established a shared long-term secret key KAS and KBS with
S. The protocol is informally described as follows.
A −→ BB −→ S
S −→ BB −→ A::::n, A, B, KAS { nA , n, A, B }n, A, B, KAS { nA , n, A, B }, KBS { nB , n, A, B }n, KAS { nA , Ks }, KBS { nB , Ks }n, KAS { nA , Ks }(4)

Here n and nA are nonces freshly generated by A, nB is a fresh nonce by B, and Ks
is a fresh session key generated by S. Recall that the notation K{ m } is for symmetricencryption.
A major difference from the Needham-Schroeder or BKE protocol is the existence oftickets: a ticket is a subterm of a received message which an agent does not look inside andjust passes on to another agent. In the above run of Otway-Rees there are two tickets for
B, namely KAS { nA , n, A, B } and KAS { nA , Ks }. Roughly speaking, the responder B
can send a message containing any ticket t after B receives the message n, A, B, t. It is
not supposed (or possible either) for B to check whether a ticket t is of the expected form
KAS { nA , n, A, B }.
Because of tickets, validity of assumptions of most rules in Section 5 are now nontrivial. Hence those rules—although they are still sound—are of little use. For example
consider the following secrecy rule (1) in Section 5.3, adapted to the current situation.
“B sends new nB at j ≤ i, encrypted by KBS ”“KBS is kept secret by B, S”`´
C Possess nonce(nB ) @ i“B, S send nB only encrypted by KBS ”=⇒

C=B∨C=S(5)

We cannot use this rule to derive secrecy of nonce nB in the above run (4). Since B is
supposed to send anything he receives as a ticket, validness of the second assumption is
now questioned.
In this section we shall introduce stronger rules which have weaker premises. These
weakened premises are trivially valid even for protocols involving tickets. For example, analternative for the above secrecy rule is as follows.
“B sends new nB at j ≤ i, encrypted by KBS ”“KBS is kept secret by B, S”`´
C Possess nonce(nB ) @ i“B, S maintain encryption of nB by KBS ”=⇒

C=B∨C=S(6)

The new second assumption “B, S maintain encryption of nB by KBS ” means: if B or S
ever sends a message in which nB appears without encryption, then the agent must havereceived nB in a non-encrypted form. This condition is verified easily in the Otway-Rees
protocol: if nB appears not encrypted in a message sent by B, then that must be in a ticket
which is received by B beforehand. Hence we can conclude secrecy of the nonce nB .
This challenge caused by tickets is implicit in [31]. Our way of coping with the challenge can be compared to the one taken there, using the notion of honest ideals. The
fundamental Theorem 6.11 of [31] about honest ideals essentially proves that the three assumptions of our stronger rule (6) yield the second assumption of our weaker rule (5). In
this sense, our strengthening of logical rules in this section corresponds to the introductionof honest ideals like in [15] or [31, Section 6].
22

7.2

New formulas

Due to the presence of tickets, we now have to take a closer look at an agent A’s actionof sending: is A just passing a message it has received as a ticket, or is she actually operating on a message e.g. by decrypting an encryption therein? For this distinction we
introduce two new basic formulas OriginatorOf and DecryptSends which are essentiallyrefinements of Sends.
The formula A OriginatorOf m roughly says that m is a part of the sent message but
not a part of any messages received before. Formally,
A OriginatorOf (m) (bc, b, i)def= ∃m1 ∈ MSG. A Sends m1 @ i ∧ m  n2p(m1 )∧ ∀j ∈ N. ∀m2 ∈ MSG. (j ≤ i ∧ A Receives m2 @ j =⇒ m 6 m2 )For example, in the Otway-Rees protocol B OriginatorOf KAS { nA , Ks } is false since
if B sends a message of that form it must be a ticket received before. We can prove thefollowing lemma (or logical rule):(O RI S AYS ) OriginatorOf implies Says.
A OriginatorOf m @ i=⇒ ∃m′ ∈ MSG. A Says m′ @ i ∧ m = n2p(m′ )The label (O RI S AYS) will be used later in Appendix B.
For an arbitrary set K of keys, the intuitive meaning of a formula A DecryptSends (m, K)
is that A decrypts an encryption (by a key from a set K) of m and sends m. A typical example of m is a nonce. Formally,
A DecryptSends (m, K) (bc, b, i)= ∃m1 ∈ MSG. A Sends m1 @ i ∧ m  n2p(m1 ) ∧ m 6K n2p(m1 )∧ ∀j ∈ N. ∀m2 ∈ MSG. (j ≤ i ∧ A Receives m2 @ j =⇒ m K m2 )def

Recall that m K m′ means: every occurrence of m in m′ is under encryption by somekey in K. Hence m 6K m′ means that there is at least one occurrence of m in m′ without
encryption by any key from K. Therefore the condition m  n2p(m1 ) above is in fact
redundant (but still there for the ease of understanding).

7.3

Strengthened logical rules

We shall present two strengthened logical rules which play crucial roles in the verificationof Otway-Rees. Their soundness against our semantics is proved in PVS. Other rules which
are less significant are presented in Appendix A.
Our first rule is for authentication and called incoming authentication test: the name ischosen after the corresponding lemma [16] for the strand space formalism.
(I NC T EST ) Incoming
 authentication test. A is a set of agents.
1.
Challenge
 A Sends mc @ ic ∧ newnonce(n)  mc∧
2.
Response
A Sees mr @ ic + iw ∧ nonce(n) K{ m1 }  mr
∧
3. K{ m1 } does not originate from A herself∀j ∈ [ic , ic + iw ].  ¬(A OriginatorOf K{ m1 } @ j)
∧4.
K
is secretly shared∀j ∈ N. Secret(A)(K) @ j=⇒Authentication result∃B ∈ A \ {A}. ∃j ∈ (ic , ic + iw ). B OriginatorOf K{ m1 } @ j
23

The basic idea is a common challenge-response style authentication. The random value
nonce(n) is not encrypted in the form of K{ m1 } in the (outgoing) challenge, because of
the assumption 3: in particular,¬(A OriginatorOf K{ m1 } @ ic )Note that nonce(n)  m1 by the assumption 2. However at stage ir , A receives an (incoming) response which contains K{ m1 }. This so-called challenge component K{ m1 } must
originate from someone who possesses the key K, hence someone in A by the assumption
4. By the assumption 3 it must not be A herself. Moreover, the creation of K{ m1 } must
be after the creation of nonce(n). This is an incoming test because the incoming response
involves particular encryption.
It is straightforward to get a variation of this rule in which nonce(n) and newnonce(n)are replaced by seckey(Ks ) and newseckey(Ks ). Less straightforward is a rule for outgoing authentication test [16]—where a nonce is encrypted in the outgoing challenge but
not in the incoming response. We have the rule in the PVS specification [20] but it is not
used for the verification of Otway-Rees.
Compared to the similar authentication rule earlier in Section 5.2, the third assumption
is weakened from “A does not say K{ m1 }”—which is not trivially valid in Otway-Rees
due to tickets—to “K{ m1 } does not originate from A”.
Our second strengthened rule is a secrecy rule corresponding to the above (6). For
future reference we present a rule for secrecy of a freshly generated key: the corresponding
rule for secrecy of a nonce is similar.
(SKSEC )∧∧=⇒Secrecy of session keys encrypted with uncompromised keys.
 A is a set of agents and K is a set of keys.
1. Long-term keys are kept secret∀j ≤ i. ∀Kl ∈ K. ∀A ∈ A. A Possess
Kl @ j =⇒ A ∈ A
2. Legitimate parties keep encryptions
∀j ∈ [i0 , i]. ∀A ∈ A. ¬  A DecryptSends ( seckey(Ks ), K ) @ j
3. Generation of session key
i0 ≤ i ∧ A0 ∈ A ∧ A0 Says newseckey(Ks ) @ i0Secrecy result ∀A ∈ A. A Possess Ks @ i =⇒ A ∈ A

As explained in Section 7.1, assumption 2 is weaker than the corresponding condition“agents in A send Ks only encrypted by a key in K”. This is crucial for the rule to beusable for Otway-Rees.

7.4

Verification of the Otway-Rees protocol

Now we shall see that the refined rules are appropriately adapted to the Otway-Rees protocol and to other protocols that make similar use of tickets. Since the Otway-Rees protocol
is aimed at key-distribution, we want to establish the following security properties.
• Secrecy of the session key Ks : Ks is known only by the legitimate agents A, B, andby the server S.
• Freshness of Ks : Ks was generated recently by S, say “after B sent the message. . . ”. (Algorithmic) cryptology says that the more data a key is used to encrypt, themore likely the key gets compromised by cryptanalysis. This type of attacks via
cryptanalysis are not present in the Dolev-Yao model, hence not in our semantics
nor in the strand space formalism [31]. Nevertheless, freshness of a session key issufficient to mitigate those risks [17].
24• Agreement on Ks : B knows, after his run of the protocol as a responder, that A wasalso running the protocol as an initiator with the same data items; in particular A has
obtained the same session key. This is B’s guarantee on agreement, and we can state
A’s guarantee in a similar manner.
As a showcase, in Appendix B we sketch the derivation (in PVS) of B’s guarantee of thefirst two properties. Namely:
B Sends n, A, B, t1 , KBS { newnonce(nB ), n, A, B } @ i∧
B Sees K#" BS { nB , Ks } @ i + jHenceForth ¬ (spy Possesses Ks ) @ i + j∧@i + j=⇒ B knows∃k ∈ [i, i + j]. S Says newseckey(Ks ) @ k(7)
In this formula t1 is an arbitrary message. The proof of this secrecy property is rather
complicated because it involves authentication in the following way. The secrecy is easy
if the session key is issued by the legitimate server S under proper encryptions. The hardpart is that B must be sure this is indeed the case. The guarantee for A is proved similarly.
The third property of agreement on distributed keys is the main topic below.

7.5

Prevention of certain replay attacks

There is an attack on the Otway-Rees protocol presented in [31] which distributes different
session keys to A and B by replaying a request to S. Due to this attack the agreementof session keys fails for Otway-Rees. Here spyX denotes the intruder impersonating a
legitimate agent X.
A→B:
B → spyS :spyB → S :S→B:
B → spyA :spyB → S :S → spyB :spyB → A :n, A, B, KAS { nA , n, A, B }n, A, B, KAS { nA , n, A, B }, KBS { nB , n, A, B }n, A, B, KAS { nA , n, A, B }, KBS { nB , n, A, B }n, KAS { nA , Ks }, KBS { nB , Ks }n, KAS { nA , Ks }n, A, B, KAS { nA , n, A, B }, KBS { nB , n, A, B }n, KAS { nA , Ks′ }, KBS { nB , Ks′ }n, KAS { nA , Ks′ }(8)

We emphasise that this attack (possible in the original strand space model) is no longer
possible in our semantics. In fact we have proved in PVS A’s guarantee on agreement ofsession keys.
∧
∧
∧
∧
=⇒

i0 ≤ i1 ≤ `i2 ≤ i3´
A Sends “newnonce(n), A, B, KAS { newnonce(nA ), newnonce(n),A, B } @ i0”`´
A Knows B Sends n, A, B, t1 , KBS { newnonce(nB ), n, A, B } @ i1`´
A Knows B Sees KBS { nB , Ks } @ i2
A Sees KAS { nA , Ks′ }`@ i3`´´
Ks = Ks′ ∧ A Knows HenceForth Secret({A, B, S})(Ks ) @ i3
(9)It states: if A has properly finished her role in a run and if A somehow knows that B has
also finished his role with the matching nonce n (which acts as an identifier of the run),25

then A is sure that the distributed session keys agree. The guarantee for B is formulated ina similar way and proved in PVS.
How does this difference arise? In our semantics, the server S keeps track of all thenonces to prevent replays. In particular, S stores among its possessions all n’s (identifiersof runs) in the requests, and S does not react to a request containing a nonce n which S
has ever seen. This is part of our formalisation of Otway-Rees—which is done in a similar
way to (3) for BKE. The additional feature of our semantics prevents the 7th message ofthe above attack (8) from being sent.
This feature is possible in our semantics because each agent has exactly one “strand”(with corresponding possessions), in which it can interleave multiple runs of the protocol.
It is not the case in the original strand space formalism: there an agent can have multiple
strands, each of which corresponds to the agent’s role in a single run. There is no mechanism which allows different strands to communicate with each other, or to share a single“memory”. In this sense, in the strand space formalism an agent is “multi-threaded”, as
opposed to the single-threaded model in our semantics. Actual implementation determines
which semantics is more appropriate, hence enables/disables certain attacks such as (8).
This issue of an agent’s inter-thread memory is studied in [18] where a translation is introduced from strand spaces to what they call strand systems. Strand systems are similar toour semantics: notably they allow multiple runs of a single agent to share a memory.
Our model of nonce management can be implemented by including a timestamp as apart of a nonce: we can fix a certain time span within which S keeps track of nonces, andS responds only to nonces with timestamps in that span.

8 Conclusions and further work
We have achieved a unification in the area of security protocols by combining the best of
several approaches [31, 4, 27, 29], namely a tool-supported sound logic. It is a further intellectual challenge to include process-based approaches (such as [1]) within this semanticalframework.
More practically-oriented further work lies in the application of this approach to other,more complex protocols, and to other properties than secrecy. This is ongoing work, that
may require adaptation and/or extension of the current semantics. Once a stable and useful
set of (semantic) rules has been identified, one may use it to formulate a proper (syntactic)
logic for security protocols. Another line of work, possibly more suitable, is to use thisformalised framework mainly to establish soundness of logical rules and to perform actual
verifications with more automatic tools.
As mentioned in Section 4.3, formal analysis of other security properties such as anonymity is another possible direction of the further research. We may re-use the current PVS
infrastructure there.

Acknowledgements
Thanks are due to Erik Poll and Martijn Warnier for helpful comments and discussions,and also to the referees for their constructive remarks and suggestions.

26

References[1] M. Abadi and A. Gordon. A calculus for cryptographic protocols. Journ. ACM,
148(1):1–70, 1999.
[2] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Number 53 in Tracts in
Theor. Comp. Sci. Cambridge Univ. Press, 2001.
[3] P. Broadfoot and A. Roscoe. Proving security protocols with model checkers by data
independence techniques. Journ. of Computer Security, 7:147–190, 1999.
[4] M. Burrows, M. Abadi, and R. Needham. A logic of authentication. Proc. Royal Soc.,
Series A, Volume 426:233–271, 1989.
[5] J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0.
Univ. of York.
www-users.cs.york.ac.uk/˜jac/papers/drareviewps.ps, 1997.
[6] A. Datta, A. Derek, J.C. Mitchell, and D. Pavlovic. A derivation system and compositional logic for security protocols. Journ. of Computer Security, 13(3):423–482,
2005.
[7] A. Datta, A. Derek, J.C. Mitchell, and A. Roy. Protocol composition logic (PCL).
Elect. Notes in Theor. Comp. Sci., 172:311–358, 2007.
[8] B. Davey and H. Priestley. Introduction to Lattices and Order. Math. Textbooks.
Cambridge Univ. Press, 1990.
[9] S.F. Doghmi, J.D. Guttman, and F.J. Thayer Fàbrega. Searching for shapes in cryptographic protocols. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’07), number 4424 in Lect. Notes Comp. Sci., pages 523–538. Springer,
Berlin, 2007. Extended version is at Cryptology ePrint Archive:
eprint.iacr.org/2006/435.
[10] D. Dolev and A. Yao. On the security of public key protocols. IEEE Trans. on
Information Theory, 29(2):198–208, 1983.
[11] N.A. Durgin, J.C. Mitchell, and D. Pavlovic. A compositional logic for proving security properties of protocols. Journ. of Computer Security, 11(4):677–722, 2003.
[12] R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning About Knowledge. MIT
Press, Cambridge, MA, 1995.
[13] F. Garcia, I. Hasuo, W. Pieters, and P. van Rossum. Provable anonymity. In R. Küsters
and J. Mitchell, editors, 3rd ACM Workshop on Formal Methods in Security Engineering (FMSE05), pages 63–72, Alexandria , VA, U.S.A., November 2005. ACM Press.
[14] R. Goldblatt. Logics of Time and Computation. CSLI Lecture Notes 7, Stanford, 2ndrev. edition, 1992.
[15] J. Guttman, J. Herzog, and F. Thayer Fàbrega. Honest ideals on strand spaces. In
Computer Security Foundations Workshop, 1998.
[16] J. Guttman and F. Thayer Fàbrega. Authentication tests and the structure of bundles.
Theor. Comp. Sci., 283(2):333–380, 2002.
27

[17] J. Guttman. Key compromise, strand spaces, and the authentication tests. In Mathematical Foundations of Programming Semantics 17, volume 47 of Elect. Notes in
Theor. Comp. Sci., pages 1–21. Elsevier, Amsterdam, 2001.
[18] J.Y. Halpern and R. Pucella. On the relationship between strand spaces and multiagent systems. ACM Trans. Inf. Syst. Secur., 6(1):43–70, 2003.
[19] J. Heather, G. Lowe, and S. Schneider. How to prevent type flaw attacks on security
protocols. J. Comput. Secur., 11(2):217–244, 2003.
[20] B. Jacobs and I. Hasuo. PVS sources for semantics and logic of security protocols.
www.cs.ru.nl/B.Jacobs/PVS/protocols-3.0.zip.
[21] G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using
CSP and FDR. In T. Margaria and B. Steffen, editors, Tools and Algorithms for theConstruction and Analysis of Systems, number 1055 in Lect. Notes Comp. Sci., pages
147–166. Springer, Berlin, 1996.
[22] C. Meadows. The NRL protocol analyzer: An overview. Journ. of Logic Programming, 26(2):113–131, 1996.
[23] C. Meadows. Identifying potential type confusion in authenticated messages. Workshop on Foundations of Computer Security, Techn. Rep. DIKU-02-12, Dep. Comp.
Sci., Univ. Copenhagen, 2002.
[24] R. Needham and M. Schroeder. Using encryption for authentication in large networks
of computers. Commun. ACM, 21(12):993–999, 1978.
[25] D. Otway and O. Rees. Efficient and timely mutual authentication. Operating Systems
Review, 21(1):8–10, 1987.
[26] S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw.
Eng., 21(2):107–125, 1995.
[27] L. Paulson. The inductive approach to verifying cryptographic protocols. Journ. ofComputer Security, 6:85–128, 1998.
[28] P. Ryan, S. Schneider, M. Goldschmith, G. Lowe, and A. Roscoe. The Modelling andAnalysis of Security Protocols: the CSP Approach. Addison-Wesley, 2001.
[29] P. Syverson. Towards a strand semantics for authentication logics. In S. Brookes,
A. Jung, M. Mislove, and A. Scedrov, editors, Mathematical Foundations of Progamming Semantics, number 20 in Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 1999.
[30] P. Syverson and I. Cervesato. The logic of authentication protocols. In C. Batini,
F. Giunchiglia, P. Giorgini, and M. Mecella, editors, Foundations of Security Analysis
and Design, number 2171 in Lect. Notes Comp. Sci., pages 63–136. Springer, Berlin,
2001.
[31] F. Thayer Fàbrega, J. Herzog, and J. Guttman. Strand spaces: Proving security protocols correct. Journ. of Computer Security, 7:191–230, 1999.

28

A

Logical rules for Otway-Rees

The following logical rules—together with (O RI S AYS), (I NC T EST) and (SKSEC) in Sections 7.2 and 7.3—are used for the verification of Otway-Rees.
The following rule for authentication is called unsolicited authentication test after [16],as opposed to incoming or outgoing test. It is unsolicited since the incoming “response” isnot really a response to any specific challenge.
(UST EST
authenticationtest.
 ) Unsolicited
Response
A
Receives
m @ i ∧ K{ m1 }  m


∧
K
is
secretly
sharedSecret(A)(K)
@i


=⇒
Authentication result∃B ∈ A. ∃j ∈ [0, i]. B OriginatorOf K{ m1 } @ j
The remaining rules state basic facts about our semantics. They are relatively easier toprove and used in the verification of Otway-Rees.
(NR AN )Randomness of newnonce.
A Sends mA @ iA ∧ newnonce(n)  mA
∧
B Sends mB @ iB ∧ newnonce(n)  mB=⇒ A = B ∧ iA = iB(SKRAN )Randomness of newseckey.
This is the same as (NR AN) but nonces are replaced by seckeys.
(LTKSEC ) Secrecy of never-sent keys (such as long-term symmetric keys).
Initially K is secretly shared
Secret({A, S})(K) @ 0∧A never sends K ∀i ∈ N. (A Sends m @ i =⇒ K 6 m)∧S never sends K ∀i ∈ N. (S Sends m @ i =⇒ K 6 m)=⇒Secrecy result ∀i ∈ N. Secret(A, S)(K)i

B Security proof of Otway-Rees

In the following derivation of (7), (P ROT) designates use of the specification of the OtwayRees protocol. Free variables are immediately replaced by fresh (Skolem) constants: forexample the steps 5 and 6 below can be read as “there exists i1 ∈ N such that ...”.
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.

`
´
B Sends` n, A, B, t1 , KBS´ { newnonce(nB ), n, A, B } @ i
B Sees KBS { nB`, Ks } @ i + j´∀k ∈ [i, i + j]. ¬ B OriginatorOf KBS { nB , Ks } @ k∀k ∈ N. Secret({B, S})(KBS ) @ k
i < i1 < i + j
S OriginatorOf KBS { nB , Ks } @ i1
S Says m1 @ i1
KBS { nB , Ks } = n2p(m1 )S Says KBS { nB , newseckey(Ks ) } @ i1
S Receives n′ , D, B, KDS { nD , n′ , D, B }, KBS { nB , n′ , D, B } @ i1 − 1∨ S Receives n′ , B, D, KBS { nB , n′ , B, D }, KDS { nD , n′ , B, D } @ i1 − 1

29Assumption
Assumption(P ROT )(P ROT ), (LTKSEC )1, 2, 3, 4, (I NC T EST)
1, 2, 3, 4, (I NC T EST)
6, (O RI S AYS)
6, (O RI S AYS)
7, 8, (P ROT)
9, (P ROT)

We refute the second disjunct of 10 as follows.
A-1.
A-2.
A-3.
A-4.
A-5.
A-6.

S Receives n′ , B, D, KBS { nB , n′ , B, D }, KDS { nD , n′ , B, D } @ i1 − 1
E=B ∨ E=S′
E OriginatorOf` KBS { nB , n , B, D } @ i2´∀k ∈ N. ¬ S OriginatorOf KBS { nB , n′ , B, D } @ k′
B OriginatorOf KBS { nB , n , B, D } @ i2
B Says KBS { newnonce(nB ), n′ , B, D } @ i2

A-7.
A-8.
A-9.

i2 = i ∧ n′ = n
B Receives n, A, B, t1 @ i − 1
newnonce(nB ) 6 t1

A-10.
A.

A`= B, hence ⊥´¬ S Receives n′ , B, D, KBS { nB , n′ , B, D }, KDS { nD , n′ , B, D } @ i1 − 1

Assumption
A-1, 4, (UST EST)
A-1, 4, (UST EST)(P ROT)
A-2, A-3, A-4
A-5,(P ROT),(O RI S AYS)
1, A-6, (NR AN)
1, (P ROT)
A-8,
newnonce(nB )only occurs in sent
messages
1, A-6, A-7, A-9
A-1, A-10

We turn back to the main line.
11.
12.

S Receives n′ , D, B, KDS { nD , n′ , D, B }, KBS { nB , n′ , D, B } @ i1 − 1
D = A ∧ n′ = n

13.
14.
15.

S Sends n, KAS { nA , newseckey(Ks ) }, KBS { nB , newseckey(Ks ) } @ i1
∀k ∈ N. Secret({A, S})(KAS ) @ k∀k ∈` N. ∀K ∈ {KAS , KBS }. ∀F ∈ AG.
´
F Possess K @ k =⇒F ∈ {A, B, S}`´∀k ∈ N. ∀F ∈ {A, B, S}. ¬ F DecryptSends (Ks , {KAS , KBS }) @ k
i+j ≤li1 ≤ l ∧ S` ∈ {A, B, S} ∧ S Says newseckey(Ks ) @ i´1∀F ∈ AG. F Possess Ks @ l =⇒ F ∈ {A, B, S}¬(spy Possess Ks @ l)∀l ≥ i + j. ` ¬(spy Possess Ks @´l)
HenceForth ¬(spy Possess Ks ) @ i + j∃k ∈ [i, i + j]. S Says newseckey(Ks ) @ k

16.
17.
18.
19.
20.
21.
22.
23.

10, A
Like A-10 is derived from
A-1, using (UST EST)11, 12, (P ROT), 9(P ROT ), (LTKSEC )4, 14(P ROT), (SKRAN)
Expanding HenceForth5, 17, 13
15, 16, 18, (SKSEC)
19
17, 2021
18, 5

By steps 22 and 23, we have shown that∧=⇒
B Sends n, A, B, t1 , KBS { newnonce(nB ), n, A, B } @ iB Sees KBS { nB , Ks } @ i + jHenceForth ¬(spy Possess Ks ) @ i + j∧∃k ∈ [i, i + j]. S Says (newseckey(Ks )) @ k

By applying rules on Knows we obtain B’s guarantee of secrecy and freshness of thesession key Ks .

30