cpsa-4.4.1: doc/cpsauser.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 4.3 User Guide</title>
<meta name="generator" content="Amaya 9.54, see http://www.w3.org/Amaya/" />
<style type="text/css">
h1 { text-align: center }
body { background: white; color: black; max-width: 48em }
</style>
</head>
<body>
<h1>CPSA 4.3 User Guide</h1>
<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>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.</p>
<p>The analyzer is designed to work well with other
tools. S-expressions are used for both input and output. The
analyzer reads all the problems in its input, writes out the
solution to each problem, and then exits. This release contains nine
tools. The <a href="#cpsainit"><code>cpsa4init</code></a> program
copies a Makefile and a Haskell script for use
with <code>ghci</code> into the current directory. They orchestrate
the use of the other tools.
The <a href="#cpsagraph"><code>cpsa4graph</code></a> program
provides a visualization of answers using Scalable Vector Graphics
(<a href="http://www.w3.org/Graphics/SVG/">SVG</a>).
The <a href="#cpsashapes"><code>cpsa4shapes</code></a> program
removes intermediate results from analyzer runs making the shapes
easy to identify.
The <a href="#cpsadiff"><code>cpsa4diff</code></a> program compares
CPSA output files S-expression by S-expression, and prints the first
skeleton that differs.
The <a href="#cpsasas"><code>cpsa4sas</code></a> program logical
formula that can be used to ensure security goals are achieved.
The <a href="#cpsagoalsat"><code>cpsa4goalsat</code></a> program
prints skeletons that do not satisfy the goal associated with the
point of view skeleton. The
<a href="#cpsaprot"><code>cpsa4prot</code></a> program translates
protocols expressed in Alice and Bob notation into
CPSA's <code>defprotocol</code> syntax.
<a href="#cpsapp"><code>cpsa4pp</code></a> program pretty prints its
input using a CPSA specific algorithm. It also translates
S-Expressions into JavaScript Object Notation
(<a href="http://json.org">JSON</a>) to ease processing in other
languages. The
<a href="#cpsajson"><code>cpsa4json</code></a> program translates
JSON encoded CPSA into CPSA S-Expressions. Finally,
the <a href="#cpsa42latex"><code>cpsa42latex</code></a> program
translates CPSA macros into equivalent LaTeX macros.</p>
<p>The input syntax is essentially the same as the output syntax. A
Lisp aware editor will pretty print input, and the output is pretty
printed. We use Emacs' Scheme mode to prepare input. This document
describes the syntax, but provides little assistance for its
interpretation. See the <a href="cpsaprimer.pdf">CPSA Primer</a> and
<a href="cpsagoals.pdf">CPSA Security Goals and Rules</a> for more
information.</p>
<p>The typical pattern of usage is to enter the set of problems to be analyzed
into a file, in this example, <code>prob.scm</code>, analyze the problems, and if
something interesting is produced, visualize the answers.</p>
<blockquote>
<pre>$ cpsa4 +RTS -M512m -RTS -o prob.txt prob.scm
$ cpsa4graph -o prob.xhtml prob.txt
$ firefox -remote "openFile(`pwd`/prob.xhtml)"</pre>
</blockquote>
<p>Often a summary of the analysis is more enlightening.</p>
<blockquote>
<pre>$ cpsa4shapes -o prob_shapes.txt prob.txt
$ cpsa4graph -o prob_shapes.xhtml prob_shapes.txt
$ firefox -remote "openFile(`pwd`/prob_shapes.xhtml)"</pre>
</blockquote>
<p id="make"> The <a href="#cpsainit"><code>cpsa4init</code></a>
program creates the file <a href="cpsa4.mk"><code>cpsa4.mk</code></a>
for inclusion into your makefile. A sample makefile is also created.</p>
<p>The CPSA program
is <a href="http://www.gnu.org/software/emacs/">Emacs</a> friendly.
If you run the above <code>makefile</code> via "<kbd>M-x
compile</kbd>", the results will be displayed in a buffer in
Compilation Mode. The command "<kbd>C-x `</kbd>" will visit
the locus of the next error message or match (<code>next-error</code>)
in your CPSA input file.</p>
<p>For platforms without GNU <code>make</code>, the Haskell
program <a href="make4.hs"><code>make4.hs</code></a> can be loaded
into a Haskell interpreter and perform a similar function. Users are
expected to copy the makefile or the Haskell program into the
directory containing a set of analysis problems
using <a href="#cpsainit"><code>cpsa4init</code></a>, and then modify
a file so it specifies the command line flags appropriate for the
problems in the directory.</p>
<h2>Syntax</h2>
<p>The syntax is extensible. Association lists in which the key is always a
symbol are allowed at various points in the grammar. Key-value pairs with
unrecognized keys are ignored, and are available for use by other tools. On
output, unrecognized key-value pairs are preserved when printing protocols, but
elided when printing skeletons, with the exception of the <code>comment</code>
key.</p>
<p>The input is an option herald form followed by a sequence of
protocol definitions and problem statements.
A <a href="#usage">herald form</a> allows options normally specified
on the command line to be specified within an input file. A problem
statement describes the initial behavior as a skeleton or a security
goal.</p>
<h3>Protocols</h3>
<p>The grammar for a protocol follows.</p>
<blockquote>
<pre>PROTOCOL ::= (defprotocol ID ALG ROLE+ RULE* PROT-ALIST)
ID ::= SYMBOL
ALG ::= SYMBOL
ROLE ::= (defrole ID VARS TRACE ROLE-ALIST)
VARS ::= (vars DECL*)
DECL ::= (ID+ SORT)
TRACE ::= (trace EVENT+)
EVENT ::= (send TERM) | (send ID TERM) | (stor ID TERM)
| (recv TERM) | (recv ID TERM) | (load ID TERM)
ROLE-ALIST ::= (non-orig POS-TERM*) ROLE-ALIST
| (pen-non-orig POS-TERM*) ROLE-ALIST
| (uniq-orig TERM*) ROLE-ALIST
| (conf ID*) ROLE-ALIST
| (auth ID*) ROLE-ALIST
| (priority POS-INT*) ROLE-ALIST
| (gen-st TERM+) ROLE-ALIST
| (critical-sections POS-INT+) ROLE-ALIST
| (facts FACTS*) ROLE-ALIST | ...
POS-TERM ::= TERM | (INT TERM)
POS-INT ::= (INT INT)
RULE ::= (defrule ID SENTENCE RULE-ALIST)
RULE-ALIST ::= ...
PROT-ALIST ::= (lang LDECL*) PROT-ALIST | ...
LDECL ::= (ID+ KIND)
KIND ::= atom | akey | hash | (tuple INT)
| enc | senc | aenc | sign</pre>
</blockquote>
<p>The syntax for <code>SORT</code>, <code>TERM</code>,
and <code>SENTENCE</code> will be presented later.</p>
<p>The protocol <code>ID</code> is a symbol that names the protocol, and the role
<code>ID</code> is a symbol that names the role. The <code>ALG</code>
symbol identifies the algebra used by the protocol. For the Basic
Cryptographic Algebra, the symbol is <code>basic</code>.
The <code>var</code> form contains symbols that declare the sort of
the variables used in this role. The set of sort symbols is algebra
specific, but must include <code>mesg</code>
and <code>chan</code>.</p>
<p>Events specify message transmission (<code>send</code>) or
reception (<code>recv</code>). A message can be sent on a channel
using the form <code>(send ID TERM)</code> where <code>ID</code> is
declared to be of sort <code>chan</code>, and similarly for message
receptions. A state value may be received or loaded from a location
using the form <code>(stor ID TERM)</code> where <code>ID</code> is
declared to be of sort <code>locn</code>. Every store event
must be in a group consisting of a number of loads followed by a
number of stores. Moreover, each <code>locn</code> in a store
event must have had a load event earlier in that group.</p>
<p>The protocol association list has no predefined keys, while the
role association list has nine predefined keys. The value associated
with <code>non-orig, pen-non-orig, uniq-orig, conf, auth</code> must
be atoms in the algebra. Each <code>non-orig</code> term must not be
carried by any event in the role's trace, but each of its variables
must occur in some term. A role non-origination assumption of the
form <code>(3 a)</code> asserts that atom <code>a</code> will not be
mapped into an instance unless its height is greater than three. For
each <code>pen-non-orig</code> term, each of its variables must occur
in some term, but unlike a non-origination assumption, the term may be
carried. Each <code>uniq-orig</code> term must originate in the
role's trace. Each <code>conf</code> term must be a channel variable,
and it asserts the channel is confidential. Each <code>auth</code>
term must be a channel variable, and it asserts the channel is
authenticated. Each <code>gen-st</code> must be a term loaded in the
role. It entails that the instances of these terms are not initial
values, and they must be explained by a previous store event on some
strand. Each <code>critical-section</code> designates the start and
end of a group of loads and stores that must occur atomically. It is
not needed when there is only one load and at most one store in the
group of events. And it is not needed if the events are not assumed
to occur atomically. Each <code>facts</code> declaration ensures
that, whenever an instance of the role proceeds long enough to have
chosen parameter values for each parameter that appears in the facts,
the corresponding instance of the fact will be inferred. Every
variable of sort <code>mesg</code> must be acquired by the role's
trace.</p>
<p>The structure of sorts and terms in the Basic Cryptographic Algebra
follows.</p>
<blockquote>
<pre>SORT ::= text | data | name | skey | akey | mesg | chan | locn
TERM ::= ID | AKEY | (ltk ID ID) | STRING
| (cat TERM+) | (enc TERM+ TERM) | (hash TERM+)
AKEY ::= ID | (invk AKEY) | (pubk ID) | (privk ID)
| (pubk STRING ID) | (privk STRING ID)</pre>
</blockquote>
<p>The form (<code>cat</code> a b c d e) is expands to
(<code>cat</code> a (<code>cat</code> b (<code>cat</code> c
(<code>cat</code> d e)))). The form (<code>enc</code> a b c d e) is
expands to (<code>enc</code> (<code>cat</code> a b c d) e).</p>
<p>A term in the Basic Crypto Algebra is an atom if it is a variable
of a sort other than <code>mesg</code>, or it if formed from one of
the following
operations: <code>pubk</code>, <code>privk</code>, <code>invk</code>,
and <code>ltk</code>.</p>
<p>The Diffie-Hellman algebra adds three
sorts: <code>rndx</code>, <code>expt</code>, and <code>base</code>.
Variables of sort <code>rndx</code> are considered atoms. The new
terms are <code>BASE</code>:</p>
<blockquote>
<pre>BASE ::= ID | (gen) | (exp BASE EXPT)
EXPT ::= ID | (one) | (mul EXPT EXPT) | (rec EXPT)</pre>
</blockquote>
<h4>Algebra Signature Extensions</h4>
<p>The signature of the message algebra used by CPSA is extensible.
There are two forms of extensibility provided by CPSA. Users can add
operations for encryption, tupling, and hashing; and add sorts for
atomic data.</p>
<p>A common extension is to add tupling operations to message algebras.
Previously, complex protocols often made use of tagged concatenation
to encode a tagged sequence of messages. In CPSA, concatenation is
implemented as sequences of pairing operations. Thus, the expression
for a certificate body of the form</p>
<blockquote>
<pre>(cat "cert-body" dn serial-no pub-key)</pre>
</blockquote>
<p>is syntax for</p>
<blockquote>
<pre>(cat "cert-body" (cat dn (cat serial-no pub-key)))</pre>
</blockquote>
<p>Algebra extensions are declared using the <code>lang</code> key in
the protocol's association list, at the end of a protocol. For the
certificate body example,</p>
<blockquote>
<pre>(defprotocol cert basic
...
(lang (cert-body (tuple 3))))</pre>
</blockquote>
<p>adds one tupling operation so that the example above can be written as</p>
<blockquote>
<pre>(cert-body dn serial-no pub-key)</pre>
</blockquote>
<p>CPSA represents this form internally as sequence of messages with a
distinguished mark. This representation is more efficient as compared
with the tagged concatenation representation.</p>
<blockquote>
<pre>LANG ::= (lang LDECL*)
LDECL ::= (ID+ KIND)
KIND ::= atom | akey | hash | (tuple INT)
| enc | senc | aenc | sign</pre>
</blockquote>
The syntax of a <code>lang</code> declaration is given above.
There are eight kinds of ways that CPSA algebras can be extended.
<ul>
<li>An atomic sort is added to the algebra when a symbol is declared
to be of kind <code>atom</code>. If <code>dollar</code> is
declared to be an atomic sort, than <code>(price dollar)</code> in
a <code>var</code> form declares <code>price</code> to be of
sort <code>dollar</code>.</li>
<li>An atomic sort is also added to the algebra when a symbol is
declared to be of kind <code>akey</code>. However, in addition to
adding the sort, CPSA adds the equation <code>(invk (invk x)) =
x</code> for variables of the new sort.</li>
<li>A unary operation is added to the algebra when a symbol is
declared to be of kind <code>hash</code>. As with the default
hash operation, the adversary cannot extract the contents of the
hash.</li>
<li>An N-ary operation is added to the algebra when a symbol is
declared to be of kind (<code>tuple</code> N). As with
concatenation, the adversary can construct and extract contents of
tuples. N must be positive.</li>
<li>A binary operation is added to the algebra when a symbol is
declared to be of kind <code>enc</code>. As with the default
encryption operation, the adversary cannot extract contents of the
encryption without access to the inverse of the key.</li>
<li>A symbol of kind <code>senc</code> is just like one of kind
<code>enc</code> except that the key supplied when it is applied
must be symmetric.</li>
<li>A symbol of kind <code>aenc</code> is just like one of kind
<code>enc</code> except that the key supplied when it is applied
must be asymmetric.</li>
<li>A symbol of kind <code>sign</code> is just like one of kind
<code>enc</code> except that the key supplied when it is applied
must be the inverse applied to an asymmetric key.</li>
</ul>
<h3>Skeletons</h3>
<blockquote>
<pre>SKELETON ::= (defskeleton ID VARS STRAND+ SKEL-ALIST)
STRAND ::= (defstrand ID INT MAPLET*) | (deflistener TERM)
MAPLET ::= (TERM TERM)
SKEL-ALIST ::= (non-orig TERM*) SKEL-ALIST
| (pen-non-orig TERM*) SKEL-ALIST
| (uniq-orig TERM*) SKEL-ALIST
| (uniq-gen TERM*) SKEL-ALIST
| (conf ID*) SKEL-ALIST
| (auth ID*) SKEL-ALIST
| (precedes NODE-PAIR*) SKEL-ALIST
| (facts FACTS*) SKEL-ALIST
| (priority NODE-INT*) SKEL-ALIST | ...
NODE-PAIR ::= (NODE NODE)
NODE ::= (INT INT)
FACT ::= (ID FTERM*)
FTERM ::= TERM | INT</pre>
</blockquote>
<p>The <code>ID</code> in the skeleton form names a protocol. It refers to the last
protocol definition of that name which precedes the skeleton form. The
<code>ID</code> in the strand form names a role. The integer in the strand form
gives the height of the strand. The sequence of pairs of terms in the strand
form specify an environment used to construct the messages in a strand from its
role's trace. The first term is interpreted using the role's variables and the
second term uses the skeleton's variables. The environment used to produce the
strand's trace is derived by matching the second term using the first term as a
pattern.</p>
<p>The first integer in a node identifies a strand, and the second one
specifies the position of the node in the strand. Zero-based indexing is used.
Zero identifies the first strand, and the first node in a strand has position
zero.</p>
<p>A variable may occur in more then one role within a protocol. The
reader performs a renaming so as to ensure these occurrences do not
overlap. Furthermore, the maplets used to specify a strand need not
specify how to map every role variable. The reader inserts missing
mappings, and renames every skeleton variable that also occurs in a
role of its protocol. The sort of every skeleton variable that occurs
in the <code>non-orig</code>, <code>pen-non-orig</code>,
<code>uniq-orig</code>, <code>uniq-gen</code>, <code>conf</code>,
or <code>auth</code> list or in a maplet must be declared.</p>
<p>On output, key-value pairs are added to all skeleton's association list.
Every skeleton in the output is labeled with a unique identifier with
<code>(label INT)</code> A skeleton has <code>(parent INT)</code> if it is a member of
the cohort of the identified parent. A skeleton has <code>(seen INT+)</code> when
members of its cohort are isomorphic to previously seen skeletons. A skeleton
lists its unrealized nodes with <code>(unrealized NODE*)</code>. The traces
associated with each strand is given by the <code>(traces ...)</code> form.
Finally, the operation used to derive this skeleton from its parent is recorded
with <code>(operation TEST KIND TERM NODE TERM*)</code>, where <code>TEST</code> is the
authentication test <code>encryption-test</code> or <code>nonce</code>, <code>KIND</code>
is <code>(added-strand ID INT)</code>,
<code>(displaced INT INT ID INT)</code>,
<code>(contracted MAPLET*)</code>,
<code>(added-listener TERM)</code>, or
<code>TERM</code> is the critical term,
<code>NODE</code> in the test node,
and the remaining terms specify the escape set.
When the operation kind is augmenting, the instance's role name and height are
provided.
For kind displacing, the first number is the strand being merged, the
second number is the strand it was merged into, and the remaining give
the new instance's role name and height.
For kind listening, a term is provided. For kind contracting, the
substitution is provided. When a substitution refers to a variable not in the
skeleton, its name is unpredictable. For generalization, the operation is
recorded as <code>(operation generalization METHOD)</code>, where <code>METHOD</code>
is one of <code>deleted NODE</code>, <code>weakened NODE-PAIR</code>, <code>separated
TERM</code> and <code>forgot TERM</code>. Generalization is used to find shapes from
realized skeletons. For shape collapsing, the operation is recorded as
<code>(operation collapsed INT INT)</code>, where the two <code>INT</code>s identify
the strands merged. Shape collapsing is used to find related shapes.</p>
<!--
<p><em>Diffie-Hellman support is experimental.</em></p>
<p>The Diffie-Hellman Algebra adds sorts and terms as follows.</p>
<blockquote>
<pre>SORT ::= ... | base | expn | expr
TERM ::= ... | (gen) | (exp TERM EXPR)
EXPR ::= (mul EXPR EXPR) | (rec EXPR) | (one)</pre>
</blockquote>
<p>Sort <code>expn</code> is a subsort of <code>expr</code> and
sorts <code>expr</code> and <code>base</code> are subsorts
of <code>mesg</code>.</p>
<p>The exponent of a Diffie-Hellman value is a free Abelian group.
Its basis elements are in sort <code>expn</code>. The basis
elements are the atoms of the group. For the Diffie-Hellman
algebra as a whole, the atoms the ones in the Basis Cryptographic
Algebra augmented with variables of sort <code>expn</code> and
terms of the form <code>(exp (gen) x)</code>,
where <code>x</code> is a variable of sort <code>expn</code>.</p>
<p>The axioms for Diffie-Hellman values are the usual ones for an
Abelian group for terms of sort <code>expr</code>. For terms of
sort <code>base</code>, <code>(exp h (one)) = h</code> and
<code>(exp (exp h x) y) = (exp h (mul x y))</code>.</p>
-->
<h3>First-order Logic and Security Goals</h3>
<p>Another way to specify a problem statement is with a security
goal. A security goal 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 formally state
authentication and secrecy goals of a protocol.</p>
<p>The <code>defgoal</code> form is used to pose an analysis problem
with a sentence instead of a skeleton. CPSA extracts a point of
view skeleton from the antecedent of the formula and then analyzes
it. When a <code>defgoal</code> form has a sequence of sentences,
they must all contain the same antecedent. CPSA will evaluate all
of the conclusions during the analysis of this shared antecedent.
When it prints a shape, it checks to see if the shape satisfies the
conclusions of the security goal sentences. When invoked with
the <code>goals-sat</code> option, CPSA will successfully terminate
any branch of its analysis as soon as the conclusions of the goals
are satisfied. See
<a href="cpsagoals.pdf">CPSA Security Goals and Rules</a> for
details.</p>
<p>To be precise, a security goal is an order-sorted first-order logic
sentence in a restricted form. The set of sort symbols available
for use in a <code>DECL</code> is the ones provided by the message
algebra augmented with the symbol <code>strd</code>. The form of a
sentence is restricted by the syntax that follows.</p>
<blockquote>
<pre>GOAL ::= (defgoal ID SENTENCE+ GOAL-ALIST)
SENTENCE ::= (forall (DECL*) (implies ANTECEDENT CONCLUSION))
CONCLUSION ::= (false) | EXISTENTIAL | (or EXISTENTIAL*)
EXISTENTIAL ::= (exists (DECL*) ANTECEDENT) | ANTECEDENT
ANTECEDENT ::= ATOMIC | (and ATOMIC+)
ATOMIC ::= (p ROLEID SVAR HGT) | (p ROLEID PARAM SVAR TERM)
| (prec SVAR POS SVAR POS) | (non TERM) | (pnon TERM)
| (uniq TERM) | (uniq-at TERM SVAR POS)
| (ugen TERM) | (ugen-at TERM SVAR POS)
| (conf ID) | (auth ID)
| (gen-st TERM) | (comm-pr SVAR POS SVAR POS)
| (same-locn SVAR POS SVAR POS) | (state-node SVAR POS)
| (trans SVAR POS) | (leads-to SVAR POS SVAR POS)
| (fact ID TERM*) | (= TERM TERM)
ROLEID ::= STRING
HGT ::= INT
POS ::= INT | ID
SVAR ::= ID
PARAM ::= STRING</pre>
</blockquote>
<p>An atomic formula asserts that a skeleton has some property. The
formula <code>(p "init" s 3)</code> asserts that
strand <code>s</code> in the skeleton is an instance of
an <code>init</code> role and is of length 3 or greater. The
formula <code>(p "init" "x" s y)</code> asserts that
strand <code>s</code> is an instance of an
<code>init</code> role and is of a length that is great enough so
that role parameter <code>x</code> occurs in the role, and the role
parameter <code>x</code> is instantiated to become
term <code>y</code>. Formula <code>(prec (x 2) (y 1))</code>
asserts that for some strands <code>x</code> and <code>y</code> in
the skeleton, the transitive closure of the precedence relation
contains the mentioned pair of nodes. Formula <code>(non t)</code>
asserts <code>t</code> is assumed to be non-originating in the
skeleton. Predicates <code>pnon</code> and <code>uniq</code> have
similar interpretations. The formula <code>(fact foo s (invk
t))</code> asserts the skeleton contains a fact
called <code>foo</code> relating a strand to the inverse of some term.
The formula <code>(= s t)</code> asserts that <code>s</code>
and <code>t</code> refer to the same object in the skeleton.</p>
<p>The empty string names the listener role of a protocol. The
role has the variable <code>x</code> of sort <code>mesg</code>
as its only role variable. There are two positions in the listener
role.</p>
<p> <code>gen-st</code> asserts that its argument is a generated state
value, and cannot be an initial value. <code>comm-pr</code> asserts
that the two nodes that follow are a transmission-reception pair
with the same message. <code>same-locn</code> asserts that the two
nodes that follow are state nodes involving the same
location. <code>same-locn</code> asserts that the node that follows
is a state node. <code>trans</code> asserts that the node that
follows is a transition node rather than a pure
observation. <code>leads-to</code> asserts that the two nodes that
follow are a transmission and a reception on the same location that
are immediately related, ie no other transition comes between them.</p>
<h3>Rules</h3>
<p>Each protocol may include a small collection of rules. A rule is
written using the language of security goals.</p>
<p>A rule is an axiom added to a protocol. CPSA uses the axiom as a
rewrite rule to derive zero or more new skeletons from a skeleton
produced after each analysis step. A protocol with a rule
follows.</p>
<blockquote>
<pre>(defprotocol doorsep basic
(defrole person
(vars (d p akey) (k skey) (t text))
(trace
(send (enc (enc k (invk p)) d))
(recv (enc t k))
(send t)))
(defrole door
(vars (d p akey) (k skey) (t text))
(trace
(recv (enc (enc k (invk p)) d))
(send (enc t k))
(recv t)))
(defrule trust
(forall ((z strd) (p d akey))
(implies
(and (p "person" z 1)
(p "person" "p" z p)
(p "person" "d" z d)
(non (invk p)))
(non (invk d))))
(comment "The trust rule"))
(comment "Doorsep protocol using unnamed asymmetric keys"))
(defskeleton doorsep
(vars (p akey))
(defstrand door 3 (p p))
(non-orig (invk p))
(comment "Analyze from the doors's perspective"))</pre>
</blockquote>
<p>The trust rule states that when CPSA finds a person strand of
length at least one, and the inverse of it's <code>p</code>
parameter is non-originating, CPSA should assume the inverse of
it's <code>d</code> parameter is non-originating.</p>
<h3>Long-term (cross-session) state</h3>
<p>Some protocols manipulate state. Key management protocols acquire
secrets and certificates, and store them so that subsequent rules can
use them. Hardware security modules store keys and other data, and
use them in a succession of controlled ways, some of which modifies
the data. Many other examples arise.</p>
<p>CPSA supports long-term state using two basic event forms,
namely <code>(load l term)</code> and <code>(stor l term)</code>.
A <code>load</code> event acquires the piece of state in
location <code>l</code> of sort <code>locn</code>. The
term <code>term</code> in <code>(load l term)</code> constrains the
value in <code>l</code> at the time this event occurs. That value
must have the form of <code>term</code>, and any variables
within <code>term</code> that are already bound constrain the value
found there. All remaining variables are newly bound here, and will
constrain the subsequent occurrences.</p>
<p>A <code>(stor l term)</code> event places the value
of <code>term</code> into location <code>l</code> so that
subsequent <code>load</code>s will receive it. We say that
a <code>stor</code> event on location <code>l</code> leads to
a <code>load</code> event on the same location <code>l</code> if the
latter happens immediately after; CPSA formalizes this internally by
creating a special value (a "point") that originates uniquely at
each <code>stor</code> and must match in an immediately
subsequent <code>load</code> event. There may be several immediately
subsequent <code>load</code> events, since several events may observe the
value without causing a transition. A transition consists of a pair
of adjacent events, one which <code>load</code>s the current value,
followed by another the <code>stor</code>es the subsequent value.
There can be at most one transition to which a
single <code>stor</code> event leads.</p>
<p>Internally, CPSA regards a location <code>l</code> of
sort <code>locn</code> as a kind of channel. It is a confidential
channel, since the location remains within the device, and the
adversary can obtain the value only via message transmissions. It is
not a channel with (full) authenticity, since we regard initial values
as always being available. However, any value that is non-initial
must be generated by a previous transition; i.e. a location offers
authenticity for values known to be non-initial.</p>
<p>We formalize this using a <code>gen-st</code> predicate in the rule
language. CPSA uses the formula <code>(gen-st term)</code> to assert
that <code>term</code> is definitely non-initial, and requires a
(regular) <code>(stor l term)</code> event to explain it being
available in location <code>l</code>. Rules with this kind of
conclusion allow CPSA to infer these formulas when needed.</p>
<p>Within a role definition, a declaration <code>(gen-st term-1
... term-i)</code> causes CPSA to generate rules that establish that
each of the terms given is <code>gen-st</code> as long as a role
instance is long enough for the variables in it to be
well-defined.</p>
<h3>Macros and Includes</h3>
<p>After reading the input, <code>cpsa4</code> expands macros before analyzing
the results. A macro definition is a top-level form.</p>
<blockquote>
<pre>(defmacro (NAME ARG*) BODY)</pre>
</blockquote>
<p>The <code>cpsa4</code> program expands all calls to macros in
non-macro defining S-expressions using the macros that have been
defined previously. A macro definition can be used to expand a call if
the first element of a list matches the name of the macro, and the
length of the remaining elements in the list matches the length of the
macro's argument list. When two macros definitions are applicable, the
last definition takes precedence. The <code>cpsa4</code> program omits
macro definitions from its output.</p>
<p>After expanding a list, elements of the list of the
form <code>(^</code> ...<code>)</code> are spliced into the output.
Thus <code>(a ^(b c) d)</code> becomes
<code>(a b c d)</code> after macro expansion.</p>
<p>A source file can be included within another with the top-level
include form,</p>
<blockquote>
<pre>(include FILE)</pre>
</blockquote>
<p>where <code>FILE</code> is a string. The <code>cpsa4</code> program
includes files while it does macro expansion.</p>
<h3 id="usage">Usage of CPSA</h3>
<blockquote>
<pre>$ cpsa4 -h
Usage: cpsa4 [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-l INT --limit=INT step count limit (default 2000)
-b INT --bound=INT strand count bound (default 8)
-d INT --depth=INT tree depth bound (default unbounded)
-m INT --margin=INT set output margin (default 72)
-e --expand expand macros only; don't analyze
-n --noisochk disable isomorphism checks
-c --check-nonces check nonces first
-t --try-old-strands try old strands first
-r --reverse-nodes try younger nodes first
-g --goals-sat Stop when goals are satisfied
-a STRING --algebra=STRING algebra (default basic)
-s --show-algebras show algebras
-h --help show help message
-v --version show version number</pre>
</blockquote>
<p>This program will abort if too many steps are taken. A skeleton is
printed for each step taken by the program. The step count limit
option is used to override the default step count limit. It will also
abort when it detects a skeleton with too many strands. The strand
count bound option is used to override the default strand count
bound. The tree depth bound option is used to override the default
tree depth bound. Another way to limit resources used by the program
is to limit the amount of memory it may use. The command-line
option <code>+RTS -M512m -RTS</code> limits memory usage to 512m.</p>
<p>The herald form can be used to specify options within a file. The
grammar for a herald form follows, where <code>ALIST</code> is an
association list with symbols as keys.</p>
<blockquote>
<pre>HERALD ::= (herald TITLE ALIST)
TITLE ::= SYMBOL | STRING</pre>
</blockquote>
<p>The title is used by <code>cpsa4graph</code> when generating XHTML.
In the following example, the herald form specifies a strand bound
of 12 in a way that is equivalent to the command line
option <code>--bound=12</code>.</p>
<blockquote>
<pre>(herald "Needham-Schroeder Public-Key Protocol" (bound 12))</pre>
</blockquote>
<p>The herald form is only interpreted by the <code>cpsa4</code> program,
and is treated as a comment by all other programs. In particular,
specifying a <code>margin</code> option effects <code>cpsa4</code> only.</p>
<p>For long running problems, SMP parallelism is available. For example, on a
quad-core machine, we would probably use <code>+RTS -N4 -RTS</code>.</p>
<p>In addition to the options provided on the command line or a herald
form, one can influence the order in which test nodes are sought.
When a role includes <code>(reverse-search)</code> in its association
list as a comment, the nodes in its instances will be searched in
reverse order.</p>
<p>When run with isomorphism checks disabled (<code>--noisochk</code>), CPSA
searches for realized skeletons, not shapes. It attempts to speed up analysis
by not identifying duplicate skeletons or generalizing realized skeletons,
however in many cases, run times increase. It is used when normal analysis
takes too much time on the chance that avoiding the checks makes more progress.
</p>
<p>In no isomorphism checking mode output, every realized skeleton is labeled a
shape even when it is not. This allows the extraction of every realized
skeletons from the output using the <a
href="#cpsashapes"><code>cpsa4shapes</code></a> program.</p>
<p>An error message that begins with "No test for unrealized node" identifies a
severe error that should be reported as a bug.</p>
<h3 id="priority">Search order</h3>
<p>In its analysis, CPSA will attempt to solve unrealized nodes until the
skeleton is realized, and then generalize until a shape is obtained. When
there are multiple unrealized nodes, by default, CPSA will chose the topmost,
rightmost unrealized node among those unrealized nodes with maximum priority.
The default priority of a node is 5, and higher numbers represent a higher
priority. When a node has non-positive priority, it is left unsolved.</p>
<p>In a role, in order to specify a priority for an event other than
the default, add a comment of the
form <code>(priority (<var>i</var> <var>p</var>))</code>,
where <var>i</var> is the index of the event in the trace,
and <var>p</var> is the priority.
Priorities are inherited
from roles, but may be overridden in a skeleton with a
<code>priority</code> comment of the form
<code>(priority (<var>n</var> <var>p</var>))</code>,
where <var>n</var> is a node.</p>
<h2 id="cpsainit">Initialization</h2>
<p>The <code>cpsa4init</code> copies the
files <code>Makefile</code>, <code>cpsa4.mk</code>,
and <code>Make4.hs</code> into the current directory. It will not
overwrite existing files of the same name. The makefile is for use
with systems that provide GNU <code>make</code>. Windows users should
load <code>Make4.hs</code> into <code>ghci</code>. Read the
comments in the script for usage instructions.</p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4init -h
Usage: cpsa4init [OPTIONS]
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsagraph">Visualization</h2>
<p>The <code>cpsa4graph</code> program produces a graphical rendering of the output
or input of an analyzer using SVG. It is viewable only with a
standards-compliant web browser such as FireFox.</p>
<p>When applied to the output of CPSA, the program groups together all the
skeletons related to each problem statement in the input. The program assembles
the related skeletons into a directed acyclic graph using the parent identifier
and renders it as a tree using SVG. Each vertex in the tree is the label added
to the skeleton by the CPSA program. Click the label in the tree to view the
skeleton. Hover over a node in a skeleton drawing to see the term associated
with it. Hover over a role to see the mapping from role variables to skeleton
variables.</p>
<p>A node ordering edge in a skeleton drawing indicates that the message
transmission at the source of the edge happened before message reception at the
destination edge. The edge is solid if the transmitting term is syntactically
identical to the receiving term, otherwise the edge is dashed. Thus in an
algebra with a commutative operation <code>*</code>, the graphing program sometimes
draws a dashed line between <code>(send (* a b))</code> and <code>(recv (* b
a))</code>.</p>
<p>In the tree drawing, the label of a shape is blue. For dead
skeletons, the label is red, unless it has been seen before, in which
case it is orange. Otherwise the label is green for skeletons seen
before. Seen skeleton labels are rendered in an italic font.</p>
<p>By the default, <code>cpsa4graph</code> generates a view of CPSA S-expressions as
a compound document that contains SVG within XHTML. This view integrates
graphics with the input text.</p>
<p>In compact mode, <code>cpsa4graph</code> generates an SVG document. The tree is
displayed immediately to the left of skeleton drawings. When there is more than
one tree, the left-hand-side of the drawing contains a vertical listing of the
trees. Compact mode output should never be used as a replacement for studying
the text version of the output. The text version contains strictly more
information, and should be displayed next to its graphical rendition.</p>
<p>In LaTeX mode, <code>cpsa4graph</code> generates LaTeX source. XY-pic is used for
drawings of skeletons. The margin specified in <a
href="cpsa4.mk"><code>cpsa4.mk</code></a> produces good results. </p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4graph -h
Usage: cpsa4graph [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-x --expanded use expanded format (default)
-z --zoom enable diagram scaling
-t --treeless use treeless expanded format
-c --compact use compact format
-l --latex use LaTeX format
-m INT --margin=INT set output margin (default 72)
-p --purge-traces purge traces
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsadiff">Output Comparisons</h2>
<p>The <code>cpsa4diff</code> program compares CPSA output files
S-expression by S-expression, and prints the first skeleton that
differs.</p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4diff -h
Usage: cpsa4diff [OPTIONS] OLD-FILE NEW-FILE
-o FILE --output=FILE output FILE
-m INT --margin=INT set output margin (default 72)
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsashapes">Shape Extraction</h2>
<p>The <code>cpsa4shapes</code> program extracts the original problems and the
shapes from the output of a CPSA run. The shapes are linked to their problem so
the output can be graphed.</p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4shapes -h
Usage: cpsa4shapes [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-m INT --margin=INT set output margin (default 72)
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsasas">Formula Extraction</h2>
<p>The <code>cpsa4sas</code> program extracts a formula in the language
of order-sorted first-order logic for each problem and its shapes
from a CPSA run. The formula is called a
<a href="https://arxiv.org/abs/1204.0480">shape analysis
sentence</a>. The formula is satisfied in all realized skeletons
when CPSA finds all the shapes for the problem.</p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4sas -h
Usage: cpsa4sas [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-m INT --margin=INT set output margin (default 72)
-a STRING --algebra=STRING algebra (default basic)
-s --show-algebras show algebras
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsagoalsat">Goal Satisfaction Checking</h2>
<p>The <code>cpsa4goalsat</code> program prints the labels of
skeletons that do not satisfy a <code>defgoal</code>. For each
point of view skeleton specified by a goal, the program prints a
list. The first element of the list is the label of the point of
view skeleton. The remaining elements of the list are labels of the
skeletons that do not satisfy the goal.</p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4goalsat -h
Usage: cpsa4goalsat [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-m INT --margin=INT set output margin (default 72)
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsaprot">Alice and Bob notation to CPSA</h2>
<p>The <code>cpsa4prot</code> program translates protocols expressed
in Alice and Bob notation into CPSA's <code>defprotocol</code>
syntax. It translates <code>defprot</code> forms, and passes all
else through unchanged. The syntax of a <code>defprot</code> form
is:</p>
<blockquote>
<pre>PROT ::= (defprot NAME ALGEBRA (vars DECLS) NOTATION* RULE* PROT-ALIST)
NOTATION ::= (msg ROLE ROLE CHMSG)
| (msg ROLE ROLE CHMSG CHMSG)
| (from ROLE CHMSG)
| (to ROLE CHMSG)
| (clone ROLE ROLE)
| (assume ROLE ASSUMPTION*)
CHMSG ::= (chmsg CHAN TERM) | (chmsg TERM) | TERM
ASSUMPTION ::= (uniq-orig ...) | (non-orig ...) | ...
RULE ::= (defrule ...)</pre>
</blockquote>
<p>The form <code>(msg A B M)</code> says role <code>A</code>
sends <code>M</code>, and role <code>B</code> receives
<code>M</code>.<br/> The form <code>(msg A B M N)</code> says
role <code>A</code> sends <code>M</code>, and role <code>B</code>
receives <code>N</code>.<br/> The form <code>(from A M)</code> says
role <code>A</code> sends <code>M</code>.<br/> The form <code>(to A
M)</code> says role <code>A</code> receives <code>M</code>.<br/>
The form <code>(clone A B)</code> says make role <code>B</code> have
the same messages as <code>A</code> up to this point in the
specification.</p>
<h3>Example</h3>
<blockquote>
<pre>$ cat blanchet.prot
(defprot blanchet basic
(vars (a b akey) (s skey) (d data))
(msg init resp (enc (enc s (invk a)) b))
(msg resp init (enc d s))
(assume init (uniq-orig s))
(assume resp (uniq-orig d))
(comment "Blanchet's protocol"))
$ cpsa4prot blanchet.prot
(defprotocol blanchet basic
(defrole init
(vars (a b akey) (s skey) (d data))
(trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))
(uniq-orig s))
(defrole resp
(vars (a b akey) (s skey) (d data))
(trace (recv (enc (enc s (invk a)) b)) (send (enc d s)))
(uniq-orig d))
(comment "Blanchet's protocol"))
$</pre>
</blockquote>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4prot -h
Usage: cpsa4prot [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-e --expand expand macros first
-m INT --margin=INT set output margin (default 72)
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsapp">Pretty Printing</h2>
<p>The <code>cpsa4pp</code> program program pretty prints its input
using the CPSA specific algorithm. It also translates S-Expressions
into JavaScript Object Notation (<a href="http://json.org">JSON</a>)
to ease processing in other languages.</p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4pp -h
Usage: cpsa4pp [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-m INT --margin=INT set output margin (default 72)
-j --json output uses JSON notation
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsa42latex">CPSA to LaTeX Macro Translation</h2>
<p>The <code>cpsa42latex</code> program translates CPSA macros
specifying message formats into equivalent LaTeX macros. CPSA
algebra primitives are mapped to unspecified LaTeX macros with the
same name and arity (sometimes with an optional tag), allowing the
user to easily customize how they would like these primitives to be
typeset. </p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa42latex -h
Usage: cpsa42latex [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2 id="cpsajson">JSON to S-Expression Translation</h2>
<p>The <code>cpsa4json</code> program translates JSON encoded CPSA into
CPSA S-Expressions.</p>
<h3>Usage</h3>
<blockquote>
<pre>$ cpsa4json -h
Usage: cpsa4json [OPTIONS] [FILE]
-o FILE --output=FILE output FILE
-m INT --margin=INT set output margin (default 72)
-h --help show help message
-v --version show version number</pre>
</blockquote>
<h2>S-expressions</h2>
<p>The S-expressions used are restricted so that most dialects of Lisp
can read them, and characters within symbols and strings never need
quoting. Every list is proper. An atom is either a symbol, an integer,
or a string. The characters that make up a symbol are the letters, the
digits, and the special characters in
"<code>+-*/<=>!?:$%_&~^</code>". A symbol may not begin with
a digit or a sign followed by a digit. The characters that make up a
string are the printing characters omitting double quote and
backslash, except when double quote and backslash are escaped using
the backslash character. Double quotes delimit a string. A comment
begins with a semicolon, or is an S-expression list at top-level that
starts with the <code>comment</code> symbol. </p>
<hr />
<p>Copyright (c) 2017 The MITRE Corporation. Permission to copy without fee all
or part of this material is granted provided that the copies are not made or
distributed for direct commercial advantage, this copyright notice and the
title of the publication and its date appear, and notice in given that copying
is by permission of The MITRE Corporation.</p>
</body>
</html>