cpsa-2.0.5: doc/cpsatheory.tex

\documentclass[12pt]{article}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage[matrix,arrow,curve]{xy}

\title{CPSA Theory}
\author{John D. Ramsdell}

\input{macros}

\hyphenation{pro-to-skel-e-ton}
\hyphenation{pro-to-role}

\theoremstyle{definition}
\newtheorem{defn}{Definition}[section]
\newtheorem{conj}{Conjecture}[section]
\newtheorem{prop}{Proposition}[section]

\newcommand{\inv}[1]{\ensuremath{\cn{inv}(#1)}}
\newcommand{\gen}{\ensuremath{\cn{g}}}
\newcommand{\expr}[2]{\ensuremath{{#1}^{#2}}}
\newcommand{\sca}{\textsc{sca}}
\newcommand{\alga}{\alg{A}}
\newcommand{\tr}{\ensuremath{\mathfrak C}}
\newcommand{\base}{\ensuremath{\mathfrak B}}
\newcommand{\ints}{\ensuremath{\mathbb Z}}
\newcommand{\solve}[1]{\stackrel{#1}{\longtwoheadrightarrow}}
\newcommand{\pubmsg}{\mathbf{P}}
\newcommand{\excl}{\mathbf{X}}
\newcommand{\transpred}{\mathbf{T}}
\newcommand{\outpred}{\fn{outpred}}
\newcommand{\avoid}{\fn{avoid}}
\newcommand{\unique}{\fn{unique}}
\newcommand{\non}{\fn{non}}
\newcommand{\dcmp}{\fn{dcmp}}
\newcommand{\carpos}{\fn{carpos}}
\newcommand{\esc}{\fn{esc}}
\newcommand{\msg}{\fn{msg}}
\newcommand{\eo}{\fn{eo}}
\newcommand{\ie}{\fn{ie}}
\newcommand{\crit}{\fn{crit}}
\newcommand{\anc}{\fn{anc}}
\newcommand{\mcow}{\fn{cow}}
\newcommand{\mncow}{\fn{ncow}}
\newcommand{\sdom}{\fn{Dom}}
\newcommand{\sran}{\fn{Ran}}
\newcommand{\evt}{\fn{evt}}
\newcommand{\role}{\mathsf{r}}
\newcommand{\skel}{\mathsf{k}}
\newcommand{\rl}{\fn{rl}}
\newcommand{\nodes}{\fn{nodes}}
\newcommand{\lsn}{\fn{lsn}}
\newcommand{\init}{\fn{init}}
\newcommand{\resp}{\fn{resp}}
%\newcommand{\pow}[1]{\wp(#1)}

\begin{document}
\maketitle
\cpsacopying

{\cpsa} takes a partial description of a run of a protocol, and
attempts to produce a compact description of all possibles runs of the
protocol compatible with the partial description.  Given a partial
description, {\cpsa} uses an authentication test to infer what else
must have happened, and thereby reduce the problem to finding
possible runs starting with a set of more refined descriptions.  The
goal of this document is to precisely describe authentication tests.

The formal definition of a partial run of a protocol is called a
skeleton, and is introduced in Section~\ref{sec:skeletons}.  To
motivate the definition, Section~\ref{sec:order-sorted mesg algs}
describes a simplified version of a message algebra used in {\cpsa}.
Section~\ref{sec:strand spaces and bundles} describes a bundle, a
model of asynchronous messages-passing that includes the behaviors of
honest and adversarial participants.  It also introduces the notion of
a protocol, and specifies what it means for a bundle to be a run of a
protocol.

Section~\ref{sec:adversary model} describes the capabilities of the
adversary.  {\cpsa} does not explicitly represents adversarial
behaviors.  Section~\ref{sec:skeletons} and Section~\ref{sec:pen deriv
  mesgs} reveal the means by which the details of adversarial
behavior is abstracted away.  Finally, Section~\ref{sec:auth tests}
describes authentication tests.

\section{Order-Sorted Message Algebras}\label{sec:order-sorted mesg algs}

{\cpsa} models a message by an equivalence class of terms over a
signature. A sort system is used to classify messages.  {\cpsa}
depends on the sort system to allow it to treat a variable that
represents an asymmetric key differently from a variable that
represents an arbitrary message.  In particular, {\cpsa} uses
order-sorted quotient term algebras~\cite{GoguenMeseguer92} for
message algebras.  This formalism enables the use of well-known
algorithms for unification and matching in the presences of equations
and sorts.

This paper makes no attempt to provide a general introduction to
order-sorted quotient term algebras.  Instead, it presents a very
simple message algebra, called the Simple Crypto Algebra (\sca), that
suffices for this document.

\begin{figure}
$$\begin{array}{ll@{{}\colon{}}ll}
\mbox{Sorts:}&\multicolumn{3}{l}{\mbox{$\top$, $S$, and $A$, where $S<\top$ and $A<\top$}}\\
\mbox{Operations:}&(\cdot,\cdot)&\top\times\top\to\top& \mbox{Pairing}\\
&\enc{\cdot}{(\cdot)}&\top\times S\to\top& \mbox{Symmetric encryption}\\
&\enc{\cdot}{(\cdot)}&\top\times A\to\top& \mbox{Asymmetric encryption}\\
&(\cdot)^{-1}&S\to S& \mbox{Symmetric key inverse}\\
&(\cdot)^{-1}&A\to A& \mbox{Asymmetric key inverse}
\end{array}$$
\caption{Simple Crypto Algebra Signature}\label{fig:signature}
\end{figure}

There are three {\sca} sorts: $\top$, the sort of all messages, $S$,
the sort of symmetric keys, and $A$, the sort of asymmetric keys.
Every symmetric key is a message (written $S<\top$), and every
asymmetric key is a message ($A<\top$).  The function symbols, or
\emph{operations}, used to form terms are given by the signature in
Figure~\ref{fig:signature}.  Notice that the encryption and key
inverse operations are overloaded.

Each variable~$x$ used to form a term has a unique sort~$s$, written
$x\colon s$.  If~$X$ is a set of variables, $X_s=\{x\mid x\colon s\}$.
For {\sca}, $X_\top$, $X_S$, and $X_A$, partition a variable set~$X$.

There are two equations in {\sca}, both associated with key inverse.
For symmetric key $x\colon S$, $x^{-1}\approx x$, and for asymmetric
key $y\colon A$, $(y^{-1})^{-1}\approx y$.

\begin{figure}
$$\begin{array}{r@{{}={}}l}
\alga_S&\{\{x^{-n}\mid n\in\nat\}\mid x\in X_S\}\\
\alga_A&\begin{array}[t]{@{}l}
\{\{x^{-2n}\mid n\in\nat\}\mid x\in X_A\}\\
\quad{}\cup\{\{x^{-2n-1}\mid n\in\nat\}\mid x\in X_A\}
\end{array}\\
\base&\alga_S\cup\alga_A\\
\alga^0_\top&\base\cup \{\{x\}\mid x\in X_\top\}\\
\alga^{n+1}_\top&\alga^n_\top
\begin{array}[t]{@{}l}
{}\cup\{\{(t_0,t_1)\mid t_0\in T_0, t_1\in T_1\}\mid
 T_0\in\alga^n_\top,T_1\in\alga^n_\top\}\\
{}\cup\{\{\enc{t_0}{t_1}\mid t_0\in T_0, t_1\in T_1\}\mid
 T_0\in\alga^n_\top,T_1\in\base\}
\end{array}\\
\alga = \alga_\top&\bigcup_{n\in\nat}\alga^n_\top
\end{array}$$
\caption{{\sca} Messages~$\alga$ and Atoms~$\base$}\label{fig:algebra}
\end{figure}

The Simple Crypto Quotient Term Algebra~$\alga$ generated by variable
set~$X$ is displayed in Figure~\ref{fig:algebra}.  The union of the
messages in~$\alga$ is set of terms generated by~$X$, and~$\alga$
partitions the set of terms into a set of equivalence classes induced
by the equations.  Terms~$t_0$ and~$t_1$ are equivalent, written
$t_0\equiv t_1$, iff $t_0\in T\land t_1\in T$ for some $T\in\alga$.
The canonical representative of a message is the $t$ in $\{t'\mid
t'\equiv t\}$ with the fewest occurrences of the $(\cdot)^{-1}$
operation.

In {\sca}, there is a least sort~$s$ associated with each term~$t$,
written $t\colon s$.  If $t\in T$ for some $T\in\alga_S$ then $t\colon
S$, else if $t\in T$ for some $T\in\alga_A$ then $t\colon A$,
otherwise $t\colon\top$.  Obviously, each message has a least sort
too.

The keys in the algebra are called \emph{atoms} and are members
of~$\base$.  We write $t\colon B$ iff $t\colon S$ or $t\colon A$.

An important property possessed by the algebra is that the terms that
make up a message either are all encryptions or are never encryptions.
As a result, a message can be identified as representing an encryption
and if it is, decomposed into its plaintext and its decryption key.
This property is a consequence of the fact that equations relate
atoms, not arbitrary messages.

We write $\alga_X$ when it is important to identify the variable
set~$X$ that generates the algebra.  Given two variable sets~$X$
and~$Y$, a \emph{substitution} is an order-sorted map~$\sigma\colon
X\rightarrow\alga_Y$ such that $\sigma(x)\neq x$ for only finitely many
elements of~$X$.  For a substitution~$\sigma$, the \emph{domain} is
the set of variables $\sdom(\sigma)=\{x\mid \sigma(x)\neq x\}$ and the
\emph{range} is the set $\sran(\sigma)=\{\sigma(x)\mid
x\in\sdom(\sigma)\}$.  Given a substitution~$\sigma\colon
X\rightarrow\alga_Y$, the unique homomorphism $\sigma^\ast\colon
\alga_X\rightarrow\alga_Y$ induced by~$\sigma$ is also denoted~$\sigma$.

In what follows, a finite sequence is a function from an initial
segment of the whole numbers.  The length of a sequence~$f$ is~$|f|$,
and sequence~$f=\seq{f(1),\ldots,f(n)}$ for $n=|f|$.  Alternatively,
$\seq{x_1,x_2,\ldots,x_n} =x_1\cons x_2\cons\ldots\cons
x_n\cons\seq{}$.  If~$S$ is a set, then~$S^\ast$ is the set of finite
sequences of~$S$, and~$S^+$ is the non-empty finite sequences of~$S$.

A \emph{position}~$p$ is a finite sequence of whole numbers.  The
term in~$t$ that \emph{occurs at}~$p$, written~$t\termat p$, is:
$$\begin{array}{l}
t\termat\seq{}=t;\\
(t_1,t_2)\termat i\cons p=t_i\termat p\mbox{ for $i\in\{1,2\}$};\\
\enc{t_1}{t_2}\termat i\cons p=t_i\termat p\mbox{ for
  $i\in\{1,2\}$};\\
t^{-1}\termat 1\cons p=t\termat p.
\end{array}$$
A term~$t$ \emph{occurs in} term~$t'$ if $t=t'\termat p$ for some~$p$.
A message~$T$ \emph{occurs in} message~$T'$ if the canonical
representative of~$T$ occurs in the canonical representative of~$T'$.

A carried term is one that can be extracted from a message reception
assuming plaintext is extractable from encryptions.  The
positions at which term $t$ is carried in
$t'$ is $\carpos(t,t')$, where
$$\carpos(t,t')=\left\{
\begin{array}{ll}
\{\seq{}\}&\mbox{if $t'\equiv t$, else}\\
\multicolumn{2}{l}{\{1\cons p \mid
p\in\carpos(t,t_1)\}}\\
& \mbox{if $t'=\enc{t_1}{t_2}$, else}\\
\multicolumn{2}{l}{\{i\cons p \mid
i\in\{1,2\}, p\in\carpos(t,t_i)\}} \\
& \mbox{if $t'=(t_1,t_2)$ else}\\
\emptyset&\mbox{otherwise.}
\end{array}\right.$$

Term~$t$ \emph{carries}~$t'$ if $\carpos(t',t)$ is not empty, and
$t'\sqsubseteq t$ when~$t'$ is carried by~$t$.  Note that for all
terms $t_0,t_1,t'_0,t'_1$, if $t_0\equiv t_1$ and $t'_0\equiv t'_1$,
then $\carpos(t_0,t'_0)= \carpos(t_1,t'_1)$.

In what follows, we will often conflate a term with the message of
which it is a member, and use lowercase letters to denote both.

\section{Strand Spaces and Bundles}\label{sec:strand spaces and bundles}

A run of a protocol is viewed as an exchange of messages by a finite
set of local sessions of the protocol.  Each local session is called a
\emph{strand}.  The behavior of a strand, its \emph{trace}, is a
sequence of messaging events.  An \emph{event} is either a message
transmission or a reception.  Outbound message $t\in\alga_X$ is
written as~$\outbnd t$, and inbound message~$t$ is written as~$\inbnd
t$.  The set of traces over $\alga_X$ is $\tr_X=(\pm\alga_X)^+$.  A
message \emph{originates} in a trace if it is carried by some event
and the first event in which it is carried is outbound.  A message is
\emph{acquired} by a trace if it first occurs in a reception event and
is also carried by that event.

A \emph{strand space}~$\Theta_X$ over algebra~$\alga_X$ is a sequence
of traces in $\tr_X$.  A strand~$s$ is a member of the domain of
$\Theta_X$, and its trace is $\Theta_X(s)$.  In a strand space, the
elements of the generator set~$X$ denote atomic message elements, such
as keys, and not composite messages, such as encryptions and pairs.
Therefore, $X_\top=\emptyset$.

Message events occur at nodes in a strand space.  For each strand~$s$,
there is a node for every event in~$\Theta(s)$.  The \emph{nodes} of
strand space $\Theta$ are $\{(s,i)\mid s\in\sdom(\Theta), 1\leq i\leq
|\Theta(s)|\}$, and the event at a node is
$\evt_\Theta(s,i)=\Theta(s)(i)$.  The relation~$\Rightarrow$ defined
by $\{(s,i)\Rightarrow(s,i+1)\mid s\in\sdom(\Theta), 1\leq i<|\Theta(s)|\}$
is called the \emph{strand succession relation}.

A \emph{bundle} in strand space $\Theta$ is a finite directed
acyclic graph $\Upsilon(\Theta,\to)$, where the vertices are the nodes
of $\Theta$, and an edge represents communication~($\rightarrow$) or
strand succession~($\Rightarrow$).  For communication, if
$n_0\rightarrow n_1$, then there is a message~$t$ such
that~$\evt_\Theta(n_0)=\outbnd t$ and~$\evt_\Theta(n_1)=\inbnd t$.
For each reception node~$n_1$, there is a unique transmission
node~$n_0$ with $n_0\rightarrow n_1$.

Each acyclic graph has a transitive asymmetric relation~$\prec$ on its
vertices.  The relation specifies the causal ordering of nodes in a
bundle.  Relation~$R$ on set~$S$ is \emph{asymmetric} iff
$x\mathbin{R}y$ implies not $y\mathbin{R}x$ for all distinct $x,y \in
S$.

An atom \emph{uniquely originates} in a bundle if it originates in
the trace of exactly one strand.  An atom is \emph{non-originating} in
a bundle if it originates on no strand, but each of its variables
occurs in some strand's trace.

In a run of a protocol, the behavior of each strand is constrained by
a role in a protocol.  Adversarial strands are constrained by roles as
are non-adversarial strands.  A protorole over $\alga_Y$ is
$\role_Y(C,N,U)$, where $C\in\tr_Y$, $N\subseteq\base_Y$, and
$U\subseteq\base_Y$.  The trace of the role is~$C$, its
non-origination assumptions are~$N$, and its unique origination
assumptions are~$U$.  A protorole is a \emph{role} if (1) $t\in N$ implies
$t$ is not carried in $C$, and all variables in $t$ occur in $C$, (2)
$t\in U$ implies $t$ originates in $C$, and (3) $x\in Y_\top$ occurs
in $C$ implies $x$ is acquired in $C$.  A \emph{protocol} is a set of
roles.

A bundle~$\Upsilon(\Theta_X,\to)$ is a \emph{run of protocol}
$P_Y$ if there is a role mapping $\rl\colon\Theta_X\to P_Y$ that
satisfies properties for each $s\in\sdom(\Theta_X)$.  Assuming
$\rl(s)=\role_Y(C,N,U)$ and $X$ and $Y$ share no variables, the
properties are (1) $|\Theta_X(s)|\leq|C|$, (2) there is a
homomorphism~$\sigma\colon\alga_Y\to\alga_X$ such that
$\sigma(C(i))=\Theta_X(s)(i)$ for all $1\leq i\leq|\Theta_X(s)|$, (3) if
the variables in $t\in N$ occur in $\sdom(\sigma)$, then $\sigma(t)$ is
non-originating in $\Upsilon(\Theta_X,\to)$, and (4) if $t\in U$
originates at index~$i$ in~$C$, and $i\leq|\Theta_X(s)|$, then
$\sigma(t)$ uniquely originates in $\Upsilon(\Theta_X,\to)$ at node
$(s,i)$.  Origination assumptions in bundles specified by roles are
called \emph{inherited origination assumptions}.

\section{Adversary Model}\label{sec:adversary model}

A fixed set of penetrator roles encodes the adversary model associated
with a message algebra.  For the Simple Crypto Algebra, there are eight
roles.  Each role makes no origination assumptions, and the trace of
each role is given in Figure~\ref{fig:pen}.  The first line of the
figure specifies two traces, one for creating symmetric keys, and
another for creating asymmetric keys.

\begin{figure}
$$\begin{array}{lll}
\mbox{Create}&
\seq{\outbnd z}&\seq{\outbnd w}\\
\mbox{Pair}&
\seq{\inbnd x,\inbnd y,\outbnd(x, y)}&
\seq{\inbnd(x, y),\outbnd x,\outbnd y}\\
\mbox{Encrypt}&
\seq{\inbnd x,\inbnd z,\outbnd\enc{x}{z}}&
\seq{\inbnd x,\inbnd w,\outbnd\enc{x}{w}}\\
\mbox{Decrypt}&
\seq{\inbnd\enc{x}{z},\inbnd z,\outbnd x}&
\seq{\inbnd\enc{x}{w},\inbnd w^{-1},\outbnd x}\\[1em]
\multicolumn{3}{c}{X_\top=\{x,y\}, X_S=\{z\}, X_A=\{w\}}
\end{array}$$
\caption{Simple Crypto Algebra Penetrator Role Traces}\label{fig:pen}
\end{figure}

A strand exhibits non-adversarial behavior when its role is not a
penetrator role.  A non-adversarial strand is called a \emph{regular}
strand as is its role.

The penetrator cannot use a non-originating atom to encrypt or decrypt
a message, because every key it uses must be carried in a message.
Consider a uniquely originating atom that originates on a regular
strand.  The penetrator cannot make the atom using a create role,
because the atom would originate at more than one node.  Therefore,
the penetrator can use a uniquely originating atom to encrypt or
decrypt a message only if it is transmitted by a regular strand
unprotected by encryption.

\section{Skeletons}\label{sec:skeletons}

The details of penetrator behavior are abstracted away when performing
protocol analysis.  The abstracted description of a bundle is
called a realized skeleton, which is defined using a protoskeleton.  A
\emph{protoskeleton} over $\alga_X$ is
$\skel_X(\rl,\Theta_X,\prec,N,U)$, where $\rl$ is a role map,
$\Theta_X$ is a sequence of traces in $\tr_X$, $\prec$ is a relation
on the nodes in $\Theta_X$, $N\subseteq\base_X$ are its
non-origination assumptions, and $U\subseteq\base_X$ are its unique
origination assumptions.  Unlike a strand space, the variable set~$X$
that generates the algebra of a protoskeleton may have variables
in~$X_\top$.

Assume the strands in bundle $\Upsilon(\Theta_X,\to)$ have been
permuted so that regular strands precede penetrator strands in
sequence~$\Theta_X$, and $\rl$ demonstrates the bundle is a run of a
protocol.  Skeleton $\skel_X(\rl',\Theta'_X,\prec,N,U)$
\emph{realizes} the bundle if $\rl'$ and $\Theta'_X$ are the
truncations of $\rl$ and $\Theta_X$ respectively that omit penetrator
strands from their domains, $\prec$ is the transitive asymmetric
relation associated with the bundle without penetrator nodes, $N$ is
the set of non-originating atoms with variables that occur in
$\Theta'_X$, and $U$ is the set of atoms that uniquely originate and
are carried by some regular node.

A protoskeleton $\skel_X(\rl,\Theta_X,\prec,N,U)$ is a \emph{preskeleton}
if the following properties hold.
\begin{enumerate}
\item Sequence $\rl$ demonstrates that the strands in $\sdom(\Theta_X)$
  satisfy the conditions for being a part of a run of the protocol.
\item Relation $\prec$ is transitive, asymmetric, and includes the
  strand succession relation $(\Rightarrow)$.
\item Each atom in $N$ is carried at no node, and each variable
  in the atom occurs at some node.
\item Each atom in $U$ is carried at some node.
\item $N$ includes the non-originating atoms inherited from roles via
  the role map.
\item $U$ includes the uniquely originating atoms inherited from roles via
  the role map.
\end{enumerate}

Let $\orig_k(t)$ be the set of nodes at which~$t$ originates in
preskeleton~$k$, and~$\acqu_k(t)$ be the set of nodes at which~$t$ is
acquired in~$k$.  Preskeleton $\skel_X(\rl,\Theta_X,\prec,N,U)$ is a
\emph{skeleton} if each atom in $U$ originates on at most one strand,
and the node of origination precedes each node that acquires the atom,
i.e.\@ for every~$t\in U$, $n_0\in\orig_k(t)$ and $n_1\in\acqu_k(t)$
implies~$n_0\prec n_1$.

Let $k_0=\skel_X(rl_0,\Theta_0,\prec_0,N_0,U_0)$ and
$k_1=\skel_Y(rl_1,\Theta_1,\prec_1,N_1,U_1)$ be preskeletons.  There
is a \emph{preskeleton homomorphism} from~$k_0$ to~$k_1$,
written~$k_0\homomorphism{\phi,\sigma}k_1$, if~$\phi$ and~$\sigma$ are
structure-preserving maps with the following properties:
\begin{enumerate}
\item $\phi$ maps strands of~$k_0$ into those of~$k_1$, and nodes as
  $\phi((s,p))=(\phi(s),p)$, that is $\phi$ is in
  $\sdom(\Theta_0)\to\sdom(\Theta_1)$;
\item $\sigma\colon\alga_X\to\alga_Y$ is a message algebra homomorphism;
\item $n\in\nodes(\Theta_0)$ implies $\sigma(\evt_{\Theta_0}(n))=\evt_{\Theta_1}(\phi(n))$;
\item $n_0\prec_0 n_1$ implies $\phi(n_0)\prec_1\phi(n_1)$;
\item $\sigma(N_0)\subseteq N_1$;
\item $\sigma(U_0)\subseteq U_1$;
\item $t\in U_0$ implies $\phi(\orig_{k_0}(t))\subseteq\orig_{k_1}(\sigma(t))$.
\end{enumerate}
A homomorphism is \emph{strandwise injective} if its strand map is
injective.  Two preskeletons are isomorphic if they are related by
strandwise injective homomorphism in both directions.  A homomorphism
is \emph{nodewise isomorphic} if the strand map~$\phi$ implies a
bijection on nodes, and $n_0\prec_1 n_1$ implies
$\phi^{-1}(n_0)\prec_0\phi^{-1}(n_1)$.  A skeleton is \emph{realized}
if there is a nodewise isomorphic homomorphism from it to a skeleton
that realizes a bundle, and message component of the homomorphism
is injective.

Our formalism requires that every protocol include a listener role of
the form: $\lsn(x\colon\top)=\role(\seq{\inbnd x,\outbnd
  x},\emptyset,\emptyset)$.  Instances of this role are sometimes used
to make penetrator derived messages visible in skeletons.  We say
skeleton~$k$ \emph{realizes modulo listeners} bundle
$\Upsilon(\Theta,\to) $ if~$k$ realizes $\Upsilon(\Theta',\to')$ and
\hbox{$\Upsilon(\Theta,\to)$} is the result of removing full length listener
strands, and adjusting the communication ordering $\to$ appropriately.

The set of bundles denoted by preskeleton~$k$, $\sembrack{k}$, is:
$$\sembrack{k_0} = \{\Upsilon\mid
\mbox{$k_0\homomorphism{\phi,\sigma}k_1$ and $k_1$ realizes modulo
  listeners $\Upsilon$}\}$$ Let~$\longrightarrow$ be an irreflexive
reduction relation on preskeletons.  The relation~$\longrightarrow$ is
semantics preserving if $\sembrack{k_0}=\bigcup_{\{k_1\in\{k_1\mid
  k_0\longrightarrow k_1\}}\sembrack{k_1}$.

\subsection{Dolev-Yao Example 1.3}
The example has an initiator and responder role.
$$\begin{array}{r@{{}={}}l}
\init(a,b\colon A, m\colon S)&
\role(\seq{\outbnd\enc{\enc{m}{b},a}{b},\inbnd\enc{\enc{m}{a},b}{a}},
\emptyset,\emptyset)\\
\resp(a,b\colon A, m\colon\top)&
\role(\seq{\inbnd\enc{\enc{m}{b},a}{b},\outbnd\enc{\enc{m}{a},b}{a}},
\emptyset,\emptyset)\\
\end{array}$$
The algebra for the initiator is generated from $X$, where
$X_\top=\emptyset$, $X_S=\{m\}$, and $X_A=\{a,b\}$, and the algebra
for the responder is generated from $Y$, where $Y_\top=\{m\}$,
$Y_S=\emptyset$, and $Y_A=\{a,b\}$,

An interesting point of view for analysis is to see if~$m$ is kept
secret after the initiator sends its message.  Let variable set
$Z=a,b\colon A, m\colon S$.  The initial scenario preskeleton is:
$$\begin{array}{r@{}ll}
\skel_Z(
&\seq{\init(a_0,b_0,m_0),\lsn(x)},
&\mbox{Roles}\\
&\seq{\seq{\outbnd\enc{\enc{m}{b},a}{b}},\seq{\inbnd m}},
&\mbox{Strands}\\
&\emptyset,
&\mbox{Node orderings}\\
&\{a^{-1},b^{-1}\},
&\mbox{Non-origination}\\
&\{m\})
&\mbox{Unique origination}
\end{array}$$
where the variable set that generates the algebra for the initiator
role has been renamed so as to avoid conflicts with the variable set~$Z$
used by the preskeleton.

\begin{figure}
$$\xymatrix{
\txt{\strut init}&\txt{\strut }&\txt{\strut resp}&\txt{\strut resp}\\
\bullet\ar[rrr]&&&\bullet\ar@{=>}[d]\\
&&\bullet\ar@{=>}[d]&\bullet\ar[l]\\
&\bullet\ar@{=>}[d]&\bullet\ar[l]&\\
&\bullet&&}$$
\caption{Dolev-Yao Example 1.3 Shape}\label{fig:dy shape}
\end{figure}

CPSA determines $m$ is not kept secret by producing the shape in
Figure~\ref{fig:dy shape}.  The added strands in the shape are
instances of responder roles.  The strands in the shape are:
$$\begin{array}{l}
\seq{\outbnd\enc{\enc{m}{b},a}{b}}\\
\seq{\inbnd m}\\
\seq{\inbnd\enc{\enc{m}{b},a'}{b},\outbnd\enc{\enc{m}{a'},b}{a'}}\\
\seq{\inbnd\enc{\enc{\enc{m}{b}, a}{b},a''}{b},
\outbnd\enc{\enc{\enc{m}{b},a}{a''},b}{a''}}
\end{array}$$
The non-origination and unique origination assumptions are as they are
in the initial scenario preskeleton.  An interesting exercise left for
the reader is to produce a bundle that is realized by the shape.

\subsection{Exercise}

Consider the following roles.
$$\begin{array}{r@{{}={}}l}
\init(a,b\colon A)&\role(\seq{\outbnd(a,b),\inbnd(b,a)},
\emptyset,\emptyset)\\
\resp(a,b\colon A)&\role(\seq{\inbnd(a,b),\outbnd(b,a)},
\emptyset,\emptyset)
\end{array}$$
Let $X=x,y\colon A$ and
$\begin{array}[t]{@{}r@{}l}
k=\skel_X(
&\seq{\init(a,b),\resp(a,b),\resp(a,b)},\\
&\seq{\begin{array}[t]{@{}l}
\seq{\outbnd(x,y),\inbnd(y,x)},\\
\seq{\inbnd(x,y),\outbnd(y,x)},\\
\seq{\inbnd(x,y),\outbnd(y,x)}},
\end{array}\\
&\mbox{Node ordering in Figure~\ref{fig:exercise}},\\
&\emptyset,\\
&\emptyset)
\end{array}$

\begin{figure}
$$\xymatrix{
\txt{\strut init}&\txt{\strut resp}&\txt{\strut resp}\\
\bullet\ar@{=>}[d]\ar@/^/[rr]\ar[r]&\bullet\ar@{=>}[d]&\bullet\ar@{=>}[d]\\
\bullet&\bullet\ar[l]&\bullet\ar@/^/[ll]}$$
\caption{Exercise Skeleton}\label{fig:exercise}
\end{figure}

What is $\sembrack{k}$?

One member is shown in Figure~\ref{fig:bundle}.

\begin{figure}
$$\begin{array}{ll}
\mbox{init}&\seq{\outbnd(x,y),\inbnd(y,x)}\\
\mbox{resp}&\seq{\inbnd(x,y),\outbnd(y,x)}\\
\mbox{resp}&\seq{\inbnd(x,y),\outbnd(y,x)}\\
\mbox{pair}&\seq{\inbnd(y,x),\inbnd(y,x),\outbnd((y,x),(y,x))}\\
\mbox{sep}&\seq{\inbnd((y,x),(y,x)),\outbnd(y,x)}
\end{array}$$

$$\xymatrix{
\txt{\strut init}&\txt{\strut resp}&\txt{\strut resp}&\txt{\strut pair}&\txt{\strut sep}\\
\bullet\ar@{=>}[dddd]\ar@/^/[rr]\ar[r]&\bullet\ar@{=>}[d]&\bullet\ar@{=>}[d]&&\\
&\bullet\ar@/_/[rrd]&\bullet\ar[r]&\bullet\ar@{=>}[d]&\\
&&&\bullet\ar@{=>}[d]&\\
&&&\bullet\ar[r]&\bullet\ar@{=>}[d]\\
\bullet&&&&\bullet\ar[llll]}$$
\caption{A Bundle Realized by the Example Skeleton}\label{fig:bundle}
\end{figure}

\section{Penetrator Derivable Messages}\label{sec:pen deriv mesgs}

To simplify notation, we write~$U_k$ to refer to~$U$ when
$k=\skel(\rl,\Theta,\prec,N,U)$, and similarly for the other
components of preskeleton~$k$.

This section specifies what the penetrator can derive in a skeleton at
a given reception node.  In the section on the adversary model, it is
explained why the penetrator cannot use create roles for atoms in the
what is called the exclusion set~$\excl_k=N_k\cup\{t\mid t\in U_k,
|\orig_k(t)|=1\}$.  At reception node~$n$, the messages available to
the penetrator due to message transmissions in the past
are~$\transpred_k(n)=\{t\mid n'\prec_k n, \evt_k(n')=\outbnd t\}$.
Therefore, for an algebra generated by~$X$, the \emph{public messages}
available to the penetrator at node~$n$ are
$\pubmsg_k(n)=\transpred_k(n)\cup(\base\setminus\excl_k)\cup X_\top$.

Penetrator roles determine what terms are derivable at a node.
Messages are decomposed using three of the penetrator's roles.  Let
$\to$ be a reduction relation on sets of messages defined as follows:
$$\begin{array}{r@{{}\to{}}ll}
\{(t_0,t_1)\}\cup T&\{t_0,t_1\}\cup T\\
\{\enc{t_0}{t_1}\}\cup T&\{t_0,\enc{t_0}{t_1}\}\cup T
&\mbox{if $t_1^{-1}\in T$ and $t_0\notin T$}
\end{array}$$
The minimum decryption set~$M(T)$ is the normal form of relation~$\to$,
i.e.\ $T\to^\ast M(T)$ and there is no~$T'$ such that $M(T)\to T'$.

Three penetrator roles construct messages.
$$\begin{array}{r@{{}={}}l}
D^0&M(T)\\
D^{n+1}&\left\{\begin{array}{r@{{}\mid{}}l}
(t_0,t_1)&t_0,t_1\in D^n\\
\enc{t_0}{t_1}&t_0,t_1\in D^n
\end{array}\right\}\\
D(T)&\bigcup_{n\in\nat}D^n
\end{array}$$
A message~$t$ is derivable from~$T$, written $T\vdash t$, if $t\in D(T)$.
A message~$t$ is derivable at node~$n$ if $\pubmsg_k(n)\vdash t$.

\section{Authentication Tests}\label{sec:auth tests}

In a realized skeleton, the message at every reception node is
derivable, but this is not so for an unrealized skeleton.  A reception
node that has a derivable message is called \emph{realized}, and
{\cpsa} infers the existence of additional regular behavior by
analyzing unrealized nodes.

It does so by identifying a so called critical message, a message
carried by the node's message.  The message is critical in the sense
that the context in which it appears can only be explained by adding
more regular strands, identifying messages, adding more constrains on
node orderings, or various combinations of these actions.

Consider a reception node~$n$ that receives $\enc{x}{k_0}$, where
critical message~$x$ is a uniquely originating symmetric key,
and~$k_0$ is an asymmetric key.  In this case, $x$ is being used as a
nonce, and not for encryption, an artifact of algebra simplification.
Assume that $\outbnd\enc{x}{k_1}$ is the only event that precedes~$n$,
where~$k^{-1}_1$ is a non-originating asymmetric key.  Message
$\enc{x}{k_0}$ is not derivable at~$n$, because
$$\{\enc{x}{k_1}\}\cup(\base\setminus\{x,k^{-1}_1\})\cup
X_\top\not\vdash\enc{x}{k_0}.$$ {\cpsa} might explain this reception
by identifying messages~$k_0$ and~$k_1$, or it might add a strand that
receives $\enc{x}{k_1}$ and transmits~$x$ before node~$n$ if a role
permits this new behavior.

A critical message might also be an encryption.  Continuing the
previous example, suppose that~$k_0$ is non-originating, which makes
$\enc{x}{k_0}$ into a critical message.  {\cpsa} might explain this
reception by identifying messages~$k_0$ and~$k_1$, or it might add a
strand that receives $\enc{x}{k_1}$ and transmits~$\enc{x}{k_0}$
before node~$n$ if a role permits the new behavior.

We proceed with making the definition of a critical message precise by
first considering the contexts of interest in which a critical message
appears.  For reception node~$n$, the contexts are encryptions derived
from the public messages at~$n$, $\pubmsg(n)$, that contain the
critical message.  Furthermore, the encryptions are members of the
minimum decryption set~$M(\pubmsg(n))$ with underivable decryption
keys.  The context is called an escape set.

\begin{defn}[Escape Set]
Let~$S$ be a set of public messages.  The \emph{escape set} for~$t$ in
the context of~$S$ is $E(S,t)=\{\enc{t_0}{t_1}\in M(S) \mid
t\sqsubseteq t_0\wedge S\not\vdash t^{-1}_1\}$ when $t\notin M(S)$.
Otherwise, $E(S,t)$ is undefined.
\end{defn}

The intuition is this, a message~$t_c$ that is carried by the message
at~$n$ is critical when the contents of the escape set cannot be used
to derive~$t_c$.  To do so, the penetrator would have to decrypt a
member of the escape set, which by definition it is not allowed to do.
A critical message is one that has escaped the protection of
previously transmitted encryptions, and {\cpsa} infers more regular
behavior in response.

We continue with the task of with making the definition of a critical
message precise by stating what it means for an escape set to protect
a message.  Suppose~$t$ is carried by~$t'$, and~$S$ is a set of public
messages.  Furthermore, suppose that at every carried position at
which~$t$ is carried in~$t'$, a subterm containing~$t$ is a member of
the escape set $E(S,t)$.  In this case, we say that term~$t$ is
carried only within $E(S,t)$ in~$t'$, and observe that the subterm
containing $t$ is derivable because every member of the escape set is
derivable.  There is nothing about the fact that~$t'$ carries~$t$ that
can be used to infer more regular behavior.  An essential property of
a critical message is that it is not carried only with the escape set
in the message received at an unrealized node.  The precise definition
of carried only within follows.

\begin{defn}[Ancestors]
For $t'=t\termat p$, the \emph{ancestors} of~$t'$ in~$t$ at~$p$ is the
set $\anc(t,p)=\{t\termat p'\mid \mbox{$p'$ a proper prefix
  of~$p$}\}$.
\end{defn}

\begin{defn}[Carried Only Within]
Term~$t$ is \emph{carried only within} $T$ in~$t'$ iff
$\mcow(t,T,t')=\all{p} p\in\carpos(t,t')$ implies
$\anc(t',p)\cap T\neq\emptyset$. Predicate $\mncow(t,T,t')$ means
$\lnot(\mcow(t,T,t'))$, and therefore $\mncow(t,T,t')=\some{p}
p\in\carpos(t,t')$ and $\anc(t',p)\cap T=\emptyset$.
\end{defn}

A critical message may be either an atom or an encryption with an
underivable encryption key.  A critical message cannot be derived from
its subterms.

\begin{defn}[Critical Message]
Term $t_c$ is a \emph{critical message} of~$t$ in the context of
public messages~$S$, written
$t_c\in\crit(S,t)$, iff
\begin{enumerate}
\item $t_c\sqsubseteq t$
\item $t_c$ is an atom or $t_c=\enc{t_0}{t_1}$ and
$S\not\vdash t_1$
\item $t_c\notin M(S)$
\item $\mncow(t_c,E(S,t_c),t)$
\end{enumerate}
\end{defn}

A critical message that is an atom is called a \emph{nonce test}, and
one that is an encryption is called an \emph{encryption test},  and
both types of tests are called an \emph{authentication test}.

\begin{defn}[Test Node]
Node~$n$ is a \emph{test node} in~$k$ if
$\evt_k(n)=\inbnd t$ and $\crit(\pubmsg_k(n),t)\neq\emptyset.$
\end{defn}

\begin{prop}
A reception node is a test node iff it is unrealized, alternatively
$S\vdash t$ iff $\crit(S,t)=\emptyset$.
\end{prop}
\begin{proof}
We show that $S\vdash t$ iff $\eo(S,t)=\emptyset$, where $\eo(S,t)$ is
defined below, and then apply a theorem by Paul Rowe that states that
$\eo(S,t)=\emptyset$ iff $\crit(S,t)=\emptyset$.
\end{proof}

\begin{defn}[Essential obstructions]\label{def:eo}
Let~$S$ be a set of public messages.  The \emph{essential
  obstructions} for~$t$ in the context of~$S$ is $\eo(S,t)$, where
$$\eo(S,t)=\left\{
\begin{array}{ll}
\emptyset&\mbox{if $t\in M(S)$, else}\\
\eo(S,t_0)\cup\eo(S,t_1)&\mbox{if $t=(t_0,t_1)$, else}\\
\eo(S,t_0)&\mbox{if $t=\enc{t_0}{t_1}$ and $S\vdash t_1$, else}\\
\{t\}&\mbox{otherwise}
\end{array}\right.$$
\end{defn}

\begin{prop}
$S\vdash t$ iff $\eo(S,t)=\emptyset$.
\end{prop}
\begin{proof}
The cases in Definition~\ref{def:eo} follow the cases for constructing
messages in Section~\ref{sec:pen deriv mesgs}.  The first case
corresponds to showing that $S\vdash t$ with $t\in D^0$.  The second
case corresponds to showing that $S\vdash (t_0,t_1)$ by finding an~$n$
such that $t_0,t_1\in D^n$.  The third case is the same, but for an
encryption.
\end{proof}

{\cpsa} makes progress by solving a test.  Suppose~$t_c$ is a critical
message at~$n$ in~$k$, i.e.\ $\evt_k(n)=\inbnd t$ and
$t_c\in\crit(\pubmsg_k(n),t)$, and suppose
$k\homomorphism{\phi,\sigma}k'$.  Let $t'_c=\sigma(t_c)$, $T=
E(\pubmsg_k(n),t_c)$, $T'=\sigma(T)$, $n'=\phi(n)$, and
$\evt_{k'}(n')=\inbnd t'$.  Message~$t_c$ at~$n$ in~$k$ is
\emph{solved} in~$k'$, written $k\solve{n,t_c}k'$, if
\begin{enumerate}
\item\label{enu:contract} $\mcow(t_c',T',t')$, or
\item\label{enu:augment} for some $t_p\in\transpred_{k'}(n')$,
$\mncow(t_c',T',t_p)$, or
\item\label{enu:escape} for some $\enc{t_0}{t_1}\in T'$,
$\pubmsg_{k'}(n')\vdash t_1^{-1}$, or
\item\label{enu:crit} $t'_c=\enc{t_0}{t_1}$, and
$\pubmsg_{k'}(n')\vdash t_1$.
\end{enumerate}

In words, {\cpsa} makes progress by a contraction
(Item~\ref{enu:contract}), where messages are identified, an
augmentation (Item~\ref{enu:augment}), where something is added to the
escape set, or a listener augmentation (Item~\ref{enu:escape} and
Item~\ref{enu:crit}), where an assumption about the lack of the
derivability of a key is shown to be invalid.

If solving a test is semantics preserving, and {\cpsa} produces a
finite set of skeletons that preserve the semantics at every step,
{\cpsa} will discover every
possible bundle associated with an initial skeleton whenever {\cpsa}
terminates.
\begin{conj}
$\sembrack{k}=\bigcup_{k'\in\{k'\mid k\solve{n,t_c}k'\}}\sembrack{k'}$.
\end{conj}

Alas, I know of no proof of this conjecture.

\appendix
\section{Unification in a Many-Sorted Algebra}

Unification in the Simple Crypto Order-Sorted Algebra can be
implemented using the unsorted unification algorithm from Laurence
Paulson's ``ML for the Working Programmer'' in a many-sorted algebra
isomorphic to the order-sorted algebra, with a modification to handle
an equation.  See Figure~\ref{fig:unifier}.

\begin{figure}
$$
\begin{array}{l}
\cn{unify}(\ell, t, t') = \cn{unify\_aux}(\ell,\cn{chase}(\ell, t),
\cn{chase}(\ell, t'))
\\
\\\cn{chase}(\ell, x)=
\\ \qquad\mbox{let }t=\cn{lookup}(x,\ell)\mbox{ in}
\\ \qquad \mbox{if }x = t\mbox{ then }x
\mbox{ else }\cn{chase}(\ell, t)
\\\cn{chase}(\ell, t^{-1})=\cn{chase\_invk}(\ell, t)\hfill(!)
\\\cn{chase}(\ell, t)=t
\\
\\\cn{chase\_invk}(\ell, x)=\hfill(!)
\\ \qquad\mbox{let }t=\cn{lookup}(x,\ell)\mbox{ in}\hfill(!)
\\ \qquad \mbox{if }x = t\mbox{ then }x^{-1}
\mbox{ else }\cn{chase\_invk}(\ell, t)\hfill(!)
\\\cn{chase\_invk}(\ell, t^{-1})=\cn{chase}(\ell, t)\hfill(!)
\\\cn{chase\_invk}(\ell, t)=t^{-1}\hfill(!)
\\
\\\cn{lookup}(x,\seq{})=x
\\\cn{lookup}(x,(y,t)\cons\ell)=
\mbox{if }x=y\mbox{ then }t\mbox{ else }
\cn{lookup}(x, \ell)
\\
\\\cn{unify\_aux}(\ell,x,x) =\ell
\\\cn{unify\_aux}(\ell,x,t) =\mbox{if }\cn{occurs}(x, t)\mbox{ then raise failure else }
(x,t)\cons\ell
\\\cn{unify\_aux}(\ell,t,x) =\cn{unify\_aux}(\ell,x,t)
\\\cn{unify\_aux}(\ell,f(t,\ldots),f(t',\ldots)) =
\cn{unify\_list}(\ell,\seq{t,\ldots},\seq{t',\ldots})
\\\cn{unify\_aux}(\ell,t,t') =\mbox{raise failure}
\\
\\\cn{unify\_list}(\ell,\seq{},\seq{}) =\ell
\\\cn{unify\_list}(\ell,t\cons u,t'\cons u') =
\cn{unify\_list}(\cn{unify}(\ell,t,t'), u, u')
\\\cn{unify\_list}(\ell,u,u') =\mbox{raise failure}
\end{array}
$$
\caption{Unifier}\label{fig:unifier}
\end{figure}

\begin{description}
\item[Signature:]
$$\begin{array}{ll@{{}\colon{}}ll}
\mbox{Sorts:}&\multicolumn{3}{l}{\mbox{$\top$, $S$, and $A$}}\\
\mbox{Operations:}&s&S\to\top& \mbox{Symmetric key inclusion}\\
&a&A\to\top& \mbox{Asymmetric key inclusion}\\
&(\cdot,\cdot)&\top\times\top\to\top& \mbox{Pairing}\\
&\enc{\cdot}{(\cdot)}&\top\times S\to\top& \mbox{Symmetric encryption}\\
&\enc{\cdot}{(\cdot)}&\top\times A\to\top& \mbox{Asymmetric encryption}\\
&(\cdot)^{-1}&S\to S& \mbox{Symmetric key inverse}\\
&(\cdot)^{-1}&A\to A& \mbox{Asymmetric key inverse}
\end{array}$$
\item[Equations:] for $x\colon S$, $x^{-1}\approx x$, and for $y\colon
  A$, $(y^{-1})^{-1}\approx y$
\item[Translation:] $\sembrack{\cdot}$ maps an order-sorted term to a
  many-sorted term
$$\sembrack{t}=\left\{
\begin{array}{ll}
t&\mbox{if $t\in X_\top$}\\
s(t)&\mbox{if $t\in X_S$}\\
\sembrack{t_0}&\mbox{if $t = t_0^{-1}$ and $t_0 : S$}\\
a(t)&\mbox{if $t\in X_A$}\\
a(x^{-1})&\mbox{if $t = x^{-1}$ and $x\in X_A$}\\
\sembrack{t_0}&\mbox{if $t = (t_0^{-1})^{-1}$ and $t_0 : A$}\\
(\sembrack{t_0},\sembrack{t_1})&\mbox{if $t=(t_0,t_1)$}\\
\enc{\sembrack{t_0}}{\sembrack{t_1}}&\mbox{if $t=\enc{t_0}{t_1}$}
\end{array}
\right.$$
\item[Canonical Terms:] BNF
$$\begin{array}{r@{{}\gets{}}l}
T&X_\top\mid S\mid A\mid(T,T)\mid\enc{T}{S}\mid
\enc{T}{A}
\\ S&s(X_S)
\\ A&a(X_A)\mid a(X_A^{-1})
\end{array}$$
\end{description}

\section{Simple Diffie-Hellman Algebra}

\begin{figure}
$$\begin{array}{ll@{{}\colon{}}ll}
\mbox{Sorts:}&\multicolumn{3}{l}{\mbox{$\top$, $S$, $A$, and $E$,
    where $S<\top$, $A<\top$, and $E<\top$}}\\
\mbox{Operations:}&(\cdot,\cdot)&\top\times\top\to\top& \mbox{Pairing}\\
&\enc{\cdot}{(\cdot)}&\top\times S\to\top& \mbox{Symmetric encryption}\\
&\enc{\cdot}{(\cdot)}&\top\times A\to\top& \mbox{Asymmetric encryption}\\
&\cn{inv}&S\to S& \mbox{Symmetric key inverse}\\
&\cn{inv}&A\to A& \mbox{Asymmetric key inverse}\\
&\gen&S&\mbox{Generator}\\
&\expr{(\cdot)}{(\cdot)}&S\times E\to S&\mbox{Exponentiation}\\
&(\cdot \cdot)& E\times E\to E&\mbox{Multiplication}\\
&(1/\cdot)&E\to E & \mbox{Reciprocal}\\
&1&E & \mbox{Identity}
\end{array}$$
\caption{Simple Diffie-Hellman Algebra Signature}\label{fig:dh signature}
\end{figure}

\begin{figure}
\begin{center}
$$\begin{array}{lll}
x(yz) \approx (xy)z&
xy \approx yx&
1x \approx x\\
x(1/x) \approx 1&
(h^x)^y \approx h^{xy}&
h^1 \approx h\\
\inv{h}\approx h&\inv{\inv{a}}\approx a
\end{array}$$
where $a\colon A$, $h\colon S$, and $x,y,z\colon E$
\end{center}
\caption{Simple Diffie-Hellman Algebra Equations}\label{fig:dh equations}
\end{figure}

\emph{This section will discuss the algebra whose signature is given
  in Figure~\ref{fig:dh signature} and equations are given in
  Figure~\ref{fig:dh equations}.}

\bibliography{cpsa}
\bibliographystyle{plain}

\end{document}