Formal Verification of Security Protocols: ProVerif and Extensions

Secure protocols are built on cryptographic algorithms, which provide a variety of secure services to realize secure communications in a network environment. To improve the quality of security protocols and ensure their reliability, sufficient verification and testing are required. ProVerif is a classic formal verification tool for security protocols, and we describe its working mechanism and verification process in detail. In this paper, we focus on ProVerif and extensions in the verification of security protocols. We introduce some representative solutions to illustrate verification with ProVerif. And we also introduce its extension tools for protocols with stateful properties, protocols with algebraic properties, and protocol implementations, then summarize the general method of ProVerif extension tools. Finally, we discuss possible future research points, including the extension of ProVerif for protocols that combined stateful and algebraic properties, verification of security applications in SDN networks, and building models from protocol implementations without source code.