| The Strand
Space Method
Introduction The Strand Space
method is a technique for analyzing cryptographic
protocols (particularly authentication and key
distribution protocols) at a very high level. The
technique (like many others) uses the Dolev-Yao model of
cryptographic protocols, and abstracts the real-world
cryptographic algorithms into abstract operations. Hence,
Strand Spaces focuses on the structure of a
protocol, rather than the protocol's use of any particular
encryption scheme. Originally designed as a
pencil-and-paper proof
method, it has also been automated. It has been extended in various ways, and its
relationship with other proof
methods has been
explored. It also seems a handy framework with which to prove general results about
protocols.
Whenever possible, links point to an authors' webspace.
Core Papers
- Strand Spaces: Why is a Security Protocol
Correct?
(web page) F. Javier Thayer
Fabrega, Jonathan
C. Herzog, Joshua D. Guttman. Proceedings, 1998 IEEE
Symposium
on Security and Privacy, May 1998.
- Honest Ideals on Strand Spaces (web page) F. Javier Thayer
Fabrega, Jonathan C. Herzog, Joshua
D. Guttman. Proceedings, 1998 Computer Security Foundations
Workshop, June 1998
- Strand Spaces: Proving Security Protocols Correct
(web page) F. Javier Thayer Fabrega, Jonathan
C. Herzog, Joshua
D. Guttman. Journal of Computer Security, 7 (1999), pages
191-230. (Contains the above papers. Winner, MITRE Best Paper, 1999)
- Authentication Tests (web page) Joshua Guttman and F. Javier Thayer
Fabrega. Proceedings of the 2000 IEEE Symposium on Security and
Privacy, Oakland, CA, May 2000.
- Authentication Tests and the Structure of Bundles (web page) Joshua Guttman and F. Javier Thayer
Fabrega. Theoretical Computer Science, 2001. (Includes above
paper.)
Books
Extensions
- Strand space pictures F. J. T. Fabrega, J. Herzog, and J. D. Guttman.
Proceedings, Workshop on Formal
Methods and Security Protocols, June 1998. Co-located with
LICS'98.
- Mixed Strand Spaces
(web page)
F. Javier Thayer Fabrega, Jonathan C. Herzog, Joshua
D. Guttman. Proceedings, 1999 Computer Security Foundations
Workshop, June 1999.
- Honest Functions and their Application to the
Analysis of Cryptographic Protocols (Web
page) Alfred P. Maneki. Proceedings, 1999 Computer Security
Foundations Workshop, June 1999.
- Nonce
Analysis and Strand Space Model (PostScript)
Koichi Takahashi, Yozo Toda
and Masami Hagiya, JSSST 2000, Japan Society for Software
Science and Technology, 2000.
- Composing Strand Spaces (Postscript)
(PDF) Federico Crazzolara and Glynn
Winskel.
FSTTCS '02.
- What are Guessing Attacks and How to Prevent
Them (PDF)
Sreekanth Malladi, Jim Alves-Foss and Sreenivas Malladi.
Proc. Seventh International Workshop on Enterprise Security,
June 2002.
- On Preventing Replay Attacks on Security
Protocols (PDF)
S. Malladi, J. Alves-Foss and R. Heckendorn.
Proc. International Conference on Security and Management, June
2002, pp. 77-83.
- Symbolic Protocol Analysis with Products and Diffie-Hellman
Exponentiation. (Forthcoming journal version: PDF)
Millen, J., and Shmatikov, V. In Proc. 16th IEEE Computer Security
Foundations Workshop (CSFW-16), pages 47-61, 2003. (See next paper for
different treatment of same problem.)
- The Diffie-Hellman Key-Agreement Scheme in the
Strand-Space
Model (Postscript)
(PDF) Jonathan C. Herzog. Proceedings, 16th
Computer Security Foundations Workshop (CSFW-16), June
2003. (See previous paper for
different treatment of same problem.)
- A compositional logic for proving security
properties of protocols (PDF)
N.A. Durgin, J.C. Mitchell, D. Pavlovic. Journal of
Computer Security, 11(2003) 677-721.
- Study on Strand Space Model Theory (Web
page) Qingguang Ji, Sihan Qing, Yongbin Zhou, Dengguo
Feng. Journal of Computer Science and Technology, 18:5,
p. 553-570, 2003.
- Trust management
in strand spaces: A rely-guarantee method (PostScript)
(PDF)
J. D. Guttman,
F. J. Thayer, J. A. Carlson, J. Herzog, J. D. Ramsdell, and
B. T. Sniffen. Programming Languages and Systems: 13th European
Symposium on Programming (D. Schmidt, ed.), no. 2986 in Lecture
Notes in Computer Science, pp. 325-339, Springer, 2004.
Automation and Implementation
- Athena, an Automatic Checker for Security Protocol Analysis (Postscript)
(PDF) D. Song. In 12th IEEE Computer Security Foundation Workshop, 1999.
- Athena, a Novel Approach to Efficient Automatic Security Protocol Analysis (Postscript)
(PDF)
D. Song, S. Berezin, and A. Perrig. In Journal of Computer
Security, 9(1,2):47-74, 2001.
- Constraint Solving for Bounded-Process Cryptographic Protocol Analysis (PostScript) Millen, J., and Shmatikov, V. In Proc. 8th ACM Conference on Computer and Communications Security (CCS '01), pages 166-175, 2001. (See also
the implementation web page)
- Introducing ASPECT - a tool for checking protocol security (Web page) Brian Monahan, HP Technical Report HPL-2002-246, 2002.
- An Improved Constraint-Based System for the Verification of Security Protocols (PDF) R. Corin and S. Etalle. 9th Int. Static
Analysis Symp. (SAS), LNCS 2477, M. V. Hermenegildo and G. Puebla
(eds.), published by Springer-Verlag, Berlin, held in Madrid, Spain, September 2002, pp. 326-341. (See also the implementation web page.)
- Programming cryptographic protocols (PDF) J. D. Guttman, J. C. Herzog, J. D. Ramsdell, and B. T. Sniffen. Proceedings, Symposium on Trustworthy Global Computing, April 2005.
- Compiling Cryptographic Protocols for Deployment on the Web (PDF) Jay McCarthy, Joshua D. Guttman, John D. Ramsdell, Shriram Krishnamurthi (World Wide Web, 2007).
Relationship With Other
Methods
- Interpreting Strands in Linear Logic (GZipped
Postscript) (GZipped
PDF) Iliano Cervesato, Nancy Durgin, Max I. Kanovich and Andre
Scedrov. 2000 Workshop on Formal Methods and Computer Security -
FMCS'00 (H. Veith, N. Heintze and
E. Clark, editors), Chicago, IL, 20 July 2000.
- Towards a Strand Semantics for Authentication Logic (Postscript)
(PDF) Paul Syverson. Electronic Notes in
Theoretical Computer Science, vol. 20, eds. Stephen Brookes, Achim
Jung, Michael Mislove and Andre Scedrov, 2000.
- Interpreting Strands in Linear Logic (Gzipped
PostScript) (PDF)
I. Cervesato, N. Durgin , M. Kanovich and
A. Scedrov. 2000 Workshop on Formal Methods and Computer
Security - FMCS'00
(H. Veith, N. Heintze and E. Clark, editors), Chicago, IL, 20
July 2000.
- Events in Security Protocols (PDF) Federico Crazzolara and Glynn
Winskel. Proc. 8th ACM Conference on Computer and Communications
Security (CCS-8), Philadelphia, November
2001. (See also Composing Strand Spaces, by Crazzolara and
Winskel above.)
- Petri nets in cryptographic protocols (Web
page) Federico Crazzolara, Glynn Winskel. 15th International
Parallel and Distributed Processing Symposium (IPDPS'01)
Workshops, p. 30149a, 2001.
- Strand Spaces and Rank Functions: More Than Distant
Cousins. (Postscript)
(PDF) James Heather. 15th IEEE Computer Security
Foundations Workshop, June 2002.
- Equal To The Task? (Postscript)
(PDF) James Heather. 7th European Symposium on
Research in Computer Security (ESORICS), 2002.
- On the relationship between strand spaces and multi-agent
systems (Postscript)
(PDF) Joseph Y. Halpern and Riccardo Pucella. ACM
Transactions on Information and System Security 6:1, pp. 43-70, 2003.
- A Comparison between Strand Spaces and Multiset Rewriting for
Security Protocol Analysis (GZipped
Postscript) (GZipped
PDF) Iliano Cervesato, Nancy Durgin, Patrick D. Lincoln, John
C. Mitchell and Andre Scedrov. Software Security - Theories and
Systems
- ISSS 2002, (Revised Papers of the 2002 Mext-NSF-JSPS International
Symposium) (M. Okada, B. Pierce, AS, H. Tokuda and A. Yonezawa,
editors), pp. 356-383, Springer-Verlag LNCS 2609, Tokyo, Japan, 8-10
November 2003.
- Attack Analysis of Cryptographic Protocols Using
Strand Spaces (Web
page) Simon Lukell and Andrew CM Hutchison. South African
Computer Journal 31:25-32 (2003).
- Relating strand spaces and distributed temporal
logic for security protocol analysis. (PDF)
C. Caleiro, L. Vigano, and D. Basin. Logic Journal of the IGPL,
13(6):637--664, 2005.
General Results
Proved Using Strand Spaces
- Protocol Independence through Disjoint Encryption (web page) Joshua Guttman and F. Javier Thayer
Fabrega. 13th IEEE Computer Security Foundations Workshop, Cambridge,
July 2000.
- Key Compromise, Strand Spaces, and the Authentication
Tests (GZipped
Postscript) Joshua Guttman. Electronic Notes in Theoretical
Computer Science, with the proceedings of Mathematical Foundations of
Programming Semantics 17 (2001). Dedicated to Bob Dylan.
- Protocol Design via the Authentication Tests (GZipped
Postscript) (PDF) Joshua D. Guttman. 15th IEEE Computer Security
Foundations Workshop, June 2002.
- A Bound on Attacks on Authentication
Protocols (PDF)
(PostScript)
Scott D. Stoller. Proceedings of the 2nd IFIP International
Conference on Theoretical Computer Science (TCS) in the 17th
IFIP World Computer Congress, pages 588-600, 2002.
- On the Freedom of Decryption (
Postscript) Millen, J. Information Processing Letters, Vol. 86,
2003, pp. 329-333.
- How To Prevent Type Flaw Attacks On Security Protocols
(Postscript)
(Postscript
mirror) (PDF) J. Heather, G. Lowe and S. Schneider,
Journal of Computer Security, Vol 11, No 2, 2003, pp 217-244.
- Analysis of a Multi-Party Fair Exchange Protocol and Formal
Proof of Correctness in the Strand Space Model. (PDF)
Aybek Mukhamedov, Steve Kremer and Eike Ritter. In
A. S. Patrick and M. Yung (eds.), Revised Papers from the 9th
International Conference on Financial Cryptography and Data
Security (FC'05), Roseau, The Commonwealth Of Dominica, August
2005, LNCS 3570, pages 255-269. Springer.
- The sizes of skeletons: security goals are
decidable (Web
page) Joshua Guttman and F. Javier Thayer. MITRE Technical
Report 05B09, January 2005.
For more information, please
contact Jonathan Herzog using the employee directory.
|
