Executive Summary
With $97,000 of support from NSA, Dr. Alan Sherman is implementing a virtual Protocol Analysis Lab that uses state-of-the-art tools to analyze cryptographic protocols for structural weaknesses. Protocols are the structured communications that take place when computers interact with each other, as for example happens when a browser visits a web page. Experience has shown that protocols are so complicated to analyze that there is tremendous value in studying them using formal methods. Additionally, Sherman and his graduate students are making it easier to use existing tools including CPSA, Maude NPA, and Tamerin, applying them to analyze particular protocols, and developing associated educational materials.
Technical Challenge/Activitites
Learning Modules for Protocol Analysis Using CPSA
Alan Sherman, Enis Golaszewski, Edward Zieglar, Akshita Gorti
Formal-Methods Analysis of Cryptographic Protocols
Alan Sherman, Edward Zieglar, Enis Golaszewski, Sasha Arsenuk
How Protocols Fail
Alan Sherman, Edward Zieglar, Enis Golaszewski, Akshita Gorti, David Williams, Ian Blumenfeld
MeetingMayhem: A Network Adversary Game
Alan Sherman, Marc Olano, Edward Zieglar, Linda Oliva, Akriti Anand, Enis Golaszewski, Sudha Snigdha Kosuri, Julie Nau, Ryan Wnuk-Fink
Other PAL-related projects:
-
Secure Remote Protocol (SRP)
-
OPAQUE
-
Post-Quantum Pake Protocols
Potential Impact