[Haskell-cafe] ANN: CPSA - Cryptographic Protocol Shapes Analyzer

[John D. Ramsdell]

The Cryptographic Protocol Shapes Analyzer (CPSA) has been released on
Hackage at <http://hackage.haskell.org/package/cpsa>.  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 descovers 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 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.