With the development of formal analysis technology of security protocols, automatic verification using tools has been realized, but modeling still needs to rely on manual modeling by professionals, which is difficult and costly and limits the further spread of formal analysis technology. In order to improve the automation of formal modeling, this paper proposed a scheme of formal assistant modeling based on security protocol code. Firstly, the method used taint analysis to obtain communication processes and record the cryptographic primitive operations. Then, it constructed the protocol communication state machine according to the sequential relationship between communication processes. Finally, it generated a formal model according to the syntax of Tamarin, a mainstream formal analysis tool for security protocols. Experimental results show that this scheme can generate the key parts of the formal model and improves the degree of automation of the formal modeling, which contributes to the spread of formal analysis technology.

[2022-12-07] Accepted Paper /doc/2022.08.0446/v1

[2023-04-05] Printed Article /doc/2022.08.0446/v2