|
Completeness of CPSA
March 2012
Moses D. Liskov, The MITRE Corporation
Paul D. Rowe, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
ABSTRACT
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.
Additional Search Keywords
Cryptographic Protocol Shapes Analyzer, CPSA, Haskell, mathematical algorithms, security protocols
|
