Paradigms in Security Protocol Verification: A Multi-Tool Analysis
DOI:
https://doi.org/10.54654/isj.v3i23.1059Keywords:
Verification protocol, falsification protocol, analysis protocol, security, cryptographyTóm tắt
In the realm of internet security, ensuring the robustness and integrity of communication protocols is paramount. This paper offers a comprehensive analysis of four leading tools for security protocol verification: Scyther, ProVerif, CryptoVerif, and Tamarin. Each tool is evaluated for its unique strengths and applications, particularly in the contexts of cloud computing and IoT. The study begins with Scyther, highlighting its proficiency in automated falsification and multi-protocol verification. Next, ProVerif is examined for its capabilities in symbolic reasoning and its efficiency in handling complex security protocols. The paper then explores CryptoVerif’s computational approach to protocol verification, focusing on how it models and verifies protocols under a variety of cryptographic assumptions. Finally, Tamarin’s advanced features in symbolic analysis and its ability to manage intricate security properties are discussed, emphasizing its depth in formal protocol verification. This comparative analysis not only underscores the distinct contributions of each tool but also provides a broader perspective on their effectiveness in addressing both current and emerging security challenges. By dissecting the methodologies and limitations of these tools, the paper aims to offer valuable insights into the evolving landscape of security protocol verification and potential future directions in this critical area of cybersecurity research.
Downloads
References
M. A. Fikri, K. Ramli, and D. Sudiana, “Formal Verification of the Authentication and Voice Communication Protocol Security on Device X Using Scyther Tool,” IOP Conf. Ser. Mater. Sci. Eng., vol. 1077, no. 1, p. 012057, Feb. 2021. doi: 10.1088/1757-899X/1077/1/012057.
N. Dalal, J. Shah, K. Hisaria, and D. Jinwala, “A Comparative Analysis of Tools for Verification of Security Protocols,” Int. J. Commun. Netw. Syst. Sci., vol. 03, no. 10, pp. 779–787, 2010. doi: 10.4236/ijcns.2010.310104.
H. A. Elbaz, M. H. Abd-elaziz, and T. M. Nazmy, “Analysis and Verification of a Key Agreement Protocol over Cloud Computing Using Scyther Tool,” vol. 2, no. 2, 2014.
L. Chen and C. Kudla, “Identity based authenticated key agreement protocols from pairings,” in 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., Pacific Grove, CA, USA: IEEE Comput. Soc, 2003, pp. 219–233. doi: 10.1109/CSFW.2003.1212715.
Y. Yang, H. Yuan, L. Yan, and Y. Ruan, “Post‐quantum identity‐based authenticated multiple key agreement protocol,” ETRI J., vol. 45, no. 6, pp. 1090–1102, Dec. 2023, doi: 10.4218/etrij.2022-0320.
C. J. Cremers, “The Scyther Tool: Verification, falsification, and analysis of security protocols,” in International Conference on Computer Aided Verification, Springer, 2008, pp. 414–418. Accessed: Nov. 04, 2016. Available: http://link.springer.com/chapter/10.1007/978-3-540-70545-1_38.
C. J. F. Cremers, “Unbounded verification, falsification, and characterization of security protocols by pattern refinement,” in Proceedings of the 15th ACM conference on Computer and communications security, Alexandria Virginia USA: ACM, Oct. 2008, pp. 119–128. doi: 10.1145/1455770.1455787.
C. Xi and L. Siqi, “Research on semantics and algorithm of formal analysis tool Scyther,” in 2022 IEEE 4th International Conference on Civil Aviation Safety and Information Technology (ICCASIT), Dali, China: IEEE, Oct. 2022, pp. 1058–1074.doi: 10.1109/ICCASIT55263.2022.9987170.
X. Zhang, Y. Zhu, C. Gu, and X. Miao, “A Formal Verification Method for Security Protocol Implementations Based on Model Learning and Tamarin,” J. Phys. Conf. Ser., vol. 1871, no. 1, pp. 012102, Apr. 2021, doi: 10.1088/1742-6596/1871/1/012102.
S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The TAMARIN Prover for the Symbolic Analysis of Security Protocols,” in Computer Aided Verification, vol. 8044, N. Sharygina and H. Veith, Eds., in Lecture Notes in Computer Science, vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 696–701. doi: 10.1007/978-3-642-39799-8_48.
Y. Xiong, C. Su, W. Huang, F. Miao, W. Wang, and H. Ouyang, “Verifying Security Protocols using Dynamic Strategies,” Aug. 25, 2019, arXiv: arXiv:1807.00669. A Jan. 18, 2024. Available: http://arxiv.org/abs/1807.00669.
D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols,” IEEE Secur. Priv., vol. 20, no. 3, pp. 24–32, May 2022, doi: 10.1109/MSEC.2022.3154689.
P.V. Hau and D. T. T. Hien, “Enhancing Web Application Security: A Deep Learning and NLP-based Approach for Accurate Attack Detection” in Journal of Science and Technology on Information Security, vol. 3, no. 20, pp. 77-87, December 2023. doi: https://doi.org/10.54654/isj.v3i20.1008.
B. Blanchet, “The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm,” Electron. Proc. Theor. Comput. Sci., vol. 373, pp. 14–22, Nov. 2022, doi: 10.4204/EPTCS.373.2.
J. Yao, C. Xu, D. Li, S. Lin, and X. Cao, “Formal Verification of Security Protocols: ProVerif and Extensions,” in Artificial Intelligence and Security, vol. 13339, X. Sun, X. Zhang, Z. Xia, and E. Bertino, Eds., in Lecture Notes in Computer Science, vol. 13339, pp. 500–512, Cham: Springer International Publishing, 2022. doi: 10.1007/978-3-031-06788-4_42.
E.-Y. Yap, J.-J. Chin, and A. Goh, “Verifying MQV-Based Protocols Using ProVerif,” in IT Convergence and Security, vol. 782, H. Kim and K. J. Kim, Eds., in Lecture Notes in Electrical Engineering, vol. 782, pp. 55–63, Singapore: Springer Singapore, 2021. doi: 10.1007/978-981-16-4118-3_6.
M. Abadi, B. Blanchet, and C. Fournet, “The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication,” 2016, arXiv. doi: 10.48550/ARXIV.1609.03003.
B. Blanchet and B. Smyth, “Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers,” in 2016 IEEE 29th Computer Security Foundations Symposium (CSF), Lisbon: IEEE, pp. 310–324, Jun. 2016. doi: 10.1109/CSF.2016.29.
B. Blanchet, “CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels),” 2023, arXiv. doi: 10.48550/ARXIV.2310.14658.
K. Cohn-Gordon, C. Cremers, B. Dowling, L. Garratt, and D. Stebila, “A Formal Security Analysis of the Signal Messaging Protocol,” J. Cryptol., vol. 33, no. 4, pp. 1914–1983, Oct. 2020. doi: 10.1007/s00145-020-09360-1.
K. Bhargavan, B. Blanchet, and N. Kobeissi, “Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate,” in 2017 IEEE Symposium on Security and Privacy (SP), San Jose, CA, USA: IEEE, pp. 483–502, May 2017, doi: 10.1109/SP.2017.26.
B. Blanchet, "Dealing with Dynamic Key Compromise in Crypto Verif," in 2024 IEEE 37th Computer Security Foundations Symposium (CSF), Enschede, Netherlands, pp. 495-510 2024. doi:10.1109/CSF61375.2024.00015.
B. Lipp, B. Blanchet, and K. Bhargavan, “A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol,” in 2019 IEEE European Symposium on Security and Privacy (EuroS&P), Stockholm, Sweden: IEEE, Jun. 2019, pp. 231–246. doi: 10.1109/EuroSP.2019.00026.
B. Blanchet, P. Boutry, C. Doczkal, B. Grégoire and P. -Y. Strub, "CV2EC: Getting the Best of Both Worlds," 2024 IEEE 37th Computer Security Foundations Symposium (CSF), Enschede, Netherlands, pp. 279-294, 2024, doi: 10.1109/CSF61375.2024.00019.
T. M. C. Le, X. T. Pham, and V. T. Le, “Advancing Security Protocol Verification: A Comparative Study of Scyther, Tamarin” in Journal of Technical Education Science, vol. 19, no. 1, pp. 43–53, Feb. 2024. doi: 10.54644/jte.2024.1523.
T. L. Vinh, H. Cagnon, S. Bouzefrane, and S. Banerjee, “Property-based token attestation in mobile computing: Property-based token attestation in mobile computing,” in Concurr. Comput. Pract. Exp., pp. e4350, Oct. 2017. doi: 10.1002/cpe.4350.
Downloads
Published
How to Cite
Issue
Section
License
Proposed Policy for Journals That Offer Open Access
Authors who publish with this journal agree to the following terms:
1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
2. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
3. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
Proposed Policy for Journals That Offer Delayed Open Access
Authors who publish with this journal agree to the following terms:
1. Authors retain copyright and grant the journal right of first publication, with the work [SPECIFY PERIOD OF TIME] after publication simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
2. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
3. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
