Protocol Analysis Lab (PAL)

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)


  • Post-Quantum Pake Protocols

Potential Impact