关键词: 形式化分析工具, Scyther工具, 比较研究, 安全模型, TLS协议

Abstract: As formal verification tools for security protocols develop rapidly, picking a suitable tool, according to the target protocols and the security models, can improve not only the reliability and accuracy of protocol analysis, but also the efficiency of it. With these considerations, we compare the properties of 9 kinds of the formal verification tools in detail and we find that the Scyther tool can be an optimal choice in terms of interface interactivity, analysis efficiency and security model validity. In an attempt to facilitate using and researching of the tool for analysts in China, we study and analyze the underlying algorithm of Scyther and translate the interface into Chinese; we also update Scyther by adding a timer that can count and output the analysis time. Finally, we use the updated Scyther to make a formal analysis of the network security protocol TLS within the DelovYao model and strong security model. The current study is of theoretical and practical value for it helping researchers to select and use formal analysis tools more accurately and effectively.

Key words: formal verification tools, Scyther tool, comparison study, security model, TLS protocol