Recent work investigated the use of rely/guarantee reasoning for verifying the Needham-Schroeder-Lowe security protocol. Rely/guarantee reasoning is an approach designed for verifying concurrent algorithms. The benefits of rely/guarantee are its compositional approach and its ability to uncover the assumptions required by the components of a system. Applying rely/guarantee to security protocols allows the underlying assumptions to be clearly understood.
This project will investigate the use of rely/guarantee reasoning on further, more complex security protocols. The use of refinement with rely/guarantee would allow families of security protocols to be verified, by reasoning about the assumptions that hold across the whole family and then using refinement to show that particular protocols in the family are correct.
Requirements: The project is suitable for Bachelor, Masters and Honours students and can be adapted to suit 12 or 24 unit projects. Students should have an interest and some understanding of formal methods and logic. No knowledge of security protocols is necessary. Feel free to arrange a chat with Nisansala Yatapanage (nisansala.yatapanage@anu.edu.au) to discuss your suitability and to find out more details about the project, to figure out whether you’re interested in it.