Strand Space and
Security Protocols
Yongjian Li
Strand space is a promising technique developed by Guttman
et al. Although strand space provides us an intuitive and clear framework to
analyze the correctness of security protocols, it seems to us that the
mechanics of the proofs tend to be quite intricate and not necessarily easy to
be formalized. To the best of our knowledge, no one has ever succeeded in
formalizing strand space theory in a theorem prover
since the theory was first introduced in 1998. Besides that, we find that few
people have extended strand space to analyze real-world protocols such as
Kerberos, TLS, SET.
In this web page, we collect our effort to narrow the above gaps in the literature, we aim to mechanizing the strand space theory to
support the analysis of real-world protocols. Several papers have been
published or prepared.
- Yongjian Li. The Inductive
Approach to Strand Space. LNCS
3731, FORTE 2005: 547-552, Springer Press,2005.
- Yongjian Li, Jung Pang. Generalized
Unsolicited Tests for Authentication Protocol Analysis. In Proc. 7th Conference on Parallel and Distributed
Computing, Applications and Technologies - PDCAT'06, pp. 509-514. IEEE
Computer Society, 2006.
- Yongjian Li, Jung Pang. Extending Strand
Space with Timestamps. In Proc. 8th Conference on Parallel and Distributed
Computing, Applications and Technologies - PDCAT'0. IEEE Computer
Society, 2007.
Case
Studies
The Isabelle/HOL proof scripts in the
papers are listed below:
o The general theory of strand spaces and case studies on the Needham-Schroeder-Lowe
protocol and the Otway-Rees protocol ( thy files and html files );
o The
extended strand space theory to model timestamp and Kerberos V protocol.
Some
notes
- All the
proof scripts have been checked by Isabelle/Isar.
The formalizing work on the classical strand space work is done by
Isabelle 2004. But the formalization of extended strand space work on
timestamp is done in Isabelle 2005. Notice the difference of the
Isabelle version when you want
to use these proof scripts.
April 22, 2006