Stanford Security Lab

Model Checking Methods for Security Protocols

Summary

Model checking, also known as finite-state analysis, involves using verification tools to exhaustively search all execution sequences for desired properties in a protocol specification. While this process often reveals errors, the absence of errors does not imply correctness of the protocol. This method has been successfully applied to a number of security protocols developed by the IEEE, IETF Working Groups, and others. Many of the examples below make use of the Murphi verification system

The following paper and set of slides provides an overview of this work. For further details, please read the other papers included below.

  • J. C. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using Murphi, Proceedings of the 1997 IEEE Symposium on Security and Privacy, May 1997, Pages 141-151. [ Paper ]
  • J. C. Mitchell, Symbolic and Computational Analysis of Network Protocol Security, Invited Talk, ASIAN Computing Science Conference, December 2006. [ Slides ]

Publications

  • J. C. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using Murphi, Proceedings of the 1997 IEEE Symposium on Security and Privacy, May 1997, Pages 141-153. [ Paper ]
  • J. C. Mitchell, V. Shmatikov, U. Stern, Finite-State Analysis of SSL 3.0, Seventh USENIX Security Symposium, 1998, Pages 201-216. [ Paper ]
  • V. Shmatikov, J. C. Mitchell, Analysis of a Fair Exchange Protocol, Network and Distributed System Security Symposium, 2000, Pages 119-128. [ Paper ]
  • V. Shmatikov, J. C. Mitchell, Analysis of Abuse-Free Contract Signing, Financial Cryptography '00, 2000. [ Paper ]
  • V. Shmatikov, J. C. Mitchell, Finite-State Analysis of Two Contract Signing Protocols, Theoretical Computer Science, 283, June 2002, Pages 419-450. [ Paper ]
  • D. Lie, J. C. Mitchell, C. Thekkath and M. Horowitz. Specifying and Verifying Hardware for Tamper-Resistant Software. In Proceedings of the 2003 IEEE Symposium on Security and Privacy . May 2003. [ Paper ]
  • V. Shmatikov, Probabilistic Model Checking of an Anonymity System (Crowds). Journal of Computer Security, special issue on selected papers of CSFW-15 (ed. Steve Schneider), 2004. [ Paper ]
  • C. He, J. C. Mitchell, Analysis of the IEEE 802.11i 4-Way Handshake, ACM Workshop on Wireless Security, October 2004. [ Paper ]
  • C. He, J. C. Mitchell, Security Analysis and Improvements for IEEE 802.11i, Network and Distributed System Security Symposium, February 2005. [ Paper ]
  • J. C. Mitchell, A. Roy, P. Rowe, A. Scedrov, Analysis of EAP-GPSK Authentication Protocol, Applied Cryptography and Network Security, 2008. [Paper]
  • J. Bau, J. C. Mitchell, A Security Evaluation of DNSSEC with NSEC3. Network and Distributed Systems Security (NDSS), March 2010. [Paper]
  • D. Akhawe, A. Barth, P. Lam, J. C. Mitchell and D. Song, Towards a formal foundation of Web Security. To appear at IEEE Symposium on Computer Security Foundations, July 2010. [Paper]

Tool Support

Other Talks

  • J. C. Mitchell, Security Analysis of Network Protocols: Logical and Computational Methods, Invited Talk, ICALP, July 2005. [ Slides ]
  • J. C. Mitchell, Symbolic and Computational Analysis of Network Protocol Security, Invited Talk, ASIAN Computing Science Conference, December 2006. [ Slides ]