Advancing Security Protocol Verification: A Comparative Study of Scyther, Tamarin
Corressponding author's email:
chaultm@hcmute.edu.vnDOI:
https://doi.org/10.54644/jte.2024.1523Keywords:
Verification Protocol, Falsification Protocol, Analysis Protocol, Scynther, TamarinAbstract
In the dynamic field of Internet security, verifying and analyzing security protocols is crucial for ensuring secure and effective communication. This paper presents an analysis of leading tools used for the verification, falsification, and analysis of security protocols, focusing particularly on Scyther and Tamarin. We examine the methodologies, capabilities, and applications of these tools in various contexts, including cloud computing and IoT, highlighting their unique approaches and contributions to the field. The paper starts with an examination of the Scyther tool, emphasizing its innovative approach to automated falsification and verification, and its application in multi-protocol analysis. We then transition to exploring the use of Scyther in verifying key agreement protocols in cloud computing. A comparative analysis of Scyther and Tamarin is also presented, shedding light on their effectiveness in identifying security properties and revealing the strengths and weaknesses of different protocols. This is further enriched by a detailed look at the unbounded verification capabilities of Scyther. Additionally, the paper covers the capabilities of the Tamarin prover, exploring its advanced features in symbolic analysis, its ability to handle complex security properties, and its application in verifying protocol implementations. Through this paper, we aim to provide a comprehensive overview of the current landscape in security protocol verification, offering insights into the methodologies, challenges, and future directions in this essential area of research.
Downloads: 0
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. DOI: https://doi.org/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. DOI: https://doi.org/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. DOI: https://doi.org/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. DOI: https://doi.org/10.4218/etrij.2022-0320
C. J. F. Cremers, “The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols,” in Computer Aided Verification, vol. 5123, A. Gupta and S. Malik, Eds., in Lecture Notes in Computer Science, vol. 5123. , Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 414–418. doi: 10.1007/978-3-540-70545-1_38. DOI: https://doi.org/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. DOI: https://doi.org/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. DOI: https://doi.org/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, p. 012102, Apr. 2021, doi: 10.1088/1742-6596/1871/1/012102. DOI: https://doi.org/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. DOI: https://doi.org/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.” arXiv, Aug. 25, 2019. Accessed: Jan. 18, 2024. [Online]. 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. DOI: https://doi.org/10.1109/MSEC.2022.3154689
Downloads
Published
How to Cite
Issue
Section
Categories
License
Copyright (c) 2024 Journal of Technical Education Science
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
Copyright © JTE.
