The Cryptographic Protocol Shapes Analyzer (CPSA) is a program for automatically characterizing the possible executions of a protocol compatible with a specifed partial execution.
Completeness of CPSA
Download Resources
PDF Accessibility
One or more of the PDF files on this page fall under E202.2 Legacy Exceptions and may not be completely accessible. You may request an accessible version of a PDF using the form on the Contact Us page.
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.