Journal of Information Security, 2010, 1, 56-67
doi:10.4236/jis.2010.12007 Published Online October 2010 (http://www.SciRP.org/journal/jis)
Extending the Strand Space Method with Timestamps:
Part II Application to Kerberos V*
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 Sep tember 14, 2010; accepted July 12, 2010
Abstract
In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we
formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new
framework. Second, we apply unsolicited authentication test to prove its secrecy and authentication goals of
Kerberos V. Our formalization and proof in this case study have been mechanized using Isabelle/HOL.
Keywords: Strand Space, Kerberos V, Theorem Proving, Verification, Isabelle/HOL
1. Introduction
The first version of Kerberos protocol was developed in
the mid eighties as part of project Athena at MIT [1].
Over twenty years, different versions of Kerberos
protocols have evolved. Kerberos V (Figure 1 and
Figure 2) is the latest version released by the Internet
Engineering Task Force (IETF) [2]. It is a password-
based system for authentication and authorization over
local area networks. It is designed with the following
aims: once a client authenticates himself to a network
machine, the process of obtaining authorization to access
another network service should be completely trans-
parent to him. Namely, the client only needs enter his
password once during the authentication phase.
As we introduced in the previous paper [3], there are
two novel semantic features in Kerberos V protocol. First,
it uses timestamps to prevent replay attacks, so this
deficiency of the strand space theory makes it difficult to
analyze these protocols. Second, it is divided into three
causally related multiple phases: authentication,
authorization, and service protocol phases. 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, Kerbeors uses 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 both the timestamps and protocol
mixture in a semantic framework.
The aim of this paper is practical. We hope to apply
the extended theory in [3] to the analysis of Kerberos V
protocol. Kerberos V is appropriate as our case study
because it covers both timestamps and protocol mixture
semantical features.
Structure of the Paper: Section 2 briefly introduces
the overview of Kerberos V. Section 3 presents the
formalization of Kerberos V. Sections 4 and 5 prove its
secrecy and authentication goals. We discuss related
work and conclude the paper in Section 6.
2. An Overview of Kerberos V
The protocol’s layout and its message exchanging are
presented in Figure 1 and Figure 2 separately. In the
infrastructure of the Kerberos V protocol, there is a
unique authentication server, and some (not necessarily
only one) ticket granting servers. The latter assumption is
different from that in [4], where only a unique ticket
granting server exists.
*This is a revised and extended version of the homonymous paper ap-
pearing in the Proceedings the Eighth International Conference on Paral-
lel 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 purpose of having
full details. The first author is supported by grants (No.
60833001,
60496321, 60421001) from National Natural Science Foundation of

Y. J. LI ET AL.
57
Figure 1. The layout of Kerberos V.
{ }
}
{
{ }
}
}
{
{ }
}
{
{
2
1. :,
2. :,,,,,,,
3.:,,,, ,,
4.:, ,,,
Tgs
Tgs
B
K
authTicket
K authK
SK
seruTick
AKasA Tgs
KasAA Tgs authK TaA TgsauthK TaKA
ATgsATgsauthKTaA tB
TgsAA B seruK T
→

→



→ 
 

→
Authentication phase
Authorisation Phase
1444442444443
{ }
}
{} {}
}
{ }
3
3
, ,,
5. :,,,,,
6. :
B
SauthK
et
SK seruK
seruK
AB seruK T
ABABseruKTA t
BA t
→
→
Service Phase
14444244443
Figure 2. Kerberos V: message exchanging.
In order to access some network service, the client
needs to communicate with two trusted 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 servers.
Tgs
is a ticket
granting server and it provides keys for communication
between clients and application servers. 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 [1,4] in that nested encryption has been cancelled.
Later we will show that this change does not affect goals
of the protocol.
Detailed explanation about Kerberos V is delayed to
Section 2, where the protocol is formalized in strand
space model with our extensions. Here we only give an
overview of the general principles to guarantee recency,
secrecy and authentication in the design of Kerberos V.
For recency,
• A regular sender should attach a timestamp to
indicate the time when the message is issued; usually
such a message is of the form
{
}
, ,
K
tK K, where
t
is
the time,
K
may be either a session key or long-term
key.
• When a regular receiver the message
{
}
, ,
K
t K K
first he need be ensured of
K
’s secrecy to guarantee
that the message is not froged by the penetrator. Second
he check the recency of the message by comparing the
timestamp
t
with the reception time. More formally, if
the receiving node is
n
, then )( ntime should be no
later than
( )
cracktime Kt
+
, meaning that this message
cannot be cracked at
( )
time n
, which in turn indicates
that the message
{
}
, ,
K
t K K is recent.
For an encrypted message
{
}
K
h
, the secrecy of a
part of the plain message h also comes from both the
secrecy of
K
and the recency of the message
{
}
K
h
itself. That is to say, when a regular receives
{
}
K
h
at
time
t
, it must be ensured that the aforementioned two
conditions must be guaranteed until
t
. From this, we
can see that recency and secrecy are closely related with
each other in a timed protocol framework.
Unsolicited tests are the main mechanism to guarantee
authentication. Because a guarantee of the existence of a
regular node can be drawn from an unsolicited test, a
regular agent uses unsolicited test to authenticate its
regular protocol participant in Kerberos V.
Now let us briefly review the main theoretical results
in [3], which will be used in this work. For interesting
readers, refer to [3] for preliminary definitions.
If an agent is not a penetrator then his shared key
cannot be penetrated, which is formalized as follows:
Axiom 1 If A
∉
Bad
, then
P
K∉
A
K .
Lemma 1 is the main technique used to reason about
authentication guarantee of a node
n
which is an
unsolicited test for an encrypted term of the form
{
}
K
h
(e.g., the tickets
{
}
, ,,
A
a
K
A TgsauthKT ,
{
}
,
authK
A t ,
and so on). That is to say, regular agents can use an
unsolicited test with other properties of the protocol to
guarantee that the agent who originates the term
{
}
K
h
should be an intended regular agent.
Lemma 1 (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

.
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
. A strand’s

Y. J. LI ET AL.
58
receiving nodes get messages 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.
Lemma 2 Let
m
be a positive node in a bundle ,
B
a
be an atomic message that uniquely originates at a
regular node
n
,
M
be a message set such that
(
)
,,,,,
B
nmaMsuite and
(
)
(
)
'
term msynth M
∈
for any
node such that
,
'
m m
+
⇒
and
(
)
(
)
,
term msynth M
∉
then
m
is regular
.
We will illustrate these general principles in detail in
the next sections when we formalize the semantics and
prove secrecy properties of Kerberos V.
3. Formalizing Kerberos V
To model the time for a penetrator to break a message
encrypted by a long-term shared key or a session key, we
define two constants imeshrKcrackt and ktimesessionKcr .
The crack time of any regular agent’s long-term shared
key is the constant shrKcracktime,
Axiom 2
() = shrKcracktime
A
cracktime K , for any regular
agent
A
in Kerberos V.
The crack time of any session key originated by an
authentication server is the constant sessionKcrktime.
Axiom 3
() =sessionKcrktime
cracktime authK , for any
session key authK originated by Kas .
The trace
tr
specifications of the regular strands of
Kerberos V (see Figure 2) are defined as predicates:1
1) Part I (Authentication Phase)
• Ag-I ],,,,,,,[
101
ttauthTicketTauthKTgsAi
a
iff
{ }
{
{ }
}
0
1 1
( , ,,),
() =(,,,
, ,,)
aKA
tA Tgs
tr itauthTicket
A TgsauthKT
 
 
+
 
 
−
 
 
 
 
where TGSs
∈
Tgs and imeshrKcrackt
1
≤−
a
Tt .
• AS ],,,,,[
10
ttauthKTgsAas iff
{ }
{ } {
{ }



















+
−
),,,
,,,,,,(
),,,,(
=)(
1
11
0
A
K
Tgs
K
tauthKTgsA
tauthKTgsAt
TgsAt
astr
where TGSs
∈
Tgs .
In the first phase, when Kas issues the second
message
{ }
{
{ }
}
,,,,,, ,
A
Tgs
aa K
K
A TgsauthKTA TgsauthKT ,
authK is the session key that will be used for the client
A
to communicate with a ticket grant server Tgs ,
Kas attaches
a
T
with the message to indicate when
this message is sent; if
A
receives this message at time
1
t
,
A
will check the condition
1
shrKcracktime
a
t T − ≤
to ensure the recency of this message. At the end of this
phase,
A
obtains a ticket authTicket and the session
key authK to communicate with Tgs.
2) Part II (Authorization Phase)
• Ag-II ,,,,,,,[
2S
TservKBauthTicketauthKAi
],,
32
ttservTicket iff ∧∃
21101
.,,,, iittTTgsi
a
a
Ag-I ∧ ],,,,,,,[
101
ttauthTicketTauthKTgsAi
a
( )
{
{ }
{
{ }
2
2
2
3
( , ,,
,,),
=( ,,,
, ,,)
authK
SauthK
t authTicket
A tB
tr it servTicket
A BservKT
 
+
 
 
 
−
 
 
 
where TGSs
∈
Tgs and imeshrKcrackt
3
≤−
a
Tt and
ktime.sessionKcr
3
≤−
S
Tt
• TGS
a
TBservKauthKTgsAtgs ,,,,,,[ , ],,
100
ttT iff
{ }
{
{ }
{ } {
{ } }
















+
−
),,,
,,,,,,(
),,,
,,,,,,(
=)(
1
11
0
0
authK
B
K
authK
Tgs
K
a
tservKBA
tservKBAt
BTA
TauthKTgsAt
tgstr
where TGSs,
∈
Tgs TGSs,
∉
B
1
sessionKcrktime
t
+ ≤
shrKcracktime
a
T+ .
In the second phase, the situation is more complex.
Both Tgs and
A
need to check whether their received
messages are recent by the same mechanism. Furthermore,
Tgs
also need ensure a side condition that
1
sessionKcrktime shrKcracktime
a
t T+≤ +
to guarantee that the application server
B
only receives
a recent service ticket. Informally speaking, this condition
means that
Tgs
can guarantee any
authK
that he
receives can only be compromised later than
servK
which is associated with the
authK
. We will comment
this side condition in analysis in the third phase. At the
end of this phase,
A
obtains a ticket
servTicket
and
the session key
servK
to communicate with
B
.
1
For simplicity, we assume any trace of a regular agent always re
spects
the time order in Kerberos V protocol, and we do not include
this side
condition in the trace specifications.

Y. J. LI ET AL.
59
3) Part III (Service Phase)
• Ag-III
34 5
[ ,,,,,]
iA servKservTicket tt
iff
10 1 223
,,,,, ,,,,,,
a S
iTgsauthKTttiauthTicketB Ttt
∃ .
(
)
3
tr i
=
{{ }
( )
{ }
( )
4 4
5 4
, ,,,,
, ,
servK
servK
tservTicketA t
t t
 
+
 
∧
 
−
 
 
Ag-I
10 1
[ ,,,,,,,]
a
iA TgsauthKTauthTickettt
∧
Ag-II
2
[ ,,,,,,
S
iA authKauthTicketBservKT
,
2 31223
, , ]
servTicket ttiiii
∧ ∧
a a
where T gs
∈
TGSs
,
5
shrKcracktime
a
t T−≤ and
5
sessionKcrktime.
S
t T− ≤
• Apps
40 1
[, , ,,,,,]
S
appsA B servK TTtt
iff
()=
tr apps
{ }
{
{ }
}
{ }
0 4
1 1
( , ,,,,,,),
( ,,)
SservK
KB
servK
tABservKTAT
t t
 
−
 
 
+
 
 
where
0
sessionKcrktime
S
t T− ≤ .
In the last phase, it is subtle for the application server
B
to check the recency of the message
{ } { }
{
}
4
, ,,,,
SservK
KB
ABservKTA T . From the ticket
{
}
,,, S
K
B
A B servKT ,
B
knows that
Tgs
must have
issued
{} {}
{
}
4
, ,,,, ,,,
S S
K authK
B
ABservKTAB TservKT
at time
S
T
. The potential compromise of
servK
is
from the message
{
}
,,, S
authK
A B servKT . A penetrator
can either directly break
{
}
,,, S
authK
A B servKT to
obtain
servK
, or have
authK
first then decrypt the
message
{
}
,,, S
authK
A B servKT to obtain
servK
. Since
authK
is also a session key which is originated by
Kas
in an earlier time than
s
T
, the guarantee for the
confidentiality of
authK
is of extreme importance. The
corresponding ticket
{
}
, ,,
Tgs
aK
A TgsauthKT is not
available for
B
,
B
cannot know the creation time of
authK
. So
B
cannot directly check whether
authK
has been compromised. Fortunately, if Tgs can guarantee
that any
authK
which it receives will be compromised
later than
servK
, associated with the
authK
, then it is
enough for
B
to check
0
sessionKcrktime
S
t T− ≤ to
ensure that the authK has not been compromised. At
the end of this stage,
A
and
B
authenticate each
other, and
A
can access the service provided by
B
.
The authentication server Kas must obey the following
principles to generate a session key
authK
:
•
authK
must never be known initially to a
penetrator, i. e.,
P
K ∉authK ;
•
authK
must be uniquely originated;
•
authK
is a symmetric key;
•
authK
must not be the same as an agent’s long-
term shared key.
We summarize these principles as the following
axiom:
Axiom 4 For any authentication server strand
as
such that
0 1
[,,,,, ]
asA TgsauthKtt
AS , we have
P
K ∉authK ,
authK
uniquely originates in
( ,1)
as
,
1
=
authK authK
−
, and
B
authK K
≠ for any agent
B
.
A ticket grant server creates the session key
servK
by three principles, which are similar to those which the
authentication server obeys to create the session key
authK
.
Axiom 5 For any ticket grant server strand
tgs
such
that
0
[, ,,,,,,,
a
tgsA TgsauthKservKBTT
T G S
0 1
, ]
t t
,
P
K ∉servK ,
servK
uniquely originates in
( ,1)
tgs
,
1
=
servK servK
−
, and
B
servK K
≠ for any agent
B
.
In the following two subsections, we verify the
secrecy and authentication properties of Kerberos V. We
use similar ways for representing these security
properties as in [5]. However, we may need formulate
secrecy properties with temporal restrictions when we
discuss them in a timed framework. A value
v
is secret
for a protocol if for every bundle
C
of the protocol the
penetrator cannot receive
v
in cleartext until some time
t
; that is, there is no node
n
in
C
such that
() =
term nv
and
( )
time nt
≤
. For Kerberos V, we
mainly discuss the secrecy of a long-term key of a
regular agent, and
,
authK
servK
issued by servers.
Authentication properties are specified as usual: for a
participant
B
(e.g. acting as a responder), for a certain
vector of parameters
x
r
, if each time principal
B
completes a run of the protocol as a responder using
x
r
supposedly with
A
, then there is a run of the protocol
with
A
acting as an initiator using
x
r
supposedly with
B. And this is formalized as follows: there is a responder
strand
Resp
(
x
r
) and the
i
-th node of the strand is in a
bundle
C
, then there is an initiator strand Init (
x
r
) and
some
j
-th node of the initiator strand is in
C
.
In order to prove the secrecy of a long-term key
A
K
,
we only need use the well-founded induction principle
on bundles. But the knowledge closure property on
penetrators is needed when we prove the secrecy of some
session key
authK
or
servK
. For instance, in order to
prove the secrecy of
authK
, we construct a set
{ }{ }
{
}
,,,, ,,,
A
df aa
K K
Tgs
MATgs authKTATgsauthK T=
{
}
| .
t authKt
∪ ⊄

Y. J. LI ET AL.
60
We will show that for any node
m
in a Kerberos
bundle
,
B
if )( mtermauthK
⊏
and
( )
time m
≤
shrKcracktime,
a
T +
then
( )
term m
must be in
( ).
synth M
Intuitively, this
fact holds because both the penetrator and regular strands
can only emit a message which is in
( )
synth M
. The
penetrator can not decrypt or crack the messages
{
}
, ,,
A
a
K
A TgsauthKT and
{
}
, ,,
aK
Tgs
A TgsauthKT
until time
.
shrKcracktime,
a
T + so it can only synthesize
any messages which is in
( );
synth M
except a unique
authentication server strand, any other regular strand can
not emit any message which has
authK
as a subterm
until that time. But for the authentication server strand,
he can only emit
{} {}
1 1
,, ,,,, ,
K K
Tgs A
A TgsauthKtA TgsauthKt
 
 
 
which is still in
( ).
synth M
Our formal proof is by
contradiction. If not so, by the well-founded induction
principle on
B
, we have a minimal element
m
such
that )( mtermauthK
⊏
and
( )().
term msynth M
∉ By
the knowledge closure property, we can exclude the
cases when
m
is in a penetrator strand. By case
analysis on the form of the trace of regular strands, we
can also exclude the case when
m
is in a regular strand.
Thus, a contradiction is concluded.
In the following two sections, we give the detailed
proof on the secrecy and authentication properties to
show how to apply the proof techniques aforementioned.
Note that we also have formalized all the proofs in
Isabelle/HOL, and the proof scripts can be obtained at
[6]. The paper proof here can be viewed as a text account
of the mechanical proof scripts at [6].
4. Proving Secrecy Goals
In Kerberos V, a long-term key of a regular agent is
never sent in the network, so it cannot be compromised.
Let
B
be a bundle of Kerberos V. For any node in the
bundle, the long-term key of a regular agent cannot be a
part of the term of the node. In order to prove this lemma,
we only need the well-founded induction principle on
bundles.
Lemma 3 Let
B
∈
n . If Bad
∉
A , then
A
Knterm ≠ )( .
Proof. Let
)}(|{= xtermKxxP
Adf
⊏
∧∈ B
We show that
P
is empty by contradiction. If there
is a node Pn
'
∈ , then by the well-foundedness of a
bundle, there exists a node
m
such that
m
is minimal
in
P
. Namely,
B
∈
m , )( mtermK
A
⊏
, and for all
B
∈
'
m , if mm
'
B

then )(
'
A
mtermK
⊏
/
.
We prove that the sign of
m
is positive. If −=)(msign ,
then by upward-closed property of a bundle there must
be another node
''
m in the bundle
B
such that
+=)(
''
msign and mm
''
→ . This contradicts with the
minimality of
m
. Then
m
is either in a regular strand
or in a penetrator strand.
• CASE 1:
m
is in a regular strand.
There are six cases. Here we only analyze the cases
when
m
is in an authentication server strand
∈
as
AS
],,,,,[
10
ttauthKTgsAas or
m
is in a client strand
∈
i Ag-II ,[i ,A ,authK ,authTicket ,B,servK ,
S
T
,servTicket
,
2
t
]
3
t . The other cases are either straightforward
or can be analyzed in a similarly.
If
m
is in an authentication server strand such that
∈
as
AS ,[ as ,A ,Tgs ,authK ,
0
t].
1
t By inspection on
the trace form of the strand, we have ,1)(= asm ,
,1)( astermK
A
⊏
, and
{} {}
1 1
(,1)=, ,,,, ,,
K K
Tgs A
termasA TgsauthKtA TgsauthKt
 
 
 
,
then
{
}
1
, ,,
AK
Tgs
KA TgsauthKt
⊏
or
{
}
1
, ,,
A
K
A
KATgsauthKt
⊏
.
In both cases, we can conclude that .=authKK
A
But
this contradicts with Axiom 4. If
m
is in a client strand
such that
[ ,
i i
∈ −
Ag II
,A ,authK ,authTicket ,B
,servK ,
S
T ,servTicket ],
32
tt . By inspection on the trace
form of the client strand, we have ,0)(= im ,
,0)(itermK
A
⊏
, and
{ }
{
}
2
( ,0) =,,,,
authK
term iauthTicketA tB
then .authTicketK
A
⊏
But by the definition of the client
strand, there exists some client strand
11
suchthatii
a
iand Ag- I
,[
1
i,A
,Tgs ,authK
,
a
T ,authTicket ].,
10
tt
From the definition of the strand
,
we have
,1).(
1
itermauthTicket
⊏
From this and
A
K
⊏
,authTicket we have (1) ,1).(
1
itermK
A
⊏
From
1
i
a
,i we have (2)
,1)(
1
i
⇒
,0).(i From (1) and (2), we
can conclude that
m
is not minimal in
P
. This
contradicts with the minimality of
m
.
• CASE 2:
m
is in a penetrator strand
p
.
Here we only analyze the cases when
p
is either
K
K (key strand) or
hg
C
,
(concatenation). Other cases
are either straightforward or can be analyzed in a similar
way.
-
p
is
K
K . We have ,0)(= pm and KK
A
⊏
.
Then
P
K ∈KK
A
= . This contradicts with Axiom 1.
-
p
is
hg
C
,
. We have ,2)(= pm
'
and
{
}
hgK
A
,
⊏
.
By the definition of
⊏
, we have gK
A
⊏
, or hK
A
⊏
. If
gK
A
⊏
, then ,0)( ptermK
A
⊏
. This contradicts with the
minimality of
m
. The case when hK
A
⊏
can be
analyzed similarly.

Y. J. LI ET AL.
61
If an authentication ticket
{
}
, ,,
A
a
K
A TgsauthKT or
{
}
, ,,
Tgs
aK
A TgsauthKT occurs as a subterm of a node in
B
,
A
is not compromised, and Tgs is a ticket
granting server, then it can be guaranteed that there must
be an authentication server strand
as
in which
{
}
, ,,
A
a
K
A TgsauthKT and
{
}
, ,,
Tgs
aK
A TgsauthKT
originate
at time
a
T . Therefore,
a
T is the earliest time when
{
}
, ,,
A
a
K
A TgsauthKT and
{
}
, ,,
Tgs
aK
A TgsauthKT
occur in
B
. With the specification of the origination of the key
authK by Kas (formulated by Axiom 4), we also are
ensured that
a
T is the earliest time when authK
occurs in
B
. The minimal property of
a
T will be used
in the proof of Lemma 5.
Lemma 4 Let
B
∈
n , Bad
∉
A , and TGSs
∈
Tgs . If
{
}
, ,,
A
a
K
A TgsauthKT or
{
}
,,,( )
A
aK
A TgsauthKTtermn
⊏
,
then there exists an authentication server strand
as
such that ,,,[ TgsAasAS ],,
0a
TtauthK for some
0
t ,
B
∈ ,1)( as , and )( ntimeT
a
≤ .
Proof.
Here we only prove the case
{
}
, ,,
A
a
K
A TgsauthKT
⊏
(
)
. nterm The other case can be proved in a similar
way. First we prove that (1)
n
is an unsolicited test for
the term
{
}
, ,,
A
a
K
A TgsauthKT We only need prove
that
A
K must be regular w.r.t.
n
. By Lemma 3, there
is no node
m
in
B
such that
(
)
,=
A
Kmterm so
A
K
must be regular w.r.t.
n
.
From (1), by Lemma 1, there exists a positive regular
node m in
B
such that nm
B

and
{
}
, ,,
A
a
K
A TgsauthKT
)( mterm
⊏
and
{
}
, ,,
A
a
K
A TgsauthKT
⊏
/
)(
'
mterm for
any node
'
m such that mm
'
B

.
From nm
B

and
B
is a bundle, we can easily
conclude )()( ntimemtime≤ and .
B
∈
m
Now we prove that
m
must be in an authentication
server strand. From the fact that
m
is regular, then we
have six cases, here we select two cases when
m
is in
an authentication server strand
as
such that AS as[,
'
A
,
'
Tgs
,
'
authK
,
0
t
,
1
]
t
or in an ticket granting server
strand
tgs
such that tgs[TGS ,
'
A
,Tg ,
'
authK , servK ,
'
B
,
'
a
T ,
0
T ,
0
t , ].
1
t
•
m
is in an authentication server strand
as
such
that AS as[,
'
A
,
'
Tgs ,
'
authK ,
0
t , ].
1
t By inspection on
the form of the strand,
(
)
,1= asm because
m
is
positive. Obviously
{ }{ }
1 1
( )
, ,,,, ,,
Tgs A
'' ''''
K K
term m
A TgsauthKtATgsauthKt
′ ′
=
 
 
 
By
{
}
, ,,
A
a
K
A TgsauthKT
⊏
),(mterm we have either (2)
{
}
, ,,
A
a
K
A TgsauthKT
⊏
{
}
1
, ,,
Tgs
' ''
K
A TgsauthKt
′
or (3)
{
}
, ,,
A
a
K
A TgsauthKT
⊏
{
}
1
, ,,
A
' ''
K
A TgsauthKt
′
. From (2),
we have
'
A
A
=
and
'
TgsTgs = and
'
authKauthK =
and
1
=tT
a
, so AS ].,,,,,[
0a
TtauthKTgsAas Case (3)
can be prove similarly.
•
m
is in an ticket granting server strand such that
TGS ].,,,,,,,,,[
100
ttTTBservKauthKTgAtgs
'
a
'''
By
inspection on the form of the strand,
(
)
,1= tgsm
because
m
is a positive node. Obviously
{ }{}
{
}
1 1
(),,,,, ,,.
B
' '' '
K authK
termmABservK tABservK t
′
′
=
From
{
}
, ,,
A
a
K
A TgsauthKT
⊏
),(mterm we have
either (2)
{
}
, ,,
A
a
K
A TgsauthKT
⊏
{
}
1
, ,,
B
' '
K
ABservK t
′
or (3)
{
}
, ,,
A
a
K
A TgsauthKT
⊏
{
}
1
, ,,
' '
authK
ABservKt
′
.
From (2), we can prove that ,=
'
BTgs then by the
assumption , TGSs
∈
Tgs we have . TGSs ∈
'
B But by
the definition of the ticket granting server, we have
∉
'
B TGSs . Therefore a contradiction is obtained. Case
(3) can be proved similarly.
Once the authentication tickets
{
}
, ,,
A
a
K
A TgsauthKT
or
{
}
, ,,
Tgs
aK
A TgsauthKT are created by the authentication
server Kas at
a
T , then the session key authK will
be not compromised until the time imeshrKcrackt +
a
T .
Lemma 5 Let
B
∈
n , Bad
∉
A , and TGSs
∈
Tgs . If
{
}
, ,,
A
a
K
A TgsauthKT or
{
}
,,,( )
Tgs
aK
A TgsauthKTtermn
⊏
,
then for any node
B
∈
m such that ( )
a
time mT
≤ +
shrKcracktime
, authKmterm ≠ )( .
Proof. First we define two sets.
{
}
{ }
{ } tauthKt
TauthKTgsA
TauthKTgsA
M
Tgs
K
a
A
K
a
df
⊏
/
∪










=|
,,,
,,,,
={.()shrKcracktime
df a
Pm mtimemT
∈ ∧≤+∧
B
(
)
( )}
term msynthM
∉ .
We show that for any node
B
∈
m such that
imeshrKcrackt)( +≤
a
Tmtime ,
(
)
Msynthmterm ∈)( . In
order to prove this, we only need show
P
is empty. We
prove the assertion by contradiction. If
P
is not
empty
,
then by the well-foundedness of a bundle, (1)
there exists a positive node
m
such that
B
∈
m ,
(
)
,)(Msynthmterm ∉ imeshrKcrackt)( +≤
a
Tmtime ,
and for all
B
∈
'
m , if mm
'
B

then
( )
term m
∈
(
)
synth M
.
First from the fact that
{
}
, ,,
A
a
K
A TgsauthKT or
{
}
,,,( )
Tgs
aK
A TgsauthKTtermn
⊏
by the Lemma 4, then

Y. J. LI ET AL.
62
there exists an authentication server strand
as
such that
,,,[ TgsAas AS ],,
0a
TtauthK for some
0
t ,
B
∈,1)(as ,
and )(ntimeT
a
≤ . From the definition of AS and
Axiom 4
,
we have (2) authK uniquely originates at
,1)(as and .=,1)(
a
Tastime
Next we prove that (3) ,M suite( ,authK
,
m
,1),(as
B
). Here we need show both
{
}
, ,,
A
a
K
A TgsauthKT and
{
}
, ,,
Tgs
aK
A TgsauthKT are components in
B
. From
A
∉
Bad and Tgs
∈
TGSs , by Lemma 3, we
have that neither
A
K nor
Tgs
K is compromised, and
they are symmetry, therefore B ),,(
1
mKregular
A
−
and
),,(
1
B mKregular
Tgs
−
; furthermore from )(mtime
≤
a
T
+
,imeshrKcrackt and by Axiom 2, )(
A
Kcracktime
=
ime,shrKcrackt with (2), we have )(mtime
≤
+ ,1)(astime
,)(
A
Kcracktime similarly we have )(mtime
≤
,1)( astime
( ),
Tgs
cracktime K + so (3) is proved
.
From (1), we have for any
'
m such that mm
' +
⇒,
term
(
)
Msynthm
'
∈ )( . With (2)(3), by Lemma 2, we
have
m
must be in a regular strand i , then there exist
six cases. Here we analyze the cases when
AS i[,
'
A
,' Tgs ,
'
authK ,' t
0
, ]
1
t , other cases are more
simpler
.
If
m
is in an authentication server strand
AS
i[,
'
A
,' Tgs ,
'
authK ,' t
0
, ].
1
t By inspection on the
form of the strand,
(
)
,1= im because
m
is positive.
Obviously
{ }{ }
1 1
( )
,,,,,,,
Tgs A
' ''' ''
K K
term m
A TgsauthKtA TgsauthKt
′ ′
=
 
 
 
.
Obviously authK
⊏
term
),(m otherwise
term
)(m
∈
.M Therefore
{
}
1
, ,,
A
' ''
K
authKATgsauthKt
′
⊏ or
{
}
1
, ,,
Tgs
' ''
K
authKATgsauthKt
′
⊏ then
.
'
authKauthK
=
From the definition of Axiom 4, we have authK
uniquely originates from the strand i . Combining with
(2), we have ias = , then
'
A
A
=
,
'
TgsTgs = ,
a
Tt =
1
,
so
{ }{}
( )
, ,,,, ,,
( )
a a
K K
Tgs A
term m
A TgsauthKTA TgsauthKT
synth M
 
=
 
 
∈
This contradicts with the fact ).()( Msynthmterm ∉
Therefore for any node
B
∈
m such that ≤)(mtime
imeshrKcrackt+
a
T,
(
)
Msynthmterm ∈)( . Next we
only need prove that
(
)
MsynthauthK ∉. We prove by
contradiction, if
(
)
,MsynthauthK ∈ by the rule inversion
of definition of synth, we have ,MauthK ∈ this
contradicts with the definition of
M
.
In order to prove the conclusion of Lemma 5, we need
the conclusion of Lemma 4, which ensures us that a
penetrator cannot crack the term
{
}
, ,,
a
K
A
A TgsauthKT
(or
{
}
,,, aK
Tgs
A TgsauthKT) to obtain .authK Because
the earliest time when authK occurs in
B
is
a
T and
authK can only occur in
{
}
, ,,
a
K
A
A TgsauthKT (or
{
}
,,, aK
Tgs
A TgsauthKT) the penetrator cannot crack
such a term until imeshrKcrackt+
a
T, and what he can
only do is to synthesize some term from
M
. Therefore,
authK must be safe until that time. Furthermore, the
intermediate result of this proof tells us that )(mterm
must be in
(
)
Msynth for any node
B
∈
m such that
ime.shrKcrackt)(+≤
a
Tmtime
If both the tickets
{
}
, ,,
S
authK
A B servKT and
{
}
, ,,
a
K
A
A TgsauthKT
occur as a part of the term of a node in
B
,
A
and
B
are not compromised, and
B
is not a ticket grant server,
and authK is still not compromised at the time when
the above two tickets occur, then it can be guaranteed
that
A
must have passed the first and second phases of
the protocol, and a ticket grant server strand
tgs
must
exist in
B
, where two tickets
{
}
, ,,
S
K
B
A B servKT and
{
}
, ,,
S
authK
A B servKT
are issued for some session key authK. Similar to
Lemma 4, this lemma ensures us that
S
T is the earliest
time when servK occurs in
B
, and this minimal
property is needed in the proof of Lemma 7.
Lemma 6 Let
B
∈
nm,, Bad
∉
A, TGSs
∈
Tgs . If
both
{
}
,,,( )
aKA
A TgsauthKTtermm
⊏
,
and
{
}
,,,( )
SauthK
A B servKTterm n
⊏
and imeshrKcrackt)( +≤
a
Tntime, then there exists a
ticket granting server strand
tgs
such that ,,[ AtgsTGS
],,,,,,,
00 Sa
TtTTBservKauthKTgs for some
0
T,
0
t,
,1)(tgs
B
∈
and )(ntimeT
S
≤.
Here we only give the proof sketch of this lemma.
First we need show that (1)
n
is an unsolicited test for
{
}
, ,,
S
authK
A B servKT in
B
. We need prove
(
)
.,,
B
nauthKregular This can be ensured by Lemma 5.
Because ime,shrKcrackt)( +≤
a
Tntime we have
( )
'
term nauthK
≠for any node
'
nsuch that
()().
'
time ntimen
≤ From (1), we can show that there is
a regular node
'
n such that
'
n n
B

and
{
}
, ,,
SauthK
A B servKT
⊏
term
)( ' n and

Y. J. LI ET AL.
63
{
}
, ,,
SauthK
A B servKT
⊄
term
)( ' m for any node
'
m
such that '' nm
B

. By the case analysis on the form of
regular strands, we can prove that
'
n must be in a ticket
granting server strand
tgs
such that
[ ,
tgs
TGS
,
A
,
Tgs
,
authK
,
servK
,
B
,
a
T
0
,
T
0
,
t
]
S
T
for some
0
T,
0
t, ' ntgs=,1)( and )(= '
SntimeT .
Moreover, by the fact a ticket
{
}
, ,,
S
authK
A B servKT
is originated at time
S
T, then the session key servK
will not be compromised until the time
ktimesessionKcr +
S
T.
Because during the interval from
S
T to
ktimesessionKcr +
S
T,
neither
{
}
, ,,
S
authK
A B servKT will be cracked, nor the
session key authK can be obtained by a penetrator to
decrypt the ticket
{
}
, ,,
S
authK
A B servKT.
Lemma 7 Let
0
m,
B
∈
n, Bad
∉
BA,, TGSs
∈
Tgs .
If both
{
}
, ,,
a
K
A
A TgsauthKT
)(
0
mterm
⊏
and
{
}
,,,( )
SauthK
A B servKTterm n
⊏
,
and imeshrKcrackt)( +≤
a
Tntime, then for any node
B
∈
m such that ktimesessionKcr)( +≤
S
Tmtime ,
servKmterm ≠ )( .
Proof. First we define:
{
}
{ }
{ } .|
,,,
,,,,
=tservKt
TservKBA
TservKBA
M
authK
S
B
K
S
df
⊏
/
∪










We will show that for any node
B
∈
m such that
ktimesessionKcr)( +≤
S
Tmtime ,
term
(
)
.)( Msynthm ∈
We prove the assertion by contradiction.
Let
.{= mP
df
m
∈
B
∧
)(mtime
≤
S
T
+
∧ktimesessionKcr
term
)(m
∉
(
)
}.Msynth If
P
is not empty
,
then by
the well-foundedness of a bundle, (1) there exists a
positive node
m
such that
B
∈
m , )(mtime
≤
S
T
+
ktimesessionKcr ,
term
(
)
,)( Msynthm ∉ and for all
B
∈
'
m , if mm
'
B

then
term
(
)
Msynthm
'
∈)( .
From the fact
{
}
, ,,
a
K
A
A TgsauthKT ),(
0
mterm
⊏
by Lemma 4, there exists an authentication server strand
as
such that ,,,[ TgsAas AS ],,
0 a
TtauthK for some
0
t ,
B
∈,1)( as . From the definition of AS , we know (2)
authK uniquely originates at ,1)(as and
a
Tastime =,1)( .
From the fact that
{
}
, ,,
a
K
A
A TgsauthKT
⊏
)(
0
mterm
and
{
}
, ,,
a
K
A
A TgsauthKT
⊏
),(nterm by Lemma 6,
then there exists a ticket granting server strand
tgs
such that ,[tgs TGS ,A ,Tgs ,authK ,servK ,B,
a
T ,
0
T
,
0
t ]
S
T for some
0
T ,
0
t . From the definition of
TGS and Axiom 5, we have (3) servK uniquely
originates at ,1)(tgs , ,=,1)(
S
Ttgstime
{
}
, ,,
aKTgs
A TgsauthKT
⊏
term
,0),(tgs
and imeshrKcracktktimesessionKcr +≤+
aS
TT . From
{
}
, ,,
aKTgs
A TgsauthKT
⊏
term
,0),(tgs by Lemma 4,
we can easily conclude that ,0)(tgstimeT
a
≤ , then (4)
,1).(tgstimeT
a
≤
Next we prove that (5) ),1),(,,,(
B
tgsmservKMsuite.
Here we need show both
{
}
, ,,
a
K
B
A TgsservKT and
{
}
, ,,
S
authK
A B servKT are components in
B
. From
Bad
∉
B , by Lemma 3, we have
B
K are never
compromised, similar to counterpart in Lemma 5, we can
prove that
(
)
.,,
1
B mKregular
B
−
From
imeshrKcracktktimesessionKcr +≤+
aS
TT
and ktimesessionKcr)( +≤
S
Tmtime , we have (6)
ime,shrKcrackt)(+≤
a
Tmtime with (4), we have
)(mtime
≤
+,1)(tgstime ).(
B
Kcracktime From (6)
and
{
}
,,,( )
aKA
A TgsauthKTtermm
⊏
for any node
'
n
such that )(
'
ntime
≤
),(mtime we have
ktimesessionKcr)( +≤
S
'
Tntime ,
then )(
'
ntime
≤
eshrKcrktim+
a
T , by Lemma 5,
term
)(
'
n
≠
;authK by Axiom 4, authK is symmetry,
therefore
1 −
authK
=
,authK so
(
)
.,,
1
B
mauthKregular
−
From ktime,sessionKcr)( +≤
S
Tmtime and by Axiom 4
again, we have )(authKcracktime =ktime,sessionKcr
then +≤
S
Tmtime)(),(authKcracktime with (3), we
have ≤)( mtime +,1)( tgstime).( authKcracktime
Therefore (5) is proved
.
From (1), we have for any
'
m such that mm
'+
⇒ ,
term
∈)(
'
m synth
(
)
M . With (2)(5), by Lemma 2, we
have
m
must be in a regular strand i , then there exists
six cases. Here we analyze the cases when ,[i AS ,
'
A
,
'
Tgs ,
'
authK ,
0
'
t]
1
t or ,[i TGS ,
'
A,
'
Tgs ,
'
authK
,
'
servK ,
'
B,
'
a
T,
0
'
T,
0
'
t]
'
S
T , other cases are more
simpler.
If ,[i AS ,
'
A,
'
Tgs ,
'
authK ,
0
'
t],
1
t then by inspection
on the form of the strand,
(
)
,1= im because
m
is
positive. Obviously
{ }{ }
1 1
( )
, ,,,, ,,
K'
Tgs
' ''' ''
KA
term m
A TgsauthKtA TgsauthKt
′
 
 
=
 
 
 
.
Obviously servK
⊏
term
),(m otherwise ∈)(mterm
.M Therefore
{
}
, ,,
A
' ''
aK
servKA TgsauthKT
′
⊏ or
{
}
, ,,
Tgs
' ''
aK
servKA TgsauthKT
′
⊏
then servK
=
.
'
authK From Axiom 5, we have
authK uniquely originates from the strand i .
Combining with (3), we can conclude i is both an
authentication server strand and a ticket granting server

Y. J. LI ET AL.
64
strand, obviously this is a contradiction.
If ],,,,,,,,,[
00
'
S
'''
a
'''''
TtTTBservKauthKTgsAiTGS ,
then by similar argument, we can prove that
'
servK
=
,servK from Axiom 5, we have servK uniquely
originates from i , with (3), we have i
=
tgs
, we can
prove that
{ }{ }
{ }
( )
, ,,,, ,,
S S
K authK
B
term m
A B servKTA B servK T=
then
term
∈)(m synth
( )
M
this contradicts with (1).
At last we only need prove that
term
∈)(m synth
( )
M
implies that
term
servKm ≠)( , this is similar to
counterpart in Lemma 5.
Both Lemma 6 and Lemma 7 have the assumption that
{
}
, ,,
a
K
A
A TgsauthKT is a subterm of the node
n
, which
can guarantee that authK must be a session key originated
by an authentication server strand. The assumption
imeshrKcrackt)( +≤
a
Tntime is used to guarantee that
authK is still safe at )(ntime . Besides, the two terms
{
}
, ,,
S
authK
A B servKT and
{
}
, ,,
a
K
A
A TgsauthKT are
intelligible for the client
A
, so these two lemmas are
secrecy properties in the view of
A
.
In Lemmas 6 and 7, both
{
}
, ,,
S
authK
A B servKT and
{
}
, ,,
a
K
A
A TgsauthKT are unintelligible for an application
server
B
because authK and
A
K cannot be known
by
B
. So the two properties are not in
B
’s view.
B
can only receive a message such as
{
}
, ,,
S
K
B
A B servKT ,
can it be ensured that servK is confidential when he
receives the message
{
}
, ,,
S
K
B
A B servKT
? The following
two lemmas are about the confidential information
inferred from the message
{
}
, ,,
S
K
B
A B servKT . They
are secrecy properties in
B
’s view.
Once a server ticket such as
{
}
, ,,
S
K
B
A B servKT occurs
in a bundle, where
A
and
B
are not compromised,
and
B
is not a ticket granting server, then conclusions
similar to those in Lemma 6 and Lemma 7 can be drawn.
Lemma 8 Let
B
∈
n , Bad
∉
BA, , and TGSs
∉
B .
If
{
}
,,,( )
SKB
A B servKTtermn
⊏
, then there exists a
ticket grant server strand
tgs
such that ,,[ AtgsTGS
],,,,,,,
00 Sa
TtTTBservKauthKTgs for some Tgs , authK ,
a
T ,
0
T , ,
0
t
B
∈,1)(tgs and )(ntimeT
S
≤ .
Lemma 9 Let
B
∈
n , Bad
∉
BA, , and TGSs
∉
B .
If
{
}
,,,( )
SKB
A B servKTtermn
⊏
, then for any node
B
∈
m such that ktimesessionKcr)( +≤
S
Tmtime ,
servKmterm ≠)( .
Here we summarize the main ideas used in the above
proof of secrecy properties.
• For a long-term key of a regular agent, its secrecy is
easily inferred because it is never sent as a part of a
message. We only need the well-founded induction
principle on bundles to prove this.
• But for a short session key authK or servK , the
cases are more complex because they are sent as a part in
a message such as
{
}
, ,,
a
K
A
A TgsauthKT or
{
}
, ,,
S
authK
A B servKT .
In kerberos V, a session key such as authK ( servK )
occurs as a part of a term of node
n
which is of the
form
{
}
K
h
,
where
K
can be either a long-term key
or another short session key, and h also contains a
timestamp
t
such as )(
Sa
TT , which indicates the time
when
{
}
K
h
is
.
t
As mentioned before, both secrecy
of
K
and recency of
{
}
K
h
should be guaranteed.
Secrecy of
K
can be directly drawn from other lemmas
on
K
. But for recency checking, firstly we need prove
that the timestamp
t
indeed indicates the time when
{
}
K
h
is originated. Lemmas 4, 6, 9 play a role in
guaranteeing that
t
is the first time when authK
( servK ) is originated. From this and the assumption that
cracktime)( +≤ tntime (
K
), the recency of
{
}
K
h
can
be proved.
5. Proving Authentication Goals
For convenience, we call that a strand i uses a term
{
}
K
h
as an unsolicited test if there is a node
n
is in
the strand i and is an unsolicited test for
{
}
K
h
in a
bundle .
B
Because a guarantee of the existence of a
regular node can be drawn from an unsolicited test, a
regular agent uses unsolicited test to authenticate its
regular protocol participant in Kerberos V.
The client strand in the authentication phase receives
{
}
, ,,
a
K
A
A TgsauthKT as an unsolicited test that authenti-
cates the positive node of the authentication server strand.
The intuition behind this authentication is quite straight-
forward. By case analysis on the form of ,i we have
{
}
, ,,
aKA
A TgsauthKT
⊏
( ,1),
term i
combining with the
assumption that
A
is not compromised, by Lemma 4,
we have
{
}
, ,,
a
K
A
A TgsauthKT can only be originated
by an authentication server. For the sake of brevity, in
the following discussion we use ],,,[yxP K
∗
to denote
],,,[.yxxPx
''
K∃ .
B
is a bundle of Kerberos V.
Lemma 10 Let Bad
∉
A . If i is a client strand in
the authentication phase such that Ag-I ,,,,[ authKTgsAi
],,,
10
ttauthTicketT
a
and
B
∈,1)(i , then there exists an
authentication server strand
as
such that ,,[ AasAS
],*,,
a
TauthKTgs ,
B
∈,1)(as .
The ticket grant server strand uses
{
}
0
,
authK
A T as an
unsolicited test to authenticate the client strand in the
authorization phase. This guarantee is ensured from the
secrecy of authK , which is in turn guaranteed by the
ticket
{
}
, ,,
aK
Tgs
A B authK T . By the trace specification
of a ticket grant server strand, we have that

Y. J. LI ET AL.
65
{} {}
0
, ,,,,
aK authK
Tgs
ABauthKTA T
 
 
 
is received by Tgs earlier than the time
ktimesessionKcr+
a
T ,
by Lemma 5, authK is safe at that time.
Lemma 11 Let Bad
∉
A , TGSs
∈
Tgs . If
tgs
is a
ticket grant server strand such that
[,,
tgs A
TGS
00 1
,,,,,,, ],
a
TgsauthKservKBT Ttt
and
B
∈,0)(tgs , then
there exists a client strand i in the authorization phase
such that
B
∈,0)(i and Ag-II ],,,,,,,,,,[
0
∗∗∗∗∗∗∗ TauthKAi .
Proof. By analysis on the form of
tgs
strand, we
have (1)
{
}
0
,
authK
A T
⊏
,0),(tgs (2)
{
}
, ,,
aK
Tgs
A B authK T
⊏
,0)(tgsterm and ,0)(tgstime
≤
a
T
+
imeshrKcrackt .
From (2), by Lemma 5, we have that
(
)
≠mterm authK
for any
B
∈
m such that
(
)
mtime
≤
,0)(tgstime ,
therefore ),0),(,(
B
tgsauthKregular . With (1), by
Lemma 1, we have (3) there is a positive regular node
m
such that ,0)(tgsm
B

and
{
}
0
,
authK
A T
⊏
( )
term n
and
{
}
0
,
authK
A T
⊄
)(
'
mterm for any node
'
m such
that .mm
'
B

Obviously
B
∈
m .
Now we need prove that
m
must be in a client strand
i in the authorization phase. From the fact that
m
is
regular, then we have six cases, here we select two cases
when (4) m is in a strand i such that Ag-II ,[i ,
'
A,
'
authK
,
'
authTicket ,
'
B,
'
servK ,
'
S
T,
'
servTicket ,
2
t]
3
t or (5)
m
is in a strand i such that
[ ,,,
' '
i AservK
Ag_III
].,,
54
ttservTicket
' Other cases are more simpler.
If (4) holds, then
m
(
)
,0= i because
m
is positive.
From
{
}
0
,( )
authK
A Ttermn
⊏
and
(
)
mterm
=
{ }
{
}
2
, ,,,
'
authK
authTicketA tB
we have either (6)
{
}
0
,
'
authK
A TauthTicket
⊏
or (7)
{
}
{
}
0 2
,,.
'
'
authK authK
A TAt ⊏
If (6) holds, then by the definition of the client strand,
there exists some client strand
1 1
such that
i i
a
iand
Ag-I ,[
1
i,
'
A,
'
Tgs ,
'
authK ,
'
a
T,
'
authTicket ].,
10
''
tt From
the definition of the strand
,
we have
{ }
1
( ,1),,,,.
'''''
aK'
A
term iauthTicketATgsauthKT
 
 
=
 
 
 
From this and (6), we have (8)
{
}
0 1
,( ,1).
authK
A Ttermi
⊏
From 1 i
a
,i ,1)( 1
i
⇒
,0)(i, then (9),1)( 1 i ,0).(i
B

But (8) and (9) contradicts with (3). If (7) holds, then
,=
'
AA ,=20tT .=
'
authKauthK So the conclusion
is obtained.
If (5) holds, then similar to the counterpart of the
argument for case (4), we have either (10)
{
}
0
,
authK
A T
⊏
'
servTicket or (11)
{
}
{
}
0 4
,,.
'
'
authK servK
A TAt ⊏ For
case (10), its proof is similar to that of case (6). If (11)
holds, then (12),=
'
AA ,= 40 tT .=
'
servKauthK By
the definition of Ag_III , (13) there is a client strand
12 ,ii such that 1
i
a
2
i and 2 i
a
i and Ag-II ,,[ 2
'
Ai
,
'
authK ,
'
authTicket ,
'
B,
'
servK ,
'
S
T,
'
servTicket ,
2
t
]
3
t and Ag-I ,[ 1 i,
'
A,
'
Tgs ,
'
authK ,
'
a
T,
'
authTicket
], 10
'' tt for some '
Tgs
∈
. TGSs Obviously,
{
}
, ,,
A
' ''
aK
A TgsauthKT
′
⊏
1
( ,1),
term i
{
}
2
,,,( ,1),
''' '
S'
authK
ABservKTterm i ⊏
and ime.shrKcrackt,1)(
2
+≤
'
a
Titime From 1 i
a
2
i and
2
i
a
i and
B
∈,0)(i, we have
B
∈,1)(1 i and
B
∈,1)(2 i. From (12), and the assumption Bad,
∉
A by
Lemma 6, (14) there is a ticket granting server strand
'
tgs such that
[ ,
'
tgs
TGS ,
'
A,
'
Tgs ,
'
authK ,
'
servK
,
'
B,
'
a
T,
0
'
T,
0
''
t]
'
S
T for some .,00
''' tT But from (2), by
Lemma 4, we have (15) there is an authentication server
as
such that ,,,[ TgsAasAS ,authK ],
0a
'Tt for some
.
0
'
t But from (12) and Axioms 4,5, we have astgs'=
because authK (
'
servK
) uniquely originates from a
strand
,
obviously this is a contradiction.
A client strand 2 i in the authorization phase receives
{
}
, ,,
S
authK
A B servK T as an unsolicited test. Note that
{
}
, ,,
S
authK
A B servK T is received in the second node in
the client strand; furthermore, from the definition of
Ag-II , we have that there exists a client strand 1 i in the
authentication phase such that 1 i
a
2
i, and the ticket
{
}
, ,,
a
K
A
A TgsauthKT must be received at the second node
of 1 i; from the definition of Ag-II ,
{
}
, ,,
S
authK
A B servK T
must have been received at an earlier time than +
a
T
imeshrKcrackt , then by Lemma 5, it can be guaranteed
that authK must be safe at the time when the client
strand receives
{
}
, ,,
S
authK
A B servK T.
Lemma 12 Let Bad
∉
BA,. If i is a client strand in
the authorization phase such that Ag-II
[ ,,,,
a
iA authKT
auth
-,,1)(and],,,,,, 10
B
∈ittservTicketTservKBTicket
S
then there exists a client strand 0 i in the authentication
phase, and a ticket grant server strand
,
tgs
and some
Tgs such that ii a
0 and
Ag-I
0
[ ,,,,,
a
iA TgsauthKT
, , ]
authTicket
∗ ∗
and
[, ,,,, ,
tgsA TgsauthKservKB
TGS
, ,,]
a s
T T
∗ ∗, and
B
∈,1)(tgs , and TGSs
∉
B.
The application server
B
receives
{
}
4
,
servK
A T,
which is an unsolicited test to guarantee that the first
received message must be from a client strand in the
service phase. This guarantee is ensured from the secrecy
of servK , which is in turn guaranteed by the ticket
{
}
, ,,
S
K
B
A B servK T. By the trace specification of an
application server strand, we have that
{ } { }
{
}
4
, ,,,,
SservKKB
ABservKTA T

Y. J. LI ET AL.
66
is received by B earlier than the time
ktimesessionKcr +
S
T .
By Lemma 9, servK is safe at that time.
Lemma 13 Let
Bad
∉
BA,
,
TGSs
∉
B . If b is an
application server strand such that
[ ,,,,
bAB servK
Apps
40 1
,,, ],
S
TT tt
B
∈ ,0)(andb , then there are two client
strands 2 i , 3 i and some servTicket such that
2 3
i i
a
and
B
∈ ,0)(
3
i and
2
[ ,,*,*,,,
iAB servK
Ag_II
, ,
S
T servTicket
*,*] and
3
[ ,,,,
iA servKservTicket
Ag_III
4
,*]
T .
The client strand in the service phase uses
{
}
4
servK
T
as an unsolicited test to authenticate the application
server strand. This guarantee is also ensured from the
secrecy of servK , which is in turn guaranteed by the
ticket
{
}
, ,,
S
authK
A B servK T
, and
{
}
, ,,
a
K
A
A TgsauthKT .
By the trace specification of an application server strand,
we have that
{
}
4
servK
T is received by
A
earlier than
the time ktimesessionKcr +
S
T and imeshrKcrackt +
a
T .
By Lemma 7, servK is safe at that time.
Lemma 14 Let Bad
∉
BA, , TGSs
∉
B . If 3 i is a
client strand in a service phase such that
3
[ ,
i
Age nt_III
],,,,,
4∗
tservTicketservKA and
B
∈ ,1)(
3
i , and 2 i is a
client strand in the authorization phase such that
2
[, ,,, ,,,,
S
iA authKauthTicketBservKTservTicket
Agent_II
2 3
, ]
t t
and
2 3
i i
a
, then there exists an application
server strand b such that 4 ,,,,,[tTservKBAb
S
Apps ,
],,
∗
∗
and
B
∈ ,1)(b .
Proof. By analysis on the form of strand 3 i and ,
2
i
we have (1) ,1)(
3
iterm
=
{
}
4
servK
t and (2)
{
, ,
A B
}
,
authK
servKTs
⊏
,1)(
2
iterm . By unfolding the
definition of Agent_II, there exists a client strand 1 i
such that 1 i
a
2
i and Ag-I ,[
1
i,A ,Tgs ,authK ,
a
T
,authTicket ,
0
t]
1
t and Tgs
∈
TGSs for some
,Tgs ,
a
T,
0
t.
1
t Obviously, (3)
{
}
, ,,
a
K
A
A TgsauthKT
⊏
,1),(
1
iterm ,1)(
1
itime
≤
a
T imeshrKcrackt +. From
1
i
a
2
i and 2 i
a
,
3
i we can easily conclude that
,1)(
1
i
+
⇒ ,1)(
3
i and ,1)(
2
i
+
⇒ ,1).(
3
i With
,1)(
3
i
∈
B
, we have ,1)(
2
i
∈
B
and ,1)(
1
i
∈
B
.
With (2)(3), by Lemma 7, (4)
(
)
mterm
≠
servK for any
node
m
such that )(mtime
≤
S
TktimesessionKcr +.
By the definition of
Agent_III,
we have (5)
,1)(
3
itime
≤
S
T ktime.sessionKcr + From (4)(5), we
have
(
)
mterm
≠
servK for any node
m
such that
)(mtime
≤
,1),(
3
itime therefore regular
(
)
.,1),(,
3
B
iservK So ,1)(
3
i is an unsolicited test for
{
}
4
servK
T in .
B
By Lemma 1, (5) there is a regular
positive node
m
such that
m
,1)(
3
i
B

and
{
}
4
servK
t
⊏
(
)
mterm and
{
}
4
authK
t
⊏
/
)( ' mterm for any node
'
m such that
'
m.m
B

Obviously
B
∈
m . By simple
case analysis, we have that
m
must be in an application
server b such that ,[b Apps ,
'
A,
'
B,
'
servK ,
'
S
T,
4
'
t
,
∗
],
∗
,1).(= bm By the definition of
Apps
,
,1)(bterm
=
.
4
'
servK
'
t With ,1)(
4
btermt
servK
⊏
, we have (6)
servKservK
'
= and .= 44tt'
Let
{
}
{ }
{ } .|
,,,
,,,,
=tservKt
TservKBA
TservKBA
M
authK
S
B
K
S
df
⊏
/
∪










Obviously ,0)(btime ,1)(btime
B

,1)(
3
itime
B

≤
S
T
+
ktimesessionKcr , by the proof of Lemma 7, we have
,0)(bterm
∈
),(Msynth i.e.,
{ }
{ }
{
}
4
, ,,,( )
B
''' '
S'servK
K
ABservKTtsynth M
′
′
′∈.
By the definition of
synth
, we have
{
}
, ,,
B
''' '
S
'
K
A B servKT
′
∈
),(Msynth
then we have (7)
{
}
, ,,
B
' '' '
S
'
K
A BservKT
′
∈
M
or (8)
{
}
, ,,
''' '
S
A B servKT
∈
).(Msynth If (7) holds, from (6)
(7) and the definition of
M
, we have
{
}
, ,,
S
A B servK T
=
{
}
, ,,
''' '
S
A B servKT
,
then
A
=
'
A
and
B
=
'
B
and
S
T
=
.
'
S
T Therefore,
the conclusion holds. If (8) holds, by the definition of
synth, we have
'
servK
∈
),(Msynth with (6), we have
servK
∈
),(Msynth then by the definition of synth,
we have servK
∈
,M but this contradicts with the
definition of
M
.
Roughly speaking, we need two steps to prove an
authentication goal that if there is a regular responder
strand Resp (
r
,
x
r
) and the k -th node of the strand is in
a bundle
B
, then there is an initiator strand Init ( i ,
x
r
)
and some j-th node of the initiator strand is in
B
.
First we prove that ),( kr is an unsolicited test for some
encrypted term
{
}
K
h
in
B
, which requires the secrecy
of
K
. This is can be easily proved by the secrecy results
on keys in section 3. Therefore, we have that there exists
some regular node
m
in
B
by Lemma 2. Second, we
need prove that
m
indeed is the intended node ),(ji .
In order to prove this, we need do case analysis on the
form of the strand which
m
possibly lies in. This proof
needs unicity property of some session keys and the
results of unsolicted tests, namely, the facts that
{
}
K
h
⊏
)(mterm and
m
is minimal.
6. Conclusions and Related Work
Our main aim is to extend and mechanize the strand
space theory to analyze Kerberos V, since mechanization
in a theorem prover not only helps us model protocols
rigorously and specify protocol goals without any
ambiguity, it also guarantees a formal proof. Besides the

Y. J. LI ET AL.
67
essential inherence from the classic strand space method,
our work is deeply inspired by Paulson and Bella’s work.
We have directly used their formalization of message
algebra, and have learned a lot about the semantics of
timestamps and replay attacks from [4]. However, we
model and analyze protocols in strand space theory
rather than in Paulson's trace theory. In detail, we model
behaviors of all the agents by strands, and mainly use the
well-founded induction principle to prove properties. So
in our Isabelle formalization, main efforts have been
devoted to definitions and lemmas about strand space
theory. e.g., we formalize strands, bundles, unique
originality, the well-founded principle on bundles, and
use this principle to prove important results such as
unsolicited authentication test and regularity of keys.
In [4], the ability of a penetrator to crack a stale en-
crypted message is modelled by the Oops rule in the
inductive definition of a trace, and the trace definition
depends on the protocol under study. However, in the
strand space theory, a penetrator’s abilities are modelled
to be independent of the protocol, that is the main reason
why we relate a key with a crack time, and model a
penetrator’s ability of cracking a stale encrypted message
by a new key cracking strand. The advantage of our
method is that modelling a penetrator’s behavior remains
independent and results such as the unsolicited authen-
tication tests can be generalized.
Regarding verification of the Kerberos protocols,
Mitchell et al. [7] analyzed a simplified version of the
protocol by model checking, and Butler et al. [8]
analyzed the Kerberos V protocol using MSR [9]. But
they did not include timestamps and replay attacks in
their model, in fact the former work ignored both nonces
and timestamps, and the latter only considered the
implementation of the Kerberos protocol basing on
nonce.
7. References
[1] 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.
[2] K. R. C. Neuman and S. Hartman, “The Kerberos Net-
work Authentication Service (v5),” Technical report, In-
ternet RFC 4120, July 2005.
[3] Y. L. and J. Pang, “Extending the Strand Space Method
with Timestamps: Part I the Theory,” Journal of Informa-
tion Security, Vol. 1, No. 2, 2010, pp. 45-55.
[4] G. Bella, “Inductive Verification of Cryptographic Pro-
tocols,” PhD Thesis, Cambridge University Computer
Laboratory, 2000.
[5] 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.
[6] Y. Li, “Strand Space and Security Protocols”. http://lcs.
ios.ac.cn/˜lyj238/strand.html.
[7] J. C. Mitchell, M. Mitchell and U. Stern, “Automated
Analysis of Cryptographic Protocols Using Murphi,”
Proceedings of 18th Symposium on Security and Privacy,
1997, pp. 141-153.
[8] 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.
[9] 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, pp. 175-190.