UMBC Cyber Defense Lab
Using CPSA to Analyze Force-Latency Protocols
Dr. Edward Zieglar, National Security Agency
12-1 Friday, 19 April 19, ITE 227
Several cryptographic protocols have been proposed to address the Man-in-the-Middle attack without the prior exchange of keys. This talk will describe a formal analysis of one such protocol proposed by Zooko Wilcox-O’Hearn, the forced-latency defense against the chess grandmaster attack. Using the Cryptographic Protocol Shapes Analyzer (CPSA), we validate the security properties of the protocol through the novel use of CPSA’s state features to represent time. We also describe a small message space attack that highlights how assumptions made in protocol design can affect the security of a protocol in use, even for a protocol with proven security properties.
Edward Zieglar is a security researcher in the Research Directorate of the National Security Agency, where he concentrates on formal analysis and verification of cryptographic protocols and network security. He is also an adjunct professor at UMBC where he teaches courses in networking and network security. He received his master’s and doctoral degrees in computer science from UMBC.