Journal of Information Security, 2010, 1, 45-55
doi:10.4236/jis.2010.12006 Published Online October 2010 (http://www.SciRP.org/journal/jis)
Extending the Strand Space Method with Timestamps:
Part I the Theory
*
Yongjian Li
1,2
, Jun Pang
3
1Chinese Academy of Sciences, Institute of Software, Laboratory of Computer Science, Beijing, China
2The State Key Laboratory of Information Security, Beijing, China
3University of Oldenburg, Department of Computer Science, Safety-critical Embedded Systems, Oldenburg, Germany
Received June 23, 2010; revised September 14, 2010; accepted July 12, 2010
Abstract
In this paper, we present two extensions of the strand space method to model Kerberos V. First, we include
time and timestamps to model security protocols with timestamps: we relate a key to a crack time and com-
bine it with timestamps in order to define a notion of recency. Therefore, we can check replay attacks in this
new framework. Second, we extend the classic strand space theory to model protocol mixture. The main idea
is to introduce a new relation
a
to model the causal relation between one primary protocol session and one
of its following secondary protocol session. Accordingly, we also extend the definition of unsolicited authen-
tication test.
Keywords: Strand Space, Kerberos V, Theorem Proving, Verification, Isabelle/HOL
1. Introduction
The strand space model [1] is a formal approach to rea-
soning about security protocols. For a legitimate regular
participant, a strand
s
represents a sequence of mes-
sages that the participant would receive or send as part of
a run as his/her role of the protocol. A typical message
has the form of
{
}
K
h denoting the encryption of h
using key
K
. An element of the set of messages is
called a term. A term
'
t is a subterm of
t
is written as
tt
'
⊏
. Usually, we call a strand element node. Nodes can
be either positive, representing the transmission of a term,
or negative, representing the reception of a term. For the
penetrator, the strand represents atomic deductions. More
complex deductions can be formed by connecting several
penetrator strands. Hence, a strand space is simply a set
of strands with a trace mapping. Two kinds of causal
relation (arrow),
→
and
⇒
, are introduced to impose
a graphic structure on the nodes of the space. The rela-
tion

is defined to be the reflexive and transitive clo-
sure of these two arrows, modelling the causal order of
the events in the protocol execution. The formal analysis
based on strand spaces can be carried on the notion of
bundles. A bundle is a causally well-founded set of
nodes and the two arrows, which sufficiently formalizes
a session of a protocol. In a bundle, it must be ensured
that a node is included only if all nodes that proceed it
are already included. For the strand corresponding to a
principal in a given protocol run, we construct all possi-
ble bundles containing nodes of the strand. In fact, this
set of bundles encodes all possible interactions of the
environment with that principal in the run. Normally,
reasoning about the protocol takes place on this set of
bundles.
However, the original strand space model has its se-
mantical limitations to analyze the real-world protocols
such as Kerbeoros protocols. First, it does not include
timestamps as formalized message components, and
therefore can not model security protocols with time-
stamps. In fact, the strand space model [1] as given by
Thayer Fábrega, Herzog, and Guttman is only bench-
marked on nonce-based protocols such as the Needham-
Schroeder protocol and the Otway-Rees protocol. But
many modern protocols use timestamps to prevent replay
attacks, so this deficiency of the strand space theory
makes it difficult to analyze these protocols. Second, it
*
This is a revised and extended version of the homonymous paper
appearing in the Proceedings the Eighth International Conference on
Parallel and Distributed Computing, Applications and Technologies
(PDCAT 2007, IEEE Computer Society). The
main modifications have
been made on the presentation of the technical material, with the pur-
pose of having full details. The first author is supported by grants
(No.60833001,
60496321, 60421001) from National Natural Science
Foundation of China.

Y. J. LI ET AL.
46
does not address issues of the protocol dependency when
several protocols are mixed together. Many real-world
protocols are divided into causally related multiple phas-
es (or subprotocols), such as the Kerberos and Neu-
man-Stubblebine protocols. One phase may be used to
retrieve a ticket from a key distribution center, while a
second phase is used to present the ticket to a security-
aware server. To make matters more complex, many
protocols such as Kerbeors use timestamps to guarantee
the recency of these tickets, that is, such tickets are only
valid for an interval, and multiple sub-protocol sessions
can start in parallel by the same agent using the same
ticket if the ticket does not expire. Little work has been
done to formalize the causal relation between protocols
in a protocol mixture environment.
The aim of this paper is twofold. The first aim is to
extend the strand space theory to cover the aforemen-
tioned two semantical features. Briefly, we include time
and timestamps to model security protocols with time-
stamps: we relate a key to a crack time and combine it
with timestamps in order to define a notion of recency.
Therefore, we can check replay attacks in this new
framework. We also extend the classic strand space
theory to model protocol mixture: a new relation
a
is
introduced to model the causal relation between one
primary protocol session and one of its following sec-
ondary protocol session. Despite the extensions, we hope
that the extended theory still maintains the simple and
powerful mechanism to reason about protocols. The
second aim is practical. We hope to apply the extended
theory to the analysis of some real-world protocols. Here
we select Kerberos V as our case study. Kerberos V is
appropriate because it covers both timestamps and pro-
tocol mixture semantical features.
2. Motivations
2.1. A Short Introduction to Kerberos V
The first version of Kerberos protocol was developed in
the mid eighties as part of project Athena at MIT [2].
Over twenty years, different versions of Kerberos proto-
cols have evolved. Kerberos V (Figure 1 and Figure 2)
is the latest version released by the Internet Engineering
Task Force (IETF) [4]. It is a password-based system for
authentication and authorization over local area networks.
It is designed with the following aims: once a client au-
thenticates himself to a network machine, the process of
obtaining authorization to access another network service
should be completely transparent to him. Namely, the
client only needs enter his password once during the au-
thentication phase. In order to access some network ser-
vice, the client needs to communicate with two trusted
Figure 1. The layout of Kerberos V.
Figure 2. Kerberos V: message exchanging.
servers Kas and Tgs . Kas is an authentication server
(or the key distribution center) and it provides keys for
communication between clients and ticket granting serv-
ers. Tgs is a ticket granting server and it provides keys
for communication between clients and application serv-
ers. The full protocol has three phases each consisting of
two messages between the client and one of the servers
in turn. Messages 2 and 4 are different from those in
Kerberos IV [2,4] in that nested encryption has been
cancelled. Later we will show that this change does not
affect goals of the protocol.
2.2. Timestamps
Timestamps are heavily used in the Kerberos protocols
to guarantee the recency of messages. The strand space
model cannot express security protocols with timestamps,
although Guttman [5] provided a notion of recency and
he used it to analyze replay attacks of a variant of the
Yahalom protocol, it is still impossible to analyze secu-

Y. J. LI ET AL.
47
rity protocols with timestamps. Timestamps are mainly
used to avoid replay attacks in the literature of security
protocols. Usually such attacks occur in protocols that
involve a message encrypted by a session key, and the
session key itself is sent as a part of a message which is
encrypted by a long-term key. Although penetrators can
never obtain a long-term key
K
if
K
is not sent as a
part of a message, it is usually assumed that
m
will be
obtained from
{
}
K
m via cryptanalysis by a penetrator
after some time
t
, especially if a session key SK is a
component of
m
, then it will be compromised after the
time
t
. Here, we say that the time
t
is the crack time
of
K
, and every key will be related to a crack time.
Although the penetrator cannot obtain
m
from
{
}
K
m
during a protocol session provided that
{
}
K
m did not
occur in any old session and
K
’s crack time is longer
than the time of a session allowed, he still may replay
stale messages and use the old compromised session
keys to launch attacks if some message of the protocol
does not contain necessary information to indicate its
recency.
For example, in the Needham-Schroeder symmetric
key protocols (see Figure 3), when
B
receives the third
message
{
}
,
B
K
A K, although
B
can infer that it was
generated by S, he is not certain of its recency because
no such information is available. Perhaps
{
}
,
B
K
A K
has occurred in an old session, and a penetrator has
cryptanalyzed the conversation to obtain the session
K
.
In that case, the penetrator can start a session by resend-
ing
{
}
,
B
K
A K, and later return
{
}
1
b
K
N+. Denning
and Sacco [6] pioneered the use of timestamps to fix the
flaw of the protocol. A timestamp
t
, which is a number,
is employed in the ticket
{
}
, ,
B
K
A Kt by S to mark
the time of issue, and will be compared with the current
time by the receiver
B
to check whether the ticket is
recent. In this paper, we will assume that all agents are
synchronized via a global clock, so an agent knows the
time when receiving or sending a message.
Figure 3. Needham-Schroeder symmetric key protocol.
In this paper, we extend the strand space model with
such features. A crack time is attached to every key. The
crack-time of a key
K
is the time needed by a penetra-
tor to break an encrypted message
{
}
K
m.1 We model a
timestamp in the same way as atomic messages. A regu-
lar agent can attach a timestamp in a message to indicate
when it sends the message, and check whether a received
message encrypted by a key
K
is recent by comparing
the timestamp in the message with the current time and
the crack time of
K
. Once a message
{
}
K
m is no longer
recent, a penetrator can break the message to obtain
m
.
2.3. Protocol Mixture
Another important feature of Kerberos, which is difficult
to model in strand space, is protocol mixture. Kerberos
protocol comprises three protocol phases: authentication,
authorization, and service protocol phases. Once a client
has passed an authentication phase and obtained an au-
thentication ticket, then he can use the ticket to start mul-
tiple sessions of the authorization protocol phases in pa-
rallel to obtain different service tickets to access the ser-
vices he needs provided that the authentication ticket
does not expire. Similarly, once the client has gone
through a session of the authorization phase, then he can
use the service ticket obtained to access the service serv-
er for many times provided that the service ticket does
not expire. Usually we refer to a protocol as one primary
protocol, and the protocol following it as a secondary
protocol. We note that other researchers have discussed
the problem of protocols mixture [7,8], but they empha-
sized more on independency between two protocols.
Namely, if they have disjoint encryption, then the first
protocol is independent of the second. By this they mean
that if the first protocol can achieve a security goal (ei-
ther an authentication goal or a secrecy goal) when ex-
ecuted in isolation, then it still achieves the same security
goal when executed in combination with the second pro-
tocol. In their theory, one primary and one secondary
strands are rather independent of each other.
However, in Kerberos protocols, a secondary strand
cannot be independent of its primary strand, and the
events of a secondary strand has temporal relation with
the events of the primary strand. For example, assuming
that a client
A
runs a session
'
s of an authorization
phase of Kerberos V, then he must have passed an au-
thentication phase
s
. When A receives the second mes-
sage in the session
'
s, he must ensure that the current
time should be before the ticket
{
}
, ,,
Tgs
aK
A TgsauthKT
expires, so
A
needs know the time
a
T when the ticket
is created, and checks how much time has elapsed until
now. This side condition cannot be expressed without the
semantical specification of
s
, because in the intended
1
It is not the time to obtain
K
from
{|
m
|
}
K
.

Y. J. LI ET AL.
48
case the ticket is a term encrypted with
Tgs
’s long-term
key, which is unintelligible to
A
,
A
cannot know
a
T
from the ticket. Then
A
can only know the time
a
T
from the previous authentication phase
s
. Therefore, we
need to formalize the facts that
'
s follows
s
, and
A
holds all the knowledge of
s
when he runs
'
s , and
there should be causal relation between events in
s
and
those in
'
s . Such semantical features are not covered in
[7,8].
In order to model the aforementioned causal relation
between a primary strand and its following secondary
strands, we introduce a new relation
a
between
strands.
'
ss a holds if
s
is a primary protocol strand
and
'
s is a subsequent secondary protocol strand. E.g.,
let
s
and
'
s be client strands in an authentication
phase and authorization phase in Kerberos V respectively,
'
ss a means that a client runs an authentication ses-
sion
s
, and subsequently starts an authorization session
'
s . In practice, if
'
ss a , then
s
and
'
s may be two
different processes started by the same client, and when
the client starts
'
s
, he knows all the events which have
occurred in
s
. This knowledge is useful for the client to
perform actions in
'
s . E.g., when a client starts an au-
thorization session, he uses an authentication ticket
which is obtained in the preceding authentication session,
and he knows the time when the ticket is created. So a
causal relation should be imposed on two events which
occur in a primary strand and its subsequent secondary
strand.
Figure 4 illustrates a possible protocol execution of
Kerberos V using the relation
.
a A client runs an in-
stance in authentication phase, which is represented by
the strand
1
i . Following the primary protocol instance,
the same client may run three authorisation subprotocol
instances in parallel, which are showed in the strands
21
i ,
,
22
i and
23
i respectively.
21
Tr is a subtree which is a
collection of client strands in the service phase.
22
Tr
and
23
Tr are similar to
21
Tr . Note that the semantics of
the relation
a
means that
21
i and
22
i and
23
i inhe-
rits all the same knowledge from ,
1
i so they shares the
same ,authTicket authK , Tgs ,
a
T , etc. Therefore,
if
( ) { }
{
}
1,1 =,,,,
A
aK
termiauthTicketA TgsauthKT then
then it must be the case that
( ) { }
{
}
{
111 1
,1 =,,,
authK
termiauthTicketA tB
and
( ) { }
{
}
{
132 2
,1 =,,,
authK
termiauthTicketA tB
for some
1
t ,
2
t ,
1
B and .
2
B Here
1 1
( )
t B
can be
different from ).(
22
Bt This means that the client use the
same authTicket to obtain two different server tickets
for accessing servers
1
B and .
2
B Without the relation
Figure 4. An illustration of protocol mixture.
,
a
21
i and
1
i are independent, therefore the know-
ledge inherence relation between them can not be im-
posed.
We extend the relation
⇒
in the strand space model
in the way that
21
nn ⇒ holds if ),(=
1
isn and
1)
,(=
2+
isn , or 1)))((,(=
1−
strlengthsn and ,0)(=
2
'
sn
and
'
ss a . Namely, the edge means either that
1
n is
an immediate causal predecessor of
2
n on the same
strand
s
or that
1
n is the last event in a primary strand
s
and
2
n is the first event in the subsequent secondary
strand
'
s .
Structure of the Paper. In Section 3, we present the
theory of the strand space method with our two exten-
sions. We devote Section 5 to a new definition of unsoli-
cited authentication test. We discuss related work and
conclude the paper in Section 6.
3. Preliminaries
3.1. Messages and Actions
The set of messages is defined as the following BNF
notation:
{ } ),(|,|
)(|)(|
)(|)(::=
21 Khhh
tK
nAh
enc
timestampkey
noncename
where
A
is an element from a set of agents,
n
from a
set of nonces,
K
from a set of keys, and
t
from a set
of times. Here we assume that Time is the set of all nat-
ural numbers.
21 <tt
means that the time
1
t is earlier

Y. J. LI ET AL.
49
than
2
t . We represent a timestamp by marking
t
as
timestamp (t). Except this extension, the definitions of
other kinds of messages are the same as those in the
classic strand space theory. We call a key symmetric if
K
K
=
1−
. Otherwise,
K
is a public key and
1−
K
is
private. For each
K
, we define )(Kcracktime as the
crack time of
K
.
{
}
1 2
,
h h
is called a composed mes-
sage. We will write
{
}
{
}
1 23
, ,
h hh
as
{
}
1 2 3
, ,
h hh
.
{
}
{
}
1 21 2
, ,
' '
h hhh
= if and only if
'
hh
11
= and
'
hh
22
= .
We abbreviate ),( Khenc as
{
}
K
h
, denoting the en-
cryption of h using key
K
. In our formulation, we use
A
K to define a long-term key shared between an agent
(also called a client)
A
and a server, and clients have
distinct keys. An element of the set of messages is also
called a term. Terms of the form name (A), nonce (n),
timestamp (t), or key (K) are said to be atomic.
2
The set
of all messages is denoted by Message . A message h is
a text message if Kh ≠ for any
K
. The set of all
atomic text messages is denoted by
T
. We frequently
need the subterm relation on messages. A term
'
g is a
subterm of
g
is written as gg
'
⊏
.
Definition 1 The subterm relation
⊏
is defined induc-
tively as the smallest relation such that
g
g
⊏
,
{
}
K
g h
⊏
if hg
⊏
, and
{
}
1 2
,
gh h
⊏
if
1
hg
⊏
or
2
hg
⊏
.
In our extended strand space model, we need to revise
the definition of actions. The main point is to record the
time when an action takes place. The transmission of a
term
g
at time
t
is denoted by ),,( gt + , and the re-
ception of a term
g
at
t
is denoted by ),,( gt − . Both
are the possible actions that participants and a penetrator
can take. We represent the set of finite sequences of ac-
tions by ( Time , ±, Message )*.
3.2. Strands and Strand Spaces
A strand space
Σ
is a set of strands with a trace map-
ping
*
),(: MessageTime ±→Σ ,tr . A strand element is
called a node. ),( is is the i -th node on strand
s
( )(<0 slengthi ≤ ). We use
s
n
∈
to denote that a node
n
belongs to the strand
s
. The set of all the nodes is
denoted by
N
. If ),(= isn and ),,(=)( gtstr
i
σ ,
then we define )( ntime and )( nterm and )( nsign to
be the occurring time, the term and the sign of the node
n
, respectively. Namely, tntime=)( , gnterm =)( , and
σ =)(nsign . We call a node positive if its term has sign
+
, and negative if its term has sign
−
. A strand is a
protocol history from the point of view of a single par-
ticipant in a protocol run, so we explicitly define an
attribute function Aattr
→
Σ
: to indicate which
agent’s peer a strand is. Namely, asattr =)( means that
a
is the agent who performs actions of the strand
s
in
the run.
As mentioned in Section 2, we introduce a relation
a
between strands to model protocol mixture, and
'
ss a holds if
s
is a primary protocol strand, and
'
s
is a subsequent secondary protocol strand. To make our
theory sound, we also restrict the relation
a
to be a
tree-like one with the following principles. First,
a
is
irreflexive, i.e. ss a
/
. Second, every strand has at most
one
a
predecessor, meaning if
''
ss a and
'''
ss a ,
then
'
ss = . The two restrictions are consistent with our
intuition on protocol mixture. The first principle says that
one protocol session can not follow itself, this simply
means that the primary protocol session and any one of
its following secondary protocol sessions are different.
The second principle shows that one secondary protocol
session follows a unique primary protocol session.
Two kinds of causal relation (arrow),
→
and
⇒
,
are introduced to impose a graph structure on the nodes
of
Σ
. To be more precise, the relation
'
nn ⇒ holds
between nodes
n
and
'
n if ),(= isn and 1),(= +isn'
and ),()( ' ntimentime ≤ or
(
)
(
)
(
)
1,= −strlengthsn and
,0)(= '' sn and
'
ss a and )()( ' ntimentime ≤ . This
relation means that the event
'
n immediately follows
n
. On the other hand, the relation
'
nn → holds for
nodes
n
and
'
n if gntermnterm
'
=)(=)( for some term
g
, +=)(nsign and −=)(
'
nsign , and )()(
'
ntimentime ≤ .
This represents that
n
sends a message
g
and
'
n
receives the message at a later time. Obviously, here we
require that the two relations must respect the order of
time. The relation

is defined to be the reflexive and
transitive closure of
→
and
⇒
, modelling the causal
order of the events in the protocol execution. We say that
a term
g
originates at a node
n
if and only if
n
is
positive, ),(ntermg
⊏
and there is no node
'
n such
that nn
' +
⇒ and )( ' ntermg
⊏
; We say that
g
uni-
quely originates if and only if there exists an unique node
n
such that
g
originates from node
n
. Nonces and
other recently generated terms such as session keys are
usually uniquely originated.
3.3. Penetrator Strands
The symbol Bad is defined to denote the set of all the
penetrators, and if an agent is not in Bad , then it is regu-
lar. There is a set of keys that are known initially to all
the penetrators, denoted as
P
K .
P
K usually contains
all the public keys, all the private keys of all the penetra-
tors, and all the symmetric keys initially shared between
all the penetrators and principals playing by the protocol
rules. It can also contain some keys to model known-key
attacks. In this paper, we only need the fact that if an
agent is not a penetrator then his shared key cannot be
penetrated, which is formalized as follows.
2
For convenience, we often write A, n, K and t instead of name (A)
,
nonce
(
n
)
,
key
(
K
)
, and
timestamp
(
t
)
.

Y. J. LI ET AL.
50
Axiom 1 If Bad
∉
A , then
P
K∉
A
K .
In the classic strand space theory, a penetrator can in-
tercept messages, generate messages that are computable
from its initial knowledge and the messages it intercepts.
These actions are modelled by a set of penetrator strands,
and they represent atomic deductions. More complex
deduction actions can be formed by connecting several
penetrator strands. In our extension, we assume that pe-
netrators share their initial knowledge and can cooperate
each other by composing their strands. Besides the beha-
viors inherited from classic strand space theory, a pene-
trator has the ability to crack an encrypted message once
the message is no longer recent (see
hK
KC
,
strand).
Definition 2 A penetrator’s trace relative to
P
K is one
of the following, where Time∈
321
,,, tttt and
321
ttt ≤≤ :
• M
g
(text message): )],,[( gt + , where Tg
∈
.
• K
K
(key): )],,[( Kt + , where
P
K∈ K .
• C
gh
(concatenation):
{
}
)],,,(),,,(),,,[(
321
hgthtgt+−− .
• S
g,h
(separation):
{
}
,,(),,,(),,,,[( 321 ++− tgthgt )]h.
• E
h,K
(encryption): ,,(),,,(),,,[(
321
+−− thtKt
{
}
)]
K
h .
• D
h,K
(decryption):
{
}
)],,(),,,(),,,[(
32
1
1
hthtKt
K
+−−
−
.
• KC
K,h
(key-crack):
{
}
)],,(),,,[(
21
htht
K
+− , where
21
<)( tKcracktimet + .
In our theory, if a strand
s
belongs to a penetrator,
namely, ( ) attr s ∈
Bad
, then
s
must be a penetrator
strand. If a strand is not a penetrator strand, then it is
regular. A node is called regular if it is not in the pene-
trator strands. Except the key crack strand (
hK
KC
,
), our
penetrator model is similar to the one in [1]. Here
g
M (or
K
K ) does not imply that a penetrator can issue
any unguessable terms which are not in his initial know-
ledge such as nonces and session keys. Because when we
introduce secrecy or authentication properties about an
unguessable term
t
for all penetrators, we usually as-
sume that
t
uniquely originates from a regular strand,
and this implicitly eliminates the possibility that any pe-
netrator can originate
t
. Intuitively, we use
a
to
model regular agents to start a primary protocol session
and then starts multiple parallel secondary protocol ses-
sions, so a penetrator strand cannot be mixed with any
other strand. To be more precise, for all penetrator
strands
s
and all strands
'
s , we have that
'
ss a
/
and
ss
'
a
/
. This implies that a penetrator strand can only be
composed with other strands by the relation
→
.
3.4. Bundles
The formal analysis based on strand spaces is carried on
the notion of bundles, which represents the protocol ex-
ecution under some configuration. A bundle is a causally
well-founded graph, which sufficiently formalizes a ses-
sion of a protocol.
Definition 3 Suppose
(
)
(
)
,,
B
B
B

B
⇒ ∪→ N ,⊆→→
B
and .⊆ ⇒⇒
B
B
is a bundle if
•
B
N and
B
→ and
B
⇒ are finite;
• If the sign of a node
n
is
−
, and
B
Nn ∈ , then
there is a unique positive node
'
n such that
B
Nn
'∈
and nn
'
B
→ ;
• If nn
'
⇒ and
B
Nn ∈ , then
B
Nn
'∈
and
nn
'
B
⇒ ;
•
B
is acyclic.
Suppose
B
is a bundle, we say
B
∈
n if
n
is a
node in
B
N , and use
B

to denote the reflexive and
transitive closure of the relation
→
and
⇒
in
B
. In
a bundle, it must be ensured that a node is included only
if all nodes that proceed it are already included. So a
bundle
B
has the following properties:
Lemma 1 (Bundle well foundedness) Let
B
be a
bundle. Then
B

is a partial order, i.e. a reflexive,
antisymmetric, transitive relation. Every non-empty sub-
set of the nodes in
B
has
B

minimal members.
We have formalized the above extended strand space
theory in the theorem prover Isabelle/HOL [9]. See [10]
for details.
4. Penetrator’s Knowledge Closure Property
In this section, we will describe a useful property on pe-
netrator strands. This property specifies what knowledge
can be obtained from some special message set. First we
need to define a key is regular w.r.t. a node
m
in a
bundle.
Definition 4 A key
K
is regular w.r.t. a node
m
in
a bundle
B
, denoted by
(
)
B
,, mkregular , if and only if
the following condition holds: for any node
n
in
B
, if
Knterm =)( and )()( mtimentime
≤
, then
n
must be
regular.
This definition is about
K
’s secrecy w.r.t. a node
m
in a bundle
B
, which means that
K
cannot be penetrated
before
m
in the bundle. In most of the cases, we only
consider security properties for a protocol in a given bun-
dle, so it is natural for us to just consider whether a key
can potentially be penetrated in this bundle. Besides, we
also need consider temporal restriction
)
()( mtimentime
≤
because we discuss
K
’s secrecy a timed framework.
Definition 5 Let
m
be a node in a bundle .
B
A
message
,
t
is a component w.r.t.
m
in bundle ,
B
denoted by
(
)
B
,, mtcomponent , if
1) g ∀ (
{
}
);,. hgth ≠
2)
{
}
(
)
(
)
(
)
B ,,=.
1
mkregularhtkh
k
−
→∀
Intuitively,
(
)
B
,, mtcomponent means that
t
basic
unit that can not be analyzed in
B
by penetrators.
Namely,
t
can not be detached because
t
is not a
concatenated form; and if
t
is an encrypted form of

Y. J. LI ET AL.
51
{
}
K
h
t
can not be decrypted before
m
in
B
be-
cause
1−
k can not be penetrated before
m
.
Definition 6 Let
m
be a node in a bundle .
B
a
is
a message which uniquely originates at some node
n
. A
message set
M
is a test suite for
a
w.r.t.
m
in ,
B
denoted by
(
)
B
,,,, nmaMsuite if
1)
→
∈
∀
taMt
⊏
.
(
)
B
,, mtcomponent
2)
(
.
→
∈
∀
t
a
M
t
⊏
{
}
k
hthk =. ∀
→
)
(
m
time
≤
))
(
)
(
k
cracktime
n
time
+
3) ;. Mttat
∈
→
/
∀
⊏
Intuitively,
(
)
B
,,,, nmaMsuite means that for any
Mt
∈
such that
,
t
a
⊏
t
can not be detached or de-
crypted before
m
because such
t
is a component w.r.t.
m
in bundle
B
; furthermore, if
t
contains
a
and is
of the form
{
}
K
h
for some k and , h
t
can not be
cracked before
m
because the duration between
m
and
n
is less than k ’s crack time, and this is guaran-
teed by (2). Recall that )( ntime is the first time when
a
occurs because
a
uniquely originates at
.
n
Now we need introduce a function synth on a mes-
sage set
H
, which captures the “building up” aspect of
penetrator's ability [4,11].
(
)
Hsynth is defined to be the
least set that includes
H
, agents, timestamps and is
closed under pairing, and encryption.
Definition 7 Consider a message set , H )( Hsynth
is a message set which is defined inductively as follows:
1)
)
(
H
synth
A
∈
if
A
is an agent name;
2) )( Hsyntht ∈ if
t
is a timestamp;
3) )( Hsynthm ∈ if Hm
∈
;
4)
{
}
),( Hsynthh
k
∈ if
)
(
H
synth
h
∈
and
;
H
k
∈
5)
{
}
),(, Hsynthhg ∈ if )( Hsynthg ∈ and
).( Hsynthh ∈
In the context of this paper, we usually assume that
a
is an unguessable atomic message such as a nonce,
which is uniquely originated from a regular strand and
encrypted in a message. Let },|{=
0
MttatM ∈∧
⊏
in
later discussions we usually assume that
0
M is the set
of messages which is emitted by some regular strands. f
M
is a test suite for
a
w.r.t.
m
in b , then the set
synth
(
)
M is a knowledge closure which penetrators
can synthesize in the bundle b from . M Namely, if
the messages received in a penetror strand are in
synth
(
)
M , then the messages sent in the strand must
still be in synth
(
)
. M
Before we prove the closure property, we need two
useful lemmas, as shown below:
Lemma 2 If
M
is a test suite for
a
w.r.t.
m
in
,
B
and
{
}
∈ hg , synth
(
)
, M then
∈
g
synth
(
)
M and
∈ h synth
(
)
. M
Lemma 3 If
{
}
(
)
, Msynthh
K
∈ then
(
)
Msynthh ∈
or
{
}
. Mh
K
∈
Let
a
be an atomic message that uniquely originates
at some node
n
,
m
be a positive penetrator node in a
bundle
B
such that and
(
)
. mterma
⊏
Suppose
M
is
a test suite for
a
w.r.t.
m
in the bundle
B
, if any
message that the penetrator can receive in the strand is in
(
)
, Msynth then the penetrator can only send a term
which is still in
(
)
Msynth . Figure 5 illustrates such
behaviors of penetrators on knowledge, where (a) shows
the cases for ,
,hg
C ,
,Kh
E and ;
,Kh
D (b) shows the
case for ;
,hg
S and (c) shows the case for .
,hK
KC
Lemma 4 Let
m
be a positive penetrator node in a
Figure 5. Penetrator’s knowledge closure property.

Journal of Information Security, 2010, 1, 45-55
doi:10.4236/jis.2010.12006 Published Online October 2010 (http://www.SciRP.org/journal/jis)
bundle ,
B
a
be an atomic message that uniquely ori-
ginates at a regular node
n
,
M
be a message set such
that
(
)
,,,,,
B
nmaMsuite and
(
)
(
)
Msynthmterm
'∈
for
any node such that ,mm
'+
⇒ then
(
)
(
)
.Msynthmterm ∈
Proof. For convenience, the assumption that
(
)
(
)
Msynthmterm ∈ for any node such that nm
+
⇒ is
referred as (1) in the proof as follows.
By case analysis on the form of penetrator strand, we
can easily exclude the cases when
m
is in a strand
g
M , .
K
K If thus, we can conclude that
a
originates
at
.
m
This contradicts with the fact that uniquely origi-
nates at a regular node
.
n
Therefore,
m
is in a strand
i such that i is
hg
C
,
, ,
,hg
S ,
,Kh
E ,
,Kh
D or
hK
KC
,
.
Case 1: i is in ,
,hg
C then
(
)
2,=mindex
(
)
,=,0giterm
(
)
,=,1 hiterm and
(
)
{
}
hgmterm,= for some
g
, ,h
and
(
)
,=,0 − isign and
(
)
− =,1isign . From the assump-
tion (1), we have
(
)
(
)
Msynthiterm ∈ ,0 and
(
)
∈
,1iterm
(
)
,Msynth then
(
)
Msynthg ∈ and
(
)
;Msynthh ∈ By
the definition of synth operator,
{
}
(
)
, ,
g hsynthM
∈
then
(
)
(
)
.Msynthmterm ∈
Case 2: i is in ,
,hg
S then
(
)
1,=mindex or
(
)
2,=mindex
(
)
{
}
,,=,0 hgiterm
(
)
,=,1 giterm and
(
)
=mterm h
for some
g
, .h From the assumption (1), we have
(
)
(
)
Msynthiterm ∈,0 ,
{
}
∈hg,synth
(
)
,M by Lemma
4, we have
(
)
Msynthg ∈ and
(
)
.Msynthh ∈ So
(
)
∈
mterm
(
)
.Msynth
Case 3: i is in ,
,Kh
E then
(
)
2,=mindex
(
)
,=,0 Kiterm
(
)
,=,1 hiterm and
(
)
{
}
K
'
hmterm =
for some
K
, ,h and
(
)
,=,0−isign and
(
)
.=,1 −isign
From the assumption (1) ,
(
)
(
)
Msynthiterm ∈,0 and
(
)
(
)
,,1 Msynthiterm ∈ then
(
)
MsynthK∈ and
(
)
;Msynthh∈ by the definition of synth , we have
{
}
(
)
,Msynthh
K
∈ then
(
)
(
)
.Msynthmterm ∈
Case 4: i is in ,
,Kh
D then
(
)
2,=mindex
(
)
,=,01− Kiterm
(
)
{
}
,=,1
K
hiterm and
(
)
hmterm = for some
K
, ,h
and
(
)
,=,0 −isign and
(
)
.=,1 −isign From the assumption
(1), we have
(
)
(
)
Msynthiterm ∈,0 and
(
)
(
)
,,1 Msynthiterm ∈
therefore
(
)
MsynthK ∈
− 1
and
{
}
(
)
,Msynthh
K
∈ by
Lemma 4, we have either (4-1)
(
)
(
)
Msynthhmterm ∈=
or (4-2)
{
}
.Mh
K
∈ From (4-1), the lemma can be
proved at once. For the case (4-2), there are also two
subcases, either (4-2-1)
{
}
K
ha
⊏
/
or (4-2-2)
{
}
.
K
K
ha
⊏
From (4-2-1), we have ,ha
⊏
/ by
M
is a test suite for
a
in b , so ,Mh∈ then h
∈
synth
M
, then ter m
'
m
∈
synth .M From (4-2-2), then by
M
is a test
suite for
a
in
b
, we have component
{
}
K
h ,b then
we have
(
)
.,,
1
B mKregular
−
From this and
(
)
B
∈,0i
and
(
)
,=,0 1
−
Kiterm then i is regular, but this contra-
dicts with that
m
is in a penetrator strand.
Case 5: i is in ,
,hK
KC then
(
)
1,=mindex
(
)
,=,1hiterm
(
)
{
}
,=,0
K
hiterm (2)
(
)
(
)
.,1<)(,0 itermKcracktimeiterm+ From the assump-
tion (1), we have
{
}
(
)
.Msynthh
K
∈ From this, by
Lemma 3, we have either (5-1)
(
)
Msynthh ∈ or (5-2)
{
}
.Mh
K
∈ From (5-1), the lemma can be proved at once.
For the case (5-2), there are also two subcases, either
(5-2-1)
{
}
K
ha
⊏
/
or (5-2-2)
{
}
.
K
ha
⊏
From (5-2-1), we
have ,ha
⊏
/
by the definition of
(
)
B
,,,, nmaMsuite , so
,Mh ∈ then
(
)
.Msynthh ∈ From (5-2-2), then by the
definition of
(
)
B
,,,, nmaMsuite , we have (3)
).()()( kcracktimentimemtime
+
≤
From
(
)
,,0iterma
⊏
and
a
uniquely originates at
,
n
we have ,0).()( itimentime ≤
Then we have
),(,0)()()( kcracktimeitimekcracktimentime
+
≤
+
with (3), we have ).(,0)()( kcracktimeitimemtime
+
≤
But this contradicts with (2).
On the other side, a strand’s receiving nodes get mes-
sages which are all in
(
)
,Msynth but a new message,
which is not in
(
)
Msynth , is sent in the strand, then the
strand must be regular because a penetrator strand can
not create such a term. The result can be simply inferred
from Lemma 4.
Lemma 5 Let mbe a positive node in a bundle ,
B
a
be an atomic message that uniquely originates at a reg-
ular node
n
,
M
be a message set such that
(
)
,,,,,
B
nmaMsuite and
(
)
(
)
Msynthmterm
'
∈ for any
node such that ,mm
' +
⇒ and
(
)
(
)
,Msynthmterm ∉ then
m
is regular
.
For Lemma 4 and 5, we have two comments:
1) Lemma 4 characterizes the knowledge closure
properties of a penetrator’s operations on messages. It
says that if a penetrator only receives messages in
(
)
,Msynth where
M
is a test suite for some atomic
message
,
a
then the augmented knowledge of the pe-
netrator is still in
(
)
Msynth after the receiving actions.
2) Lemma 5 provides a key technique to prove the au-
thentication guarantee that
m
is regular. Intuitively,
condition (1) of suite requires the secrecy of the in-
verse key
1−
k for any key k which is used to encrypt
any message in
M
containing
a
; condition (2) of op-
erator suite is a recency restriction that these encrypted
messages containing
a
can not be cracked until
.
m
Therefore this lemma provides a means of using secrecy
and recency restriction to prove authentication guarantee.
We will see this result is very useful for us to check
whether a strand is regular in the next sections.
Note that the two lemmas relates the algebraic opera-
tor synth in trace theory [4,11] with penetrator’s strand
ability to deduce knowledge, which is the most important

Y. J. LI ET AL.
53
one which differs our work from the classical strand
space theory. Such closure properties are not available in
the classical strand space theory because message alge-
bra operators such as synth are not formalized.
5. Unsolicited Tests
In [12] (Subsection 4.2.3), a negative node
n
is an un-
solicited test for
{
}
K
h
, if
{
}
K
h
is a test component
for any atomic text
a
in
n
, and
K
cannot be pene-
trated in the strand space. Then an unsolicited test for
{
}
K
h
in a bundle
B
can guarantee the existence of a
positive regular node of which
{
}
K
h
is a component.
We simplify this definition of unsolicited tests by the
following two aspects:
1) we consider a node
n
is an unsolicited test for
{
}
K
h
in a bundle
B
;
2) we only require that
{
}
K
h
is a subterm of the
term of
n
, and
K
is regular w.r.t.
n
in the bundle
B
instead of a strand space.
In our formulation, unsolicited authentication test is a
kind of regularity about an encrypted term
{
}
K
h
, which
is a subterm of a node
n
where
K
cannot be pene-
trated before
n
in a bundle
B
. Then it can be ensured
that there is a positive regular node
m
originating
{
}
K
h
as a subterm, i.e.,
m
has
{
}
K
h
as a subterm
and it also holds that
{
}
)(
'
K
mtermh
⊏
/
for any node
mm
'
B

. Intuitively, the reason why
m
must be regular
lies in that
K
cannot be penetrated before
m
in
B
.
So the penetrator cannot create
{
}
K
h
by encrypting h
with
K
.
Definition 8 Given a bundle
B
. A node
n
in
B
is
an unsolicited test for
{
}
K
h
if
{
}
)(ntermh
K
⊏
, and
K
is regular w.r.t.
n
in
B
.
Lemma 6 (Unsolicited authentication test)
B
is a
given bundle. Let
n
be an unsolicited test for
{
}
K
h
.
Then there exists a positive regular node
m
in
B
such
that nm
B

and
{
}
)(mtermh
K
⊏
and
{
}
)(
'
K
mtermh
⊏
/
for any node
'
m such that mm
'
B

.
Proof. Let
{
}
)}(|{= xtermhnxxP
K
df
⊏

∧
B. Ob-
viously, Pm
∈
. By Lemma 1, there exists a node
'
m
such that
'
m is minimal in
P
, which means that
{
}
)(
'
K
mtermh
⊏
, nm
'
B

, and for all
y
such that
'
my
B

, Py
∉
. Hence,
{
}
)( ytermh
K
⊏
/
.
First, we prove that the sign of
'
m is positive by
contradiction. If −=)(
'
msign , then by the upward-
closed property of a bundle there must be another node
''
m in
B
such that +=)(
''
msign and
'''
mm→ . Then
we have (a)
'''
mm
B

and (b) )(=)(
'''
mtermmterm .
By (a) and nm
'
B

, we have nm
''
B

. By (b) and
{
}
)(
'
K
mtermh
⊏
, we have
{
}
)(
''
K
mtermh
⊏
. Hence,
Pm
''
∈ which contradicts with the minimality of
'
m .
Second, we prove that
'
m is regular. We show that a
contradiction can be derived if
'
m is in a penetrator
strand. Here, we only analyze cases when
'
m is in ei-
ther
'
gg
C
,
(concatenation strand),
'
Kg
E
,
(encryption
strand), or
g
'
K
KC
,
(key crack strand). Other cases are
either straightforward or can be analyzed in a similar
way.
•
'
m is in
'
gg
Ci
,
∈ .
By the form of the strand
'
gg
C
,
and the fact that
'
m
is a positive node, we have ,2)(= im
'
,
{
}
''
ggmterm ,=)( , giterm =,0)( , and
'
giterm=,1)(
for some
g
,
'
g . By the upwards-closed property of a
bundle, we have that nodes ,0)(i and ,1)(i must be in
B
. By
{
}
{
}
,
'
K
hg g
⊏ , we have either
{
}
K
h g
¤
or
{
}
K
h g
′
⊏
, i.e.
{
}
,0)(itermh
K
⊏
or
{
}
,1)(itermh
K
⊏
.
So either node Pi ∈,0)( , or node Pi ∈,1)( . Both cases
contradict with the minimality of
'
m .
•
'
m is in
'
Kg
Ei
,
∈ .
By the form of the strand
'
Kg
E
,
and the fact that
'
m
is a positive node, we have ,2)(= im
'
,
{
}
'
K
'
gmterm =)( ,
'
Kiterm =,0)( , and giterm =,1)(
for some
g
and
'
K
. So
{
}
{
}
K K
h g
′
⊏
. Then it is
straightforward that either (1)
{
}
K
h g
⊏
or (2) gh=
and
'
K
K
=
. For the first case, we have
{
}
,1)(itermh
K
⊏
. It is easy to derive a contradiction by
the same argument as before. For the second case, by the
definition of the relation
⇒
, we have (a)
,2)(,0)( itimeitime
≤
. And by definition of
P
, we also
have (b) )()( ntimemtime
'
≤ . Hence, )(,0)( ntimeitime≤ .
However, by the assumption that
K
must be regular
w.r.t.
n
in
B
, ,0)(iterm must be regular, and this
contradicts with the fact that i is a penetrator strand.
•
'
m is in
g
'
K
KCi
,
∈ .
By the form of the strand
g
'
K
KC
,
, and the fact that
'
m is a positive node, we have ,1)(= im
'
, gmterm
'
=)( ,
{
}
'
K
giterm=,0)( for some
g
and
K
′
, and
)(<)(,0)(
'
mtimeKcracktimeitime + .
By
{
}
gmtermh
'
K
=)(
⊏
, so
{
}
{
}
'
KK
gitermh =,0)(
⊏
.
Obviously nmi
'
B
B


,0)( . So Pi ∈,0)( , which contra-
dicts with the minimality of
'
m .
The proof totally depends on the well-founded induc-
tion principle on bundles, and we have formalized the
proof of this lemma in Isabelle/HOL in our inductive
strand space model, and the proof scripts are available at
[10]. In fact, lemma 6 provides a useful proof method to
reason about authentication properties basing on secrecy
properties. Note that the premise that
n
is an unsoli-
cited test for
{
}
K
h
requires that
K
is regular w.r.t.
n
in
B
, which is an assumption on the secrecy of
K
.
And the conclusion is an authentication guarantee of the
existence of a regular node
m
. Besides, compared with
the original version of unsolicited test, our result also has

Y. J. LI ET AL.
54
two extensions that nm
B

and
m
is minimal (i.e.,
{
}
)(
'
K
mtermh
⊏
/
for any node
'
m such that )mm
'
B

.
We find that the extended version of unsolicited authen-
tication test is quite useful in many cases, especially in
the verification of authentication properties of symmetric
key based protocols. In [13], we have used a version of
unsolicited authentication test in the classical strand
space theory to give new proofs of authentication proper-
ties of the Otway-Rees protocol. In this work, we have
successfully applied unsolicited authentication test to our
study of the Kerberos V protocol in the next paper.
6. Conclusions and related Work
This work is an extension of [14]. We have added two
new semantical features in our new framework: time-
stamp and protocol mixture. In essence, our treatment of
timestamps is to add a global clock to the underlying
execution model, and to extend every action by a tem-
poral annotation. This allows us to align the timestamps
sent in the protocol messages with the actual occurrence
times of the corresponding actions. Although it is quite
straightforward, it gives a powerful mechanism to reason
about recency of a message. For protocol mixture, we
admit a realistic assumption that a regular agent can start
multiple parallel secondary sessions once he has finished
a primary protocol session, and he holds all the informa-
tion of the primary protocol session when he begins a
secondary protocol session. So we introduce a causal
relation
a
between strands to model the protocol de-
pendency. The above two semantical features are seldom
discussed in previous works of strand space literature.
Despite the aforementioned extensions in semantics,
the definition of a bundle, which is the cornerstone of the
strand space theory, remains unchanged. So the induction
principle on the well-foundedness of a bundle is still ef-
fective in our model. Based on this principle, we have
proved an extended result of the unsolicited authentica-
tion test.
In the literature, most of the existing approaches for
protocol analysis have not concentrated on timestamps
and replay attacks. These include the CSP model-
checking approach [15], the rank functions [16], and the
Multi-Set Rewriting formalism (MSR) [17]. Paulson and
Bella's inductive method [4,11] is one exception. They
not only have extended their method to model replay
attacks, but also have succeeded in applying their method
to the Yahalom protocol and the Kerberos IV protocol.
Recently, Bozga et al. [18] proposed an approach based
on timed automata, symbolic verification techniques and
temporal logic to analyze security protocols with time-
stamps. But they haven’t applied their approach to any
real-world security protocols.
For protocol mixture, there have been a few works to
reason rigorously about protocol interactions. For in-
stance, Meadows studied the Internet Key Exchange
protocol, emphasizing the potential interactions among
its specific sub-protocols [19]. The analysis work was
conducted in the NRL protocol analyzer. Recently, Cre-
mers discussed the feasibility of multi-protocol attacks,
and his work is done in the operational semantical frame-
work which considers a so-called type flaw attacks [20].
All these works, including [7], focus on protocol interac-
tions by message exchanging. Instead, our work empha-
sizes on the dependency between a primary protocol ses-
sion and a secondary protocol session. Here we assume
that when a regular agent starts a secondary protocol
session, he should be aware that he has finished a cor-
responding primary protocol session, and he maintains
all the information obtained in the primary protocol ses-
sion, such as tickets and the creation time of the tickets.
These modelling assumptions fit well with the real-world
environments where the Kerberos protocols run.
7. References
[1] F. Javier Thayer, J. C. Herzog and J. D. Guttman, “Strand
Spaces: Proving Security Protocols Correct,” Journal of
Computer Security, Vol. 7, No. 1, 1999, pp. 191-230.
[2] S. P. Miller, J. I. Neuman, J. I. Schiller and J. H. Saltzer,
“Kerberos Authentication and Authorisation System,”
Technical Report, Technical Plan Section E.2.1, MIT,
Athena, 1989.
[3] K. R. C. Neuman and S. Hartman, “The Kerberos Net-
work Authentication Service (v5),” Technical report, In-
ternet RFC 4120, July 2005.
[4] G. Bella, “Inductive Verification of Cryptographic Pro-
tocols,” PhD thesis, Cambridge University Computer
Laboratory, 2000.
[5] J. D. Guttman, “Key Compromise, Strand Spaces, and the
Authentication Tests,” Proceedings of 7th Conference on
the Mathematical Foundations of Programming Seman-
tics, ENTCS 45, 2001, pp. 1-21.
[6] D. Denning and G. Sacco, “Timestamps in Key Distribu-
tion Protocols,” Communications of the ACM, Vol. 24,
No. 8, 1981, pp. 533-536.
[7] F. Javier Thayer, J. C. Herzog and J. D. Guttman, “Mixed
Strand Spaces,” Proceedings of 12th IEEE Computer Se-
curity Foundations Workshop, 1999, pp. 72-82.
[8] J. D. Guttman and F. Javier Thayer, “Protocol Indepen-
dence through Disjoint Encryption,” Proceedings of 13th
IEEE Computer Security Foundations Workshop, 2000,
pp. 24-34.
[9] T. Nipkow, L. C. Paulson and M. Wenzel, “Isabelle/HOL—
A Proof Assistant for Higher-Order Logic,” LNCS 2283.
Spinger, 2002.
[10] Y. Li, “Strand Space and Security Protocols”. http://lcs.
ios.ac.cn/˜lyj238/strand.html

Y. J. LI ET AL.
55
[11] L. C. Paulson, “The Inductive Approach to Verifying
Cryptographic Protocols,” Journal of Computer Security,
Vol. 6, No. 1-2, 1998, pp. 85-128.
[12] J. D. Guttman and F. Javier Thayer, “Authentication
Tests and the Structure of Bundles,” Theoretical Com-
puter Science, Vol. 283, No. 2, 2002, pp. 333-380.
[13] Y. Li and J. Pang, “Generalized Unsolicited Tests for
Authentication Protocol Analysis,” Proceedings of 7th
Conference on Parallel and Distributed Computing, 2006,
pp. 509-514.
[14] Y. Li, “The Inductive Approach to Strand Space,” Pro-
ceedings of 25th IFIP Conference on Formal Techniques
for Networked and Distributed Systems, LNCS 3731,
2005, pp. 547-552.
[15] G. Lowe, “Breaking and Fixing the Needham-Schroeder
Public-Key Protocol Using FDR,” Proceedings of 2nd
International Conference on Tools and Algorithms for the
10 Construction and Analysis of Systems, LNCS 1055,
pages 147-166, 1996.
[16] J. Heather and S. A. Schneider, “Toward Automatic Ve-
rification of Authentication Protocols on an Unbounded
Network,” Proceedings of 13th IEEE Computer Security
Foundations Workshop, 2000, pp. 132-143.
[17] F. Butler, I. Cervesato, A. Jaggard and A. Scedrov, “A
Formal Analysis of Some Properties of Kerberos 5 Using
MSR,” Proceedings of 15th IEEE Computer Security
Foundations Workshop, 2002, 175-190.
[18] L. Bozga, C. Ene and Y. Lakhnech, “A Symbolic Deci-
sion Procedure for Cryptographic Protocols with Time
Stamps,” Journal of Logic and Algebraic Programming,
Vol. 65, No. 1, 2005, pp. 1-35.
[19] C. Meadows, “Analysis of the Internet Key Exchange
Protocol Using the NRL Protocol Analyzer,” Proceedings
of 12th IEEE Computer Security Foundations Workshop,
1999, pp. 216-231.
[20] C. J. F. Cremers, “Feasibility of Multi-Protocol Attacks,”
Proceedings of 1st Conference on Availability, Reliability
and Security, 2006, pp. 287-294.