Research on Security Protocol Analysis Tool SmartVerif

Abstract

Security protocols have been designed to protect the security of the network. However, many security protocols cannot guarantee absolute security in real applications. Therefore, security tests of the network protocol become particularly important. In this paper, firstly, we introduce SmartVerif, which is the first formal analysis tool to automatically verify the security of protocols through dynamic strategies. And then, we use SmartVerif to verify the pseudo-randomness of the encapsulated key of the Two-Pass AKE protocol, which was proposed by Liu’s in ASIACRYPT in 2020. Finally, we summary our work and show some limitations of SmartVerif. At the same time, we also point out the direction for future improvement of SmartVerif.