UMBC Cyber Defense Lab

Verifying Security Properties of
Cryptographic Protocols with CPSA

Edward V. Zieglar Jr.
Analysis and Design Methods
DoD Trusted Systems Research Group

12-1pm, Friday, 15 May 2015, ITE 227

The design of cryptographic protocols with well understood properties is a difficult problem. Many simple cryptographic protocols that have been designed over the years by experienced designers have been found to have subtle flaws or incorrect assumptions that have led to attacks against them. Much effort has gone into the development of theories, techniques and tools to formally analysis the security properties of cryptographic protocols in an attempt to identify and eliminate such security flaws. This talk will address basic paradigms used in the analysis and verification of the security properties of cryptographic protocols, discuss efforts to develop tools to assist designers in developing protocols with verifiable security properties and demonstrate one such tool, the Cryptographic Protocol Shapes Analyzer (CPSA), available at https://hackage.haskell.org/package/cpsa.