Abstract
Computer-aided cryptography offers a variety of tools that are essential for ensuring the security of cryptographic protocols. These tools can assist in designing the protocol, verifying its correctness during implementation, and detecting potential side-channel attacks. In the functional correctness branch of computer-aided cryptography, program specifications are compared against program behavior using a specification language. JML is a specification language for programs written in Java, and OpenJML is one of the verifiers that can check if a Java program meets its corresponding JML specifications.
In this study, we investigate the implementation of 5GAKA from [69] and utilize the JML specification language to write specifications. We then use the OpenJML verifier to check whether the implementation satisfies these specifications, and make necessary changes to ensure that the implementation meets the specifications. Through this process, we perform a detailed analysis and uncover several flaws and bugs in the initial implementation. In other words, our study serves as a proof by construction that an implementation of the 5G-AKA specification can be automatically verified using the JML language.
Overall, this study serves as a case study for writing specifications in JML language from multiple documents written in English, highlighting the importance of using computer-aided cryptography tools to ensure the correctness of an implementation of cryptographic protocols.
Supervisor: Mahesh Tripunitara