cpsa: Symbolic cryptographic protocol analyzer

[ bsd3, cryptography, program ] [ Propose Tags ]

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.

For each input problem, the CPSA program is given some initial behavior, and it discovers what shapes are compatible with it. Normally, the initial behavior is from the point of view of one participant. The analysis reveals what the other participants must have done, given the participant's view. The search is based on a high-level algorithm that was claimed to be complete, i.e. every shape can in fact be found in a finite number of steps. Further theoretical work showed classes of executions that are not found by the algorithm, however it also showed that every omitted execution requires an unnatural interpretation of a protocol's roles. Hence the algorithm is complete relative to natural role semantics.

The package contains a set of programs used to perform and display the analysis. A standards complient browser, such as Firefox, Safari, or Chrome, is required to display the results. Program documentation is in the doc directory in the source distribution, and installed in the package's data directory. You can locate the package's data directory by typing "cpsa --help" to a command prompt. New users should start learning to use the tool from the manual, found at "cpsamanual.pdf" in the data directory. Examples referenced in the manual can be found in the data directory as well. It is suggested that users make an examples directory and copy "*.scm *.xhtml" to their local examples directory, both so that they may be modified and for ease of access.

Serious Windows users should install MSYS so as to allow the use of make and script execution.

The theory and algorithm used by CPSA was developed with the help of Joshua D. Guttman, John D. Ramsdell, Jon C. Herzog, Shaddin F. Doghmi, F. Javier Thayer, Paul D. Rowe, and Moses D. Liskov. John D. Ramsdell and Moses D. Liskov implemented the algorithm in Haskell. CPSA was designed and implemented at The MITRE Corporation.

[Skip to Readme]
Versions [faq] 2.0.0, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.1.0, 2.1.1, 2.1.2, 2.2.0, 2.2.1, 2.2.2, 2.2.3, 2.2.4, 2.2.5, 2.2.6, 2.2.7, 2.2.8, 2.2.9, 2.2.10, 2.2.11, 2.2.12, 2.2.13, 2.3.0, 2.3.1, 2.3.2, 2.3.3, 2.3.4, 2.3.5, 2.4.0, 2.5.0, 2.5.1, 2.5.2, 2.5.3, 2.5.4, 3.3.0, 3.3.1, 3.3.2, 3.4.0, 3.4.1, 3.5.0, 3.5.1, 3.6.0, 3.6.1, 3.6.2, 3.6.3, 3.6.4, 3.6.5
Change log ChangeLog
Dependencies array, base (>=3 && <5), containers, parallel [details]
License BSD-3-Clause
Maintainer mliskov@mitre.org
Category Cryptography
Uploaded by mliskov at Fri Jun 3 19:25:19 UTC 2016
Distributions NixOS:3.6.5
Executables cpsasas, cpsadiff, cpsajson, cpsapp, cpsaannotations, cpsashapes, cpsagraph, cpsa
Downloads 27114 total (1728 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
All reported builds failed as of 2016-11-24 [all 3 reports]


Maintainer's Corner

For package maintainers and hackage trustees

Readme for cpsa-3.3.1

[back to package description]
CPSA: Cryptographic Protocol Shapes Analyzer

This program has been built and tested using Haskell Platform.
It is available from <http://haskell.org> or from an operating
system specific source.  The name of the Linux package is usually

If the Internet is available, install CPSA with:

$ cabal update
$ cabal install cpsa

Find the documentation directory by typing "cpsa -h" in a command
shell, and view index.html in a browser.



: To build and install CPSA type:
$ make
$ make install

: To analyze a protocol you have put in prob.scm type:
$ cpsa -o prob.txt prob.scm
$ cpsagraph -o prob.xhtml prob.txt
$ firefox -remote "openFile(`pwd`/prob.xhtml)"

: Documentation and samples are in the directory given by
$ cpsa -h

: To view the user guide:
$ firefox -remote "openFile($HOME/share/cpsa-X.Y.Z/doc/cpsauser.html)"
: where X.Y.Z is the CPSA version number.


: To build and install CPSA type:
$ make
$ make install

: To analyze a protocol you have put in prob.scm type:
$ cpsa -o prob.txt prob.scm
$ cpsagraph -o prob.xhtml prob.txt
$ open prob.xhtml

: Documentation and samples are in the directory given by
$ cpsa -h

: To view the user guide:
$ open $HOME/share/cpsa-X.Y.Z/doc/cpsauser.html
: where X.Y.Z is the CPSA version number.


The software has been tested on a Windows system on which neither
MinGW or Cygwin has been installed.  Install GHC and then run the
"setup.bat" batch file with administrator privileges.

If you do not have administrator privileges, run:

C:\...> runghc Setup.hs configure --user
C:\...> runghc Setup.hs build

The executables will be found in the dist\build subdirectories.

Documentation and samples are in the directory given by
C:\...> cpsa -h

The installed programs can be run from the command prompt or via a
batch file.  Alternatively, copy doc/Make.hs into the directory
containing your CPSA problem statements, and load it into a Haskell
interpreter.  Read the source for usage instructions.


The file $HOME/share/cpsa-X.Y.Z/doc/cpsa.mk contains useful GNU Make
rules for inclusion, where X.Y.Z is CPSA version number.

Alternatively, copy the file Make.hs in the same directory into the
directory containing your CPSA problem statements.  The source file
has usage instructions.


CPSA is built so it can make use of multiple processors.  To make use
of more than one processor, start CPSA with a runtime flag that
specifies the number of processors to be used, such as "+RTS -N4
-RTS".  The GHC documentation describes the -N option in detail.


The starting point for CPSA documentation doc/index.html.  Most users
should read it and skip the rest of this section.

To build the documentation, the file supp-pdf.tex must be installed.
It is part of the TexLive texmf ConTeXt package.  On Linux, the name
of the package is context or texlive-context.  The design document and
the specification document require the xy-pic package, which is
included in texlive-pictures.

The documentation includes a user guide as an XHTML document, and
three LaTeX documents.  The CPSA Primer provides the background
required to make effective use of the CPSA tool collection.  For those
interested in the implementation, The CPSA Theory contains a
high-level description of the algorithm and the current state of the
effort to show that when program terminates, it produces a description
of every possible execution of the protocol consistent with the
initial point-of-view skeleton.  The CPSA Specification formally
describes the implemented algorithm as a term reduction system.  The
CPSA Design describes implementation details and assumes The CPSA
Specification has been read.  The CPSA Design should be read if one is
interested in reading the Haskell source for the tool collection.


: To run the test suite type:
$ ./cpsatst

Tests with the .scm extension are expected to complete without error,
tests with the .lsp extension are expected to fail, and tests with the
.lisp extension are not run.  New users should read tst/README, and
then browse the files it suggests while reading CPSA documentation.

Don't develop your protocols in the tst directory.  The Makefile is
optimized for testing the cpsa program, not analyzing protocols.


The src directory of the source distributions includes programs
written in Scheme, Prolog, and Elisp for performing tasks.  Use them
as templates for your special purpose CPSA analysis and transformation
needs.  Also, when given the --json option, the CPSA pretty printer
cpsapp will transform CPSA S-expressions into JavaScript Object
Notation (JSON).

On Linux, the GHC runtime can request so much memory that thrashing
results.  The script in src/ghcmemlimit sets an environment variable
that limits memory to the amount of free and reclaimable memory on
your machine.


Variable separation in generalization fails to separate variables in
terms of the form (ltk a a).