Journal of Information Security, 2010, 1, 56-67
doi:10.4236/jis.2010.12007 Published Online October 2010 (http://www.SciRP.org/journal/jis)
Copyright © 2010 SciRes. 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
E-mail: lyj238@ios.ac.cn, jun.pang@informatik.uni-oldenburg.de
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.
Copyright © 2010 SciRes. JIS
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.
Copyright © 2010 SciRes. JIS
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.
Copyright © 2010 SciRes. JIS
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
0 ls0 ws3b">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.
Copyright © 2010 SciRes. JIS
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.