Research on semantics and algorithm of formal analysis tool Scyther

Current security analysis on security protocols mainly relies on computational complexity and formalization. Based on the research of formal analysis method, this paper analyze the basic semantics, security attributes and verification algorithms of Scyther in detail, including the semantic derivation rules, the structure building of the security attribute and the realization mechanism of the algorithm of the tool, and systematically present the whole structure and technical details of the semantic and algorithm of the formal analysis tool. This paper lays a foundation for the optimization and design of subsequent formal analysis tools.