Symbolic cryptographic protocol analyzer

Latest on Hackage:3.5.0

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

BSD3 licensed
Maintained by mliskov@mitre.org
CPSA: Crptographic Protocol Shapes Analyzer Version 3

The Cryptographic Protocol Shapes Analyzer (CPSA), is a software tool
designed to assist in the design and analysis of cryptographic
protocols. A cryptographic protocol is a specific pattern of
interaction between principals. TLS and IKE are some examples of
well-known cryptographic protocols.

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.

CPSA version 3 features support for Diffie-Hellman and state. The
manual in <doc/cpsamanual.pdf> provides a comprehensive description of
the program.

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.


With Cygwin or MinGW, the installation is similar to the Linux
install. The software has been tested on a Windows system on which
neither MinGW or Cygwin has been installed. Install Haskell Platform
Core and then run:

C:\...> cabal update
C:\...> cabal install parallel
C:\...> cabal configure
C:\...> cabal build
C:\...> cabal install

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.


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


2018-04-17 John D. Ramsdell <ramsdell@mitre.org>

* cpsa.cabal (Version): Tagged as 3.5.0.

2018-03-20 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/DiffieHellman/Algebra.hs (displayVar, mkVar): Changed
sort names. expn -> rndx and expr -> expt.

2018-02-12 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/SAS/SAS.hs (disjoin): Changed output to (false) on an
empty disjunction instead of (or).

2018-01-12 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Loader.hs (mkListenerRole): Changed do pattern to
be irrefutable.

2017-09-15 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/DiffieHellman/Algebra.hs (unifyTerms): Added calls to
chase before calling unifyBase which prevents a failure in the
occurs check.

2017-09-14 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Strand.hs (tryPerm): Add missing inverse
permutation to second checkOrigs in tryPerm.

2017-09-12 John D. Ramsdell <ramsdell@mitre.org>

* cpsa.cabal: Removed CPSA.Lib.CPSA globally and removed
unnecessary dependencies.

2017-08-30 John D. Ramsdell <ramsdell@mitre.org>

* cpsa.cabal: Added missing modules and source repository

* src/CPSA/Lib/DebugLibrary.hs (zi): Fixed erroneous parameters in

2017-08-28 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Cohort.hs (solved): Fixed condition 5. It was
using ct instead of ct'.

2017-06-30 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Cohort.hs (transformingNode, maybeAug, nextNode):
Rewrote code so that it no longer fails the ambiguity check.

2017-05-26 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/DiffieHellman/Algebra.hs (mkInitMatchDecis): Ensure
initial distinctions to not include fresh variables.
(partition): Do not move variables of sort expn to lhs, even if
they are freshly generated.

2017-05-16 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/DiffieHellman/Algebra.hs (displaySubst): Removed
erroneous substitution to fix substitution displaying.

2017-05-10 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Strand.hs (findReplacement, permutations): Merge
generators so that no variable in a term has an identifier that is
greater than or equal to the generator.

2017-02-02 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Basic/Algebra.hs (loadInvk): Added support for reading
(invk (privk ...)) and (invk (invk ...)).

2017-01-17 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/SAS/SAS.hs (strandForm): Remove conjoin and use
concatMap when creating a characteristic skeleton.

2017-01-09 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Loader.hs (loadPrimary): Removed generator
parameter that was not used.

2016-12-21 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Cohort.hs (solved): In Condition 4, applied
substitutions to the encryption keys before testing for

2016-10-04 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Basic/Algebra.hs (matchRenaming): Make isomorphism
check work in presence of asymmetric keys.

2016-09-30 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Algebra.hs: Added isObtainedVar for variables of
sort expr in the Diffie-Hellman algebra.

2016-08-12 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/SAS/SAS.hs (form): Changed "defsas" to "defgoal" as the
keyword for a generated shape analysis sentence. This makes the
program compatible with its documentation.

2016-06-22 John D. Ramsdell <ramsdell@mitre.org>

* cpsa.cabal (Extension): Add allow ambiguous types when compiling
with GHC 8.0.0 or later.

2016-06-21 Moses D. Liskov <mliskov@mitre.org>

* src/CPSA/DiffieHellman/Algebra.hs: Added code to implement the
"tag" sort, which quoted string tags belong to.

2016-06-03 Moses D. Liskov <mliskov@mitre.org>

* doc/examples/IKE_variants.tar.gz: Added this compressed archive
of IKEv1 and IKEv2 variant input files.

2016-03-30 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/SAS/SAS.hs: Added support for fringe skeletons so that
cpassas makes use of depth limited output. When a tree depth
limit is exceeded, a fringe labeled skeleton is printed. cpsasas
produces a sentence with a right-hand-side that encodes both the
shapes and the fringe. Thus, when cpsa is running the a tree
depth limit of one, cpsasas computes a cohort analysis sentence.

2016-03-29 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Reduction.hs (LPreskel): Added a depth field, so
that CPSA aborts when the depth of one branch exceeds a bound.

* src/CPSA/Lib/Algebra.hs: Added escapeSet to Term class and remove
protectors, thus computing the escape set in a more
straightforward way.

2015-11-23 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/SAS/Main.hs (main): Changed start up so that the herald
is read and used to find the correct algebra for further

2015-10-02 John D. Ramsdell <ramsdell@mitre.org>

* doc/{index,cpsauser}.html: Added width limit of 48em.

2015-07-09 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Graph/ExpandedView.hs (purgeTraces): By default, the
graph program now does not show traces in skeletons. Added
--show-traces option to the graph program, which restores the
previous behavior and traces are displayed in skeletons.

2015-07-02 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Algebra.hs: Added constituent to the algebra
interface and the algebras. An atom is a constituent of a term if
the atom is among the set of atoms required to construct the term.
Changed occursIn so that it just applies to variables.

2015-07-01 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/{Basic,DiffieHellman}/Algebra.hs (occursIn): Restricted
first argument of occursIn to variables and atoms and corrected
the implementation.

2015-06-30 John D. Ramsdell <ramsdell@mitre.org>

* cpsa3.cabal (Version): Tagged as 3.2.2.

2015-06-25 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Strand.hs (geq): Removed dynamic role specific test
because it erroneously reports violations. The existing static
role specific test correctly does the job.

2015-05-26 John D. Ramsdell <ramsdell@mitre.org>

* cpsa3.cabal (Version): Tagged as 3.2.1.

* src/CPSA/DiffieHellman/Algebra.hs (displayTerm): Made it so
that CPSA prints each bltk atoms in a canonical form so that the
graph program draws solid arrows when it should.

2015-04-27 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Loader.hs (ReturnFail): Added ReturnFail Monad so
that fail is correctly handled. Added Functor and Applicative
instance to support GHC 7.10 base library.

2015-04-20 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Characteristic.hs (mkDcls): Fixed tag for non-orig
and pen-non-orig.

2015-04-10 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Strand.hs (mkListener): The role used for listener
strands is now the one stored in the protocol. It has a single
variable x of sort mesg as its set of variables. This change
enables satisfaction checking on skeleton that include listeners.

2015-04-07 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Strand.hs (toSkeleton): Removed hulling to the
process of converting an input preskeleton into a skeleton as it
causes bugs in printing.

* Imported CPSA2's implementation of goals and expunged support
for subgoals.

2015-03-27 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Strand.hs (toSkeleton): Added hulling to the
process of converting an input preskeleton into a skeleton.

2015-03-25 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Goal.hs: Added uniq to goal language.

2015-03-17 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/SAS/SAS.hs (form): Generate a defsas form rather than a
naked sentence.

* src/CPSA/Lib/Loader.hs (loadPrimary): Renamed equals function
symbol to =.

2015-03-05 John D. Ramsdell <ramsdell@mitre.org>

* cpsa3.cabal (Version): Tagged as 3.2.0.

2015-02-20 John D. Ramsdell <ramsdell@mitre.org>

* Added support for subgoals within point-of-view skeletons. The
subgoals are evaluated for each shape, and (satisfies-a-subgoal)
is added to a shape when it satisfies one of the subgoals.

2014-12-11 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Entry.hs (defaultOptions): Changed the default
strand bound to 12.

2014-11-15 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/SAS/SAS.hs: Changed the language used for a shape
analysis sentence to be node-oriented.

2014-11-07 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Loader.hs (loadPriorities): Allowed priority
declarations on state synchronization nodes other than

2014-11-07 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Cohort.hs (explainable): Added the nodes reachable
by strand succession so that a transition can be explained by a
previous transition within a strand.

2014-10-31 John D. Ramsdell <ramsdell@mitre.org>

* Changed the name of the logic producing program to cpsa3sas.

2014-09-01 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/Strand.hs (noStateSplit): An observer node should have
at most one transition node after it too.

2014-08-31 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/State.hs: Made labels optional. Use "tran" for
state synchronization events with labels, and "sync" for ones

2014-08-29 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/Lib/*.hs: Added support for analyzing protocols with
state. A state synchronization event sync was added to the events
that can occur in a trace, along with a new method for state-based
augmentation. An example using sync events is in

2014-08-26 John D. Ramsdell <ramsdell@mitre.org>

* cpsa3.cabal: Removed cpsaparameters program.

2014-08-25 John D. Ramsdell <ramsdell@mitre.org>

* src/split.py: Added the skeleton split program that copies the
skeletons in a CPSA source file into separate files.

2014-08-23 John D. Ramsdell <ramsdell@mitre.org>

* src/cpsajson.py (load): Added a reader in Python for JSON
produced by CPSA's pretty printer program cpsa3pp -j.

2014-08-22 John D. Ramsdell <ramsdell@mitre.org>

* src/CPSA/JSON/Main.hs: Added the program cpsa3json that
translates JSON encoded CPSA into CPSA S-Expressions. It expects
the JSON input to follow the conventions of the JSON produced by
the cpsapp program when given the -j option.

* src/CPSA/Lib/SExpr.hs (numOrSym): Enabled parsing a number with
a plus sign by removing the sign before translating the string of
digits into a number.

2014-06-12 John D. Ramsdell <ramsdell@mitre.org>

* cpsa3.cabal (Version): Tagged as 3.0.3.

2014-02-06 John D. Ramsdell <ramsdell@mitre.org>

* cpsa3.cabal (Version): Tagged as 3.0.2.

2013-12-14 John D. Ramsdell <ramsdell@mitre.org>

* cpsa3.cabal (Version): Tagged as 3.0.1.

* cpsa3.cabal (Extra-Source-Files): Added more DH tests

2013-03-12 John D. Ramsdell <ramsdell@mitre.org>

* src/CPET/Annotations/Annotations.hs (obligation): Replaced an
irrefutable pattern that raised an exception with a maybeToList.

2013-02-21 John D. Ramsdell <ramsdell@mitre.org>

* src/CPET/DiffieHellman/Algebra.hs: Added the Diffie-Hellman
algebra based on Abelian groups.

* src/CPET/Basic/Algebra.hs: Removed support for GHC 6.x.

2013-02-06 John D. Ramsdell <ramsdell@mitre.org>

* cpet.cabal (Version): Tagged as 0.0.0.
Depends on 3 packages:
Used by 1 package:
comments powered byDisqus