[CPSA User Guide] [CPSA Primer] [CPSA and Formal Security Goals] [CPSA Overview] [CPSA Introductory Slides] [CPSA Correctness Proof]
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, an overview, and some slides. The user guide provides usage information for each program in the CPSA package. The primer provides an English language description of the CPSA algorithm and is the primary user documentation. The overview is another attack at user documentation and includes an introduction to the Rely-Guarantee Method of demonstrating that a protocol achieves its security goals. This is an advanced technique beginners should feel free to ignore.
At this point, new users should open the introductory slides and 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, click on Make.hs and type build at
the GHCi prompt *Make>.
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,
Safari, and later versions of Internet Explorer. See the section
on visualization in the user
guide for help interpreting these documents.
New users should study CPSA's analysis of the following protocols
in order, Blanchet (blanchet.xhtml), 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.
An analysis of Needham-Schroeder
using security goals is
in goals.xhtml. This example can safely be ignored by
new users.
To make effective use of CPSA, new users should scan the user guide to get a flavor of its contents, and then read the primer. The remainder of this document contains some usage tips to be read after running CPSA and learning to understand its output.
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.
The source distribution contains additional programs and a test suite with many examples. The README in the top-level directory of the source distribution contains the installation instructions and is essential reading for its effective use. Serious users should favor the source distribution if on a Unix-like platform.
Authentication tests guide the search for new skeletons in CPSA.
The authentication test solved at each step of the search is
described by the operation form in CPSA output. When CPSA
generates unexpected output, find the first skeleton in the
derivation tree that exhibits the problem and read
the operation form to find out what happened.
Authentication tests are introduced in
the primer and described in full
detail in the The CPSA
Specification.
An origination assumption
(non-orig, pen-non-orig,
and unig-orig), can be specified in a role or in a
skeleton. Be sure to read the advice in
the primer on the proper placement of
origination assumptions.
Variables of sort message unify with any message. See Otway-Rees
(or.xhtml) for an example of the use of variables of this
sort.
A quoted string is a constant of sort message and is called a tag. Tags can be used to distinguish messages that have similar structure in the case where the implementation of the protocol contains protections against message conflation.
Lisp-like macros in cpsa input can be used to replace
multiple occurrences of a message with one named definition of it.
Macros are described in the primer.
When the cpsagraph program is given
the --zoom option, it produces diagrams that scale.
This is useful when viewing large diagrams.
In CPSA, a security goal is expressed as a sentence in first-order
logic. It asserts that if some properties hold for a skeleton, then
some other properties must hold for all shapes computed by CPSA
starting with the skeleton. Security goals can be used to state
authentication and secrecy goals of a protocol. See
CPSA and Formal Security Goals. An
analysis of Needham-Schroeder using first-order logic is
in goals.xhtml.
When the cpsapp program is given
the --json option, it translates S-expressions into
JavaScript Object Notation (JSON). The cpsajson
program translates JSON into S-expressions. These two programs
makes it easy to manipulate CPSA input and output using Python or
other languages with JSON libraries.
The goal of CPSA is to automatically characterize the possible executions of a protocol compatible with a specified partial execution. There is a rigorous proof that the algorithm enumerates all of these characterizations.
The specification describes the CPSA algorithm as a term reduction system. The design describes implementation choices made and should be read when viewing the source code.