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

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.