ICTACT Journal on Communication Technology

Open Access Open Access  Restricted Access Subscription Access
Open Access Open Access Open Access  Restricted Access Restricted Access Subscription Access

Cryptographic Protocols Specification and Verification Tools-A Survey


Affiliations
1 Department of Information Technology, Walchand College of Engineering, India
2 Scientific Analysis Group, Defence Research & Development Organisation, New Delhi, India
     

   Subscribe/Renew Journal


Cryptographic protocols cannot guarantee the secure operations by merely using state-of-the-art cryptographic mechanisms. Validation of such protocols is done by using formal methods. Various specialized tools have been developed for this purpose and are being used to validate real life cryptographic protocols. These tools give feedback to the designers of protocols in terms of loops and attacks in protocols to improve security. In this paper, we discuss the brief history of formal methods and tools that are useful for the formal verification of the cryptographic protocols.

Keywords

Formal Verification, Security Protocols, Tools for Formal Analysis.
Subscription Login to verify subscription
User
Notifications
Font Size

  • C. Meadows, “Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends”, IEEE Journal on Selected Areas in Communications, Vol. 21, No. 1, pp. 44-54, 2003.

  • R.M. Needham and M.D. Schroeder, “Using Encryption for Authentication in Large Networks of Computers”, ACM Communications, Vol. 21, No. 12, pp. 993-999, 1978.

  • D. Dolev and A.C. Yao, “On the Security of Public Key Protocols”, IEEE Transactions on Information Theory, Vol. 29, No. 2, pp. 198-207, 1983.

  • D. Dolev, S. Even and R.M. Karp, “On the Security of PingPong Protocols”, Information and Control, Vol. 55, No. 1-3, pp. 57-68, 1982.

  • M. Burrows, M. Abadi and R.M. Needham, “A Logic of Authentication”, Proceedings of the Royal Society A Mathematical, Physical and Engineering Science, pp. 18-36, 1990.

  • G. Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR”, Software-Concepts and Tools, Vol. 17, No. 3, pp. 93-102, 1996.

  • A.W. Roscoe, “Modelling and Verifying Key-Exchange Protocols using CSP and FDR”, Proceedings of 8th IEEE Computer Security Foundations Workshop, pp. 98-107, 1995.

  • J.K. Millen, S.C. Clark and S.B. Freedman, “The Interrogator: Protocol Security Analysis”, IEEE Transactions on Software Engineering, Vol. 13, No. 2, pp. 274-288, 1987.

  • S.T. Eckmann and R.A. Kemmerer, “Inatest: An Interactive Environment for Testing Formal Specifications”, ACM SIGSOFT Software Engineering Notes, Vol. 10, No. 4, pp. 17-18, 1985.

  • J. Scheid and S. Holtsberg, “Ina Jo Specification Language Reference Manual”, Technical Report, Paramax Systems Corporation, Unisys Company, 1992.

  • Catherine Meadows, “The NRL Protocol Analyzer: An Overview”, The Journal of Logic Programming, Vol. 26, No. 2, pp. 113-131, 1996.

  • B. Blanchet, “Automatic Verification of Correspondences for Security Protocols”, Journal of Computer Security, Vol. 17, No. 4, pp. 363-434, 2009.

  • C.J.F. Cremers, “The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols”, Proceedings of 20th International Conference Computer Aided Verification, pp. 414-418, 2008.

  • Luca Vigano, “Automated Security Protocol Analysis with the AVISPA Tool 1”, Electronic Notes in Theoretical Computer Science, Vol. 155, pp. 61-86, 2006.

  • S. Meier, B. Schmidt, C. Cremers and D.A. Basin, “The TAMARIN Prover for the Symbolic Analysis of Security Protocols”, Proceedings of International Conference on Computer Aided Verification, pp. 696-701, 2013.

  • B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, E. Gimenez, H. Herbelin, G. Huet, C. Munoz and C. Murthy, “The Coq Proof Assistant Reference Manual: Version 6.1”, Available at: https://hal.archives-ouvertes.fr/inria00069968/document.

  • Y. Bertot and P. Casteran, “Interactive Theorem Proving and Program Development”, 1st Edition, Springer, 2004.

  • Lawrence C. Paulson, “Isabelle: The Next 700 Theorem Provers”, Logic and computer science, Vol. 31, pp. 361-386, 1990.

  • L.C. Paulson, “Logic and Computation: Interactive Proof with Cambridge LCF”, Cambridge University Press, 1990.

  • P. Martin Lef, “Intuitionistic Type Theory”, Naples: Bibliopolis, 1984.

  • J.C. Mitchell, M. Mitchell and U. Stern, “Automated Analysis of Cryptographic Protocols using Murphi”, Proceedings of IEEE Symposium on Security and Privacy, pp. 141-151, 1997.

  • D.X. Song, S. Berezin and A. Perrig, “Athena: A Novel Approach to Efficient Automatic Security Protocol Analysis”, Journal of Computer Security, Vol. 9, No. 1-2, pp. 47-74, 2001.

  • F.J. Thayer, J.C. Herzog and J.D. Guttman, “Strand Spaces: Why is a Security Protocol Correct?”, Proceedings of IEEE Symposium on Security and Privacy, pp. 160-171, 1998.

  • E.M. Clarke, S. Jha and W.R. Marrero, “Verifying Security Protocols with Brutus”, ACM Transactions on Software Engineering and Methodology, Vol. 9, No. 4, pp. 443-487, 2000.

  • G. Lowe, “Casper: A Compiler for the Analysis of Security Protocols”, Journal of Computer Security, Vol. 6, No. 1-2, pp. 53-84, 1998.

  • C.A.R. Hoare, “Communicating Sequential Processes”, Prentice-Hall, 1985.

  • A. W. Roscoe, “Model-Checking Csp”, Prentice-Hall, 1994.

  • D. Longley and S. Rigby, “An Automatic Search for Security Flaws in Key Management Schemes”, Computers and Security, Vol. 11, No. 1, pp. 75-89, 1992.

  • C. Meadows, “Formal Verification of Cryptographic Protocols: A Survey”, Proceedings of 4th International Conference on the Theory and Applications of Cryptology, pp. 135-150, 1994.

  • R.A. Kemmerer, C. Meadows and J.K. Millen, “Three System for Cryptographic Protocol Analysis”, Journal of Cryptology, Vol. 7, No. 2, pp. 79-130, 1994.

  • M. Tatebayashi, N. Matsuzaki and D.B. Newman, “Key Distribution Protocol for Digital Mobile Communication Systems”, Proceedings of Conference on the Theory and Application of Cryptology, pp. 324-334, 1990.

  • C.A. Meadows, “Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches”, Proceedings of European Symposium on Research in Computer Security, pp. 351-364, 1996.

  • C. Meadows, “Analysis of the Internet Key Exchange Protocol using the NRL Protocol Analyzer”, Proceedings of IEEE Symposium on Security and Privacy, pp. 216-231, 1999.

  • S. Delaune, S. Kremer, M.D. Ryan and G. Steel, “A Formal Analysis of Authentication in the TPM”, International Workshop on Formal Aspects in Security and Trust, pp. 111125, 2011.

  • M. Abadi, N. Glew, B. Horne, and B. Pinkas, “Certified Email with A Light On-Line Trusted Third Party: Design and Implementation”, Proceedings of the 11th International Conference on World Wide Web, pp. 387-395, 2002.

  • M. Abadi and B. Blanchet, “Computer-Assisted Verification of a Protocol for Certified Email”, Science of Computer Programming, Vol. 58, No. 1, pp. 3-27, 2005.

  • W. Aiello, S.M. Bellovin, M. Blaze, R. Canetti, J. Ioannidis, A.D. Keromytis and O. Reingold, “Just Fast Keying: Key Agreement in A Hostile Internet”, ACM Transactions on Information and System Security, Vol. 7, No. 2, pp. 242-273, 2004.

  • M. Abadi, B. Blanchet and C. Fournet, “Just Fast Keying in the Pi Calculus”, ACM Transactions on Information and System Security, Vol. 10, No. 3, p. 1-9, 2007.

  • M. Kallahalla, E. Riedel, R. Swaminathan, Q. Wang, and K. Fu, “Plutus: Scalable secure file sharing on untrusted storage”, Available at: https://www.usenix.org/legacy/event/fast03/tech/full_paper s/kallahalla/kallahalla_html/main.html

  • B. Blanchet and A. Chaudhuri, “Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage”, Proceedings of IEEE Symposium on Security and Privacy, pp. 417-431, 2008.

  • Pascal Lafourcade, Vanessa Terrade and Sylvain Vigier, “Comparison of Cryptographic Verification Tools Dealing with Algebraic Properties”, Proceedings of International Workshop on Formal Aspects in Security and Trust, pp. 173-185, 2010.

  • Nitish Dalal, Jenny Shah, Khushboo Hisaria and Devesh Jinwala, “A Comparative Analysis of Tools for Verification of Security Protocols”, International Journal of Communications, Network and System Sciences, Vol. 3, No. 10, pp. 779-787, 2010.

  • The Avispa Project, Available at: http://www.avispa-project.org/, Accessed on 2015.

  • B. Schmidt, S. Meier, C. Cremers and D. Basin, “Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties”, Proceedings of 25th IEEE Computer Security Foundations Symposium, pp. 78-94, 2012.

  • S. Meier, B. Schmidt, C. Cremers and D. Basin, “The TAMARIN Prover for the Symbolic Analysis of Security Protocols”, Proceedings of the 25th International Conference on Computer Aided Verification, pp. 696-701, 2013.

  • B. Schmidt, R. Sasse, C. Cremers and D. Basin, “Automated Verification of Group Key Agreement Protocols”, Proceedings of IEEE Symposium on Security and Privacy, pp. 179-194, 2014.

  • D.A. Basin, C.J.F. Cremers, T.H. Kim, A. Perrig, R. Sasse and P. Szalachowski, “ARPKI: Attack Resilient Public-Key Infrastructure”, Proceedings of Conference on Computer and Communications Security, pp. 382-393, 2014.

  • T.H. Kim, C. Basescu, L. Jia, S. B. Lee, Y. Hu and A. Perrig, “Lightweight Source Authentication and Path Validation”, Proceedings of ACM SIGCOMM Conference, pp. 271-282, 2014.

  • F. Zhang, L. Jia, C. Basescu, T.H. Kim, Y. Hu and A. Perrig, “Mechanized Network Origin and Path Authenticity Proofs”, Proceedings of Conference on Computer and Communications Security, pp. 346-357, 2014.

  • J. Aransay, C. Ballarin and J. Rubio, “A Mechanized Proof of the Basic Perturbation Lemma”, Journal of Automated Reasoning, Vol. 40, No. 4, pp. 271-292, 2008.

  • C. Pusch, “Verification of Compiler Correctness for the WAM”, Proceedings of International Conference on Theorem Proving in Higher Order Logics, pp. 347-361, 1996.

  • Vitaly Shmatikov and John C. Mitchell, “Analysis of a Fair Exchange Protocol”, Proceedings of Network and Distributed System Security Symposium, pp. 1-6, 2000.

  • Vitaly Shmatikov and John C. Mitchell, “Finite-State Analysis of Two Contract Signing Protocols”, Theoretical Computer Science, Vol. 283, No. 2, pp. 419-450, 2002.

  • C. He and J.C. Mitchell, “Analysis of the 802.11i 4-way Handshake”, Proceedings of 3rd ACM Workshop on Wireless Security, pp. 43-50, 2004.

  • J.C. Mitchell, M. Mitchell and U. Stern, “Automated Analysis of Cryptographic Protocols using Mur/splphi/”, Proceedings of IEEE Symposium on Security and Privacy, pp. 141-151, 1997.

  • J.A. Clark and J.L. Jacob, “A Survey of Authentication Protocol Literature: Version 1.0”, Available at: http://e-centre.mdx.ac.uk/staffpages/m_cheng/link/clarkjacob.pdf.

  • B. Donovan, P. Norris and G. Lowe, “Analyzing a Library of Security Protocols using Casper and FDR”, Proceedings of Workshop on Formal Methods and Security Protocols, pp. 36-43, 1999.

  • G. Lowe and B. Roscoe, “Using CSP to Detect Errors in the TMN Protocol”, IEEE Transactions on Software Engineering, Vol. 23, No. 10, pp. 659-669, 1997.

  • L. Xinfeng, L. Xinghua, L. Jun and X. Junmo, “Specification and Verification of Cryptographic Protocols based on TCPL”, Proceedings of 4th International Conference on Computer Science and Education, pp. 1216-1220, 2009.

  • G. Denker, J.J. Garcia-Luna-Aveces, J. Meseguer, P.C. Olveczky, Y. Raju, B. Smith and C. Talcott, “Specification and Analysis of a Reliable Broadcasting Protocol in Maude”, Proceedings of 37th Annual Allerton Conference on Communication, Control, and Computation, pp. 21-26, 1999.

  • Bruno Blanchet, “CryptoVerif: Cryptographic Protocol Verifier in the Computational Model”, Available at: http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif

  • The Cpsa Package, Available at: https://hackage.haskell.org/package/cpsa.

  • KISS (Knowledge In Security protocolS), Available at: http://www.lsv.ens-cachan.fr/~ciobaca/kiss

  • Study on Cryptographic Protocols, Available at: https://www.enisa.europa.eu/publications/study-oncryptographicprotocols.


Abstract Views: 232

PDF Views: 3




  • Cryptographic Protocols Specification and Verification Tools-A Survey

Abstract Views: 232  |  PDF Views: 3

Authors

Amol H. Shinde
Department of Information Technology, Walchand College of Engineering, India
A. J. Umbarkar
Department of Information Technology, Walchand College of Engineering, India
N. R. Pillai
Scientific Analysis Group, Defence Research & Development Organisation, New Delhi, India

Abstract


Cryptographic protocols cannot guarantee the secure operations by merely using state-of-the-art cryptographic mechanisms. Validation of such protocols is done by using formal methods. Various specialized tools have been developed for this purpose and are being used to validate real life cryptographic protocols. These tools give feedback to the designers of protocols in terms of loops and attacks in protocols to improve security. In this paper, we discuss the brief history of formal methods and tools that are useful for the formal verification of the cryptographic protocols.

Keywords


Formal Verification, Security Protocols, Tools for Formal Analysis.

References