The cpsa package

[Tags: bsd3, program]

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.

We are working towards a version of CPSA with the property that whenever it successfully terminates, every possible execution is described by its output. However, the current implementation occasionally fails to find some executions.

The package contains a set of programs used to perform and display the analysis. 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 searching for the file cpsauser.html. New users should study the documentation and the sample inputs in the data directory. The source distribution includes a test suite with an expanded set of input files and program design documentation.

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, and Paul D. Rowe. John D. Ramsdell implemented the algorithm in Haskell.

[Skip to ReadMe]


Versions2.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
Change logChangeLog
Dependenciesbase (<=, containers, parallel [details]
Executablescpsapp, cpsaparameters, cpsaannotations, cpsashapes, cpsagraph, cpsa
UploadedWed Mar 31 13:27:37 UTC 2010 by JohnRamsdell
Downloads5143 total (262 in last 30 days)
0 []
StatusDocs not available [build log]
All reported builds failed as of 2015-10-07 [all 2 reports]


parEnable use of the parallel construct parEnabledAutomatic
oldEnable support for cabal < 1.6DisabledAutomatic

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Maintainers' corner

For package maintainers and hackage trustees

Readme for cpsa-2.0.3

CPSA: A Crptographic Protocol Shapes Analyzer

This program has been built and tested using the Glasgow Haskell
Compiler (GHC), version 6.10, which is available for Linux, Macs, and
Windows.  The instructions assume GHC has been installed on your

CPSA has been built and tested with GHC 6.8 too, but to handle its old
version of Cabal, configure with:

$ runghc Setup.hs configure -fold --ghc --user --prefix="${HOME}"

The Hackage version of the Cabal file needs editing to support GHC
6.8.  Simply remove occurrences of the string "--Hackage".


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

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

: 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 in prob.scm type:
$ cpsa -o prob.txt prob.scm
$ cpsagraph -c -o prob.svg prob.txt
$ open prob.svg

: 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 from a
command prompt type:

C:\...> runghc Setup.hs configure
C:\...> runghc Setup.hs build
C:\...> runghc Setup.hs install

If you do not have administrator privileges, configure with:

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

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/ 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.


By default, 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.

If the Control.Parallel library is not installed, configure CPSA using:

$ runghc Setup.hs configure -f-par


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 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.


To make CPSA service available:

(1) Install the four programs into the CGI bin directory.

(2) Change directory to the src directory, and copy cpsacgi and into the CGI bin directory.

(3) Copy index.html, ../doc/cpsauser.html, and ../doc/cpsaprimer.pdf
into your choice of the web document directory.

(4) Make an examples directory in the web document directory.

(5) Copy ../tst/*.scm into the examples directory.


You must modify the default policy to allow unconfined executables to
make their heap memory executable, has CPSA is written in Haskell, and
its runtime puts executable code in its heap.  The policy module is in


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