Formal-Methods Analysis of Cryptographic Protocols

We use the Cryptographic Shapes Analyzer (CPSA) to analyze protocols for structural weaknesses in the Dolev-Yao adversarial model.

Current Projects:

We carry out case studies of several instructive examples of how cryptographic protocols fail.

We perform formal-methods analysis of the OPAQUE protocol, which is the best-of-breed PAKE protocols.

We study the importance of cryptographic binding in protocols, including a case study of the FIDO authentication protocol. Lead by PhD student Enis Golaszewski.

We have developed a virtual protocol analysis lab featuring CPSA and two other protocol analysis tools. We are developing CPSA-based learning modules for teaching protocol analysis, and Enis Golaszewski runs sessions open to interested students based on these modules.