Extending the Strand Space Method with Timestamps: Part I the Theory

Yongjian Li, Jun Pang

.

DOI: 10.4236/jis.2010.12006                

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.

Keywords

Strand Space, Kerberos V, Theorem Proving, Verification, Isabelle/HOL

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	G. Bella, “Inductive Verification of Cryptographic Protocols,” PhD thesis, Cambridge University Computer Laboratory, 2000.
[2]	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.
[3]	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.
[4]	K. R. C. Neuman and S. Hartman, “The Kerberos Network Authentication Service (v5),” Technical report, Internet RFC 4120, July 2005.
[5]	C. J. F. Cremers, “Feasibility of Multi-Protocol Attacks,” Proceedings of 1st Conference on Availability, Reliability and Security, 2006, pp. 287-294.
[6]	D. Denning and G. Sacco, “Timestamps in Key Distribution Protocols,” Communications of the ACM, Vol. 24, No. 8, 1981, pp. 533-536.
[7]	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.
[8]	J. D. Guttman and F. Javier Thayer, “Protocol Independence through Disjoint Encryption,” Proceedings of 13th IEEE Computer Security Foundations Workshop, 2000, pp. 24-34.
[9]	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.
[10]	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.
[11]	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.
[12]	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.
[13]	Y. Li, “Strand Space and Security Protocols,” http://lcs. ios.ac.cn/?lyj238/strand.html.
[14]	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.
[15]	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.
[16]	G. Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR,” Proceedings of 2nd International Conference on Tools and Algorithms for the 10 Construction and Analysis of Systems, LNCS 1055, pages 147-166, 1996.
[17]	C. Meadows, “Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer,” Proceedings of 12th IEEE Computer Security Foundations Workshop, 1999, pp. 216-231.
[18]	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.
[19]	T. Nipkow, L. C. Paulson and M. Wenzel, “Isabelle/HOL— A Proof Assistant for Higher-Order Logic,” LNCS 2283. Spinger, 2002.
[20]	L. C. Paulson, “The Inductive Approach to Verifying Cryptographic Protocols,” Journal of Computer Security, Vol. 6, No. 1-2, 1998, pp. 85-128.