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.


Interested in MITRE's Work?

MITRE provides affordable, effective solutions that help the government meet its most complex challenges.
Explore Job Openings

Publication Search