Completeness of CPSA

March 2012
Topics: Data Encryption, Information Security Technologies
Moses D. Liskov, The MITRE Corporation
Paul D. Rowe, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
Download PDF (910.43 KB)

The Cryptographic Protocol Shapes Analyzer (CPSA) is a program for automatically characterizing the possible executions of a protocol compatible with a specifed partial execution. This paper presents a mathematically rigorous theory that backs up the implementation of CPSA in Haskell, and proves the algorithm produces characterizations that are complete, and that the algorithm enumerates these characterizations.


Publication Search