ekmixon / cpsaexp Goto Github PK

CPSA4: Crptographic Protocol Shapes Analyzer Version 4

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.

CPSA4 is based on a refactoring of CPSA2.  It is destinct from CPSA3.
It is used to experiment with new features.  It is where a different
security goal language, the strand-oriented language described in
"Deducing Security Goals From Shape Analysis Sentences"
<https://arxiv.org/abs/1204.0480>, was first implemented.  The size of
the formulas expressed in the strand-oriented language is typically
smaller than the ones produced using the previous node-oriented
language, an important property when the formulas are used to interact
with theorem provers and proof assistants.

CPSA4 provides rules and facts.  Rules are associated with protocols,
and facts are associated with skeletons.  A rule is a geometric
formula that is used as a rewrite rule, and a fact is a named relation
between values.

CPSA4 provides channels.  Channels are designed to model confidential
and authenticated communication channels.

This program has been built and tested using the Haskell miminal
installer and Haskell Platform.  THese are available from
<http://haskell.org> or from an operating system specific source.  The
name of the Linux package is usually haskell-platform.  If you have
problems installing Haskell, try using Haskell Stack, and issue the
commands "stack init; stack build, stack install".

INSTALLING FROM A TARBALL

Build and install with:

$ cabal build
$ cabal install
: To find the directory containing documentation and samples, type:
$ cpsa4 -h

QUICK START (Linux)

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

QUICK START (Mac)

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

QUICK START (Windows)

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 build
C:\...> cabal install

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

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

MAKEFILE

To start your own project, create a fresh directory and then type:

$ cpsa4init

This will create a Makefile that automates the analysis process.  For
Windows, it will also create Make4.hs, a cpsa build script written in
Haskell.

PARALLELISM

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

DOCUMENTATION

The starting point for CPSA documentation doc/index.html.  Most users
should read it and skip the rest of this section.  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.

TEST SUITE

Cabal currently fails to preserve permissions correctly.  To fix this
problem, type:

$ /bin/sh fixperms

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

ADDITIONAL PROGRAMS

The src directory of the source distributions includes programs
written in Scheme, Prolog, Elisp, and OCamlq 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.

KNOWN BUGS

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