Thesis Defense
"Deployment Analyses of Cryptographic Protocols"
Jay McCarthy
Friday, July 18, 2008 at 1:00 P.M.
Lubrano Conference Room (CIT 4th Floor)
Few cryptographic protocols are used in practice, even though the security goals they provide are needed. We identify and alleviate two problems that contribute to their lack of use.
First, high-level protocol implementation languages do not accept programs that match the style used by the protocol design community. These languages are designed to implement protocol roles independently, not whole protocols. Therefore, a different program must be written for each role. Our language, WPPL, avoids this problem. It avoids the need to create a new tool-chain, however, by compiling protocol descriptions into an existing, standard role-based protocol implementation language.
Second, the practical systems properties of many cryptographic protocols are unproven. We develop analyses that automatically enable two systems properties in protocol role implementations. The first enables fault-tolerance by determining provably minimal backups. The second enables scalability by determining the session state necessary to support concurrency.
Our entire work is formalized in a mechanical proof checker, the Coq proof assistant, to ensure its theoretical reliability. Our implementations are automatically extracted from the formal Coq theory, so they are guaranteed to implement the theory.
Host: Shriram Krishnamurthi
| Page Owner: Webmaster | Last Modified: Tue Jul 8 15:38:27 2008 |