POSTER: Towards Precise and Automated Verification of Security Protocols in Coq
Pages 2567 - 2569
Abstract
Security protocol verification using commonly-used model-checkers or symbolic protocol verifiers has several intrinsic limitations. Spin suffers the state explosion problem; Proverif may report false attacks. An alternative approach is to use Coq. However, the effort required to verify protocols in Coq is high for two main reasons: correct protocol and property specification is a non-trivial task, and security proofs lack automation. This work claims that (1) using Coq for verification of cryptographic protocols can sometimes yield better results than Spin and Proverif, and (2) the verification process in Coq can be greatly alleviated if specification and proof engineering techniques are applied. Our approach is evaluated by verifying several representative case studies. Preliminary results are encouraging, we were able to verify two protocols that give imprecise results in Spin and Proverif, respectively. Further, we have automated proofs of secrecy and authentication for an important class of protocols.
References
[1]
Bruno Barras, Samuel Boutin, Cristina Cornes, et almbox. 2002. The Coq proof assistant reference manual--version 7.2. bibinfotypeTechnical Report. bibinfoinstitutionTechnical Report 0255, INRIA.
[2]
Noomene Ben Henda. 2014. Generic and efficient attacker models in SPIN. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software. ACM, 77--86.
[3]
Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. 2017. Verified models and reference implementations for the TLS 1.3 standard candidate. bibinfothesistypePh.D. Dissertation. bibinfoschoolInria Paris.
[4]
Bruno Blanchet, Ben Smyth, and Vincent Cheval. 2016. ProVerif 1.94 pl1: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. (2016).
[5]
Tom Chothia, Ben Smyth, and Chris Staite 2015. Automatically checking commitment protocols in proverif without false attacks International Conference on Principles of Security and Trust. Springer, 137--155.
[6]
Dorothy E Denning and Giovanni Maria Sacco 1981. Timestamps in key distribution protocols. Commun. ACM Vol. 24, 8 (1981), 533--536.
[7]
Whitfield Diffie and Martin E Hellman 1976. New directions in cryptography. Information Theory, IEEE Transactions on Vol. 22, 6 (1976), 644--654.
[8]
Danny Dolev and Andrew C Yao 1983. On the security of public key protocols. Information Theory, IEEE Transactions on Vol. 29, 2 (1983), 198--208.
[9]
Mohamed Amine Ferrag, Leandros A Maglaras, Helge Janicke, and Jianmin Jiang 2016. Authentication Protocols for Internet of Things: A Comprehensive Survey. arXiv preprint arXiv:1612.07206 (2016).
[10]
Murat Moran and Dan S Wallach 2017. Verification of STAR-Vote and Evaluation of FDR and ProVerif. arXiv preprint arXiv:1705.00782 (2017).
[11]
Roger M Needham and Michael D Schroeder 1978. Using encryption for authentication in large networks of computers. Commun. ACM Vol. 21, 12 (1978), 993--999.
[12]
Makoto Tatebayashi, Natsume Matsuzaki, and David B Newman. 1989. Key distribution protocol for digital mobile communication systems Conference on the Theory and Application of Cryptology. Springer, 324--334. endthebibliography
Index Terms
- POSTER: Towards Precise and Automated Verification of Security Protocols in Coq
Recommendations
Local abstract verification and refinement of security protocols
FMSE '08: Proceedings of the 6th ACM workshop on Formal methods in security engineeringThe verification problem for security protocols is undecidable, but it is feasible to verify protocols by abstract interpretation. This paper presents a method based on local abstraction and refinement for verifying security protocols terminably. Local ...
Strategy for Verifying Security Protocols with Unbounded Message Size
We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy ...
A Method for Patching Interleaving-Replay Attacks in Faulty Security Protocols
The verification of security protocols has attracted a lot of interest in the formal methods community, yielding two main verification approaches: i) state exploration, e.g. FDR [Gavin Lowe. Breaking and fixing the needham-schroeder public-key protocol ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2017
2682 pages
ISBN:9781450349468
DOI:10.1145/3133956
- General Chair:
- Bhavani Thuraisingham,
- Program Chairs:
- David Evans,
- Tal Malkin,
- Dongyan Xu
Copyright © 2017 Owner/Author.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 30 October 2017
Check for updates
Author Tags
Qualifiers
- Poster
Conference
CCS '17
Sponsor:
CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security
October 30 - November 3, 2017
Texas, Dallas, USA
Acceptance Rates
CCS '17 Paper Acceptance Rate 151 of 836 submissions, 18%;
Overall Acceptance Rate 1,261 of 6,999 submissions, 18%
Upcoming Conference
CCS '25
- Sponsor:
- sigsac
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 209Total Downloads
- Downloads (Last 12 months)10
- Downloads (Last 6 weeks)3
Reflects downloads up to 25 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in