Research ArticleOpen AccessGoogle Scholar indexed
Extending the Strand Space Method with Timestamps: Part I the Theory
- 1
- 2
Journal of Information Security·Volume 01 (2010)·Pages 45–55·Published 29 October 2010·DOI10.4236/jis.2010.12006
Copy link · social · email
Abstract
In this paper, we present two extensions of the strand space method to model Kerberos V. First, we include time and timestamps to model security protocols with timestamps: we relate a key to a crack time and combine it with timestamps in order to define a notion of recency. Therefore, we can check replay attacks in this new framework. Second, we extend the classic strand space theory to model protocol mixture. The main idea is to introduce a new relation to model the causal relation between one primary protocol session and one of its following secondary protocol session. Accordingly, we also extend the definition of unsolicited authentication test.
KeywordsStrand SpaceKerberos VTheorem ProvingVerificationIsabelle/HOL
- G. Bella, “Inductive Verification of Cryptographic Protocols,” PhD thesis, Cambridge University Computer Laboratory, 2000.
- L. Bozga, C. Ene and Y. Lakhnech, “A Symbolic Decision 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, 175-190.
- K. R. C. Neuman and S. Hartman, “The Kerberos Network Authentication Service (v5),” Technical report, Internet RFC 4120, July 2005.
- C. J. F. Cremers, “Feasibility of Multi-Protocol Attacks,” Proceedings of 1st Conference on Availability, Reliability and Security, 2006, pp. 287-294.
- D. Denning and G. Sacco, “Timestamps in Key Distribution Protocols,” Communications of the ACM, Vol. 24, No. 8, 1981, pp. 533-536.
- J. D. Guttman, “Key Compromise, Strand Spaces, and the Authentication Tests,” Proceedings of 7th Conference on the Mathematical Foundations of Programming Semantics, ENTCS 45, 2001, pp. 1-21.
- J. D. Guttman and F. Javier Thayer, “Protocol Independence through Disjoint Encryption,” Proceedings of 13th IEEE Computer Security Foundations Workshop, 2000, pp. 24-34.
- J. D. Guttman and F. Javier Thayer, “Authentication Tests and the Structure of Bundles,” Theoretical Computer Science, Vol. 283, No. 2, 2002, pp. 333-380.
- J. Heather and S. A. Schneider, “Toward Automatic Verification of Authentication Protocols on an Unbounded Network,” Proceedings of 13th IEEE Computer Security Foundations Workshop, 2000, pp. 132-143.
- F. Javier Thayer, J. C. Herzog and J. D. Guttman, “Mixed Strand Spaces,” Proceedings of 12th IEEE Computer Security Foundations Workshop, 1999, pp. 72-82.
- 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. ios.ac.cn/?lyj238/strand.html.
- Y. Li, “The Inductive Approach to Strand Space,” Proceedings of 25th IFIP Conference on Formal Techniques for Networked and Distributed Systems, LNCS 3731, 2005, pp. 547-552.
- Y. Li and J. Pang, “Generalized Unsolicited Tests for Authentication Protocol Analysis,” Proceedings of 7th Conference on Parallel and Distributed Computing, 2006, pp. 509-514.