Paper Menu >>
Journal Menu >>
Y. J. LI ET AL.
Copyright © 2010 SciRes. JIS
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 . 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 , 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.  analyzed a simplified version of the
protocol by model checking, and Butler et al. 
analyzed the Kerberos V protocol using MSR . 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
 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,
 K. R. C. Neuman and S. Hartman, “The Kerberos Net-
work Authentication Service (v5),” Technical report, In-
ternet RFC 4120, July 2005.
 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.
 G. Bella, “Inductive Verification of Cryptographic Pro-
tocols,” PhD Thesis, Cambridge University Computer
 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.
 Y. Li, “Strand Space and Security Protocols”. http://lcs.
 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.
 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.
 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.