Show simple item record

dc.contributor.authorSabour, Negar
dc.date.accessioned2023-04-24 12:54:46 (GMT)
dc.date.available2023-04-24 12:54:46 (GMT)
dc.date.issued2023-04-24
dc.date.submitted2023-04-20
dc.identifier.urihttp://hdl.handle.net/10012/19310
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.language.isoenen
dc.publisherUniversity of Waterlooen
dc.subjectstatic verificationen
dc.subjectJMLen
dc.subjectOpenJMLen
dc.subject5G AKAen
dc.titleStatic Verification of an Implementation of 5G-AKAen
dc.typeMaster Thesisen
dc.pendingfalse
uws-etd.degree.departmentElectrical and Computer Engineeringen
uws-etd.degree.disciplineElectrical and Computer Engineeringen
uws-etd.degree.grantorUniversity of Waterlooen
uws-etd.degreeMaster of Applied Scienceen
uws-etd.embargo.terms0en
uws.contributor.advisorTripunitara, Mahesh
uws.contributor.affiliation1Faculty of Engineeringen
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.typeOfResourceTexten
uws.peerReviewStatusUnrevieweden
uws.scholarLevelGraduateen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record


UWSpace

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