TY - GEN
T1 - A Formally Verified Scheme for Security Protocols with the Operational Semantics of Strand Space
AU - Li, Yongjian
AU - Jiang, Hongjian
AU - Zhao, Yongxin
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
PY - 2024
Y1 - 2024
N2 - Security protocols are essential to ensure privacy, integrity, and authentication. However, to guarantee the security objectives of a protocol, formal tools are necessary. Currently, existing formal tools employ specific input languages to model protocols. Typically, protocols are presented in strand space specification format in textbooks, which depict the messages shared among trusted communication participants during a correct protocol operation. Strand space specifications prioritize conciseness and readability over formal preciseness, and their formal semantics are only considered and clarified in specific contexts. Therefore, a gap exists between strand space specifications and the modelling languages of formal tools. To address this issue, we propose a verified security scheme with the operational semantics of strand space. We successfully tested our framework on several typical protocol benchmarks using the model checker Murphi and identified potential attacks on them. In summary, our framework offers an innovative and comprehensible scheme for model checking security protocols.
AB - Security protocols are essential to ensure privacy, integrity, and authentication. However, to guarantee the security objectives of a protocol, formal tools are necessary. Currently, existing formal tools employ specific input languages to model protocols. Typically, protocols are presented in strand space specification format in textbooks, which depict the messages shared among trusted communication participants during a correct protocol operation. Strand space specifications prioritize conciseness and readability over formal preciseness, and their formal semantics are only considered and clarified in specific contexts. Therefore, a gap exists between strand space specifications and the modelling languages of formal tools. To address this issue, we propose a verified security scheme with the operational semantics of strand space. We successfully tested our framework on several typical protocol benchmarks using the model checker Murphi and identified potential attacks on them. In summary, our framework offers an innovative and comprehensible scheme for model checking security protocols.
UR - https://www.scopus.com/pages/publications/105001431078
U2 - 10.1007/978-3-031-64626-3_18
DO - 10.1007/978-3-031-64626-3_18
M3 - 会议稿件
AN - SCOPUS:105001431078
SN - 9783031646256
T3 - Lecture Notes in Computer Science
SP - 306
EP - 323
BT - Theoretical Aspects of Software Engineering - 18th International Symposium, TASE 2024, Proceedings
A2 - Chin, Wei-Ngan
A2 - Xu, Zhiwu
PB - Springer Science and Business Media Deutschland GmbH
T2 - 18th International Symposium on Theoretical Aspects of Software Engineering, TASE 2024
Y2 - 29 July 2024 through 1 August 2024
ER -