cpsa-4.4.1: doc/index.html
<?xml version="1.0" encoding="UTF-8"?>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type"
content="application/xhtml+xml; charset=UTF-8" />
<title>CPSA</title>
<style type="text/css">
h1 { text-align: center }
body { background: white; color: black; max-width: 48em }
img.pic { float: left; margin-top: 0em; margin-right: 1em }
</style>
</head>
<body>
<p>[<a href="cpsauser.html">CPSA User Guide</a>]
[<a href="cpsaprimer.pdf">CPSA Primer</a>]
[<a href="cpsagoals.pdf">CPSA Security Goals and Rules</a>]
[<a href="cpsaintroslides.pdf">CPSA Introductory Slides</a>]
[<a href="http://www.mitre.org/publications/technical-papers/completeness-of-cpsa">CPSA Correctness Proof</a>]</p>
<h1>CPSA</h1><img class="pic" src="cpsalogo.svg" alt="CPSA Logo"/>
<p>The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to
enumerate all essentially different executions possible for a
cryptographic protocol. We call them the <i>shapes</i> 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.</p>
<p>CPSA comes with a user guide, a manual, a primer, goal
documentation, and some slides. The user guide provides usage
information for each program in the CPSA package. The
<a href="cpsa4manual.pdf">manual</a> is the primary documentation.
Its sources are contained in the <a href="src/cpsa4manual/">manual
source directory</a>, and a large set of examples discussed in the
manual are in the <a href="src/cpsa4manual/examples/">examples</a>
subdirectory. The primer provides an English language description
of the CPSA algorithm.</p>
<p>At this point, new users should open the
<a href="cpsaintroslides.pdf">introductory slides</a> and start
using CPSA by analyzing the protocols that come with this document.
Copy the contents of this directory to a place that allows it to be
modified. In a Unix shell, type:</p>
<blockquote>
<pre>$ echo build | ghci Make.hs</pre>
</blockquote>
<p>In Windows, click on <code>Make.hs</code> and type <code>build</code> at
the <code>GHCi</code> prompt <code>*Make></code>.
The <a href="cpsauser.html#make">CPSA User Guide</a> describes a
better way to analyze protocols when GNU Make is available.</p>
<p>After running the analysis, you will note files with the extension
<code>.xhtml</code>. These are XHTML/SVG compound documents that can
be viewed by standards compliant browsers. See the section
on <a href="cpsauser.html#cpsagraph">visualization</a> in the user
guide for help interpreting these documents.</p>
<p>New users should study CPSA's analysis of the following protocols
in order, Blanchet (<code>blanchet.xhtml</code>), Needham-Schroeder
(<code>ns.xhtml</code>), Woo-Lam (<code>woolam.xhtml</code>),
Yahalom (<code>yahalom.xhtml</code>), ffgg
(<code>ffgg.xhtml</code>), and finally Otway-Rees
(<code>or.xhtml</code>). When studying the full output,
simultaneously display the extracted shapes. The shapes file has an
extension of <code>_shapes.xhtml</code>.
<p>An analysis of Needham-Schroeder
using <a href="cpsagoals.pdf">security goals</a> is
in <code>goals.xhtml</code>. Examples of using the security goal
language for rewrite rules is in <code>rules.xhtml</code>. These
examples can safely be ignored by new users.</p>
<p>To make effective use of CPSA, new users should scan the
<a href="cpsauser.html">user guide</a> to get a flavor of its
contents, and then read the <a href="cpsaprimer.pdf">primer</a>.
The remainder of this document contains some usage tips to be read
after running CPSA and learning to understand its output.</p>
<h2>Tips</h2>
<p>Choose a small, simple protocol for your first analysis task. When
analyzing complex protocols, analyze small parts of the protocol
first, and then enrich the description of the problem. </p>
<p>The source distribution contains additional programs and a test
suite with many examples. The README in the top-level directory of
the source distribution contains the installation instructions and
is essential reading for its effective use. Serious users should
favor the source distribution if on a Unix-like platform.</p>
<p>Authentication tests guide the search for new skeletons in CPSA.
The authentication test solved at each step of the search is
described by the <code>operation</code> form in CPSA output. When CPSA
generates unexpected output, find the first skeleton in the
derivation tree that exhibits the problem and read
the <code>operation</code> form to find out what happened.
Authentication tests are introduced in
the <a href="cpsaprimer.pdf">primer</a> and described in full
detail in the <a href="cpsaspec.pdf">The CPSA
Specification</a>.</p>
<p>An origination assumption
(<code>non-orig</code>, <code>pen-non-orig</code>,
and <code>unig-orig</code>), can be specified in a role or in a
skeleton. Be sure to read the advice in
the <a href="cpsaprimer.pdf">primer</a> on the proper placement of
origination assumptions.</p>
<p>Variables of sort message unify with any message. See Otway-Rees
(<code>or.xhtml</code>) for an example of the use of variables of this
sort.</p>
<p>A quoted string is a constant of sort message and is called a tag.
Tags can be used to distinguish messages that have similar
structure in the case where the implementation of the protocol
contains protections against message conflation.</p>
<p>Lisp-like macros in <code>cpsa</code> input can be used to replace
multiple occurrences of a message with one named definition of it.
Macros are described in the <a href="cpsaprimer.pdf">primer</a>.</p>
<p>When the <code>cpsagraph</code> program is given
the <code>--zoom</code> option, it produces diagrams that scale.
This is useful when viewing large diagrams.</p>
<p>In CPSA, a security goal is expressed as a sentence in first-order
logic. It asserts that if some properties hold for a skeleton, then
some other properties must hold for all shapes computed by CPSA
starting with the skeleton. Security goals can be used to state
authentication and secrecy goals of a protocol. See
<a href="cpsagoals.pdf">CPSA Security Goals and Rules</a>. An
analysis of Needham-Schroeder using first-order logic is
in <code>goals.xhtml</code>. Examples of using the security goal
language for rewrite rules is in <code>rules.xhtml</code>.</p>
<p>When the <code>cpsapp</code> program is given
the <code>--json</code> option, it translates S-expressions into
JavaScript Object Notation (JSON). The <code>cpsajson</code>
program translates JSON into S-expressions. These two programs
makes it easy to manipulate CPSA input and output using Python or
other languages with JSON libraries.</p>
<p>The goal of CPSA is to automatically characterize the possible
executions of a protocol compatible with a specified partial
execution. There is a rigorous
<a href="http://www.mitre.org/publications/technical-papers/completeness-of-cpsa">proof</a>
that the algorithm enumerates all of these characterizations.</p>
<p>The <a href="cpsaspec.pdf">specification</a> describes the CPSA
algorithm as a term reduction system.
The <a href="cpsadesign.pdf">design</a> describes implementation
choices made and should be read when viewing the source code.</p>
</body>
</html>