We use the Cryptographic Shapes Analyzer (CPSA) to analyze protocols for structural weaknesses in the Dolev-Yao adversarial model.
How Protocols Fail
We carry out case studies of several instructive examples of how cryptographic protocols fail.
Formal-Methods Analysis of OPAQUE
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.
Protocol Analysis Lab (PAL)
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.