A short introduction to two approaches in formal verification of security protocols: model checking and theorem proving

Document Type: ORIGINAL RESEARCH PAPER

Authors

1 Department of Mathematical Science, Sharif University of Technology, Tehran, Iran

2 Department of Mathematical Science, Ferdowsi University of Mashhad, Mashhad, Iran

Abstract

In this paper, we shortly review two formal approaches in verification of security protocols; model checking and theorem proving. Model checking is based on studying the behavior of protocols via generating all different behaviors of a protocol and checking whether the desired goals are satisfied in all instances or not. We investigate Scyther operational semantics as n example of this approach and then we model and verify some famous security protocols using Scyther. Theorem proving is based on deriving the desired goals from assumption of protocols via a deduction system. We define a deduction system named Simple Logic for Authentication to formally define the notion of authenticated communication based on the structure of the messages, and then we several famous protocols using our proposed deduction system and compare it with the verification results of Scyther model checking.

Keywords


[1] Roger M Needham and Michael D Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993_999, 1978.

[2] Dorothy E Denning and Giovanni Maria Sacco. Timestamps in key distribution protocols. Communications of the ACM, 24(8):533_536, 1981.

[3] Stuart G Stubblebine and Virgil D Gligor. On message integrity in cryptographic protocols. IEEE, 1992.

[4] Wenbo Mao and Colin Boyd. On the use of encryption in cryptographic protocols. Codes and Cyphers: Cryptography and Coding IV, pages 251_262, 1995.

[5] Paul Syverson. A taxonomy of replay attacks [cryptographic protocols]. In Computer Security Foundations Workshop VII, 1994. CSFW 7. Proceedings, pages 187_191. IEEE, 1994.

[6] Mike Burmester. On the risk of opening distributed keys. In Advances in Cryptology- CRYPTO94, pages 308_317. Springer, 1994.

[7] Colin Boyd and Anish Mathuria. Protocols for authentication and key establishment. Springer Science & Business Media, 2013.

[8] Ray Bird, Inder Gopal, Amir Herzberg, Philippe Janson, Shay Kutten, Refik Molva, Moti Yung, et al. Systematic design of a family of attack resistant authentication protocols. Selected Areas in Communications, IEEE Journal on, 11(5):679_693, 1993.

[9] Tuomas Aura and Pekka Nikander. Stateless connections. Information and Communications Security, pages 87_97, 1997.

[10] Catherine Meadows. A formal framework and evaluation method for network denial of service. In Computer Security Foundations Workshop, 1999. Proceedings of the 12th IEEE, pages 4_13. IEEE, 1999.

[11] Ari Juels and John G Brainard. Client puzzles: A cryptographic countermeasure against connection depletion attacks. In NDSS, volume 99, pages 151_165, 1999.

[12] Dave Otway and Owen Rees. Efficient and timely mutual authentication. ACM SIGOPS Operating Systems Review, 21(1):8_10, 1987.

[13] Casimier Joseph Franciscus Cremers. Scyther: Semantics and verification of security protocols. Eindhoven University of Technology, 2006.

[14] Cas Cremers and Sjouke Mauw. Operational semantics and verification of security protocols. Springer Science & Business Media, 2012.

[15] Markus Müller-Olm, David Schmidt, and Bernhard Steffen. Model-checking. In Static Analysis, pages 330_354. Springer, 1999.

[16] Edmund M Clarke and E Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Springer, 1982.

[17] Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in cesar. In International Symposium on Programming, pages 337_351. Springer, 1982.

[18] Amir Pnueli. The temporal semantics of concurrent programs. Theoretical computer science, 13(1):45_60, 1981.

[19] David L Dill. The mur Ø verification system. In Computer Aided Verification, pages 390_393. Springer, 1996.

[20] John C Mitchell, Mark Mitchell, and Ulrich Stern. Automated analysis of cryptographic protocols using murʄ. In Security and Privacy, 1997. Proceedings., 1997 IEEE Symposium on, pages 141_151. IEEE, 1997.

[21] Makoto Tatebayashi, Natsume Matsuzaki, and David B Newman Jr. Key distribution protocol for digital mobile communication systems. In Advances in CryptologyCRYPTO89 Proceedings, pages 324_334. Springer, 1990.

[22] B Clifford Neuman and Theodore Ts' O. Kerberos: An authentication service for computer networks. Communications Magazine, IEEE, 32(9):33_38, 1994.

[23] Edmund M Clarke, Somesh Jha, and Will Marrero. Verifying security protocols with brutus. ACM Transactions on Software Engineering and Methodology (TOSEM), 9(4):443_487, 2000.

[24] Cas JF Cremers. The scyther tool: Verification, falsification, and analysis of security protocols. In Computer Aided Verification, pages 414_418. Springer, 2008.

[25] Michael Burrows, Martin Abadi, and Roger M Needham. A logic of authentication. In Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, volume 426, pages 233_271. The Royal Society, 1989.

[26] Michael Burrows, Martin Abadi, and Roger M Needham. A logic of cryptographic. ACM Transactions on Computer Systems, 8(1):18_36, 1990.

[27] Stefanos Gritzalis, Diomidis Spinellis, and Panagiotis Georgiadis. Security protocols over open networks and distributed systems: Formal methods for their analysis, design, and verification. Computer Communications, 22(8):697_709, 1999.

[28] Recommendation X CCITT. 509: The directory authentication framework, 1988.

[29] Steven P Miller, B Clifford Neuman, Jeffrey I Schiller, and Jermoe H Saltzer. Kerberos authentication and authorization system. In In Project Athena Technical Plan. Citeseer, 1987.

[30] Dan M Nessett. A critique of the burrows, abadi and needham logic. ACM SIGOPS Operating Systems Review, 24(2):35_38, 1990.

[31] Paul Syverson. The use of logic in the analysis of cryptographic protocols. In Research in Security and Privacy, 1991. Proceedings., 1991 IEEE Computer Society Symposium on, pages 156_170. IEEE, 1991.

[32] Wenbo Mao and Colin Boyd. Towards formal analysis of security protocols. In Computer Security Foundations Workshop VI, 1993. Proceedings, pages 147_158. IEEE, 1993.

[33] Li Gong, Roger Needham, and Raphael Yahalom. Reasoning about belief in cryptographic protocols. In Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on, pages 234_248. IEEE, 1990.

[34] Martin Abadi and Mark R Tuttle. A semantics for a logic of authentication. In Proceedings of the tenth annual ACM symposium on Principles of distributed computing, pages 201_216. ACM, 1991.

[35] Paul F Syverson and Paul C Van Oorschot. On unifying some cryptographic protocol logics. In Research in Security and Privacy, 1994. Proceedings., 1994 IEEE Computer Society Symposium on, pages 14_28. IEEE, 1994.

[36] Volker Kessler and GabrieleWedel. Autlog-an advanced logic of authentication. In Computer Security Foundations Workshop VII, 1994. CSFW 7. Proceedings, pages 90_99. IEEE, 1994.

[37] Paul van Oorschot. Extending cryptographic logics of belief to key agreement protocols. In Proceedings of the 1st ACM Conference on Computer and Communications Security, pages 232_243. ACM, 1993.

[38] ITU-TS, Recommendation Z.120: Message Sequence Chart (MSC) ITU-TS, Geneva. 1999.

[39] Danny Dolev and Andrew C Yao. On the security of public key protocols. Information Theory, IEEE Transactions on, 29(2):198_208, 1983.

[40] Whitfield Diffie and Martin E Hellman. New directions in cryptography. Information Theory, IEEE Transactions on, 22(6):644_654, 1976.

[41] Gavin Lowe. Breaking and fixing the needhamschroeder public-key protocol using fdr. In Tools and Algorithms for the Construction and Analysis of Systems, pages 147_166. Springer, 1996.

[42] Mihir Bellare and Phillip Rogaway. Entity authentication and key distribution. In Advances in CryptologyCRYPTO93, pages 232_249. Springer, 1994.

[43] Jim Alves-Foss. Provably insecure mutual authentication protocols: The two party symmetric encryption case. In Proc. 22nd National Information Systems Security Conference, pages 44_55. Citeseer, 1999.

[44] Mahadev Satyanarayanan. Integrating security in a large distributed system. ACM Transactions on Computer Systems (TOCS), 7(3):247_280, 1989.

[45] John Clark and Jeremy Jacob. Attacking authentication protocols. High Integrity Systems, 1:465_474, 1996.

[46] ISO. Information Technology - Security Techniques - Entity Authentication - Part 2: Mechanisms Using Symmetric Encipherment Algorithms ISO/IEC 9798-2, 2nd edition, 1999, International Standard.

[47] ISO. Information Technology - Security Techniques - Key Management - Part 2: Mechanisms Using Symmetric Techniques ISO/IEC11770-2, 2nd edition, 1996, International Standard.

[48] ISO. Information Technology - Security Techniques - Entity Authentication Mechanisms – Part 3: Entity Authentication Using a Public Key Algorithm ISO/IEC 9798-3, 2nd edition, 1998, International Standard.

[49] ISO. Information Technology - Security Techniques - Key Management - Part 3: Mechanisms Using Asymmetric Techniques ISO/IEC 11770-3, 2nd edition, 1999, International Standard.