Show simple item record

dc.contributor.authorSabour, Negar 12:54:46 (GMT) 12:54:46 (GMT)
dc.description.abstractComputer-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 5G-AKA 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.en
dc.publisherUniversity of Waterlooen
dc.subjectstatic verificationen
dc.subject5G AKAen
dc.titleStatic Verification of an Implementation of 5G-AKAen
dc.typeMaster Thesisen
dc.pendingfalse and Computer Engineeringen and Computer Engineeringen of Waterlooen
uws-etd.degreeMaster of Applied Scienceen
uws.contributor.advisorTripunitara, Mahesh
uws.contributor.affiliation1Faculty of Engineeringen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages