Formal verification of TLS 1.2 by automatically generating proof scores
Duong Dinh Tran, Kazuhiro Ogata
Abstract
Our previous work has proposed an approach and a tool supporting it, called Invariant Proof Score Generator (IPSG), that can automatically generate formal proofs, called proof scores, for formal verification of invariant properties. In this work, we present some improvements of the tool that are helpful when conducting formal verification in practice. We demonstrate the practicability of the tool with the TLS 1.2 Handshake Protocol, which is one of the most important cryptographic protocols in use today, securing numerous internet communications. We formally verify that the protocol enjoys two properties including the secrecy property and the authentication property by employing IPSG to infer proof scores. TLS is much more complex than academic protocols, and hence, through the case study, the practicability of the tool is confirmed. Moreover, the correctness of the generated proof scores is once more verified with the use of two extensions of CafeInMaude - a CafeOBJ interpreter implemented in Maude, ensuring that there is not any subtle error in the proof scores generated by our tool. In addition to the case studies reported in our previous work as well as the TLS case study presented in this paper, we also report experimental results of the tool with several other protocols.