We use the Cryptographic Shapes Analyzer (CPSA) to analyze protocols for structural weaknesses in the Dolev-Yao adversarial model.
Current Projects:
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.
Cryptographic Binding
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. Learn more
Provenance and Authenticity Standards Assessment Working Group
The objective of our project is twofold: To employ formal-method analysis to verify that C2PA specification can indeed provide the provenance guarantees it is intended to provide; and to provide solutions to remediate any vulnerabilities that we find during our analysis. To achieve that objective, we are developing a formal model of the C2PA specification and will use that model to assess whether the C2PA specification is indeed able to provide a mechanism for the producers and custodians of any given content to assert, in a verifiable manner, that any information that has been disclosed about the creation of a given content, and actions taken since its creation, are indeed authentic. Learn more