cpsa-2.1.0: doc/cpsaspec.tex
\documentclass[12pt]{article}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{url}
\usepackage{graphicx}
\usepackage{makeidx}
\usepackage[matrix,arrow,curve]{xy}
% Include this for a hyperlinked version of the document
% \usepackage{hyperref}
\theoremstyle{definition}
\newtheorem{defn}{Definition}[section]
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}
\newtheorem{cor}{Corollary}
\input{macros}
% This environment is used for comments about this draft.
\newenvironment{note}{\itshape\par\noindent}{}
\makeindex
\title{The CPSA Specification:\\
A Reduction System for Searching for Shapes in Cryptographic Protocols}
\author{John D.~Ramsdell\quad Joshua D.~Guttman\quad Paul D.~Rowe\\
The MITRE Corporation}
\begin{document}
\maketitle
\cpsacopying
\begin{note}
This is a draft and many of the theorems lack proofs. The draft has
an index and a table of contents at its end. Hopefully, the final
paper will support an abstract of the following form.
\end{note}
\begin{abstract}
We describe a term reduction system that enumerates all essentially
different executions possible for a cryptographic protocol. We call
them the \emph{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. Our Cryptographic Protocols Shapes Analyzer ({\cpsa})
program is a direct implementation of the reduction system described
within, and the form of the reduction system is partially determined
by the implementation.
The reduction system is a purely syntactic description of an abstract
version of the algorithm published previously. Order-sorted term
algebras are used for message algebras, and allow us to extend the
algorithm to algebras with an associative-commutative operation.
During the process of refining the description of the algorithm, we
found a significant simplification of the algorithm and that
elaborating some abstractions required great care.
This paper describes the reduction system and shows it possesses
desired correctness properties. In particular, its search is
\emph{complete} meaning when analyzing a protocol starting with
some initial behavior, every shape can be found in a finite number of
steps.
\end{abstract}
\begin{note}
Background material should be here.
\end{note}
Initial attempts at implementing the Cryptographic Protocols Shapes
Analyzer ({\cpsa}) algorithm in~\cite{DoghmiGuttmanThayer07} revealed
that the strand space framework required extensions and modifications
to specify the design and implementation of a {\cpsa} program. The
first step was to capture the essence of a strand space algebra in the
order-sorted algebra framework. The second step was to choose data
structures, and the third step was to specify operations on the data
structures that produce the desired results.
When using strand space theory, one normally hypothesizes the
existence of a single global strand space. This is a very reasonable
assumption for theoretical analysis, but from the point view of an
implementer, it turns out that it is better to assume there are many
local strand spaces and the design specification task is to describe
the relations between these local spaces. Our reformulation of strand
space notation provides an implementation oriented way of describing
the concept of a local strand space, and a direct link between from
algorithm specification to the data structures used in the
implementation.
In this specification, each reduction step in the search algorithm
relates a term to a set of terms. The correctness properties of the
algorithm justify a reduction step by placing restrictions on the
relations relative to their respective local strand spaces. The fact
that an efficient implementation is available is due in part to the
fact the reduction system is confluent, thus greatly reducing the
search space.
\begin{note}
The sections that follow should described here.
\end{note}
In what follows, a finite sequence is a function from an initial
segment of the natural numbers. The length of a sequence~$f$
is~$|f|$, $f_0\append f_1$ is the concatenation of sequences~$f_0$
and~$f_1$, and sequence~$f=\seq{f(0),\ldots,f(n-1)}$ for $n=|f|$.
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$. \index{sequence}
Section~\ref{sec:skeletons} will define the terms ``skeleton'' and
``pruned skeleton''. Starting in Section~\ref{sec:auth tests}, all
skeletons are pruned, so ``skeleton'' is used for pruned skeletons.
\section{Overview}\label{sec:overview}
An implementation-oriented view of strand spaces and bundles
\cite{ThayerEtal99} follows. In this paper, a run of a protocol is
viewed as an exchange of messages by a finite set of local sessions of
the protocol. Consider the class of $\Sigma,\Gamma$-algebras,
algebras over signature~$\Sigma$ that satisfy
equations~$\Gamma$~\cite[Chapter~3]{BaaderNipkow98}. A message is an
element of~$\alg{M}_{\Sigma,\Gamma}(X)$, a free
$\Sigma,\Gamma$-algebra generated by set~$X$.
Each local session is called a \emph{strand}, and is an element of the
strand set~$\Theta$. The behavior of a participant, its \emph{trace},
is a sequence of messaging events. An \emph{event} is either a
message transmission or a reception. Outbound message
$t\in\alg{M}_{\Sigma,\Gamma}(X)$ is written as~$\outbnd t$, and
inbound message~$t$ is written as~$\inbnd t$. A \emph{strand space}
over algebra~$\alg{M}_{\Sigma,\Gamma}(X)$ is the strand set~$\Theta$
together with a trace mapping $\fn{tr}\colon\Theta\to
(\pm\alg{M}_{\Sigma,\Gamma}(X))^+$. In a strand space, the elements
of the generator set~$X$ denote atomic message elements, such as keys
and text data, and not composite messages, such as encryptions and
pairs. Later in this paper, strand sets~$\Theta$ will be initial
segments of the natural numbers, so a trace mapping will be a
sequence.
Message events occur at nodes in a strand space. For each strand~$s$,
there is a node for every message in~$\fn{tr}(s)$. The \emph{nodes}
of strand space $(\Theta,\fn{tr})$ are $\{(s,p)\mid s\in\Theta, 0\leq
p < |\fn{tr}(s)|\}$, and the event at a node is
$\fn{evt}(s,p)=\fn{tr}(s)(p)$. The relation~$\Rightarrow$ defined by
$\{(s,p-1)\Rightarrow(s,p)\mid s\in\Theta, 0<p<|\fn{tr}(s)|\}$ is
called the \emph{strand succession relation}.
A \emph{bundle} in strand space $(\Theta,\fn{tr})$ is a finite
directed acyclic graph $\bundle(\Theta,\fn{tr},\to)$, where the
vertices are the nodes of $(\Theta,\fn{tr})$, 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~$\fn{evt}(n_0)=\outbnd t$
and~$\fn{evt}(n_1)=\inbnd t$. For each reception node~$n_1$, there is
a unique transmission node~$n_0$ with $n_0\rightarrow n_1$.
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 role is a sequence of message transmission
and reception terms that serves as a template for its strands. Let
$\alg{A}_{\Sigma,\Gamma}(Y)$ be a $\Sigma,\Gamma$-term algebra
generated by variable set~$Y$. A \emph{role} is a trace in
$(\pm\alg{A}_{\Sigma,\Gamma}(Y))^+$. A \emph{protocol} is a set of
roles.
A strand space $(\Theta,\fn{tr})$ \emph{respects protocol}~$P$ if
there is a role mapping $\fn{rl}\colon\Theta\to P$ with the following
properties. For each strand~$s$, $|\fn{tr}(s)|\leq|\fn{rl}(s)|$, and
there is a $\Sigma$-homomorphism
$\sigma\colon\alg{A}_{\Sigma,\Gamma}(Y)\rightarrow\alg{M}_{\Sigma,\Gamma}(X)$
such that $\sigma(\fn{rl}(s)(p))=\fn{tr}(s)(p)$ for all $0\leq
p<|\fn{tr}(s)|$. A bundle $\bundle(\Theta,\fn{tr},\to)$ is a
\emph{run of protocol}~$P$ if $(\Theta,\fn{tr})$ respects
protocol~$P$.
In what follows, $\alg{M}_{\Sigma,\Gamma}(X)$ is replaced by term algebra
$\alg{A}_{\Sigma,\Gamma}(Z)$, where $|Z|=|X|$, so that the two
algebras are isomorphic.
Now, on to the refinement of the definitions in this section. The
next section adds structure to message algebras using a sort system.
Later on, Definition~\ref{def:role} adds information to a role
and Definition~\ref{def:bundle} refines the notion of a run of a
protocol using the additional information.
\section{Messages}\label{sec:messages}
The {\cpsa} program implements a message algebra as an order-sorted term
algebra~\cite{GoguenMeseguer92}. The signature of one of the
implemented algebras is given in Figure~\ref{fig:bcs}.
Sort~\dom{mesg} is the sort of all messages, the elements of the
algebras in the previous section.
The use of order-sorted algebras is a partial solution to the
following problem. When a strand receives the
pair~$\cn{pair}(t_0,t_1)$, it can extract both~$t_0$, and~$t_1$. When
a strand receives the encryption~$\cn{enc}(t_0,t_1)$, it can
extract~$t_0$ if it has the decryption key associated with~$t_1$. And
if a strand receives the asymmetric key $\cn{invk}(t)$, it can never
extract~$t$. How does the {\cpsa} program distinguish these cases?
It classifies a term by its sort and the position at which it occurs
within another term. The sort system used to classify terms is
presented first.
Following~\cite{GoguenMeseguer92}, the set of messages used by {\cpsa}
is specified by an order-sorted signature $(S, \leq, \Sigma)$, where
$(S,\leq)$ is a partially ordered set of sort symbols, and~$\Sigma$ is
an $S^\ast\times S$-sorted family $\{\Sigma_{w,s}\mid w\in S^\ast,
s\in S\}$ of operation (or function) symbols. The operations satisfy
the following monotonicity condition,
$f\in\Sigma_{w,s}\cap\Sigma_{w',s'}$ and $w\leq w'$ imply $s\leq s'$,
where $w\leq w'$ iff $|w|=|w'|$ and $w(i)\leq w'(i)$ for $i<|w|$. A
variable set~$X$,\index{variable set} is an $S$-sorted
family~$X=\{X_s\mid s\in S\}$ of disjoint sets of symbols. No symbol
is both a variable and an operation. When $S$ and $\leq$ are clear,
we write~$\Sigma$ for $(S,\leq,\Sigma)$.
\begin{defn}[Regular Signature]\index{regular signature}
An order-sorted signature~$\Sigma$ is \emph{regular} iff given
$f\in\Sigma_{w',s'}$ and given $w''\leq w'$ in~$S^\ast$, there is a
least $(w,s)\in S^\ast\times S$ such that $w''\leq w$ and
$f\in\Sigma_{w,s}$.
\end{defn}
\begin{defn}[Order-Sorted Algebra]
Let~$(S,\leq,\Sigma)$ be an order-sorted signature. Then an
$(S,\leq,\Sigma)$-\emph{algebra}~\alg{A} is a family $\{\alg{A}_s\mid
s\in S\}$ of sets called the \emph{carriers} of~\alg{A}, together with
a function $\alg{A}_f:\alg{A}_w\to\alg{A}_s$ for each
$f\in\Sigma_{w,s}$ where $\alg{A}_w=\alg{A}_{w(0)}\times\cdots\times
\alg{A}_{w(n-1)}$, where $n=|w|$. Moreover,
\begin{enumerate}
\item $s\leq s'$ in~$S$ implies $\alg{A}_s\subseteq\alg{A}_{s'}$ and
\item $f\in\Sigma_{w,s}\cap\Sigma_{w',s'}$ and $w\leq
w'$ imply $\alg{A}_f:\alg{A}_{w}\to\alg{A}_{s}$ equals
$\alg{A}_f:\alg{A}_{w'}\to\alg{A}_{s'}$ on $\alg{A}_{w}$.
\end{enumerate}
\end{defn}
\begin{defn}[Order-Sorted Terms]
The order-sorted $\Sigma$-terms $\terms_\Sigma(X)$ generated by
variable set~$X$ is the least family $\{\terms_{\Sigma,s}(X)\mid
s\in S\}$ such that
\begin{enumerate}
\item $\Sigma_{\seq{},s}\subseteq\terms_{\Sigma,s}(X)$
and $X_s\subseteq\terms_{\Sigma,s}(X)$ for $s\in S$;
\item $\terms_{\Sigma,s'}(X)\subseteq\terms_{\Sigma,s}(X)$
if $s'\leq s$;
\item if $f\in\Sigma_{w,s}$ and $t_i\in\terms_{\Sigma,w(i)}(X)$
for $i<|w|$, then $f(t_0,\ldots,t_{|w|-1})\in
\terms_{\Sigma,s}(X)$.
\end{enumerate}
\end{defn}
In~\cite{GoguenMeseguer92}, it is proved that $\terms_\Sigma(X)$
is an order-sorted algebra and when~$\Sigma$ is regular, each term has
a least sort.
An \emph{equation} is a triple $(X,t,t')$, written $t\approx t'$,
where~$X$ is a variable set and $t,t'$ are in $\terms_\Sigma(X)$ and
have the same least sort. See~\cite{GoguenMeseguer92} on how to relax
the sort restriction. The review of order-sorted algebras ends here.
\begin{defn}[Encryption Signature]
A regular order-sorted signature is an \emph{encryption signature} if
it contains a distinguished sort symbol~$\top$, the sort of all
messages, and a binary encryption operation $\cn{enc}$ defined so that
the least sort of every term of the form $\cn{enc}(t_0,t_1)$
is~$\top$.
\end{defn}
\begin{defn}[Strand Space Signature]
A \emph{strand space signature}~$(\Sigma, B)$ is an encryption
signature~$\Sigma$, and a non-empty subset~$B$ of sort symbols
in~$\Sigma$ such that $s\in B$ implies $s<\top$. Each member of~$B$
is called a \emph{base sort}. Every operation in~$\Sigma$ with a base
sorted result must have base sorted arguments.
\end{defn}
\begin{defn}[Strand Space Equations]
Equations in~$\Gamma$ for strand space signature $(\Sigma,B)$ are
\emph{strand space equations} if the least sort of the terms that
define each equation in~$\Gamma$ is a base sort in~$B$.
\end{defn}
The unification type\index{unification type} of~$\Gamma$
w.r.t.\ signature~$\Sigma$ is \emph{unitary}\index{unitary unification
type} if every problem has a minimal complete set of unifiers that
has at most one element~\cite[Chapter~8,
Section~3.1]{RobinsonVoronkov01}.
\begin{defn}[Strand Space Algebra]\label{def:algebra}
Given strand space signature~$(\Sigma,B)$ and strand space
equations~$\Gamma$, a \emph{strand space
algebra}~$\alg{A}_{\Sigma,B,\Gamma}(X)$ is the quotient of
$\terms_\Sigma(X)$ by the equivalence relation on $\terms_\Sigma(X)$
derived from the equations in~$\Gamma$, where the unification type
of~$\Gamma$ w.r.t.\ signature~$\Sigma$ is unitary.
\end{defn}
\begin{figure}
\begin{center}
Base sort symbols: \dom{name}, \dom{text}, \dom{data}, \dom{skey},
\dom{akey}\\
Non-base sort symbol: \dom{mesg} (implementation of $\top$) \\[1ex]
Subsorts: \dom{name}, \dom{text}, \dom{data}, \dom{akey},
$\dom{skey}<\dom{mesg}$\\[1ex]
\begin{tabular}{@{}ll}
$\cn{enc}\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg}$
&Encryption\\
$\cn{pair}\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg}$
&Pairing\\
$C_i\colon\dom{mesg}$& Tag constants ($i\in\nat$)\\
$\cn{pubk}\colon\dom{name}\rightarrow\dom{akey}$
&Public key of name\\
$\cn{invk}\colon\dom{akey}\rightarrow\dom{akey}$
&Inverse of asymmetric key\\
$\cn{ltk}\colon\dom{name}\times\dom{name}\rightarrow\dom{skey}$
& Long term shared key
\end{tabular}\\[1ex]
Equation: $\cn{invk}(\cn{invk}(x))\approx x$ for $x\colon\dom{akey}$
\end{center}
\caption{Basic Crypto Signature and Equation}\label{fig:bcs}
\end{figure}
\begin{figure}
\begin{center}
\includegraphics{carriers-0.mps}\\
Carrier set of sort \dom{mesg}\\
$X_\top$: variables of sort \dom{mesg}
\caption{Basic Crypto Carrier Sets}
\label{fig:bc carrier sets}
\end{center}
\end{figure}
\begin{figure}
\begin{center}
\begin{tabular}{lll}
New base sorts:
&\dom{base}, $\dom{expn} <\dom{mesg}$\\
New operations:
&$\cn{gen}\colon\dom{base}$
&Generator\\
&$\cn{exp}\colon\dom{base}\times\dom{expn}\to\dom{base}$
&Exponentiation\\
&$\cn{mul}\colon\dom{expn}\times\dom{expn}\to\dom{expn}$
&Multiplication\\
&$\cn{one}\colon\dom{expn}$
&Unit\\
&$\cn{rec}\colon\dom{expn}\to\dom{expn}$
&Reciprocal\\
New equations:&$\cn{exp}(\cn{exp}(g,x),y)\approx\cn{exp}(g,\cn{mul}(x,y))$\\
&$\cn{exp}(g,\cn{one})\approx g$\\
&$\cn{mul}(x,y)\approx\cn{mul}(y,x)$&Commutativity \\
&$\cn{mul}(x,\cn{mul}(y,z))\approx\cn{mul}(\cn{mul}(x,y),z)$& Associativity\\
&$\cn{mul}(x,\cn{one})\approx x$&Identity\\
&$\cn{mul}(x,\cn{rec}(x))\approx \cn{one}$&Cancellation
\end{tabular}
\end{center}
\caption{Additions for Diffie-Hellman Key Exchange}\label{fig:dhke}
\end{figure}
In the remainder, the strand space signature and equations are fixed,
and its algebras are written as~$\alg{A}(X)$ and as~$\alg{A}$ when the
variable set~$X$ is available from the context, and the term algebras
as $\terms(X)$ and~$\terms$ respectively. Relation $\equiv$ is the
equivalence relation on~$\terms_\top$ derived from the equations
in~$\Gamma$, and the equivalence class $[t]$ is $\{t'\mid t\equiv
t'\}$. We assume each equivalence class has a canonical
representative. At times we conflate a term with the equivalence
class of which it is a member to simplify the presentation. Given a
sort~$s$, $t\colon s$ asserts that $[t]\in\alg{A}_s$, and $t\colon S$
asserts that for some~$s\in S$,~$t\colon s$. Term~$t$ is a
\index{message}\emph{message} if $[t]\in\alg{A}_\top$. Message~$t$ is
an \index{atom}\emph{atom} iff~$t\colon B$. The message
$\cn{enc}(t_0,t_1)$ is written $\enc{t_0}{t_1}$.
In the Basic Crypto algebra, sort \dom{mesg} implements sort~$\top$,
and all of its other sorts are base sorts. A term of the form
$\cn{invk}(t)$ is an atom. Figure~\ref{fig:bc carrier sets} shows the
classification of terms in the Basic Crypto algebra. In text, we use
comma as a right associative binary operation for pairing and $K_a$
for $\cn{pubk}(a)$, as in the caption of Figure~\ref{fig:term tree}.
\begin{thm}[Encryption Freely Generated]\label{thm:encryption}
Suppose $t,t_0,t_1\in\terms_\top$ and $\enc{t_0}{t_1}\equiv t$. Then
there exists $t'_0,t'_1$ such that $t=\enc{t'_0}{t'_1}$, $t_0\equiv
t'_0$, and~$t_1\equiv t'_1$.
\end{thm}
\begin{proof}
Consider $\terms^0_\top(X)\subseteq \terms_\top(X)$, where
$\terms^0_\top(X)=\Sigma_{\seq{},\top}\cup X_\top\cup\bigcup_{s\in
B}\terms_s(X)$. Observe that the encryption operation does not
occur in $\terms^0_\top(X)$ and that $\terms^0_\top(X)$ freely
generates $\terms_\top(X)$. Thus $\alg{A}^0_\top(X)=\{[t]\mid t\in
\terms^0_\top(X)\}$ freely generates $\alg{A}_\top(X)$. No equation
applies to messages in $\alg{A}_\top(X)\setminus\alg{A}^0_\top(X)$ and
so induction on term formation gives the result.
\end{proof}
Figure~\ref{fig:bc carrier sets} shows the carrier sets for the Basic
Crypto Algebra.
\begin{defn}[Position]\label{defn:position}
A \emph{position}~$p$ is a finite sequence of natural numbers. The
term in~$t$ that \emph{occurs at}~$p$, written~$t\termat p$, is:
$$\begin{array}{l}
t\termat\seq{}=t;\\
f(t_0,\ldots,t_{|w|-1})\termat\seq{i}\append p=
t_i\termat p\mbox{ if }f\in\Sigma_{w,s}\mbox{ and }i<|w|.
\end{array}$$
A term~$t$ \emph{occurs in} $t'\in\terms_\top(X)$ if $t=t'\termat p$
for some~$p$. A message~$t$ \emph{occurs in} $t'\in\alg{A}_\top(X)$
if the canonical representative of~$t$ occurs in the canonical
representative of~$t'$.
\end{defn}
Some positions within a message are distinguished. A position~$p$
\emph{traverses a key edge} in~$t$ if $t\termat p_0=\enc{t_0}{t_1}$
and $p=p_0\append\seq{1}\append p_1$. A position~$p$ \emph{traverses
an atom edge} in~$t$ if $t\termat p_0=f(t_0,\ldots,t_{|w|-1})$ is an
atom and $p=p_0\append\seq{i}\append p_1$, where $f\in\Sigma_{w,s}$
and $i<|w|$. A position is a \emph{carried position}\index{carried
position} in~$t$ if it traverses no key or atom edge in~$t$. In
Figure~\ref{fig:term tree}, variable~$x$ occurs at two carried
positions, but~$a$ occurs at no carried positions.
\begin{figure}
\begin{center}
\includegraphics{termtree-0.mps}
\end{center}
\vspace{-2ex}
\caption{Tree for $\enc{x}{K_a},\enc{\enc{x}{K_a}}{K_b}$}\label{fig:term tree}
\end{figure}
The concept of an accessible term is used in Definition~\ref{def:used}.
\begin{defn}[Accessible]\label{def:accessible}
Message~$t_0$ is \emph{accessible in}~$t_1$, written~$t_0\ll t_1$,
if~$t_0$ occurs at a position in~$t_1$ that traverses no atom edge.
\end{defn}
A carried term is one that can be extracted from a message reception
given the right set of decryption keys.
\begin{defn}[Carries]\label{def:carries}
Message~$t_0$ \emph{carries}~$t_1$, written~$t_1\sqsubseteq t_0$,
if~$t_1$ occurs at a carried position in~$t_0$.
\end{defn}
Carried positions respect equality modulo the equations.
\begin{defn}[Carried Positions]
\label{def:carried positions}
\index{carried positions}
Given a term~$t$, the set of positions at which~$t'$ carries~$t$ is
$\fn{carpos}(t,t')$, where
$$\fn{carpos}(t,t')=\left\{
\begin{array}{ll}
\{\seq{}\}&\mbox{if $t'\equiv t$, else}\\
\multicolumn{2}{l}{\{\seq{0}\append p \mid
p\in\fn{carpos}(t,t_0)\}}\\
& \mbox{if $t'=\enc{t_0}{t_1}$, else}\\
\multicolumn{2}{l}{\{\seq{i}\append p \mid
p\in\fn{carpos}(t,t_i),i<n\}} \\
& \mbox{if $t'=f(t_0,\ldots,t_{n-1})$ and}\\
&\mbox{$t'$ is not an atom, else}\\
\{\}&\mbox{otherwise.}
\end{array}\right.$$
\end{defn}
Note that $\fn{carpos}(x,\cn{invk}(\cn{invk}(x)))=\{\seq{}\}$, not
$\{\seq{}, \seq{0,0}\}$, and~$t'$ carries~$t$ iff $\fn{carpos}(t,t')$
is non-empty.
\begin{thm}\label{thm:carpos}
For all $t_0,t_1,t'_0,t'_1\in\terms_\top(X)$, $t_0\equiv t_1$ and
$t'_0\equiv t'_1$ implies $\fn{carpos}(t_0,t'_0)=
\fn{carpos}(t_1,t'_1)$.
\end{thm}
\begin{proof}
When $t'_0$ and $t'_1$ are atoms, the result is obvious. Otherwise,
Theorem~\ref{thm:encryption} applies.
\end{proof}
The key insight discovered while implementing strand space algebras is
that ordinary order-sorted algebras with restricted signatures,
coupled with the \fn{carpos} function, captures the essence of strand
space algebras required to implement the {\cpsa} algorithm.
Section~\ref{sec:cow} will explain why the details of the \fn{carpos}
function are important, and why an implementation of the carries
relation does not suffice.
\begin{defn}[Strand Space with Asymmetric Encryption]
A strand space algebra $\alg{A}_{\Sigma,B,\Gamma}(X)$ with asymmetric
encryption has a signature with a distinguished base sort
symbol~$\cn{akey}$, an
operation~$\cn{invk}\colon\cn{akey}\to\cn{akey}$, and~$\Gamma$
contains the equation $\cn{invk}(\cn{invk}(x))\approx x$ for
$x\colon\dom{akey}$.
\end{defn}
\begin{defn}[Inverse Key]
For a strand space with asymmetric encryption, the decryption key of
encryption~$\enc{t_0}{t_1}$ is~$\fn{inv}(t_1)$, where
$$\fn{inv}(t) =\left\{
\begin{array}{ll}
\cn{invk}(t)&\mbox{if $t\colon\dom{akey}$;}\\
\mbox{undefined}&\mbox{if $t$ is a variable of sort $\top$;}\\
t&\mbox{otherwise.}
\end{array}\right.$$
\end{defn}
\index{substitutions} Both unification and matching are used to solve
equations. First, a few more definitions from~\cite{GoguenMeseguer92}
and~\cite{RobinsonVoronkov01}. Given two $S$-sorted variable sets~$X$
and~$Y$, an \emph{order-sorted substitution} is an $S$-sorted
map~$\sigma\colon X\rightarrow\alg{A}(Y)$ such that $\sigma(x)\neq x$
for only finite many elements of~$X$. For a substitution~$\sigma$,
the \index{domain of substitution}\emph{domain} is the set of
variables $\fn{Dom}(\sigma)=\{x\mid \sigma(x)\neq x\}$ and the
\index{range of substitution}\emph{range} is the set of terms
$\fn{Ran}(\sigma)=\{\sigma(x)\mid x\in\fn{Dom}(\sigma)\}$.
Substitution~$\sigma_0$ is \index{more general substitution}\emph{more
general than}~$\sigma_1$, written~$\sigma_0\unlhd\sigma_1$, if there
exists a substitution~$\sigma_2$ such that
$\sigma_1(x)\equiv\sigma_2(\sigma_0(x))$ for $x\in X$, the variable
set that generates the term algebra. It is possible to have
$\sigma_0\unlhd\sigma_1$ and $\sigma_1\unlhd\sigma_0$. In this case,
$\sigma_1=\sigma_2\circ\sigma_0$ and $\sigma_0=\sigma_2'\circ
\sigma_0$ where $\sigma_2$ and~$\sigma_2'$ are renamings. That is,
$Dom(\sigma_2)=Ran(\sigma_2)$ and likewise for~$\sigma_2'$. In this
case we say that $\sigma_0$ and $\sigma_1$ are renamings of each
other. Given an $S$-sorted map~$\varphi\colon
X\rightarrow\alg{A}(Y)$, the unique order-sorted
$\Sigma$-homomorphism\index{homomorphism!order-sorted}
$\varphi^\ast\colon\alg{A}(X)\rightarrow\alg{A}(Y)$ induced
by~$\varphi$ is also denoted~$\varphi$.
The algorithms used to solve unification and matching problems
typically solve many equations at once. To facilitate this
requirement, algebras provide functions with the following signatures.
\index{unify}\index{match}
$$\begin{array}{l}
\fn{unify}\colon
\mathcal{T}_\top(X)\times\mathcal{T}_\top(X)\times
(X\rightarrow\mathcal{T}_\top(X))\rightarrow
(X\rightarrow\mathcal{T}_\top(X))^\ast\\
\fn{match}\colon
\mathcal{T}_\top(X)\times\mathcal{T}_\top(Y)\times
(X\rightarrow\mathcal{T}_\top(Y))\rightarrow
(X\rightarrow\mathcal{T}_\top(Y))^\ast
\end{array}$$
Suppose $\sigma_0$ has the property that $\sigma_0(t_i)\equiv
\sigma_0(t_i')$ for~$i < n$. Then $\sigma_1(t_i)\equiv \sigma_1(t_i')$
for~$i \leq n$ if $\sigma_1\in\fn{unify}(t_n,t'_n,\sigma_0)$. The
$\fn{unify}$ function has this property:
$$\fn{unify}(t_0,t_1,\sigma_0)=\{\comp{\sigma_1}{\sigma_0}\mid
\sigma_1\in\fn{unify}(\sigma_0(t_0),\sigma_0(t_1),\idsigma)\},$$
where~$\idsigma$ is the identity substitution. Furthermore, it must
produce a minimal complete set of unifiers.
\begin{lem}[Order of Unification]\label{lem:unification}
Suppose that the underlying message algebra has single most general unifiers
for any two unifiable terms. Suppose also that
$\fn{unify}(t_0,t_1,\idsigma)=\{\sigma_0\}$ and that
$\fn{unify}(s_0,s_1,\idsigma)=\{\sigma_1\}$. Then
$\fn{unify}(s_0,s_1,\sigma_0)\cong \fn{unify}(t_0,t_1,\sigma_1)$.
That is, when one side exists so does the other, and the two
substitutions will be renamings of each other.
\end{lem}
A proof of this result can be found for example in~\cite{BaaderNipkow98}.
By a simple induction, given any system of equations,
$E=\{t_1\eqq t_1',\ldots,t_n\eqq t_n'\}$, we may solve them in
any order and we will end up with the same substitution (up to
renaming).
This justifies more general definitions that will be used later.
Let $A_0$ be a set of terms which you would like to jointly unify.
That is, $A_0$ represents the equations $\{t_i\eqq t_j\mid t_i,t_j\in A_0\}$.
Then we may define
$\fn{Unif}(A_0,\sigma)=\fn{unify}(t_{n-1},t_n,\fn{unify}(\dots ,\fn{unify}(t_0,t_1,\sigma)\dots)).$
By Lemma~\ref{lem:unification} this definition does not depend on the order
of the terms $t_0,\dots,t_n$. The result will be the same up to renaming
for any ordering of the terms.
It then follows by further induction that
$\fn{Unif}(A_1,\fn{Unif}(A_0,\sigma))\cong \fn{Unif}(A_0,\fn{Unif}(A_1,\sigma))$.
This justifies the more general definition
$$U(A_0,\dots,A_n;\sigma)=\fn{Unif}(A_n,\fn{Unif}(\dots ,\fn{Unif}(A_0,\sigma)\dots)).$$
Again we could have defined it in terms of any order of the
sets $A_0,\dots,A_n$. The result might be a different substitution
but it would be a renaming of the one defined.
\iffalse
When solving a system of equations $E=\{t_1\eqq t_1',\ldots,t_n\eqq
t_n'\}$, we rely on the fact that the order is which the equations are
solved is irrelevant in the following sense. Let $\mcsu(E)$ be a
minimal complete set of unifiers that solves~$E$,
i.e.\ $\sigma\in\mcsu(E)$ and $t\eqq t'\in E$ implies $\sigma(t)\equiv
\sigma(t')$. Let $E=E_0\uplus E_1$ be a partition of~$E$, and
let~$S=\{\sigma_1\circ\sigma_0\mid\sigma_0\in\mcsu(E_0)\land
\sigma_1\in\mcsu(\sigma_0(E_1))\}$. Then~$S$ is a complete set of
unifiers that solve~$E$.
\fi
\subsection*{Discussion}
The message algebra that appears in strand space
papers~\cite{ThayerEtal99,GuttmanThayer02} was not implemented because
there is no syntactic method that can be used to determine if an
encryption denotes symmetric or asymmetric encryption. The signature
in Figure~\ref{fig:bcs} resolves this problem.
The OSA conjecture of this paper is that the results in every strand
space paper would remain unchanged if it used algebras from
Definition~\ref{def:algebra} as long as unification in the algebra
produces at most one most general unifier. Notice there is no
prohibition on constants being atoms in the definition of a strand
space algebra in this paper, in contrast with the algebras defined in
other papers.
Readers of this paper are encouraged to consider other algebras, such
as those that contain an Abelian group and modular exponentiation.
Such algebras allow the analysis of Diffie-Hellman Key Exchange, for
example. See Figure~\ref{fig:dhke}.
Some strand space papers defined the word occurs to mean carried by.
This document uses it to assert a message is within another message.
\section{Data Structures}\label{sec:data structures}
The data structures used in the implementation are modeled as elements
in an order-sorted term algebra. The signature for the algebra is the
extension of a strand space signature shown in
Table~\ref{tab:strands}. In this specification, it is assumed the
strand space signature uses the sort symbol \dom{mesg} to implement
sort~$\top$.
\begin{table}
\begin{center}
Additional sort symbols: \dom{atom}, \dom{evt}, \dom{role}, \dom{maplet},\\
\dom{instance}, \dom{node}, \dom{ordering}, and \dom{preskel} \\[1ex]
Subsorts: for each $s\in B, s\leq\dom{atom} < \dom{mesg}$\\[1ex]
$\begin{array}{rl}
\outbnd\colon\dom{mesg}\rightarrow\dom{evt}\hspace{2\arraycolsep}
\inbnd\colon\dom{mesg}\rightarrow\dom{evt}&
\cn{r}\colon\dom{evt}\dom{list}\times\dom{atom}\dom{set}\times
\dom{atom}\dom{set}\rightarrow\dom{role}\\
\cn{m}\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{maplet}&
\cn{i}\colon\dom{role}\times\dom{nat}\times\dom{maplet}\dom{set}
\rightarrow\dom{instance}\\
\cn{n}\colon\dom{nat}\times\dom{nat}\rightarrow\dom{node}
&\cn{o}\colon\dom{node}\times\dom{node}\rightarrow\dom{ordering}
\end{array}$\\
$\cn{k}\colon\dom{role}\dom{set}\times
\dom{instance}\dom{list}\times
\dom{ordering}\dom{set}\times\dom{atom}\dom{set}\times
\dom{atom}\dom{set}\rightarrow\dom{preskel}$\\[1ex]
\begin{tabular}{rl}
\dom{mesg}& the sort of all messages (implementation of $\top$)\\
\dom{atom}& the sort of all base sorted messages\\
\dom{evt}& a transmission or reception event\\
\dom{trace}& a sequence of events used in a role\\
\dom{role}& a trace, a non-originating set, and a uniquely-originating
set\\
\dom{protocol}& a set of roles\\
\dom{nat}& a natural number\\
\dom{maplet}& a map from a role variable to a preskeleton term\\
\dom{instance}& a strand's trace and inheritance as instantiated from a role\\
\dom{node}& a pair of numbers, a strand identifier and a strand position\\
\dom{ordering}&a causal ordering between a pair of nodes\\
\dom{preskel}& a preskeleton
\end{tabular}
\end{center}
\caption{{\cpsa} Signature}\label{tab:strands}
\end{table}
Every element of the sort \dom{atom} is intended to be an element of
some base sort. Furthermore, elements of the other sorts added by a
{\cpsa} signature correctly model an implementation when there are no
variables of those sorts. As a result, the algebras that model an
implementation are {\cpsa} algebras.
\begin{defn}[{\cpsa} Algebra]\label{def:cpsa algebra}
\index{CPSA@{\cpsa} algebra} Consider the class of
$\Sigma,\Gamma$-algebras, algebras over {\cpsa} signature~$\Sigma$
that satisfy equations~$\Gamma$. Algebra~$\alg{C}(X)$ is a
\emph{{\cpsa} algebra} if it is a free $\Sigma,\Gamma$-algebra
generated by variable set~$X$, and the variable set~$X$ has the
following property. For sort~$s$, $X_s$ is empty when~$s$ is
\dom{atom}, \dom{evt}, \dom{role}, \dom{maplet}, \dom{instance},
\dom{node}, \dom{ordering}, and \dom{preskel}.
\end{defn}
Section~\ref{sec:protocols} on protocols defines events (\dom{evt}),
traces (\dom{env} \dom{list}), and roles (\dom{role}).
Section~\ref{sec:executions} on executions defines instances
(\dom{instance}) and role substitutions (\dom{maplet} \dom{set}).
Section~\ref{sec:skeletons} on skeletons defines, nodes (\dom{node}),
node orderings (\dom{ordering} \dom{set}), and preskeletons
(\dom{preskel}).
\section{Algorithms as Term Reduction Systems}\label{sec:algorithms}
Algorithms in this paper are specified as abstract
reduction systems~\cite[Chapter~2]{BaaderNipkow98}. A reduction
system is a pair $(A,\to)$, where reduction~$\to$ is a binary relation
$\mathord{\to}\subseteq A\times A$. Element $x\in A$ is a
\emph{normal form} if there is no~$y$ such that $x\to y$. The
transitive closure of~$\to$ is~$\to^+$. The reflexive transitive
closure of~$\to$ is~$\to^\ast$. A reduction is confluent if
$x\to^\ast y_0$ and $x\to^\ast y_1$ implies there is a~$z$ such that
$y_0\to^\ast z$ and $y_1\to^\ast z$. A reduction is terminating if
there are no infinite descending chains. A reduction is convergent if
it is confluent and terminating.
Let $\alg{K}$ be $\alg{A}_{\dom{preskel}}(X)$. Algorithms are
specified as reduction systems of the form $(\alg{K},\to)$, which are
then used to specify a related setwise reduction system of the form
$(\pow{\alg{K}},\mathord\twoheadrightarrow)$. Setwise reduction
systems are the ones with the interesting normal forms and confluence
properties. In a setwise reduction system, reduction rewrites one
element of a set to a set of elements.
\begin{defn}[Setwise Reduction System]
The \emph{setwise reduction system} of binary relation
$\rightsquigarrow\subseteq\alg{K}\times\pow{\alg{K}}$ is a reduction
system $(\pow{\alg{K}},\twoheadrightarrow)$, where for each
$K_0\in\pow{\alg{K}}$, $K_0\twoheadrightarrow K_1$ if for some $k_0\in
K_0$, $k_0\rightsquigarrow K_2$, $K_1=K_2\cup (K_0\setminus\{k_0\})$,
and $K_1\neq K_0$.
\end{defn}
The {\cpsa} algorithm will be specified as a setwise term reduction
system, where the initial problem is given a singleton
in~$\pow{\alg{K}}$, and the answers computed by an implementation of
the algorithm are a normal form of the setwise reduction
relation~$\twoheadrightarrow_k$ defined in Section~\ref{sec:skeleton
reduction}.
In what follows the relation $k\rightsquigarrow K$ is defined in terms
of $\to\subseteq\alg{K}\times\alg{K}$ by specifying
$\{k\}\twoheadrightarrow K$ using~$\to$, so the $\rightsquigarrow$
relation is not explicitly defined.
We regard sets of preskeletons as factored by isomorphism, where each
set has at most one representative of the equivalence class of
isomorphic preskeletons. The definition of isomorphic preskeletons
is given in Definition~\ref{def:homomorphism}.
\section{Protocols}\label{sec:protocols}
A protocol defines the patterns of allowed behavior for each
participant in an execution of the protocol. Protocol participants
send and receive messages.
\begin{defn}[Event]
An \emph{event} is either a message transmission or a reception.
Formally, an event is a pair~$(d,t)$ with $t\in\alg{A}_{\top}$ and~$d$
one of the symbols~$\outbnd$ or~$\inbnd$. A positive
message~$\outbnd t$ is \index{outbound}\emph{outbound}, and a negative
message~$\inbnd t$ is \index{inbound}\emph{inbound.}
\end{defn}
In a {\cpsa} algebra, an event is a term of sort \dom{evt}.
\begin{defn}[Trace]
A \emph{trace} is a non-empty sequence of events, an
element of $(\pm\alg{A}_{\top})^+$
\end{defn}
In a {\cpsa} algebra, a trace is a term of sort \dom{evt} \dom{list}.
\begin{defn}[Originates]\index{originates}
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.
\end{defn}
\begin{defn}[Gained]\index{gained}
A message is \emph{gained} in a trace if it is carried by some
event and the first event in which it is carried is outbound.
\end{defn}
\begin{defn}[Acquired]\index{acquired}
A message is \emph{acquired} by a trace if it first occurs in an
inbound message and is also carried by that message.
\end{defn}
The next definition describes syntactic constraints on
``uniquely-originating'' and ``non-originating'' atoms. The meaning
of these adjectives is not revealed until Definition~\ref{def:bundle}.
\begin{defn}[Role]\label{def:role}
A \emph{role}~$r$ consists of a trace~$\fn{rtrace}(r)$, a set of
non-originating atoms~$\fn{rnon}(r)$, and a set of uniquely
originating atoms~$\fn{runique}(r)$. The variable set~$\fn{rvar}(r)$
of the role is the set of variables that occur in~$\fn{rtrace}(r)$.
The following properties hold.
\begin{enumerate}
\item Each uniquely originating atom originates in the trace.
\item Each non-originating atom is not carried by any event in the
trace, and each variable that occurs in the atom occurs in the
trace.
\item Every non-base sorted variable is acquired by the trace.\index{acquired}
\end{enumerate}
\end{defn}
In a {\cpsa} algebra, a role is a term of the form~$\cn{r}(C,N,U)$,
where
$$\begin{array}{r@{}c@{}l}
\fn{rtrace}(\cn{r}(C,N,U))&{}={}&C,\\
\fn{rnon}(\cn{r}(C,N,U))&{}={}&N,\\
\fn{runique}(\cn{r}(C,N,U))&{}={}&U.
\end{array}$$
\begin{defn}[Protocol]
A \emph{protocol} is a set of roles with pairwise disjoint variable sets.
\end{defn}
\subsection*{Discussion}
The refinement of strand space protocols is mostly just a change in
representation for the same information. The change is motivated by
the way protocols are used. In this refinement, a protocol is defined
without reference to the concept of a strand, a node, or a strand
space.
In~\cite{DoghmiGuttmanThayer07}, a protocol is a triple
$(\Pi,\fn{strand\_non},\fn{strand\_unique})$, where~$\Pi$ is a finite
set of strands, \fn{strand\_non} and \fn{strand\_unique} map a strand
to a set of atoms, and the mappings have properties analogous to the
ones in the Definition~\ref{def:role}, the definition of a role. The
set of roles is $\{r\mid s\in\Pi, \fn{rtrace}(r)=\fn{tr}(s),
\fn{runique}(r)=\fn{strand\_unique}(s), \fn{rnon}(r)=
\fn{strand\_non}(s)\}$.
In~\cite{DoghmiGuttmanThayer07}, non-originating messages were assumed
to be keys of the form~$K$ or~$K^{-1}$, thereby excluding long term
shared symmetric keys of the form $\cn{ltk}(A,B)$. The definition of
role allows symmetric keys to be assumed to be non-originating.
\section{Executions}\label{sec:executions}
Executions of a protocol are formalized by a bundle, which is
described in this section. A key difference in this approach to
formalizing strand spaces is that the parameters used to instantiate a
strand's trace from a role are preserved, so as to support role
origination assumptions.
\begin{defn}[Instance]
An \emph{instance}~$i$ consists of a role $\fn{role}(i)$, a positive
number $\fn{height}(i)$, and an order-sorted substitution
$\fn{subst}(i)$. Let~$r$,~$h$, and~$\sigma$ be the role, height, and
substitution for a given instance~$i$. Let $\prefix{C}{h}$ be the prefix of
sequence~$C$ of length~$h$. The following properties hold.
\begin{enumerate}
\item The height of an instance cannot exceed the length of it's
role's trace.
\item $\fn{Dom}(\sigma)$ is the set of variables that occur in
$\prefix{\fn{rtrace}(r)}{h}$.
\item No variable in an instance's role may occur in
$\fn{Ran}(\sigma)$.
\end{enumerate}
\end{defn}
In a {\cpsa} algebra, an instance is a term of the form~$\cn{i}(r,h,M)$
where
$$\begin{array}{r@{}c@{}l}
\fn{role}(\cn{i}(r,h,M))&{}={}&r,\\
\fn{height}(\cn{i}(r,h,M))&{}={}&h,\\
\fn{subst}(\cn{i}(r,h,M))&{}={}&\sigma
\end{array}$$
and $\sigma(x)=y$ for each $\cn{m}(x,y)\in M$.
\begin{defn}[Trace of Instance]
The trace of an instance~$i$, $\fn{trace}(i)$, is a sequence of
length $\fn{height}(i)$ such that for $\sigma=\fn{subst}(i)$ and all
$j<\fn{height}(i)$,
$\fn{trace}(i)(j)=\sigma(\fn{rtrace}(\fn{role}(i))(j))$.
\end{defn}
For every instance~$i$, the definitions imply that the set of
variables that occur in $\fn{trace}(i)$ is a subset of the set of
variables that occur in $\fn{Ran}(\fn{subst}(i))$. The Diffie-Hellman
algebra provides an example in which the subset relation is proper.
Consider a role with a trace of $\seq{\cn{exp}(x,\cn{mul}(y,z))}$.
The definitions allow an instance of the role with height one and
substitution $\{x\mapsto a, y\mapsto\cn{mul}(b,d),
z\mapsto\cn{mul}(c,\cn{rec}(d))\}$, giving the instance a trace of
$\seq{\cn{exp}(a,\cn{mul}(b,c))}$.
\begin{defn}[Instance Origination Assumptions]
Let $\sigma=\fn{subst}(i)$ for an instance~$i$, $r=\fn{role}(i)$, and
$h=\fn{height}(i)$. Instance~$i$ inherits the non-origination
assumption~$\sigma(t)$ if~$t\in\fn{rnon}(r)$, and the variables in~$t$
are in $\fn{Dom}(\sigma)$. Instance~$i$ inherits the unique
origination assumption~$\sigma(t)$ if~$t\in\fn{runique}(r)$, and $t$
originates in $\prefix{\fn{rtrace}(r)}{h}$.
\end{defn}
\begin{defn}[Strand Space~\protect{\cite[Definition~2.2]{ThayerEtal99}}]
A \emph{strand space} over algebra~$\alg{A}_{\top}$ is a set~$\Theta$
together with a trace mapping $\fn{tr}\colon\Theta\to
(\pm\alg{A}_{\top})^+$.
\end{defn}
In this document, a strand set~$\Theta$ is an initial segment of the
natural numbers, so a trace mapping is a sequence. Thus a strand
space is the trace sequence $\fn{tr}:((\pm\alg{A}_{\top})^+)^+$, and
its strand set is the domain of $\fn{tr}$.
A finite sequence of instances~$I$ is a \emph{protocol respecting
strand space}. The strand space of~$I$ is $\fn{tr}=\fn{trace}\circ
I$. By construction, the trace of each strand is an instance of a
role.
The variable set $\fn{var}(I)$ is the set of variables that occur in
the range of the substitution of its instances. In what follows,
definitions are simplified by assuming the variable set associated
with an instance sequence is disjoint from the set of variables that
occur in its roles.
\begin{defn}[Strand Space Nodes]
The set of \emph{nodes} of~$I$ is $\fn{nodes}(I)=\{(s,p)\mid s<|I|,
p<\fn{height}(I(s))\}$. The event at a given node is
$\fn{evt}(I,(s,p))=\fn{trace}(I(s))(p)$. A node is \emph{transmitting}
if its event is outbound, otherwise it is \emph{receiving}.
The message at a node is written $\fn{msg}(I,n)$.
\end{defn}
\begin{defn}[Strand Succession]
The \emph{strand succession relation}~$\Rightarrow$ is
$\{(s,p)\Rightarrow(s,p+1)\mid s<|I|, p<\fn{height}(I(s))-1\}$.
\end{defn}
\begin{defn}[Bundle]\label{def:bundle}
A \emph{protocol respecting bundle} $\bundle(I,\to)$ is a directed
acyclic graph, where the vertices are the nodes of~$I$, and an edge
represents communication~($\rightarrow$) or strand
succession~($\Rightarrow$). For communication, $n_0\rightarrow n_1$
only if there is a message~$t$ such that~$\fn{evt}(I,n_0)=\outbnd t$
and~$\fn{evt}(I,n_1)=\inbnd t$. For each reception node~$n_1$, there
is a unique transmission node~$n_0$ with $n_0\rightarrow n_1$.
Finally, each inherited uniquely originating atom originates on its
trace and on no other, and no event in a trace carries an inherited
non-originating atom.
\end{defn}
Notice that no non-base sorted variables may occur in the trace of an
instance in a bundle.
\begin{defn}[Causal Order]
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 \index{asymmetric
relation}\emph{asymmetric} iff $x\mathbin{R}y$ implies not
$y\mathbin{R}x$ for all distinct $x,y \in S$.
\end{defn}
\begin{defn}[Unique Origination]
An atom uniquely originates in a execution if it originates on exactly
one trace.
\end{defn}
\begin{defn}[Non-Originating]
An atom is non-originating in an execution if the atom originates in
no trace, but each of its variables occurs in some trace.
\end{defn}
\subsection*{Discussion}
Strand space papers use the word positive to describe an outbound
message or a transmitting node, and the word negative to describe an
inbound message or a receiving node. The adjectives used in this
paper were selected because they are mnemonic.
\section{Skeletons}\label{sec:skeletons}
Strands in executions represent both adversarial and non-adversarial
behaviors. A strand that represents adversarial behavior is called a
\index{penetrator strand}\emph{penetrator} strand. The roles
available to a penetrator are determined by the message signature.
For the Basic Crypto Signature in Figure~\ref{fig:bcs}, the traces of
the roles are in Figure~\ref{fig:pen}. Penetrator roles make no
origination assumptions.
\begin{figure}
$$\begin{array}{l}
\fn{base}(t)=\seq{\outbnd t},\mbox{ where $t$ is an atom}\\
\fn{tag}(t)=\seq{\outbnd t},\mbox{ where $t$ is a tag}\\
\fn{cat}(t_0,t_1)=\seq{\inbnd t_0,\inbnd t_1, \outbnd(t_0,
t_1)}\\
\fn{sep}(t_0,t_1)=\seq{\inbnd(t_0, t_1),\outbnd
t_0,\outbnd t_1}\\
\fn{enc}(t_0,t_1)=\seq{\inbnd t_0,\inbnd t_1,
\outbnd\enc{t_0}{t_1}}\\
\fn{dec}(t_0,t_1)=\seq{\inbnd\enc{t_0}{t_1},
\inbnd t_2,\outbnd t_0},\mbox{ where $t_2=\fn{inv}(t_1)$}
\end{array}$$
\caption{Penetrator Traces}\label{fig:pen}
\end{figure}
A non-adversarial strand is called \index{regular strand}
\emph{regular}. A typical protocol contains a small finite
set of roles used by regular strand. In addition, a regular strand
may be an instance of a listener role. For a given message~$t$, a
listener's trace is~$\seq{\inbnd t,\outbnd t}$. A listener strand is
used to assert that a message is not a secret and is available from
the penetrator.\index{listener strand}
The {\cpsa} program uses a skeleton to represent the regular behavior
that might make up part of an execution.
\begin{defn}[Preskeleton]
A \emph{preskeleton}~$k$ consists of instance sequence
$\fn{insts}(k)$, a transitive asymmetric node ordering~$\kprec{k}$, a
set of uniquely originating atoms $\fn{unique}(k)$, and a set of
non-originating atoms $\fn{non}(k)$. The following properties hold.
\begin{enumerate}
\item The relation~$\kprec{k}$ includes strand succession~($\Rightarrow$).
\item Each atom in $\fn{unique}(k)$ is carried in the trace of some
instance in $\fn{insts}(k)$.
\item Every inherited unique origination assumption is in
$\fn{unique}(k)$, each inherited atom originates on the
inheriting strand, and the origination position of the inherited
atom is the same as the origination position of the inherited atom
in the strand's trace.
\item Each atom in $\fn{non}(k)$ is not carried by an event in the
trace of some instance in $\fn{insts}(k)$, and each of
variable that occurs in the atom occurs in some trace.
\item Every inherited non-origination assumption is in $\fn{non}(k)$.
\end{enumerate}
\end{defn}
The set $\alg{K}(X)$ is the set of preskeletons~$k$ such that
$\fn{var}(\fn{insts}(k))\subseteq X$, written~$\alg{K}$ when the
variable set~$X$ is available from the context. To simplify notation,
let $\fn{ht}(k,s)=\fn{height}(\fn{inst}(k)(s))$.
In a {\cpsa} algebra, a preskeleton is a term of the
form~$\cn{k}(P,I,O,N,U)$ where
$$\begin{array}{r@{}c@{}l}
\fn{insts}(\cn{k}(P,I,O,N,U))&{}={}&I,\\
\fn{non}(\cn{k}(P,I,O,N,U))&{}={}&N,\\
\fn{unique}(\cn{k}(P,I,O,N,U))&{}={}&U.
\end{array}$$
The implementation of a preskeleton keeps track of its protocol as a
set of roles, $P$, but we ignore the protocol here as well as the fact
in a well formed preskeleton, the role of every instance is an element
of~$P$. The implementation of a preskeleton node ordering is not so
obvious. For preskeleton~$k$, only a subset of~$\kprec{k}$ is
explicit: $\cn{o}(n_0,n_1)\in O$ if $n_0\kprec{k}n_1$,~$n_0$ and~$n_1$
are on different strands,~$n_0$ is transmitting, and~$n_1$ is
receiving.
To ease the task of isomorphism testing (Section~\ref{sec:preskeleton
reduction}) and generalization by weakening
(Section~\ref{generalization}), the implementations normalizes a
preskeleton by performing the transitive reduction on~$O$. The
transitive reduction of a relation is the minimal relation such that
both have the same transitive closure.
\begin{defn}[Hulled Preskeleton]
A preskeleton~$k$ is a \emph{hulled preskeleton} if each atom in
$\fn{unique}(k)$ originates in at most one trace.
\end{defn}
Let $\orig(k,t)$ be the set of nodes at which~$t$ originates in~$k$,
and~$\gain(k,t)$ be the set of nodes at which~$t$ is gained
in~$k$.\index{gained}
\begin{defn}[Skeleton]
A preskeleton~$k$ is a \emph{skeleton} if each atom in
$\fn{unique}(k)$ originates in at most one trace, and the node of
origination precedes each node that gains the atom, i.e.\@ for
every~$t\in\fn{unique}(k)$, $n_0\in\orig(k,t)$ and $n_1\in\gain(k,t)$
implies~$n_0\kprec{k}n_1$.
\end{defn}
\begin{defn}[Preskeleton Homomorphism]\label{def:homomorphism}
\index{homomorphism!preskeleton}
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)$;
\item $\sigma$ is a $\Sigma$-homo\-morph\-ism;
\item $n\in\fn{nodes}(k_0)$ implies $\sigma(\fn{evt}(\fn{insts}(k_0),n))\equiv
\fn{evt}(\fn{insts}(k_1),\phi(n))$;
\item $n_0\kprec{k_0}n_1$ implies $\phi(n_0)\kprec{k_1}\phi(n_1)$;
\item $\sigma(\fn{non}(k_0)) \subseteq \fn{non}(k_1)$;
\item $\sigma(\fn{unique}(k_0)) \subseteq \fn{unique}(k_1)$;
\item\label{enu:orig} $t\in \fn{unique}(k_0)$ implies
$\phi(\orig(k_0,t))\subseteq\orig(k_1,\sigma(t))$.
\end{enumerate}
A homomorphism is \index{homomorphism!strandwise injective}\emph{strandwise
injective} if its strand map is injective. Two preskeletons are
isomorphic if they are related by strandwise injective homomorphism in
both directions.
\end{defn}
Condition~\ref{enu:orig} ensures that if $t\in unique(k_0)$ originates
at $(s,p)$ then when we apply $\sigma$ to the strand $s$, $\sigma(t)$
neither originates nor is gained at $(\phi(s),j)$ for $j<p$
($\sigma(t)$ can never originate or be gained later). In other words,
$\sigma$ alone will either satisfy or violate the last clause.
\begin{defn}[Homomorphism Composition]\label{def:composition}
Let $k_0\homomorphism{\psi_0}k_1\homomorphism{\psi_1}k_2$ where
$\psi_0 = (\phi_0,\sigma_0)$ and $\psi_1=(\phi_1,\sigma_1).$ Then the
composition of $\psi_0$ and $\psi_1$ is defined as
$\psi_1\circ\psi_0 = (\phi_1\circ\phi_0,\sigma_1\circ\sigma_0)$
where $k_0\homomorphism{\psi_1\circ\psi_0}k_2$.
\end{defn}
Since homomorphisms may arbitrarily add some structure such as adding terms
to $unique$ and $non$, it is possible to have
$k_0\homomorphism{\phi,\sigma}k_1$ and $k_0\homomorphism{\phi,\sigma}k_2$
with $k_1\ne k_2$.
For example $k_1$ and $k_2$ could be identical except that $non(k_1)\subsetneq
non(k_2)$. We would like to be able to talk about the image of $k_0$
under $(\phi,\sigma)$.
\begin{defn}[Image of Homomorphism]\label{def:image}
Preskeleton $k_1$ is the \emph{image of $k_0$ under $\psi=(\phi,\sigma)$}
written $\psi(k_0)=k_1$ iff
\begin{enumerate}
\item $k_0\homomorphism{\phi,\sigma}k_1$
\item $\kprec{k_1}=\phi(\kprec{k_0})^*$
\item $\fn{unique}(k_1)=\sigma(\fn{unique}(k_0))$
\item $\fn{non}(k_1)=\sigma(\fn{non}(k_0))$
\item $\fn{ht}(k_1,\phi(s))=\max \{\fn{ht}(k_0, s')\mid \phi(s')=\phi(s)\}$
for $s<|\fn{inst}(k_0)|$
\item $\phi$ is surjective
\end{enumerate}
\end{defn}
This definition guarantees that the image does not contain extra strands or
nodes, and that it only contains ordering relations and origination assumptions
necessary for $\psi$ to be a homomorphism. Whenever there is a skeleton $k_1$
such that $k_0\homomorphism{\psi}k_1$, then $\psi(k_0)$ is well-defined, and
we can view $\psi(k_0)$ as being included into $k_1$. That is,
$k_0\homomorphism{\psi}\psi(k_0)\homomorphism{\idphi,\idsigma}k_1$.
Given $(\idphi,\sigma)$, it is still possible for $(\idphi,\sigma)(k_0)$ not
to exist because $\sigma$ may violate the last clause of
Definition~\ref{def:homomorphism}. However, if there is some $\phi$
for which $(\phi,\sigma)(k_0)$ is well-defined, then $(\idphi,\sigma)(k_0)$
is also well-defined.
\begin{lem}\label{lem:decompose}
If $k_0\homomorphism{\phi,\sigma}k_1$, then there is a preskeleton $k$ such
that $k_0\homomorphism{\phi_{id},\sigma}k\homomorphism{\phi,\sigma_{id}}k_1$.
\end{lem}
\begin{proof}
Let $k=(\idphi,\sigma)(k_0)$. Then the
homomorphism $k\homomorphism{\phi,\sigma_{id}}k_1$ is well-defined which the
reader can easily check by verifying each of the seven clauses of
Definition~\ref{def:homomorphism}.
\end{proof}
\begin{cor}\label{cor:commute}
If $k_0\homomorphism{\phi,\sigma_{id}}k_1\homomorphism{\phi_{id},\sigma}k_2,$
then there is a preskeleton $k$ such that
$k_0\homomorphism{\phi_{id},\sigma}k\homomorphism{\phi,\sigma_{id}}k_2$.
\end{cor}
\begin{proof}
We can compose the two homomorphisms to see that
$k_0\homomorphism{\phi,\sigma}k_2$. We then apply the previous lemma to find $k$.
\end{proof}
\begin{note}
The following definition is frivolous as it is not used anywhere.
We're just trying out definitions to explore links to category theory.
\end{note}
\begin{defn}[{\cpsa} Category]\label{def:cpsa category}
\index{CPSA@{\cpsa} category}
Let $\alg{C}(X)$ be a {\cpsa} algebra
generated by~$X$ (see Definition~\ref{def:cpsa algebra}), and
$\alg{K}(X)$ be a free
algebra defined by the carrier set for sort \dom{preskel}
in~$\alg{C}(X)$. In a {\cpsa} category
\begin{enumerate}
\item $\alg{K}(X)$ is an object, for each variable set~$X$,
\item the set of arrows is $(\nat\to\nat)\times
(\alg{A}_\top(X)\to\alg{A}_\top(Y))$, where the second component is a
homomorphism of the message algebra,
\item Definition~\ref{def:homomorphism} defines the domain and the
codomain of each arrow,
\item component function composition defines arrow composition, and
\item component identity functions define the arrow identity.
\end{enumerate}
\end{defn}
\begin{defn}[Pruned Skeleton]
A skeleton~$k$ has a set of \emph{redundant strands}~$S$ if there is a
substitution~$\sigma$ that is a variable renaming, a strand
mapping~$\phi$ such that $s\in S$ implies there is some $s'\notin S$
such that $\phi(s)=\phi(s')$ and the height of~$s$ is no greater than
the height of~$s'$, a skeleton~$k'$ such that
$k\homomorphism{\phi,\sigma}k'$ where $k'=(\phi,\sigma)(k)$, and a
homomorphism $k'\homomorphism{\phi',\sigma'}k$ such that
$\sigma\circ\sigma'=\idsigma$ and $\phi\circ\phi'=\idphi$. A
skeleton~$k$ is \emph{pruned} if it contains no redundant strands.
\end{defn}
\begin{note}
Suggestion from Carolyn Talcott: Define pruned skeleton as the result
of deleting redundant set of strands. Then prove that we can use
homomorphisms with the right properties to perform this `deletion'.
\end{note}
The concept of an execution skeleton is introduced to relate a skeleton
that contains only regular strands with its executions. An execution
skeleton may include penetrator strands.
\begin{defn}[Used]\label{def:used}
Message~$t_0$ is \emph{used in}~$t_1$
if~$t_0$ or $\fn{inv}(t_0)$ is accessible in $t_1$ and~$t_0$ is not
carried by~$t_1$.
\end{defn}
The accessibility of a term is defined in
Definition~\ref{def:accessible}.
\begin{defn}[Execution Skeleton]\label{def:execution skeleton}
The \emph{execution skeleton}~$k$ of bundle~{\bundle}
over instances~$I$ has the following properties.
\begin{enumerate}
\item $\fn{insts}(k)=I$.
\item $\kprec{k} = \prec$.
\item $\fn{unique}(k)$ is the set of atoms that originate uniquely
in~{\bundle}.
\item $\fn{non}(k)$ is the set of atoms used in the traces of~$I$.
\end{enumerate}
\end{defn}
\begin{defn}[Skeleton Compatible Executions]
A bundle~{\bundle} is \emph{compatible} with skeleton~$k$ if
there is a homomorphism from~$k$ to the execution skeleton
of~{\bundle}.
\end{defn}
\begin{defn}[Realized Skeleton]
A bundle~{\bundle} \emph{realizes} skeleton~$k$ if~$\bundle$ is
compatible with~$k$, and the structure preserving map $(\phi,\sigma)$
has the property that~$\sigma$ is a bijection,~$\phi$ is a
bijection between the strands in~$k$ and the regular strands in the
bundle's execution skeleton, and~$\phi$ preserves the height of the
strands it maps.
\end{defn}
A bundle models a realized skeleton if it realizes it. A
bundle~{\bundle} models a preskeleton~$k_0$ if there is a realized
skeleton~$k_1$ such that $k_0\homomorphism{\phi,\sigma} k_1$
and~{\bundle} models~$k_1$.
\subsection*{Discussion}
In the refinement of strand space theory, there is no global strand
space on which all analysis is based. Instead, each skeleton and
execution defines its own strand space, and homomorphisms establish
relations between them. The definition of a protocol depends on no
strand space.
The definitions in this section are the obvious refinements that
result from using finite ordered strand spaces. In the {\cpsa}
program, pruned skeletons are used for skeletons in the implementation
of the {\cpsa} algorithm in~\cite{DoghmiGuttmanThayer07}.
In~\cite{DoghmiGuttmanThayer07}, skeletons were not required to
respect origination, but that was just an oversight.
\section{Reductions on Preskeletons}\label{sec:preskeleton reduction}
This section describes the algorithm used to transform a preskeleton
into a skeleton as a setwise term reduction system
$(\alg{K},\twoheadrightarrow)$. Recall that the relation
$k\rightsquigarrow K$ in Section~\ref{sec:algorithms} is defined in
terms of $\to\subseteq\alg{K}\times\alg{K}$ by specifying
$\{k\}\twoheadrightarrow K$ using~$\to$.
If a preskeleton $k$ is not a skeleton, then it is either because
some $t\in unique(k)$ actually originates at more than one node,
or because for some $t\in unique(k)$, there is a node $n_1\in\gain(k,t)$,
and a node $n_0\in\orig(k,t)$ such that $n_0\nprec_k n_1$.
These obstructions are resolved via identifying strands and
enriching node orderings respectively. We show that we can always
resolve the first obstruction before resolving the second obstruction.
Moreover, if the first obstruction is resolvable, then there is a
canonical resolution (although there may be non-canonical choices
to reach it). We call this canonical resolution a pre-hull. Then
if the second obstruction is also resolvable, it also has a canonical
resolution. This canonical resolution is a skeleton which we call
a hull. We begin by giving the definitions of pre-hull and of hull.
\begin{defn}
Given a preskeleton $k$, a \emph{pre-hull} of $k$ is a hulled preskeleton
$k_0$ together with a homomorphism $k\homomorphism{\psi_0}k_0$ such that
for any homomorphism $k\homomorphism{\psi_1}k_1$ to a hulled preskeleton,
there is a unique homomorphism $k_0\homomorphism{\psi}k_1$ such that
$\psi_1=\psi\circ\psi_0$
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{defn}
A preskeleton $k$ may not have a pre-hull, but if it does, then the definition
implies that it is unique up to isomorphism. Also, every hulled preskeleton
is its own pre-hull where $\psi_0$ is the identity homomorphism.
\begin{defn}
Given a preskeleton $k$, a \emph{hull} of $k$ is a skeleton
$k_0$ together with a homomorphism $k\homomorphism{\psi_0}k_0$ such that
for any homomorphism $k\homomorphism{\psi_1}k_1$ to a skeleton,
there is a unique homomorphism $k_0\homomorphism{\psi}k_1$ such that
$\psi_1=\psi\circ\psi_0$
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{defn}
Just like pre-hulls, a preskeleton may not have a hull, but if it does, then
it is unique up to isomorphism. Also, every skeleton is its own hull
where $\psi_0$ is the identity homomorphism.
We next show how to take advantage of unification in the
$\Sigma$-algebra to provide a sort of unification of strands. Before unifying
two strands, we will unify their traces.
\begin{defn}[Trace Unification]\label{def:trace-unification}
Let $k$ be a preskeleton which contains strands~$s$ and~$s'$. We
say that substitution $\sigma$ \emph{unifies the messages of~$s$
and~$s'$} iff $\sigma(evt(k,(s,p))) \equiv \sigma(evt(k,(s',p)))$
for every $p < height(s)$. We say that homomorphism
$k\homomorphism{\phi,\sigma}k_0$ \emph{unifies the traces of~$s$
and~$s'$} iff $\sigma$ unifies the messages of~$s$ and~$s'$.
We say that the traces of $s$ and $s'$ are
\emph{unifiable} if there is a $(\phi,\sigma)$ which unifies them.
\end{defn}
Thus, if $(\phi,\sigma)$ unifies the traces of~$s$ and~$s'$,
not only does $\sigma$ unify the messages
but also $t\in \fn{unique}(k_0)$ implies
$\phi(\orig(k_0,t))\subseteq\orig(k_1,\sigma(t))$ by Clause 7 in the
definition of a homomorphism (Definition~\ref{def:homomorphism}).
In fact, as we already saw, it is generally possible for $\sigma$
to unify the messages, without respecting Clause 7. In this case,
$\sigma$ unifies the messages of~$s$ and~$s'$, but the traces
of~$s$ and~$s'$ are not unifiable. By pairing
$\sigma$ with $\phi$, trace unification only allows homomorphisms
with substitutions $\sigma$ which do not violate Clause 7.
By recalling the discussion which follows Definition~\ref{def:image},
we can see that if $(\phi,\sigma)$ unifies the traces of~$s$ and~$s'$,
then so does $(\idphi,\sigma)$. Furthermore, if $(\idphi,\sigma)$ unifies
the traces of~$s$ and~$s'$, then so does $(\idphi,\sigma')$ where
$\sigma'$ unifies the messages of~$s$ and~$s'$, and
$\sigma'\unlhd\sigma$. We can view this another way. Let $\sigma$
be the most general unifier of the messages of~$s$ and~$s'$. If $(\idphi,\sigma)$
does not unify the traces, then the traces are not unifiable.
\begin{defn}[Substitution Reduction]
Preskeleton~$k_0$ reduces to preskeleton~$k_1$ by the
substitution~$\sigma$, written~$k_0\reduction{\ops{S}_\sigma}k_1$, iff
$k_1=\psi(k_0)$ where $\psi=(\idphi,\sigma)$.
\end{defn}
The next lemma states that if $k$ is a skeleton in which the traces of
two strands~$s$ and~$s'$ are unifiable, then there is a kind of most
general trace unifier. Since this most general trace unifier will
turn out to always have the form $(\idphi,\sigma)$, we can use the
corresponding $\ops{S}_{\sigma}$ as a way of implementing this trace
unification.
\begin{lem}\label{lem:substitution}
Let $k$ be a preskeleton which contains strands $s$ and $s'$. Suppose the
traces of $s$ and $s'$ are unifiable. Then there is a preskeleton $k_0$ and
a homomorphism $k\homomorphism{\psi_0}k_0$ which unifies the traces
of $s$ and $s'$ such that for every
homomorphism $k\homomorphism{\psi_1}k_1$ which
unifies the traces of $s$ and $s'$, there is a unique homomorphism
$k_0\homomorphism{\psi}k_1$ so that $\psi_1=\psi\circ\psi_0$.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{lem}
\begin{proof}
Since the traces of $s$ and $s'$ are unifiable by some $(\hat{\phi},\hat{\sigma})$,
we know that $(\idphi,\hat{\sigma})$ also unifies the traces. Furthermore,
there is a most general unifier $\sigma_0$ which unifies the messages
of~$s$ and~$s'$. Since
$\sigma_0\unlhd\hat{\sigma}$ we know that $(\idphi,\sigma_0)$ also unifies
the traces. Let $\psi_0=(\idphi,\sigma_0)$ and let $k_0=\psi_0(k).$
We show that this is the preskeleton and homomorphism we want.
The homomorphism $\psi_0$ unifies the traces of $s$ and $s'$ by construction.
Now let $k\homomorphism{\psi_1}k_1$ with $\psi_1=(\phi_1,\sigma_1)$,
be a homomorphism which unifies the traces of~$s$ and~$s'$. Since
$\sigma_0$ is the most general unifier of the messages of~$s$ and~$s'$,
there is a unique
$\sigma$ such that $\sigma_1=\sigma\circ\sigma_0$. Then by letting
$\psi=(\phi_1,\sigma)$ we see that $\psi\circ\psi_0 = (\phi_1,\sigma)
\circ (\phi_{id},\sigma_0) = (\phi_1,\sigma\circ\sigma_0) =
(\phi_1,\sigma_1) = \psi_1$. It is clear that $\phi_1$ is the unique
node map that will work, and we already noted that $\sigma$ must also
be unique.
\end{proof}
We can find the $k_0$ of Lemma~\ref{lem:substitution} (when it exists)
by finding the most general $\sigma_0$ which
simultaneously unifies the corresponding messages in the traces of~$s$
and~$s'$ and applying the reduction $\ops{S}_{\sigma_0}$ to $k$. This
reduction will fail if the traces of~$s$ and~$s'$ are not unifiable, and
it will succeed otherwise. Furthermore, Lemma~\ref{lem:substitution}
guarantees that there is at most a single $k_0$ such that
$k\reduction{\ops{S}_{\sigma_0}}k_0$ where $\sigma_0$ is the most general
unifier of the messages of strands~$s$ and~$s'$.
\begin{defn}[Strand Unification]\label{def:strand-unification}
Let $k$ be a preskeleton with strands $s$ and $s'$.
We say that a homomorphism $\psi=(\phi,\sigma)$ \emph{unifies
the strands} $s$ and $s'$ iff $\phi(s)=\phi(s')$.
We say the strands $s$ and $s'$ are \emph{unifiable}
if there is a homomorphism which unifies them.
\end{defn}
Note that if $\psi$ unifies two strands, then $\psi$ unifies their traces,
but the converse is not true in general. Thus, unification of two strands
can be broken into two steps. First we unify their traces, then we unify
the strands in a very simple way. We already saw that the first step can
be performed in a most general way, as codified by Lemma~\ref{lem:substitution}.
We now want to provide a similar notion for the second step.
Suppose the trace of strand~$s$ is a prefix of the trace of
strand~$s'$ in preskeleton~$k_0$. In other words, $(\idphi,\idsigma)$
unifies the traces of~$s$ and~$s'$. This would be the case, for example,
if $k_0$ was the result of unifying the traces of~$s$ and~$s'$ in some
other preskeleton.
In that case, there is a
$\psi$ which unifies the strands~$s$ and~$s'$, namely
$\psi=(\phi_{s,s'},\idsigma)$ where
$$\begin{array}{r@{}c@{}l}
\phi_{s,s'}(j)&{}={}&\left\{
\begin{array}{ll}
\phi_s(s')&\mbox{if $j=s$}\\
\phi_s(j)&\mbox{otherwise}
\end{array}\right.\\
\phi_s(j)&{}={}&\left\{
\begin{array}{ll}
j-1&\mbox{if $j>s$}\\
j&\mbox{otherwise.}
\end{array}\right.
\end{array}
$$
\begin{defn}[Compression Reduction]
Preskeleton~$k_0$ reduces to preskeleton~$k_1$ by compressing the
strand~$s$ into~$s'$, written $k_0\reduction{\ops{C}_{s,s'}}k_1$,
iff $\psi(k_0)=k_1$, with $\psi=(\phi_{s,s'},\idsigma)$.
\end{defn}
The compression reduction $\ops{C}_{s,s'}$ can only be performed on
$k_0$ if $(\idphi,\idsigma)$ unifies the traces of~$s$ and~$s'$, because
otherwise $(\phi_{s,s'},\idsigma)(k_0)$ is not well-defined. We generally
use this reduction when unifying strands after having unified their
traces. This reduction is used to implement a kind of most general
unification of two strands once their traces have been unified.
\begin{lem}\label{lem:compression}
Let $k$ be a preskeleton in which $(\idphi,\idsigma)$ unifies the traces
of two strands $s$ and $s'$, and suppose
the strands~$s$ and~$s'$ are unifiable. Then
there is a preskeleton $k_0$ and a homomorphism $k\homomorphism{\psi_0}k_0$
which unifies the strands $s$ and $s'$ such that for every
homomorphism $k\homomorphism{\psi_0}k_0$ which unifies the
strands $s$ and $s'$, there is a unique homomorphism
$k_0\homomorphism{\psi}k_1$ so that $\psi_1=\psi\circ\psi_0$.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{lem}
\begin{proof}
Let $\psi_0=(\phi_{s,s'},\sigma_{id})$, and $\psi_0(k)=k_0$. We will
show that this is the preskeleton and homomorphism we want.
By the definition of $\phi_{s,s'}$ we see that $\psi_0$ unifies the
strands $s$ and $s'$. Let $k\homomorphism{\psi_1}k_1$ with
$\psi_1=(\phi_1,\sigma_1)$ be any homomorphism
which unifies the strands $s$ and $s'$. We
let $\psi=(\phi,\sigma_1)$ where $\phi$ is a node map we still need to define.
Since $\phi_{s,s'}$ maps onto the strands of $k_0$, $\phi$ is completely
determined by where it sends $\phi_{s,s'}(j)$. But in order for
$\psi_1=\psi\circ\psi_0$ we are forced to define
$\phi(\phi_{s,s'}(j))=\phi_1(j)$. We can do this because $\phi_{s,s'}$
does not identify any strands except for $s$ and $s'$, and because $\phi_1$
also identifies $s$ and $s'$. Using this $\phi$, it is clear that
$\psi_1=\psi\circ\psi_0$. To see that $\psi$ is unique, we note that we
had no choice for either the substitution $\sigma_1$ or the node map
$\phi$.
\end{proof}
We can find the $k_0$ of Lemma~\ref{lem:compression} (when it exists)
by applying $\ops{C}_{s,s'}$ to $k$. This reduction will fail if
the strands~$s$ and~$s'$ are not unifiable or if the trace of~$s$ is
not a prefix of the trace of~$s'$, and it will succeed otherwise.
Moreover, Lemma~\ref{lem:compression} guarantees that there is at most
a single $k_0$ such that $k\reduction{\ops{C}_{s,s'}}k_0$.
The substitution and compression reductions are used to unify two
strands in two separate steps. When two strands are unifiable, then
their traces are also unifiable. We may thus use Lemma~\ref{lem:substitution}
to unify their traces in a most general way. This will cause the trace
of one of the strands to be a prefix of the other, thereby enabling
compression. The resulting preskeleton is the most general one which
unifies the two strands, as we show in the following lemma.
\begin{lem}\label{lem:hulling}
Let $k$ be a preskeleton containing strands $s$ and $s'$
which are unifiable.
Then there is a preskeleton $k_0$ and a homomorphism
$k\homomorphism{\psi_0}k_0$ which unifies $s$ and $s'$ such that
for every homomorphism $k\homomorphism{\psi_1}k_1$ which unifies
$s$ and $s'$, there is a unique homomorphism
$k_0\homomorphism{\psi}k_1$ so that $\psi_1=\psi\circ\psi_0$.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{lem}
\begin{proof}
Since the strands $s$ and $s'$ are unifiable, their traces are also
unifiable. Thus, by Lemma~\ref{lem:substitution}, we can find a
preskeleton $k_0'$ and a homomorphism $k\homomorphism{\psi_0'}k_0'$
so that any homomorphism from $k$ which unifies the traces of $s$ and $s'$
factors through $\psi_0'$. The preskeleton $k_0'$ now satisfies
the hypotheses of Lemma~\ref{lem:compression}, so we can find a
preskeleton $k_0''$ and a homomorphism
$k_0'\homomorphism{\psi_0''}k_0''$ so that any homomorphism from
$k_0'$ which unifies $s$ and $s'$ factors through $\psi_0''$.
Let $\psi_0=\psi_0''\circ\psi_0'=(\phi_{s,s'},\sigma)$ where
$\sigma$ is the mgu of the traces of $s$ and $s'$, and let $k_0=k_0''$.
It remains to show that this $\psi_0$ and $k_0$ have the desired
properties.
First, it is clear that $\psi_0$ unifies $s$ and $s'$. Now let
$k\homomorphism{\psi_1}k_1$ be an arbitrary homomorphism which unifies
$s$ and $s'$. By Lemma~\ref{lem:substitution}, $\psi_1$ factors uniquely
through $\psi_0'$ as $\psi'\circ\psi_0'$. Moreover, $\psi'$ is a
homomorphism from $k_0'$ which unifies $s$ and $s'$, thus by
Lemma~\ref{lem:compression}, $\psi'$ factors uniquely through
$\psi_0''$ as $\psi'=\psi''\circ\psi_0''$. Thus $\psi_1$ factors
uniquely through $\psi_0=\psi_0''\circ\psi_0'$ as desired.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0'} \ar@{|->}[rrdd]_{\psi_1} &
k_0' \ar@{|->}[rdd]^{\psi'} \ar@{|->}[r]^{\psi_0''} &
k_0 \ar@{|->}[dd]^{\psi}\\
& &\\
& &k_1}$$
\end{proof}
We thus now have a canonical way of unifying two strands when they
are unifiable.
\begin{lem}\label{lem:unify-commute}
Let $k$ be a preskeleton containing strands $s_0,s_0',s_1,s_1'$
(not necessarily all distinct) such that the pairs of strands
$(s_0,s_0')$ and $(s_1,s_1')$ are simultaneously unifiable. Let
$k_0$ be the result of first unifying $s_0$~and~$s_0'$ and then
$s_1$~and~$s_1'$ according to Lemma~\ref{lem:hulling}. Let
$k_1$ be the result of first unifying $s_1$~and~$s_1'$ and then
$s_0$~and~$s_0'$ also according to Lemma~\ref{lem:hulling}.
Then $k_0$ and $k_1$ are isomorphic.
\end{lem}
\begin{proof}
We can repeatedly apply Lemma~\ref{lem:hulling} to obtain the
following diagram.
$$
\xymatrix@C=3em{
& k\ar@{|->}[ld]_{\psi_0'}
\ar@{|->}[rd]^{\psi_1'} &\\
k_0'\ar@{|->}[d]_{\psi_0} %\ar@{|->}[rrd]
& &
k_1'\ar@{|->}[d]^{\psi_1} %\ar@{|->}[lld]
\\
k_0\ar@{|->}[rr]^{\psi_2} & & k_1\ar@{|->}[ll]^{\psi_2'}
}$$
The preskeleton $k_0'$ is the result of unifying strands $s_0$~and~$s_0'$
of $k$ in a most general way, and $k_0$ is the result of unifying
strands $\psi_0'(s_1)$~and~$\psi_0'(s_1')$ of $k_0'$ in a most general
way. Similarly, $k_1'$ is the result of unifying strands $s_1$~and~$s_1'$
of $k$ in a most general way, and $k_1$ is the result of unifying
strands $\psi_1'(s_0)$~and~$\psi_1'(s_0')$ of $k_1'$ in a most general way.
We can infer the homomorphism $k_0\homomorphism{\psi_2}k_1$ and
$k_1\homomorphism{\psi_2'}k_0$ from Lemma~\ref{lem:hulling}
as the unique homomorphisms which make the diagram commute. By the
uniqueness of these arrows we can infer that $\psi_2\circ\psi_2'=id_{k_1}$
and that $\psi_2'\circ\psi_2=id_{k_0}$. Thus $\psi_2$~and~$\psi_2'$ are
isomorphisms and they are inverses of each other. Thus $k_0$ and $k_1$
are isomorphic.
\end{proof}
Lemma~\ref{lem:unify-commute} implies that if we want to simultaneously
unify several sets of strands which are simultaneously unifiable,
any order of pairwise strand unification
will result in a skeleton which is isomorphic to the result of every
other order. However, given a preskeleton $k$ which is not a hulled
preskeleton, we do not want to unify \emph{every} pair of strands
which are unifiable. We only want to unify those pairs of strands
which demonstrate that for some $t\in unique(k)$, $\orig(k,t)$ has
more than one node. For this purpose we use another reduction
which is built out of~$\ops{S}_{\sigma}$ and~$\ops{C}_{s,s'}$.
Recall that the relation $k\rightsquigarrow K$ in
Section~\ref{sec:algorithms} is defined in terms of
$\to\subseteq\alg{K}\times\alg{K}$ by specifying
$\{k\}\twoheadrightarrow K$ using~$\to$.
\begin{defn}[Hulling Reduction]\label{def:hulling}
Preskeleton $k_0$ reduces to preskeleton $k_1$ by hulling strands~$s$
and~$s'$, written $k_0\reduction{\ops{H}_{s,s'}}k_1$, iff there is
some $t\in unique(k_0)$ and there are distinct strands~$s$ and~$s'$
such that $\{(s,p),(s',p')\}\subseteq\orig(k_0,t)$, and the
strands~$s$ and~$s'$ are unifiable, and $k_1$ is the preskeleton
guaranteed by Lemma~\ref{lem:hulling}. For the setwise hulling
relation, $\{k_0\}\setreduction{\ops{H}_{s,s'}}\{k_1\mid
k_0\reduction{\ops{H}_{s,s'}}k_1\}$, when $k_0$ has a message in
$\fn{unique}(k_0)$ that originates on both~$s$ and~$s'$.
\end{defn}
This hulling reduction $\ops{H}_{s,s'}$ implements the
``most general strand unifier" $\psi_0$ from Lemma~\ref{lem:hulling}
when it exists, but it is only applicable when
$s$~and~$s'$ originate the same $t\in unique(k)$.
By the proof of Lemma~\ref{lem:hulling},
$k_0\reduction{\ops{H}_{s,s'}}k_1$, iff there is a (unique) preskeleton $k$ such
that $k_0\reduction{\ops{S}_{\sigma}}k\reduction{\ops{C}_{s,s'}}k_1$,
where $\sigma$ is the most general unifier of the messages of~$s$
and~$s'$.
Given a preskeleton $k$ which is not a hulled preskeleton,
it is possible that simultaneously unifying
all pairs of strands $s$~and~$s'$ which both originate some
$t\in unique(k)$ will not produce a hulled preskeleton. The unification
process may introduce more points of origination of terms which are
meant to be uniquely originating. However, the next lemma shows that
repeatedly resolving these obstructions will yield a pre-hull.
\begin{lem}\label{lem:prehull-exist}
Suppose that there is a homomorphism from $k$ into a hulled
preskeleton. Then $k$ has a pre-hull.
\end{lem}
\begin{proof}
If $k$ is not a hulled preskeleton, then it has (possibly several)
pairs of strands $s$~and~$s'$ which each originate the same term
$t\in unique(k)$. All of these pairs are simultaneously unifiable
since the homomorphism from $k$ into a hulled preskeleton which is
assumed to exist performs that unification. Therefore by
Lemmas~\ref{lem:hulling} and~\ref{lem:unify-commute}, we may
unify these pairs $s$~and~$s'$ in any order in a most general way
to find a homomorphism $k\homomorphism{\psi_0}k_0$ which simultaneously
unifies all the pairs $s$~and~$s'$, such that for any homomorphism
$k\homomorphism{\psi_1}k_1$ which unifies these pairs there is a unique
$k_0\homomorphism{\psi}k_1$ such that $\psi_1=\psi\circ\psi_0$.
By the properties of $\psi_0$ and $k_0$, if $k_0$ is a hulled
preskeleton it is the pre-hull of $k$. If not, then $k_0$
again satisfies the hypothesis of this lemma, so we can repeat the
process of the above paragraph. Since each iteration reduces the
number of strands, this process will eventually terminate. By
the properties of the resulting preskeleton at each step, it will
terminate with the pre-hull.
\end{proof}
\begin{lem}\label{lem:prehull-compute}
If a preskeleton $k$ has a pre-hull, then repeated applications
of $\ops{H}_{s,s'}$ will terminate in the pre-hull of $k$.
\end{lem}
\begin{proof}
For every pair of strands $s$~and~$s'$ which are eventually unified
in the pre-hull, there is a sequence of hulling reductions which
causes $s$~and~$s'$ to originate the same term which should
be uniquely originating. Furthermore, by Lemma~\ref{lem:unify-commute}
this obstruction is introduced by the end of every reordering of such
a sequence, although it may be introduced earlier. Thus, we may apply
the hulling reductions in any order, and we will eventually unify the
same sets of strands. Again by Lemma~\ref{lem:unify-commute},
the preskeletons resulting from each order of hulling reductions will
all be isomorphic. Since Lemma~\ref{lem:prehull-exist} shows that
at least one such order results in the pre-hull, every order will
result in the pre-hull.
\end{proof}
\begin{defn}[Order Enrichment]
Suppose hulled preskeleton~$k_0$ is not a skeleton. Hulled
preskeleton~$k_0$ reduces to skeleton~$k_1$ by order enrichment, written
$k_0\reduction{\ops{O}}k_1$, iff~$k_1$ is the result of adding node
orderings implied by origination. That is,
\begin{enumerate}
\item $\kprec{k_1}= (\kprec{k_0}\cup\{n_0,n_1\mid n_0\in\orig(k_0,t)\land
n_1\in\gain(k_0,t)\})^\ast$,
\item $\fn{ht}(k_1,s)=
\fn{ht}(k_0,s)$ for $s<|\fn{inst}(k_0)|$,
\item $\fn{unique}(k_1)=\fn{unique}(k_0)$, and
\item $\fn{non}(k_1)=\fn{non}(k_0)$.
\end{enumerate}
There is a homomorphism from~$k_0$ to~$k_1$ that is an embedding. For
the setwise order enrichment reduction,
$\{k_0\}\setreduction{\ops{O}}\{k_1\mid k_0\reduction{\ops{O}}k_1\}$
when $k_0$ is a hulled preskeleton that is not a skeleton.
\end{defn}
\begin{lem}\label{lem:order-enrichment}
Suppose $k$ is a preskeleton such that every $t$ in $unique(k)$ originates
in $k$ at most once. Suppose also that there is a homomorphism from
$k$ to a skeleton. Then there is a skeleton $k_0$ and a homomorphism
$k\homomorphism{\psi_0}k_0$ such that for every homomorphism
$k\homomorphism{\psi_1}k_1$ to a skeleton $k_1$, there is a unique
homomorphism $k_0\homomorphism{\psi}k_1$ so that $\psi_1=\psi\circ\psi_0$.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{lem}
\begin{proof}
Let $k_0$ be obtained from $k$ by adding edges to the node
ordering relation. That is, $n_0\kprec{k_0}n_1$ is the transitive
closure of pairs such that
either $n_0\kprec{k}n_1$ or for some $t\in unique(k)$, $t$ originates
at $n_0$ and $n_1\in\gain(k,t)$. Let $\psi_0$ be the obvious
embedding of $k$ into $k_0$. We must show that $k_0$ is
a skeleton. It will be sufficient to check that we did not introduce
any cycles into the node ordering. But, in fact, if $\kprec{k_0}$
had a cycle, then so would the
First, we chose $k_0$ to be a skeleton. Now let $k\homomorphism{\psi_1}k_1$
be an arbitrary homomorphism to a skeleton $k_1$. Then we can also
apply $\psi_1$ to $k_0$, but we must be careful to check that it remains
a homomorphism. Only clause 4 of Definition~\ref{def:homomorphism} could
potentially fail. However, assume
\end{proof}
\begin{note}
Our current understanding of pruning is this. We have an example that
shows that pruning one strand at a time does not remove all redundant
strands. We are searching for efficient ways to perform multiple
strand pruning in one step, but haven't found one yet.
We also do not know if single strand pruning is confluent.
\end{note}
\begin{defn}[Pruning]\label{def:pruning}
Suppose skeleton~$k_0$ has a redundant strand~$s$. Then there exists
a distinct strand~$s'$ that describes more specific behavior.
Skeleton~$k_0$ reduces to skeleton~$k_1$ by pruning, written
$k_0\reduction{\ops{P}_s}k_1$, iff there is a substitution~$\sigma$
such that $\sigma(\fn{evt}(k_0,(s,p)))\equiv \fn{evt}(k_0,(s',p))$ for
all $p<h$, where~$h$ is the height of strand~$s$ in~$k_0$, no variable
in $\fn{Dom}(\sigma)$ occurs in the trace of any strand other
than~$s$, $t\in\fn{unique}(k_0)$ implies
$\sigma(t)\in\fn{unique}(k_0)$, $t\in\fn{non}(k_0)$ implies
$\sigma(t)\in\fn{non}(k_0)$, there is a~$k$ such that
$k_0\reduction{\ops{S}_\sigma}k\reduction{\ops{C}_{s,s'}}k_1$, and if
$(s,p)\kprec{k_0}(s'',p'')$ then $(s',p')\kprec{k_0}(s'',p'')$, and if
$(s'',p'')\kprec{k_0}(s,p)$ then $(s'',p'')\kprec{k_0}(s',p')$. For
the setwise pruning reduction,
$\{k_0\}\setreduction{\ops{P}_s}\{k_1\mid
k_0\reduction{\ops{P}_s}k_1\}$, when there is a $k_1$ such that
$k_0\reduction{\ops{P}_s}k_1$.
\end{defn}
\begin{lem}[Pruning]\label{lem:pruning}
Let~$k$ be a skeleton with redundant strand~$s$. For every pruned
skeleton~$k_1$ such that $k\homomorphism{\psi_1}k_1$, there is a
skeleton~$k_0$ and homomorphisms~$\psi_0$ and~$\psi$ with
$k\reduction{\ops{P}_s}k_0$, $k\homomorphism{\psi_0}k_0$,
$\psi_1=\psi\circ\psi_0$, and $\psi_0=(\phi_{s,s'},\sigma)$, where
strand~$s'$ and substitution~$\sigma$ are as specified in
Definition~\ref{def:pruning}.
\end{lem}
\begin{proof}
Pruning operations commute. Suppose~$k$ has two redundant
strands,~$s$ and~$s'$. If~$s$ describes more specific behavior and
is used to justify pruning~$s'$, then the strand that justifies the
pruning of~$s$ can serve the same purpose.
\begin{note}
The proof is not complete. Something more needs to be added here.
\end{note}
\end{proof}
Notice that a setwise hulling reduction may produce the empty set, but
a setwise order enrichment and pruning reduction never does.
Let reduction $\twoheadrightarrow=
\bigcup_{s,s'}\setreduction{\ops{H}_{s,s'}}\cup\setreduction{\ops{O}}\cup
\bigcup_s\setreduction{\ops{P}_s}$.
\begin{thm}
The reduction $\twoheadrightarrow$ is convergent.
\end{thm}
\begin{proof}
The reduction $\twoheadrightarrow$ is confluent by
Lemmas~\ref{lem:hulling} and~\ref{lem:pruning}. It's convergent
because the number of hulling and pruning steps is bounded by the
number of strands in a preskeleton.
\end{proof}
\begin{defn}[Preskeleton Reduction System]
Preskeleton~$k_0$ reduces to pruned skeleton~$k_1$,
written~$k_0\reduction{\fn{skel}}k_1$, if
$\{k_0\}\twoheadrightarrow^\ast K$, $k_1\in K$, and~$K$ is a normal
form of~$\twoheadrightarrow$.
\end{defn}
It is easy to show $k_0\reduction{\fn{skel}}k_1$ implies~$k_0\mapsto
k_1$. Furthermore, the structure-preserving map that demonstrates the
homomorphism is easy to derive. For each pruned skeleton~$k$,
$k\reduction{\fn{skel}}k$.
\begin{thm}[Preskeleton Reduction System Correct]\label{thm:prsc}
Let~$k$ be a preskeleton. For every pruned skeleton~$k_1$ such that
$k\homomorphism{\psi_1}k_1$, there is a pruned skeleton~$k_0$ and
homomorphisms~$\psi_0$ and~$\psi$ with $k\reduction{\fn{skel}}k_0$,
$k\homomorphism{\psi_0}k_0$, and $\psi_1=\psi\circ\psi_0$.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{thm}
\begin{note}
Old stuff.
\end{note}
\begin{lem}[Hulling]
Suppose $k\mapsto k'$ with~$k$ a preskeleton and~$k'$ a hulled
preskeleton. There exists a set of homomorphisms~$\Psi$ and a set of
hulled preskeletons~$K$, such that for every hulled preskeleton~$k_1$ and
every homomorphism~$k\homomorphism{\psi_1}k_1$, for
some~$\psi_0\in\Psi$, $k_0\in K$, and~$\psi$,
$\psi_1=\psi\circ\psi_0$,~$\psi$ is unique to within isomorphism,
and~$k_0$ is isomorphic to some~$k_2$ with
$k\to^\ast k_2$, where reduction $\to=\bigcup_{s,s'}\reduction{\ops{H}_{s,s'}}$.
\end{lem}
\begin{thm}
Suppose $k\mapsto k'$ with~$k$ a preskeleton and~$k'$ a pruned
skeleton. There exists a set of homomorphisms~$\Psi$ and a set of
pruned skeletons~$K$, such that for every pruned skeleton~$k_1$ and
every homomorphism~$k\homomorphism{\psi_1}k_1$, for
some~$\psi_0\in\Psi$, $k_0\in K$, and~$\psi$,
$\psi_1=\psi\circ\psi_0$,~$\psi$ is unique to within isomorphism,
and~$k_0$ is isomorphic to some~$k_2$ with
$k\reduction{\fn{skel}}k_2$.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{thm}
\section{Penetrator Derivable}\label{penetrator}
For each algebra, the powers of the adversary are defined by a set of
roles. For the Basic Crypto Signature in Figure~\ref{fig:bcs}, the
traces of the penetrator roles are in Figure~\ref{fig:pen}.
Penetrator roles make no origination assumptions.
The context in which penetrator strands appear determine the messages
the adversary can derive. The context includes previously sent
messages and atoms it is forbidden to originate. An atom that is
assumed to be non-originating must be avoided as is a uniquely
originating atom that is assumed to originate on a regular strand.
The ternary relation \der{t}{T_p}{T_a} states that message~$t$ is
penetrator derivable from previously sent messages~$T_p$ while
avoiding atoms~$T_a$. The relation is defined by a set of inference
rules. Most of the rules are justified by a penetrator role that when
instantiated, derives a message in the conclusion of the rule.
The first rule states that no additional penetrator behavior is required
to derive~$t$ if it has been previously sent.
$$\infer{t\in{T_p}}{\der{t}{T_p}{T_a}}$$
A uniquely originating atom need not be avoided if it has been sent.
\begin{equation}\label{eqn:avoid}
\infer{\der{t}{T_p}{T_a}}%
{\der{t}{\{t_0\}\cup T_p}{\{t_0\}\cup T_a}}
\end{equation}
There are two decomposition steps available to the penetrator.
\begin{equation}\label{eqn:sep}
\infer{\der{t}{\{t_0,t_1\}\cup T_p}{T_a}}%
{\der{t}{\{(t_0,t_1)\}\cup T_p}{T_a}}\quad
[\mbox{by $\fn{sep}(t_0,t_1)$}]
\end{equation}
\begin{equation}\label{eqn:dec}
\infer{\der{\fn{inv}(t_1)}{T_p}{T_a}\qquad
\der{t}{\{t_0,\enc{t_0}{t_1}\}\cup T_p}{T_a}}%
{\der{t}{\{\enc{t_0}{t_1}\}\cup T_p}{T_a}}\quad
[\mbox{by $\fn{dec}(t_0,t_1)$}]
\end{equation}
There are two constructive steps.
$$\infer{\der{t_0}{T_p}{T_a}\qquad\der{t_1}{T_p}{T_a}}%
{\der{(t_0,t_1)}{T_p}{T_a}}\quad
[\mbox{by $\fn{cat}(t_0,t_1)$}]$$
$$\infer{\der{t_0}{T_p}{T_a}\qquad\der{t_1}{T_p}{T_a}}%
{\der{\enc{t_0}{t_1}}{T_p}{T_a}}\quad
[\mbox{by $\fn{enc}(t_0,t_1)$}]$$
There are three rules for indivisible messages.
$$\der{C_i}{T_p}{T_a}\quad
[\mbox{by $\fn{tag}(C_i)$}]$$
$$\infer{t\notin T_a\qquad\mbox{$t$ an atom}}%
{\der{t}{T_p}{T_a}}\quad
[\mbox{by $\fn{base}(t)$}]$$
A non-base sorted variable is derivable in a bundle that instantiates
it with any message other than an element of $X_\top$.
$$\infer{t\in X_\top}{\der{t}{T_p}{T_a}}$$
\begin{defn}[Outbound predecessors]
The \emph{outbound predecessors} of skeleton~$k$ at~$n$ is
$\fn{outpred}(k,n)=\{\fn{msg}(k,n_0)\mid n_0 \kprec{k} n, n_0\mbox{~is
transmitting}\}$.
\end{defn}
\begin{defn}[Avoidance Set]\label{def:avoid}
The \emph{avoidance set} of skeleton~$k$ is
$\fn{avoid}(k)=\fn{non}(k)\cup\{t\mid
t\in\fn{unique}(k)\land|\orig(k,t)|=1\}$.
\end{defn}
An atom in $\fn{avoid}(k)$ is not available to the penetrator, except
if it is exposed by a messages transmission. Clearly, only uniquely
originating atoms can be exposed.
\begin{defn}[Derivable Before]\label{def:der}
A message~$t$ is \emph{derivable before} reception node~$n$ in
skeleton~$k$, written $\fn{der}(k,n,t)$, if $\der{t}{T_p}{T_a}$ where
$T_p=\fn{outpred}(k,n)$ and $T_a=\fn{avoid}(k)$.
\end{defn}
\begin{defn}[Realized Node]
A reception node~$n$ is \emph{realized} in skeleton~$k$ if
$\fn{msg}(k,n)$ is derivable before~$n$ in~$k$.
\end{defn}
Notice that one can read off penetrator behavior from the proof tree
used to demonstrate that $\fn{msg}(k,n)$ is derivable before~$n$
in~$k$. For example, if a decryption step is required by the proof,
an instance of the penetrator's decryption role is indicated. In a
bundle, for a non-base sorted variable, there is a substitution that
maps the variable to a message that is not a non-base sorted variable.
The substitution determines the penetrator behavior associated with
the variable.
\begin{thm}[Realized Skeleton]
A skeleton is realized if and only if all of its reception nodes are
realized.
\end{thm}
\begin{proof}
Given a skeleton~$k$ in which all of its reception nodes are realized,
the combination of the regular behavior in the skeleton, the
penetrator behavior specified by the proof trees used to demonstrate
each node is realized, and a substitution for non-base sorted
variables determines a bundle. The skeleton of the bundle may have
more non-originating atoms than is in $\fn{non}(k)$, however since the
extra non-originating atoms are derivable by the bundle that
realizes~$k$, the proof trees for those atoms specify any additional
penetrator behavior required.
\begin{note}
I haven't figure out how to do the ``only if'' part of this proof yet.
\end{note}
\end{proof}
\subsection{Implementation}\label{sec:derivable implementation}
The derivable before a node predicate is implemented using auxiliary
functions.
\begin{defn}[Buildable]
Message~$t$ is \emph{buildable} from previously sent messages~$T_p$
while avoiding~$T_a$, written $\fn{bld}(t,T_p,T_a)$, if
\der{t}{T_p}{T_a} without the use of Inference Rules \ref{eqn:avoid},
\ref{eqn:sep}, and~\ref{eqn:dec}.
\end{defn}
Consider the following reduction system based on Inference Rules
\ref{eqn:avoid}, \ref{eqn:sep}, and~\ref{eqn:dec}.
$$\begin{array}{r@{}c@{}ll}
\dctx{\{t\}\cup T_p}{T_a}&{}\to{}&\dctx{T_p}{T_a}\setminus\{t\}
&\mbox{if $t$ is an atom or in $X_{\top}$}\\
\dctx{\{(t_0,t_1)\}\cup T_p}{T_a}&{}\to{}&\dctx{\{t_0,t_1\}\cup T_p}{T_a}\\
\dctx{\{\enc{t_0}{t_1}\}\cup
T_p}{T_a}&{}\to{}&\dctx{\{t_0,\enc{t_0}{t_1}\}\cup T_p}{T_a}
&\mbox{if $t_0\notin T_p$ and}\\
&&&\fn{bld}(\fn{inv}(t_1),T_p,T_a)
\end{array}$$
\begin{defn}[Decompose]
Previously sent messages~$T_p$ and avoidance set~$T_a$
\emph{decompose} to $T'_p,T'_a$, written
$\fn{decompose}(T_p,T_a)=(T'_p,T'_a)$, if
$\dctx{T_p}{T_a}\to^\ast\dctx{T'_p}{T'_a}$
and $(T'_p,T'_a)$ is a normal form of reduction~$\to$.
\end{defn}
The penetrator derivable predicate $\der{t}{T_p}{T_a}$ is implemented as
\begin{center}
\begin{tabular}{l}
$\der{t}{T_p}{T_a}={}$\\
\quad\textbf{let} $T'_p, T'_a=\fn{decompose}(T_p,T_a)$ \textbf{in}\\
\quad$\fn{bld}(t,T'_p,T'_a)$
\end{tabular}
\end{center}
The decomposition at a node function is
\begin{center}
\begin{tabular}{l}
$\fn{dcmp}(k,n)={}$\\
\quad$\fn{decompose}(\fn{outpred}(k,n),\fn{avoid}(k))$
\end{tabular}
\end{center}
The derivable before a node predicate is implemented as
\begin{center}
\begin{tabular}{l}
$\fn{der}(k,n,t)={}$\\
\quad\textbf{let} $T_p, T_a=\fn{dcmp}(k,n)$ \textbf{in}\\
\quad$\fn{bld}(t,T_p,T_a)$
\end{tabular}
\end{center}
\subsection*{Discussion}
\begin{note}
Add discussion.
\end{note}
\section{Carried Only Within}\label{sec:cow}
A set of encryptions~$T_e$ protects critical message~$t$ in
message~$t'$ if~$t$ is carried by~$t'$ only within a member of~$T_e$.
The definition of the carried only within ({\cow}) relation to follow makes
this concept precise. The concept is used when solving authentication
tests (Section~\ref{sec:auth tests}).
The question of the protection of a critical message is posed within
the context of a given pruned skeleton~$k$. The message algebra is
$\alg{A}_\top(X)$, where~$X$ is the finite variable
set~$\fn{vars}(k)$. Thus all substitutions in this section are finite
maps.
\begin{defn}[Ancestors]
Let $t'=t\termat p$. The \emph{ancestors} of~$t'$ in~$t$ at~$p$ is
the set $\fn{anc}(t,p)=\{t\termat p'\mid \mbox{$p'$ a proper prefix
of~$p$}\}$.
\end{defn}
\begin{defn}[Carried Only Within]\label{def:cow}
Message~$t$ is \emph{carried only within} set~$T_e$ in~$t'$, written
$t\nncow{T_e}t'$, if for all carried positions~$p$ of~$t$ in~$t'$,
there exists an ancestor~$t_a\in\fn{anc}(t',p)$ and $t_e\in T_e$ such
that~$t_a\equiv t_e$. The negation, $\neg(t\nncow{T_e}t')$ is written
$t\ncow{T_e}t'$.
\end{defn}
Definition~\ref{def:carried positions} defines $\fn{carpos}(t,t')$, the
set of positions at which~$t'$ carries~$t$.
The details of a reduction on skeletons called a augmentation will be
described in Section~\ref{augmentations}. In simplified form, for
an augmentation, given~$t$,~$T_e$, and~$t'$, one must find all most
general unifiers~$\sigma$ such that~$\sigma(t)$ is carried only within
set~$\sigma(T_e)$ in~$\sigma(t')$.
A carried only within solution cannot be directly computed using
Definition~\ref{def:cow}. Given terms~$t_a$ and~$t_e$, the
$\fn{unify}$ function specified at the end of
Section~\ref{sec:messages} finds substitutions~$\sigma$ such
$\sigma(t_a)\equiv \sigma(t_e)$, however, the carried positions
$\fn{carpos}(\sigma(t),\sigma(t'))$, are used before the $\fn{unify}$
function computes the substitution~$\sigma$. Figure~\ref{fig:cows}
displays the iterative procedure that breaks the cyclic dependencies.
Each step of the iteration improves an approximation of a solution to
the problem. The correctness of this function is the subject a paper
in preparation.
\begin{figure}
\begin{center}
\begin{tabular}{l}
$\fn{cows}(t,T,t') ={}$\\
\quad $\fn{cows}_0(t,T,t',\idsigma)$
\quad --- $\idsigma$ is the identity
subst \\
\\
$\fn{cows}_0(t,T,t',\sigma) ={}$\\
\quad \textbf{if} $\sigma(t)$ is {\cow} $\sigma(T)$ at
$\sigma(t')$ \textbf{then}\\
\qquad $\{\sigma\}$\\
\quad \textbf{else}\\
\qquad\textbf{let}
$S=\fn{fold}(t,T,t',\sigma)$
\textbf{in}\\
\qquad$\bigcup_{\sigma'\in S}
\fn{cows}_0(t, T, t',\sigma')$\\
\\
$\fn{fold}(t,T,t',\sigma)={}$\\
$\quad\{\sigma'\circ\sigma\mid\sigma'\in
\fn{fold}_0(\sigma(T),\sigma(t'),\{\idsigma\},
\fn{carpos}(\sigma(t),\sigma(t')))$\\
\\
$\fn{fold}_0(T,t',S,\{\})=S$\\
$\fn{fold}_0(T,t',S,\seq{p}\append P)={}$\\
\quad $\fn{fold}_0(T,t',\fn{solve}(\fn{anc}(t',p),T,S),P)$\\
\\
$\fn{solve}(T,T',S)={}$\\
\quad$\{\sigma'\mid t\in T, t'\in T',
\sigma\in S, \sigma'\in\fn{unify}(t,t',\sigma)\}$
\end{tabular}
\end{center}
\caption{The \fn{cows} Function}\label{fig:cows}
\end{figure}
\section{Authentication Tests}\label{sec:auth tests}
In what follows, we assume all skeletons are pruned, and use the word
``skeleton'' to mean pruned skeleton.
\begin{defn}[Protectors]
Let \fn{deriv} be a boolean valued function that determines if a
message is derivable. The encryptions that protect~$t_c$ in~$t$ is
$\fn{protectors}(\fn{deriv},t_c, t) = \fn{prot}(t)$ where
$$\fn{prot}(t) =\left\{
\begin{array}{ll}
\mbox{undefined}&\mbox{if $t\equiv t_c$, else}\\
\{\}&\mbox{if $t=\enc{t_0}{t_1}$ and $t_c$ is not carried by~$t_0$, else}\\
\{\enc{t_0}{t_1}\}&
\mbox{if $t=\enc{t_0}{t_1}$ and $\lnot\fn{deriv}(\fn{inv}(t_1))$, else}\\
\fn{prot}(t_0)&\mbox{if $t=\enc{t_0}{t_1}$, else}\\
\bigcup_{i<n}\fn{prot}(t_i)&\mbox{if $t=f(t_0,\ldots,t_{n-1})$ and~$t$
is not an atom, else}\\
\{\}&\mbox{otherwise.}
\end{array}\right.$$
\end{defn}
\begin{defn}[Escape Set]
The escape set for message~$t_c$ at~$n$ in skeleton~$k$ is the set of
encryptions $\fn{esc}(k,n,t_c)$ where
$$\fn{esc}(k,n,t_c)=\{t_e\mid t_e\in\fn{protectors}(\lambda
t\mathpunct.\fn{der}(k,n,t),t_c,t_o), t_o\in\fn{outpred}(k,n)\}$$
and~$\fn{der}(k,n,t)$ is true when $t$ is derivable before~$n$ in~$k$
(See Definition~\ref{def:der}).
\end{defn}
The $\fn{der}$ function is implemented as
$\fn{der}(k,n,t)=\fn{bld}(t,T_p,T_a)$ where
$(T_p,T_a)=\fn{dcmp}(k,n)$, so that~$T_p$ and~$T_a$ need not be
recomputed.
\begin{defn}[Critical Position]
Position~$p$ is a \emph{critical position} of $t=\fn{msg}(k,n)$ if
\begin{enumerate}
\item $p$ is a carried position in~$t$,
\item either $t\termat p\in\fn{unique}(k)$ and $t\termat p$ originates
in~$k$, or $t\termat p=\enc{t_0}{t_1}$ and~$t_1$ is not derivable
before~$n$ in~$k$,
\item $\fn{esc}(k,n,t\termat p)$ is defined, and
\item $\fn{anc}(t,p)\cap \fn{esc}(k,n,t\termat p)=\emptyset$.
\end{enumerate}
\end{defn}
The message at a critical position is called a \emph{critical
message}. It is a \emph{critical nonce} if the message is an atom,
otherwise it is a \emph{critical encryption}. Observe that every
critical message at a node in a skeleton is not derivable at the node.
\begin{thm}
A reception node is unrealized iff it has a critical position.
\end{thm}
\begin{defn}[Critical Position Solved]\label{def:critical position solved}
Suppose~$p$ is a critical position at~$n_0$ in~$k_0$ and
$k_0\homomorphism{\phi,\sigma}k_1$. Let~$t_0=\fn{msg}(k,n)\termat p$,
$t_1=\sigma(t_0)$,
$T=\sigma(\fn{esc}(k_0,n_0,t_0))$, $n_1=\phi(n_0)$,
and~$t=\fn{msg}(k_1,n_1)$. Critical position~$p$ is solved in~$k_1$
after~$k_0$ at~$n_0$ if:
\begin{enumerate}
\item $\fn{anc}(t,p)\cap T\neq\emptyset$, or
\item for some~$t_p\in\fn{outpred}(k_1,n_1)$, $t_1$ is not carried
only within~$T$ in~$t_p$, or
\item the decryption key of a member of~$T$ is derivable
before~$n_1$ in~$k_1$, or
\item $t_1$ is an encryption and its encryption key is derivable
before~$n_1$ in~$k_1$.
\end{enumerate}
\end{defn}
\begin{defn}[Contraction]\label{def:contraction}
Let~$p$ be a critical position at~$n$ in~$k$, $t=\fn{msg}(k,n)$, and
$T_e= \fn{esc}(k,n,t\termat p)$. Suppose there is a
substitution~$\sigma$ such that for some~$t_a\in\fn{anc}(t,p)$,
$t_e\in T_e$, $\sigma(t_a)=\sigma(t_e)$.
Skeleton~$k_1$ is a \emph{contraction} if
$k\reduction{\ops{S}_\sigma}k_0\reduction{\fn{skel}}k_1$.
\end{defn}
{\cpsa} computes a set of substitutions for each critical position, and
then removes some substitutions to form a complete set of most
general unifiers. Only most general unifiers are used for
contractions.
The function~$\ops{A}_{i,n}$ augments a preskeleton with a new strand.
It appends the instance~$i$ to the sequence of instances, adds node
orderings, and adds atoms as specified by the role of the instance.
The function orders the last node in the strand before some node~$n$
in the preskeleton.
\begin{defn}[Augmentation]\label{def:augmentation}
Skeleton~$k_0$ reduces to preskeleton~$k_1$ by the augmentation~$i,n$,
written $k_0\reduction{\ops{A}_{i,n}}k_1$ if
\begin{enumerate}
\item $\fn{insts}(k_1)=\fn{insts}(k_0)\append\seq{i}$;
\item $\kprec{k_1}=(\mathord{\kprec{k_0}}\cup\mathord{\Rightarrow_{k_1}}\cup
\mathord{\{(n_0, n)\}})^\ast$, where $n_0=(|\fn{insts}(k_0)|,
\fn{height}(i)-1))$;
\item $\fn{unique}(k_1)$ is $\fn{unique}(k_0)$ and the inherited
uniquely originating atoms in~$i$;
\item $\fn{non}(k_1)$ is $\fn{non}(k_0)$ and the inherited
non-originating atoms in~$i$.
\end{enumerate}
\end{defn}
\begin{defn}[Regular Augmentation]
Let~$t_c$ be a critical message at~$n$ in~$k$, and~$i$ be an instance
of a regular, non-listener role. Skeleton~$k_2$ is a \emph{regular
augmentation} if
$k\reduction{\ops{S}_\sigma}k_0\reduction{\ops{A}_{i,n}}k_1
\reduction{\fn{skel}}k_2$ for some substitution~$\sigma$ and~$t_c$ is
solved in~$k_2$ after~$k_0$ at~$n$.
\end{defn}
The details of regular augmentation is the subject of the next section.
\begin{defn}[Listener Augmentation]
Let~$t_c$ be a critical message at~$n$ in~$k$, and
$T=\fn{esc}(k,n,t_c)$. For each $\enc{t_0}{t_1}\in T$,
skeleton~$k_1$ is a \emph{listener augmentation} if
$k\reduction{\ops{A}_{i,n}}k_0\reduction{\fn{skel}}k_1$ and~$i$ is a
listener for $\fn{inv}(t_1)$. If $t_c=\enc{t_0}{t_1}$, then
skeleton~$k_1$ is a \emph{listener augmentation} if
$k\reduction{\ops{A}_{i,n}}k_0\reduction{\fn{skel}}k_1$ and~$i$ is a
listener for $t_1$.
\end{defn}
\begin{defn}[Cohort Member]
For unrealized node~$n$ in a skeleton~$k_0$, and a position~$p$ at~$n$, $k_0\reduction{n,p}k_1$ asserts that $k_1$ is a
member of the cohort of~$k_0$, where~$k_1$ is derived using
contraction, regular augmentation, or listener augmentation, and~$p$
is solved in~$k_1$ after~$k_0$ at~$n$. For the setwise cohort member
reduction, $\{k_0\}\setreduction{n,t}\{k_1\mid k_0\reduction{n,p}k_1\}$,
when~$n$ is unrealized in~$k_0$, and~$p$ is a critical position at~$n$.
\end{defn}
\begin{thm}[Cohort Correct]
Let node~$n$ be unrealized in skeleton~$k$, and~$p$ be a critical
position at~$n$. For every realized skeleton~$k_1$ such that
$k\homomorphism{\psi_1}k_1$, there is a~$k_0$,~$\psi_0$, and~$\psi$
with $k\reduction{n,p}k_0$, $k\homomorphism{\psi_0}k_0$, and
$\psi_1=\psi\circ\psi_0$.
$$\xymatrix@C=3em{
k\ar@{|->}[r]^{\psi_0} \ar@{|->}[rd]_{\psi_1} &
k_0 \ar@{|->}[d]^{\psi}\\
&k_1}$$
\end{thm}
\begin{thm}[Cohort]
Reduction $\setreduction{\fn{co}}=\bigcup_{n,t}\setreduction{n,p}$ is
confluent.
\end{thm}
\begin{thm}[Critical Message Solved]
If $k_0\reduction{n_0,p_0}k_1 \reduction{n_1,p_1}\ldots
\reduction{n_{\ell-1},p_{\ell-1}}k_\ell$ is a sequence of cohort member
reductions, then for positive~$\ell$,~$p_0$ is solved in~$k_\ell$
after~$k_0$ at~$n_0$.
\end{thm}
\section{Finding Regular Augmentations}\label{augmentations}
Let~$t_c$ be the critical message that demonstrates~$n$ is a test node
in skeleton~$k$. For each substitution-instance pair~$(\sigma,i)$
that satisfies some properties, there is a potential regular
augmentation with~$\comp{\reduction{\fn{skel}}}%
{\comp{\reduction{\ops{A}_{i,n}}}{\reduction{\ops{S}_\sigma}}}$.
When successful, the message~$t$ in the last node of the added strand
is outbound, carries~$\sigma(t_c)$, but~$\sigma(t_c)$ is not carried
only within escape set~$\sigma(T_e)$ in~$t$. Moreover, for every
other message~$t$ in the strand,~$\sigma(t_c)$ is carried only within
escape set~$\sigma(T_e)$ in~$t$. The last node in the strand is
called a \emph{transforming node}, as this node no longer protects the
critical message, but nodes that precede it do.
When generating a candidate substitution-instance pair~$(\sigma,i)$
for augmentation, $\fn{trace}(i)$ must contain a member of~$T_t$, the
set of \emph{target messages}. The critical message~$t_c$ is a member along
with each ancestor of the critical message~$t_c$ on every path to a place
at which~$t_c$ is carried in every member of the escape set~$T_e$,
with the exception of the members of~$T_e$. That is,
$T_t=\{t_c\}\cup\{t_t\mid t_e\in T_e,p\in\fn{carpos}(t_c, t_e),
t_t\in\fn{anc}(t_e,p)\}\setminus T_e$.
To find all candidate substitution-instance pairs, each role in the
protocol is considered. For each role~$r$, a substitution~$\sigma_r$
is created. The domain of~$\sigma_r$, $\fn{Dom}(\sigma_r)$, is the
variables that occur in the role's trace. The substitution~$\sigma_r$
is a bijection, and each variable in $\fn{Ran}(\sigma_r)$ is chosen in
a way that ensures it does not occur in the skeleton~$k$ or in any of
its roles.
Consider each outbound message~$t_{n-1}$ in $\fn{rtrace}(r)=\seq{\pm
t_0,\ldots,+t_{n-1},\ldots}$. Let substitutions~$S$ be a complete
set of most general unifiers~$\sigma'$ such that for every message~$t$
that is carried by $t_{n-1}$ and message~$t_t\in T_t$,
$\sigma'(t)\equiv\sigma'(t_t)$, and $\sigma_r\unlhd\sigma'$. This
operation inserts the critical message into the trace
$\sigma_r\circ\fn{rtrace}(r)$.
\begin{figure}
\begin{center}
\begin{tabular}{l}
$\fn{cowt}(t,T,C,S) ={}$\\
$\quad\bigcup_{\sigma\in S}\fn{cowt}_0(t,T,C,\sigma)$\\
\\
$\fn{cowt}_0(t,T,C,\sigma) ={}$\\
\quad \textbf{if} $\all{t}\pm t\in C\to\sigma(t)$ is {\cow} $\sigma(T)$ at
$\sigma(t')$ \textbf{then}\\
\qquad $\{\sigma\}$\\
\quad \textbf{else}\\
\qquad$\fn{cowt}(t,T,C,\fn{foldn}(t, T, C, \{\sigma\}))$\\
\\
$\fn{foldn}(t,T,\seq{},S)=S$\\
$\fn{foldn}(t,T,\seq{\pm t'}\append C,S)={}$\\
$\quad\fn{foldn}(t,T,C,\bigcup_{\sigma\in S}\fn{fold}(t,T,t',\sigma))$
\end{tabular}
\end{center}
\caption{The $\fn{cowt}$ Function}\label{fig:cowt}
\end{figure}
The next step is to explore ways to extend the substitution~$\sigma'$
so that for events in $\sigma'\circ\fn{rtrace}(r)$ that
precede~$t_{n-1}$, the critical message is carried only within the
escape set. The function \fn{cowt}, presented in
Figure~\ref{fig:cowt}, performs the explorations, producing the
substitutions $S'=\fn{cowt}(t_c,T_e,\prefix{\fn{rtrace}(r)}{n-1},S)$.
Function $\fn{fold}$ is defined in Figure~\ref{fig:cows}.
The final step is to remove substitutions $\sigma\in S'$ such that
$\sigma(t_c)$ is carried only within $\sigma(T_e)$
in~$\sigma(t_{n-1})$ and produce a complete set of most general
unifiers~$S''$ by removing less general unifiers. For each
$\sigma'\in S''$,
there is a potential regular augmentation constructed from
$(\sigma,i)$, where $\fn{role}(i)=r$, $\fn{height}(i)=n$,
$\fn{subst}(i)=\sigma$, and~$\sigma$ is~$\sigma'$ stripped of
mappings to messages with variables that do not occur in
$\sigma'\circ\prefix{\fn{rtrace}(r)}{n}$.
\begin{note}
For target terms to be the reasonable set for insertion of the
critical message, one must require that variables of sort message are
acquired. This fact needs to be explained and noted as another reason
for the acquired variable constraint.
\end{note}
\subsection{Regular Augmentation and Hulling}
Consider regular augmentation
$k\reduction{\ops{S}_\sigma}k_0\reduction{\ops{A}_{i,n}}k_1
\reduction{\fn{skel}}k_2$, where $k_1$ is not a hulled preskeleton.
Let~$k_3$ be the result of one hulling step. It is crucial that
$k\longmapsto k_2$, but it need not be the case that $k_1\longmapsto
k_3$. The reason is that a point of origination on the augmenting
strand may move during hulling, but that's okay since the augmenting
strand is not in the image of a homomorphism from~$k$. An
implementation must be careful not to check the preservation of
origination points in this particular case.
\section{Generalization}\label{generalization}
Each problem statement for {\cpsa} is expressed as a preskeleton. If
the preskeleton cannot be transformed into a single skeleton using the
Preskeleton Reduction System, an error is signaled. Otherwise, the
first skeleton is designated as the \index{point-of-view
skeleton}point-of-view skeleton. For each skeleton generated from a
point-of-view skeleton via contraction, augmentation, and
generalization, there is a homomorphism from the point-of-view
skeleton. Simplifying the implementation is the motivation for
restricting the algorithm to problem statements that are expressed by
a single skeleton.
\begin{defn}[Generalize]
A skeleton~$k_0$ \emph{generalizes}
skeleton~$k_1$, written $k_1\reduction{<}_k k_0$, if
both~$k_0$ and~$k_1$ are realized,~$k_0$ and~$k_1$ are not isomorphic,
there is a homomorphism from a point-of-view skeleton~$k$ to~$k_0$, and
a strandwise injective homomorphism $k_0\mapsto k_1$.
\end{defn}
\begin{note}
Recent experiments show that pruning must not be performed when
generalizing.
\end{note}
If skeletons are allowed to be isomorphic, we
write~$k_1\reduction{\leq}_k k_0$, and note that $\reduction{\leq}_k$
defines a partial ordering. Therefore, there are maximal elements in
the partial ordering. A shape associated with a preskeleton
is a maximally generalized realized skeleton derived from the
preskeleton.
\begin{defn}[Shape]
Let~$k_0$ be a preskeleton such that $k_0\reduction{\fn{skel}}k$
and~$k$ is unique, and let~$k_1$ be a realized skeleton such that
$k\mapsto k_1$. Skeleton~$k_2$ is a \emph{shape} of~$k_0$ if
$k_1\reduction{\leq}_k k_2$, and~$k_2$ is maximal among skeletons that
generalize~$k_1$.
\end{defn}
There are four generalization reductions used to transform a realized
skeleton into its shapes: deletion, weakening, forgetting, and
separation.
\begin{defn}[Deletion]
Skeleton~$k_0$ \emph{generalizes by deletion} skeleton~$k_1$, written
$k_1\reduction{\ops{D}_n}_k k_0$, if $k_1\reduction{<}_k k_0$,
$k_2\reduction{\fn{skel}}k_0$, and~$k_2$ is the result of deleting
node~$n$ in~$k_1$ and all of the nodes that follow it in its strand.
\end{defn}
\begin{defn}[Weakening]
Skeleton~$k_0$ \emph{generalizes by weakening} skeleton~$k_1$, written
$k_1\reduction{\ops{W}_{n,n'}}_k k_0$, if $k_1\reduction{<}_k k_0$,
$k_2\reduction{\fn{skel}}k_0$, and~$k_2$ is~$k_1$ except
$\kprec{k_2}=(\kprec{k_1}\setminus\{(n,n')\})^\ast$.
\end{defn}
\begin{defn}[Forgetting]
Skeleton~$k_0$ \emph{generalizes by origination assumption forgetting}
skeleton~$k_1$, written $k_1\reduction{\ops{F}_t}_k k_0$, if
$k_1\reduction{<}_k k_0$, $k_2\reduction{\fn{skel}}k_0$, and~$k_2$
is~$k_1$ except $\fn{unique}(k_2)=\fn{unique}(k_1)\setminus\{t\}$ and
$\fn{non}(k_2)=\fn{non}(k_1)\setminus\{t\}$.
\end{defn}
Sometimes a more general skeleton can be found by replacing some
occurrences of one variable by a fresh variable. For variable
separation, the location of an occurrence of a variable is defined
using a skeleton's instance sequence.
\begin{defn}[Location]
Message~$t$ is at \emph{location} $(s,x,p)$ in~$k$ if
$t=\fn{subst}(I(s))(x)\termat p$ and $I=\fn{insts}(k)$.
\end{defn}
\begin{defn}[Separation]
Skeleton~$k_0$ \emph{generalizes by variable separation}
skeleton~$k_1$, written $k_1\reduction{\ops{V}_t}_k k_0$, if
$k_1\reduction{<}_k k_0$, $k_2\reduction{\fn{skel}}k_0$, and~$k_2$
is~$k_1$ except ~$t$ is a variable that occurs in multiple locations
in~$k_1$, and~$k_2$ is the result of replacing~$t$ with a variable~$t_0$
of the same sort at a subset of~$t$'s locations, where~$t_0$ occurs
nowhere in~$k_1$.
\end{defn}
When separating a non-originating term, both the term and its clone
are non-originating. When separating a uniquely originating term,
either the term or its clone is uniquely originating.
\begin{note}
What happens when separating~$t$ in~$k$ into~$t$ and~$t_0$, and
$\cn{ltk}(t,t)\in\fn{non}(k)$? Should a skeleton~$k_0$ with
$\cn{ltk}(t,t_0)\in\fn{non}(k_0)$ be a candidate separation?
Currently, only skeletons~$k_1$ with $\cn{ltk}(t,t)\in\fn{non}(k_1)$
and $\cn{ltk}(t_0,t_0)\in\fn{non}(k_1)$ are considered.
\end{note}
\begin{defn}[Generalization]
The reduction~$\reduction{\fn{gen}}_k
=\bigcup_n\reduction{\ops{D}_n}_k\cup
\bigcup_{n,n'}\reduction{\ops{W}_{n,n'}}_k\cup
\bigcup_t\reduction{\ops{F}_t}_k\cup \bigcup_t\reduction{\ops{V}_t}_k$
is the \emph{generalization} relation. For the setwise generalization
reduction, $\{k_0\}\setreduction{\fn{gen}}_k\{k_1\}$ when
$k_0\reduction{\fn{gen}}_k k_1$.
\end{defn}
\begin{note}
The fact that each generalization reduction replaces a singleton with
just a singleton requires explanation. We're not sure it's justified,
and harbor serious doubts. It is justified if we can prove the
conjecture that the cohort reduction relation produces every shape,
and generalization just identifies which realized skeletons are
shapes. However, one member of the test suite provides a counter
example to the conjecture. Barring a bug in {\cpsa}, the conjecture
must be false.
\end{note}
\begin{thm}[Generalization]
The relation~$\setreduction{\fn{gen}}_k$ is terminating.
\end{thm}
\subsection*{Discussion}
In~\cite{DoghmiGuttmanThayer07}, the shapes of a point-of-view
skeleton are said to be minimal, in the partial ordering induced by
injective homomorphism, among all realized homomorphic images of the
point-of-view skeleton. Minimal corresponds to maximally generalized.
The need for origination assumption forgetting was not known
when~\cite{DoghmiGuttmanThayer07} was written. Generalization by
variable separation uses non-carried positions, and in particular,
positions that traverse an atom edge. Algebras in previous strand
space papers have no concept of a position that traverses an atom
edge, and therefore cannot be used to specify generalization by
variable separation.
\section{Collapsing}\label{collapsing}
Let reduction $\setreduction{\fn{cg}}_k=(\setreduction{\fn{co}}\cup
\setreduction{\fn{gen}}_k)^+$, the transitive closure of the cohort
and generalization setwise reduction relations. The normal forms of
this relation are sets of shapes, however, shapes may be missing from
each set. The missing shapes are found by collapsing other shapes.
\begin{defn}[Collapsing]
Let $k_0$ and $k_1$ be two skeletons such that there are two
strands,~$s$ and~$s'$, and a substitution~$\sigma$ with
$\sigma(\fn{evt}(k_0,(s,p)))= \sigma(\fn{evt}(k_0,(s',p)))$ for all
$p<h$, where~$h$ is the height of strand~$s$ in~$k_0$. Then~$k_0$
\emph{collapses} to~$k_1$, written $k_0\reduction{\fn{clp}}k_1$, if
$k_0\reduction{\ops{S}_\sigma}k\reduction{\ops{C}_{s,s'}}k'
\reduction{\fn{skel}}k_1$.
\end{defn}
\begin{defn}[Setwise Collapsing]
For the collapsing relation $\setreduction{\fn{clp}}_k\subseteq
\pow{\alg{K}}\times\pow{\alg{K}}$,
$K_0\setreduction{\fn{clp}}_k K_1$ if~$K_0$ is a normal form of
$\setreduction{\fn{cg}}_k$, for some $k_0\in K_0$, $k_0
\reduction{\fn{clp}}k$, $\{k\}\cup K_0\setreduction{\fn{cg}}_k K_1$,
and $K_0\neq K_1$.
\end{defn}
Notice that a setwise cohort reduction may produce the empty set, but
a setwise generalization and collapsing reduction never does.
\section{Skeleton Reduction System}\label{sec:skeleton reduction}
Let reduction
$\twoheadrightarrow_k=\setreduction{\fn{cg}}_k\cup
(\setreduction{\fn{clp}}_k)^+$.
\begin{thm}
The reduction~$\twoheadrightarrow_k$ is confluent.
\end{thm}
\begin{thm}[Soundness]
Let~$k_0$ be a preskeleton such that $k_0\reduction{\fn{skel}}k$
and~$k$ is unique and unrealized. Skeleton~$k_1$ is a shape of~$k_0$
if $\{k\}\twoheadrightarrow_k K$, $k_1\in K$, and~$K$ is a normal
form.
\end{thm}
\begin{thm}[Completeness]
Let~$k_0$ be a preskeleton such that $k_0\reduction{\fn{skel}}k$
and~$k$ is unique and unrealized. If $\{k\}\twoheadrightarrow_k K$,
and~$K$ is a normal form, then~$k_1$ is a shape of~$k_0$ only if
$k_1\in K$.
\end{thm}
\appendix
\section{Programs Specified by a Role's Trace}\label{sec:traces}
The behavior associated with a role's trace is possible as long as some
messages are available initially. The required initial messages are
specified by a pair of ternary relations, $\flow{T_0}{C}{T_1}$ and
$\flow{T_0}{\pm t}{T_1}$. The relation $\flow{T_0}{C}{T_1}$ asserts
that messages in~$T_1$ are available after a run of~$C$ given the
messages in~$T_0$ are available initially. The relation is defined
using the $\flow{T_0}{\pm t}{T_1}$ relation.
$$\flow{T}{\seq{}}{T}\qquad
\infer{\flow{T_0}{\pm t}{T}\quad\flow{T}{C}{T_1}}%
{\flow{T_0}{\seq{\pm t}\append C}{T_1}}$$
The $\flow{T_0}{\pm t}{T_1}$ relation is defined using the
$\flow{T_0}{C}{T_1}$ relation. An outbound message can be formed if
it is available initially
$$\infer{t\in T}{\flow{T}{+t}{T}}$$
or if it can be formed by construction.
$$\infer{\flow{T}{\seq{+t_0,\ldots,+t_{n-1}}}{T}}%
{\flow{T}{+f(t_0,\ldots,t_{n-1})}{T}}\quad
\left[\begin{array}{l}
f\in\Sigma_{w,s}\land n=|w|\land {}\\
\mbox{$f(t_0,\ldots,t_{n-1})$ not an atom}
\end{array}\right]$$
An inbound message makes atoms, acquired variables, and
encryptions available.
$$\flow{T}{-t}{T\cup\{t\}}\quad [\mbox{$t$ an atom or a variable}]$$
When the decryption key is available, the contents of the encryption
is also available. Furthermore, the encryption can be sent in future
messages without access to its encryption key.
$$\infer{\flow{T_0}{+\fn{inv}(t_1)}{T_0}\quad
\flow{T_0}{-t_0}{T_1}}{\relax
\flow{T_0}{-\enc{t_0}{t_1}}{T_1\cup\{\enc{t_0}{t_1}\}}}$$ A received
encryption that can be sent ensures the encyption agrees with
currently available terms and makes nothing new available.
$$\infer{\flow{T}{+\enc{t_0}{t_1}}{T}}{\relax
\flow{T}{-\enc{t_0}{t_1}}{T}}$$
Consider an operation $f\in\Sigma_{w,s}$ other than the encryption
operation. The order in which messages that occur in a message
constructed using~$f$ are made available may determine if the
decryption key of an encryption is available. Let~$\pi_n$ be a
permutation on the domain of a sequence of length~$n$.
$$\infer{\flow{T_0}{\seq{-t_0,\ldots,-t_{n-1}}\circ\pi_n}{T_1}}%
{\flow{T_0}{-f(t_0,\ldots,t_{n-1})}{T_1}}\quad
\left[\begin{array}{l}
f\in\Sigma_{w,s}\land n=|w|\land f\neq\cn{enc}\land {}\\
\mbox{$f(t_0,\ldots,t_{n-1})$ not an atom}
\end{array}\right]$$
\begin{defn}[Trace Parameters]
The set of atoms~$T_0$ are \emph{parameters} of trace~$C$ if
$\flow{T_0}{C}{T_1}$ for some~$T_1$, and~$T_0$ is minimal, that is for
all~$T'_0$ such that $\flow{T'_0}{C}{T_1}$, $T'_0\not\subset T_0$.
\end{defn}
The role $\seq{\outbnd\enc{a,n}{K_b},\inbnd\enc{n}{K_a}}$ has
two sets of parameters, $\{a,n,K_b,K^{-1}_a\}$
and $\{a,n,K_b,K_a\}$. A program that implements the role using the
second set is useless, so it will be ignored. The intended program
for the role follows.
$$\begin{array}{ll}
\cn{proc}(a,n,K_b,K^{-1}_a)\\
\quad \cn{send}(\enc{a,n}{K_b});\\
\quad x_0\gets \cn{recv}();\\
\quad x_1\gets \cn{decrypt}(x_0,K^{-1}_a);\quad\mbox{--- may fail}\\
\quad x_1 \neq n \to \cn{fail};\\
\cn{end}
\end{array}$$
Let $T_0=\{a,n,K_b,K^{-1}_a\}$ and $T_1=T_0\cup\{\enc{n}{K_a}\}$. The
derivation tree that specifies the intended program has the following
outline.
$$\begin{array}{l}
\mbox{\ldots~construct outbound message} \\
\flow{T_0}{\outbnd\enc{a,n}{K_b}}{T_0}\\
\mbox{\ldots~decode inbound message} \\
\flow{T_0}{\inbnd\enc{n}{K_a}}{T_1} \\
\mbox{\ldots~compose trace} \\
\flow{T_0}{\seq{\outbnd\enc{a,n}{K_b},\inbnd\enc{n}{K_a}}}{T_1}
\end{array}$$
The decoding of the inbound message is specified by this derivation.
$$\infer{\flow{T_0}{\outbnd K^{-1}_a}{T_0}\qquad
\infer{\flow{T_0}{\outbnd n}{T_0}}{\flow{T_0}{\inbnd n}{T_0}}}
{\flow{T_0}{\inbnd\enc{n}{K_a}}{T_1}}$$
\section*{Acknowledgment}
Carolyn Talcott and Leonard Monk provided valuable feedback on drafts
of this document.
\bibliography{cpsa}
\bibliographystyle{plain}
\printindex
\tableofcontents
\end{document}