[CPSA User Guide] [CPSA Primer] [CPSA Overview]

CPSA

The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to enumerate all essentially different executions possible for a cryptographic protocol. We call them the shapes of the protocol. Naturally occurring protocols have only finitely many, indeed very few shapes. Authentication and secrecy properties are easy to determine from them, as are attacks and anomalies.

CPSA comes with a user guide, a primer, and an overview. To make effective use of CPSA, new users should read the primer.

Start using CPSA by analyzing the protocols that come with this document. Copy the contents of this directory to a place that allows it to be modified. In a Unix shell, type:

$ echo build | ghci Make.hs

In Windows, you can click on Make.hs and type build. The CPSA User Guide describes a better way to analyze protocols when GNU Make is available.

After running the analysis, you will note files with the extension .xhtml. These are XHTML/SVG compound documents that can be viewed by standards compliant browsers such as Firefox, Chrome, or Safari.

New users should study CPSA's analysis of the following protocols in order, Needham-Schroeder (ns.xhtml), Woo-Lam (woolam.xhtml), Yahalom (yahalom.xhtml), ffgg (ffgg.xhtml), and finally Otway-Rees (or.xhtml). When studying the full output, simultaneously display the extracted shapes. The shapes file has an extension of _shapes.xhtml.

Choose a small, simple protocol for your first analysis task. When analyzing complex protocols, analyze small parts of the protocol first, and then enrich the description of the problem.