Mechanical Verification of Cryptographic Protocols

  • Xiaochun Cheng
  • Xiaoqi Ma
  • Scott C.-H. Huang
  • Maggie Cheng


Information security is playing an increasingly important role in modern society, driven especially by the uptake of the Internet for information transfer. Large amount of information is transmitted everyday through the Internet, which is often the target of malicious attacks. In certain areas, this issue is vital. For example, military departments of governments often transmit a great amount of top-secret data, which, if divulged, could become a huge threat to the public and to national security. Even in our daily life, it is also necessary to protect information. Consider e-commerce systems as an example. No one is willing to purchase anything over the Internet before being assured that all their personal and financial information will always be kept secure and will never be leaked to any unauthorised person or organisation.


Model Checker Authentication Protocol Security Protocol Cryptographic Protocol Encrypt Message 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    G. Bella. Inductive Verification of Cryptographic Protocols, PhD Thesis, University of Cambridge, Cambridge, UK, 2000.Google Scholar
  2. 2.
    D. Bolignano. An Approach to the Formal Verification of Cryptographic Protocols, In Proceedings of the 3rd ACM Conference on Computer and Communications Security, pp. 106–118, New Delhi, India, March 1996.Google Scholar
  3. 3.
    M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication, in ACM Transactions on Computer Systems, 8(1):18–36, February 1990.CrossRefGoogle Scholar
  4. 4.
    A. Liebl. Authentication in Distributed Systems: A Bibliography, in ACM SIGOPS Operating Systems Review, 27(4):122–136, October 1993.CrossRefGoogle Scholar
  5. 5.
    G. Lowe. An Attack on the Needham-Schroeder Public-Key Authentication Protocol, in Information Processing Letters, 56(3):131–133, November 1995.MATHCrossRefGoogle Scholar
  6. 6.
    G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR, in Margaria and Steffen (Eds.) Tools and Algorithms for the Construction and Analysis of System, Vol. 1055 of Lecture Notes in Computer Science, pp. 147–166. Springer, 1996.Google Scholar
  7. 7.
    C.A. Meadows. Analyzing the Needham-Schroeder Public-Key Protocol: A Comparison of Two Approaches, in E. Bertino, H. Kurth, G. Martella and E. Montolivo (Eds.) Computer Security ESORICS 96, Vol. 1146 of Lecture Notes in Computer Science, pp. 351–346. Springer, 1996.Google Scholar
  8. 8.
    C.A. Meadows. The NRL Protocol Analyzer: An Overview, in Journal of Logic Programming, 26(2):113–131, February 1996.MATHCrossRefGoogle Scholar
  9. 9.
    R. Needham, and M. Schroeder. Using Encryption for Authentication in Large Networks of Computers, in Communications of the ACM, 21(12):993–999, 1978.MATHCrossRefGoogle Scholar
  10. 10.
    T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Springer, 2003.Google Scholar
  11. 11.
    L.C. Paulson. Proving Properties of Security Protocols by Induction, in Proceedings of the 10th Computer Security Foundations Workshop, pp. 70–83, Rockport, Massachusetts, June 1997.Google Scholar
  12. 12.
    L.C. Paulson. Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys, Technical Report 413, Computer Laboratory, University of Cambridge.Google Scholar
  13. 13.
    L.C. Paulson. Mechanized Proofs for a Recursive Authentication Protocol, in Proceedings of the 10th Computer Security Foundations Workshop, pp. 84–95, Rockport, Massachusetts, June 1997.Google Scholar
  14. 14.
    L.C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols, in Journal of Computer Security, 6(1–2):85–128, 1998.Google Scholar
  15. 15.
    L.C. Paulson. Proving Security Protocols Correct, in Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pp. 370–383, Trento, Italy, July 1999.Google Scholar
  16. 16.
    E. Snekkenes. Roles in Cryptographic Protocols, in Proceedings of the 1992 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 105–119, Oakland, California, USA, May 1992.Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  • Xiaochun Cheng
    • 1
  • Xiaoqi Ma
  • Scott C.-H. Huang
  • Maggie Cheng
  1. 1.Department of Computer ScienceThe University of ReadingReadingUK

Personalised recommendations