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, Symbolic and Computational Analysis of Network Protocol Security, Invited Talk, ASIAN Computing Science Conference, December 2006. [ Slides ]

  • 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 ]

Publications

  • J. C. Mitchell, Symbolic and Computational Analysis of Network Protocol Security, Invited Talk, ASIAN Computing Science Conference, December 2006. [ Slides ]
  • C. He, J. C. Mitchell, Security Analysis and Improvements for IEEE 802.11i, Network and Distributed System Security Symposium, February 2005, [ Paper ]
  • C. He, J. C. Mitchell, Analysis of the IEEE 802.11i 4-Way Handshake, ACM Workshop on Wireless Security, October 2004, [ Paper ]
  • V. Shmatikov, J. C. Mitchell, Finite-State Analysis of Two Contract Signing Protocols, Theoretical Computer Science, 283, June 2002, Pages 419-450 [ Paper ]
  • V. Shmatikov, J. C. Mitchell, Analysis of Abuse-Free Contract Signing, Financial Cryptography '00, 2000 [ Paper ]
  • V. Shmatikov, J. C. Mitchell, Analysis of a Fair Exchange Protocol, Network and Distributed System Security Symposium, 2000, Pages 119-128 [ Paper ]
  • J. C. Mitchell, V. Shmatikov, U. Stern, Finite-State Analysis of SSL 3.0, Seventh USENIX Security Symposium, 1998, Pages 201-216 [ Paper ]
  • 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 ]

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 ]