Mathematical proofs are difficult to verify by a human and even those verifications are error prone. This issue is everlasting and problematic in the field of cryptography. For this reason automatic provers and computer-aided toolsets are on the rise to achieve irrevocable verifications. Our goal is to have a computer-checked security proof for IPsec. For TLS this was already done in a project called miTLS (see Microsoft, Inria, and the Joint Centre, 2014a). They have verified a security proof for the TLS handshake (see Bhargavan, Fournet, Kohlweiss, Pironti, Strub, and Zanella-Béguelin, 2014). Inspired by this we use the same computer-aided toolset, EasyCrypt (see Institute, Inria, and École Polytechnique, 2014), which is suited for cryptographic proofs.
We focus on a specific security aspect of the authenticated key exchange (AKE) model for IPsec, namely the real-or-random scenario. This means that we check if it is possible to distinguish between a randomly generated key and an exchanged key. We use the proof in progress by Heussen, Loebenberger, and Nüsken (2017), reformulate and implement it in EasyCrypt. This yields a computer checked proof for IPsec with more restrictions compared to a proof done manually. Furthermore this work presents general difficulties and limitations in the usage of EasyCrypt.