A Comparative Analysis of Tools for Verification of Security Protocols

Nitish Dalal, Jenny Shah, Khushboo Hisaria, Devesh Jinwala

.

DOI: 10.4236/ijcns.2010.310104                

Abstract

The area of formal verification of protocols has gained substantial importance in the recent years. The research results and subsequent applications have amply demonstrated that the formal verification tools have indeed helped correct the protocols even after being standardized. However, the standard protocol verification tools and techniques do not verify the security properties of a cryptographic protocol. This has resulted in the emergence of the security protocol verifiers to fill the need. In this paper, taking the two popular security verification tools namely Scyther and ProVerif as the basis, we identify a few security protocols and implement them in both Scyther and ProVerif, to aptly evaluate the tools, in terms of the security properties of the selected protocols. In the process, we not only characteristically present a comparative evaluation of the two tools, but also reveal interesting security properties of the protocols selected, showing their strengths and weaknesses. To the best of our knowledge, this is a unique attempt to juxtapose and evaluate the two verification tools using the selected security protocols.

Keywords

Formal Verification, Security Protocols, Attacks

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	W. Stallings, “Cryptography and Network Security: Principles and Practices.” 4th Edition, Pearson Education, ISBN-10: 0131873164 ISBN-13: 9780131873162, 2006.
[2]	D. Denning and G. Sacco, “Timestamps in Key Distribution Protocols,” Communications of the ACM, Vol. 24, No. 8, 1981, pp. 533-536.
[3]	R. Needham and M. Schroeder, “Using Encryption for Authentication in Large Networks of Computers,” Communications of the ACMx, Vol.21, No. 12, 1978, pp. 993- 999.
[4]	R. Needham and M. Schroeder, “Authentication Revisited,” ACM SIGOPS Operating Systems Review, Vol. 21, No. 1, 1987, p. 7.
[5]	G. J. Holzmann, “Software Model Checking with SPIN,” Advances in Computers, Vol. 65, 2005, pp. 78-109.
[6]	C. J. F. Cremers, “Scyther-Semantics and Verification of Security Protocols.” Ph.D. Thesis, Eindhoven University of Technology, 2006.
[7]	B. Blanchet, “An E?cient Cryptographic Protocol Veri?er Based on Prolog Rules,” Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW), Cape Breton, IEEE Computer Society, 2009, pp. 82-96.
[8]	D. Song, “Athena: A New E?cient Automatic Checker for Security Protocol Analysis,” Proceedings of the12th IEEE Computer Security Foundations Workshop (CSFW), IEEE Computer Society, 1999, pp. 192-202.
[9]	A. Armando et al., “The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications,” Proceedings of Computer Aided Veri?cation’05 (CAV), Vol. 3576 of Lecture Notes in Computer Science, Springer, 2005, pp. 281-285.
[10]	I. Kao, Lung and R. Chow, “An Efficient and Secure Authentication Protocol Using Uncertified Keys,” SIGOPS Operating Systems Review, Vol. 29, No. 3, 1995, pp. 14-21.
[11]	Verified By Visa 3-D Secure Protocol. [Online] Available: https://usa.visa.com/personal/security/vbv/index.html, last retrieved on 2nd June 2010.
[12]	M. Satyanarayanan, “Integrating Security in a Large Distributed System,” ACM Transactions on Computer Systems, Vol. 7, No. 3, 1989, pp. 247-280.
[13]	W. Simpson, “PPP Challenge Handshake Authentication Protocol (CHAP),” August 1996 http://www.ietf.org/rfc/ rfc1994.txt, last retrieved on 2nd June 2010.
[14]	W. Diffie and M. E. Hellman, “New Directions in Cryptography,” IEEE Transactions on Information Theory, Vol. 22, No. 6, 1976, pp. 644-654.
[15]	C. J. Cremers, P. Lafourcade and P. Nadeau, “Comparing State Spaces in Automatic Security Protocol Analysis,” Formal to Practical Security: Papers Issued from the 2005 -2008 French-Japanese Collaboration, Springer-Verlag, 2009, pp. 70-94.
[16]	C. J. Cremers, “Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement,” CCS’08: Proceedings of the 15th ACM conference on Computer and communications security, ACM Press, 2008, pp. 119-128.