cpsagoals.tex

\documentclass[12pt]{article}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{graphicx}
\usepackage{alltt}
\usepackage[matrix,arrow,curve]{xy}
\input{macros}

\newcommand{\sym}[1]{\textup{\texttt{#1}}}
\newcommand{\iv}[1]{\ensuremath{{#1}^{-1}}}

\newtheorem{axiom}{Trust Assumption}

\title{CPSA Security Goals and Rules}
\author{Joshua D. Guttman and John D.~Ramsdell\\
  The MITRE Corporation\\ CPSA Version \version}

\begin{document}
\maketitle
\cpsacopying

\tableofcontents

\newpage

\listoffigures

\listoftables

\newpage

\section{Introduction}

\begin{sloppypar}
Analyzing a cryptographic protocol means finding out what security
properties---essentially, authentication and secrecy properties---are
true in all its possible executions.
\end{sloppypar}

Given a protocol definition and some assumptions about executions,
{\cpsa} attempts to produce descriptions of all possible executions of
the protocol compatible with the assumptions.  Naturally, there are
infinitely many possible executions of a useful protocol, since
different participants can run it with varying parameters, and the
participants can run it repeatedly.

However, for many naturally occurring protocols, there are only
finitely many of these runs that are essentially different.  Indeed,
there are frequently very few, often just one or two, even in cases
where the protocol is flawed.  We call these essentially different
executions the \emph{shapes} of the protocol.  Authentication and
secrecy properties are easy to ``read off'' from the shapes, as are
attacks and anomalies, according to the introduction in the {\cpsa}
Primer~\cite{cpsaprimer09}.

But how easy is it to read off authentication and secrecy properties?
What precisely is it that an expert sees?  This paper describes
{\cpsa}'s support for reasoning about security goals using first-order
logic.  With security goals expressed in first-order logic, intuition
is replaced by determining if a formula is true in all executions of
the protocol.

% \emph{Something about the benefits of first-order logic goes here.}

This treatment of security goals relies heavily on a branch of
first-order logic called model theory.  It deals with the relationship
between descriptions in first-order languages and the structures that
satisfy these descriptions.  In our case, the structures are skeletons
that denote a collection of executions of a protocol.  This paper
attempts to describe the language of security goals and its
structures without requiring the reader to have studied model theory.

The model theoretical foundation of this approach to security goals
appears in~\cite{Guttman14}.  A practical use of security goals in
protocol standardization is described in~\cite{GuttmanLiskovRowe14}.
The precise semantics of the goal language is
in~\cite[Appendix~C]{cpsaspec09}.  The syntax of security goals
appears in~\cite[Table~2]{cpsaprimer09}.

The distribution in which this paper is included contains the sample
input {\cpsa} file \texttt{goals.scm}.  It contains the examples in
this paper.  You are encouraged to run the examples and examine the
output while reading this paper.

%% Use a margin width of 62 for S-expressions

\begin{figure}
\begin{center}
\includegraphics{cpsadiagrams-0.mps}\hfil
\includegraphics{cpsadiagrams-1.mps}\\
\end{center}
\begin{center}
\begin{minipage}{3in}
\begin{verbatim}
(defprotocol ns basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace
     (send (enc n1 a (pubk b)))
     (recv (enc n1 n2 (pubk a)))
     (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace
     (recv (enc n1 a (pubk b)))
     (send (enc n1 n2 (pubk a)))
     (recv (enc n2 (pubk b))))))
\end{verbatim}
\end{minipage}
\end{center}
\caption{Needham-Schroeder Initiator and Responder Roles}
\label{fig:ns roles}
\end{figure}

\begin{figure}
\begin{verbatim}
(defgoal ns                ; Goal
  (forall ((b name) (n1 text) (z0 strd))
    (implies
      (and (p "init" z0 3) (p "init" "n1" z0 n1)
        (p "init" "b" z0 b) (non (privk b)) (uniq n1))
      (exists ((z1 strd))
        (and (p "resp" z1 2) (p "resp" "b" z1 b))))))

(defskeleton ns            ; Point of view skeleton
  (vars (a b name) (n1 n2 text))
  (defstrand init 3 (a a) (b b) (n1 n1) (n2 n2))
  (non-orig (privk b))
  (uniq-orig n1))
\end{verbatim}
\begin{center}
\includegraphics{cpsadiagrams-9.mps}
\end{center}
\begin{verbatim}
(defskeleton ns            ; Shape
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig n1)
  (satisfies yes))
\end{verbatim}
\caption{Needham-Schroeder Initiator Point of View}
\label{fig:ns init}
\end{figure}

The {\cpsa} Primer~\cite{cpsaprimer09} is a prerequisite for reading
this paper.  In particular, the Needham-Schroeder Protocol in
Section~10 is reanalyzed using security goals here.  The roles are
displayed in Figure~\ref{fig:ns roles}.

The protocol is analyzed from the point of view of a complete run of
one instance of the initiator role.  The input security goal, followed
by the point of view skeleton it generates and the shape produced by
{\cpsa}, are shown in Figure~\ref{fig:ns init}.  The syntax and
semantics of the goal will be explained later.  Roughly speaking, it
asserts that if a realized skeleton contains a full length initiator
strand, its private key is uncompromised, and it uniquely generates
\texttt{n1}, then the skeleton will contain a responder strand that
agrees with the initiator on the name \texttt{b}.  The shape produced
by {\cpsa} contains the annotation \texttt{(satisfies yes)}.  This
indicates that its structure satisfies the description given by the
security goal.  It will be explained later why the properties of
{\cpsa} allows us to conclude that this goal is true in all executions
of the protocol, and therefore conclude that the Needham-Schroeder
protocol achieves this authentication goal.

\section{Syntax}\label{sec:syntax}

To be precise, a security goal is an order-sorted first-order logic
sentence in a restricted form.  The sentence in Figure~\ref{fig:ns
  init} has the form shared by all security goals.  It is a
universally quantified implication.  The antecedent is a conjunction
of atomic formulas.  For this sentence, the conclusion is an
existentially quantified conjunction of atomic formulas, but in
general, the conclusion is a disjunction of existentially quantified
conjunctions of atomic formulas.  In what follows, \sym{(false)} is a
synonym for the empty disjunction, \sym{(or)}.

\begin{center}\scshape
  \begin{tabular}{rcl}
  goal&$\leftarrow$&(\sym{defgoal} prot sent$+$ comments)
  \\ sent&$\leftarrow$&(\sym{forall} (decl$\ast$) (\sym{implies} antec concl))
  \\ concl&$\leftarrow$&(\sym{false})
  $\mid$ existl $\mid$ (\sym{or} existl$\ast)$
  \\ existl&$\leftarrow$&(\sym{exists}
  (decl$\ast$) antec) $\mid$ antec
  \\ antec&$\leftarrow$&atomic $\mid$ (\sym{and} atomic+)
  \end{tabular}
\end{center}

Variables are declared as they are for roles and skeletons with one
exception, there is a new sort symbol \sym{strd} for strands.  Notice
that in the sentence in Figure~\ref{fig:ns init}, variables \sym{z0}
and \sym{z1} have sort \sym{strd}.  Every universally quantified
variable must occur in the antecedent of the implication.

The signature as been expanded to include the natural numbers.  A
natural number has sort \sym{nat}.

The predicates used to construct an atomic formula (\textsc{atomic})
are listed in Table~\ref{tab:predicates}.  There are two classes of
predicates, protocol specific and protocol independent predicates, and
two kinds of protocol specific predicates, role strand length and role
parameter predicates.  Protocol specific predicates are distinguished
from protocol independent predicates by beginning with the symbol
\texttt{p}.

The first line of the table gives the syntax of a role strand length
predicate.  It contains two tokens, \texttt{p} and a string that names
a role.  That is, for role~$r$, there is a role strand length
predicate, \mbox{\texttt{p} $r$}.  Thus \verb|(p "init" z0 3)| is an
atomic formula using the role strand length predicate for length 3 in the
\texttt{init} role of the protocol in Figure~\ref{fig:ns roles}.

The second line gives the syntax of a role parameter predicate.  It
contains three tokens, \texttt{p}, a string that names a role, and a
string that names a role variable.  For role~$r$, there is role
parameter predicate for each variable declared by~$r$.  Thus
\verb|(p "init" "n1" z0 n1)| is an atomic formula using the role
parameter predicate for parameter \text{n1} in the \texttt{init} role
of the protocol.

The empty string names the listener role of a protocol.  The role
has the variable \texttt{x} of sort \texttt{mesg} as its only role
variable.  There are two positions in the listener role.  Its trace is
\texttt{(trace (recv x) (send x))}.

When a variable of sort \sym{strd} occurs in a formula, its length
must be specified using a role strand length formula.  When an algebra
variable occurs in a formula, its association with the parameter of
some role must be specified using a role parameter formula.

\begin{table}
\begin{center}
  \begin{tabular}{lcl}
    Symbol & Sort & Description\\
    \hline
    \scshape\sym{p} role & $\dom{strd}\times\dom{nat}$ & \mbox{Role
      strand length} \\
    \scshape\sym{p} role param & $\dom{strd}\times\dom{mesg}$
    & \mbox{Role parameter} \\
    \sym{prec}& $\dom{strd}\times\dom{nat}\times\dom{strd}\times\dom{nat}$
    & \mbox{Precedes} \\
    \sym{non}& \dom{atom}
    & \mbox{Non-origination} \\
    \sym{pnon}& \dom{atom}
    & \mbox{Penetrator non-origination} \\
    \sym{uniq}& \dom{atom}
    & \mbox{Unique origination} \\
    \sym{uniq-at}& $\dom{atom}\times\dom{strd}\times\dom{nat}$
    & \mbox{Unique origination on strand} \\
    \sym{auth}& \dom{chan}
    & \mbox{Authenticated channel} \\
    \sym{conf}& \dom{chan}
    & \mbox{Confidential channel} \\
    $=$ & $\dom{all}\times\dom{all}$ & Equality
  \end{tabular}
\end{center}
\caption{Predicates}\label{tab:predicates}
\end{table}

\section{Semantics}\label{sec:semantics}

In a \texttt{defgoal} sentence, the antecedent specifies the point of
view skeleton.  We focus on the antecedent.  In the example,

\begin{quote}
\begin{verbatim}
(defstrand init 3 (a a) (b b) (n1 n1) (n2 n2))
\end{verbatim}
\end{quote}
is extracted from
\begin{quote}
\begin{verbatim}
(and (p "init" z0 3)
  (p "init" "n1" z0 n1) (p "init" "b" z0 b)).
\end{verbatim}
\end{quote}
Notice that {\cpsa} adds a binding for \texttt{a} and \texttt{n2} just
as it does had
\begin{quote}
\begin{verbatim}
(defstrand init 3 (b b) (n1 n1))
\end{verbatim}
\end{quote}
been given as input.

Our aim now is to specify how to decide if a security goal is true in
all possible executions of a protocol.  A skeleton defines a set of
executions that contain the skeleton's structure.  We say a skeleton
\emph{satisfies} a formula if the skeleton contains all of the
structure specified by the formula.  To decide if a skeleton
satisfies a formula, we decide if it satisfies each of its atomic
formulas, and combine the results using the rules of first-order
logic.

Atomic formula \texttt{(p "init" z0 3)} is called a role strand length
formula.  A skeleton~$k$ satisfies the formula if \texttt{z0} maps to
a strand~$s$ in~$k$ such that
\begin{enumerate}
\item the trace of strand~$s$ in~$k$ has a length greater than 2, and
\item the trace when truncated to length 3 is an instance of the init
  role.
\end{enumerate}
Consider the shape in Figure~\ref{fig:ns init}.  It satisfies
\texttt{(p "init" z0 3)} when \texttt{z0} maps to~0.

Atomic formula \texttt{(p "init" "n1" z0 n1)} is called a role
parameter formula.  A skeleton~$k$ satisfies the formula if
\texttt{z0} maps to strand~$s$ in~$k$, \texttt{n1} first occurs in at
position~$i$ in the trace of the init role, and \texttt{n1} maps to a
message algebra term~$t$ in~$k$ such that
\begin{enumerate}
\item the trace of strand~$s$ in~$k$ has a length greater than~$i$,
\item the trace truncated to length $i+1$ is an instance of the
  init role, and
\item the truncated trace is compatible with mapping the init role's
  \texttt{"n1"} role variable to~$t$.
\end{enumerate}
The shape in Figure~\ref{fig:ns init} satisfies \texttt{(p "init" "n1"
  z0 n1)} when \texttt{z0} maps to~0 and \texttt{n1} maps to the
message algebra term \texttt{n1}.

Collectively, a skeleton satisfies the formula
\begin{quote}
\begin{verbatim}
(and (p "init" z0 3)
     (p "init" "a" z0 a) (p "init" "b" z0 b)
     (p "init" "n1" z0 n1) (p "init" "n2" z0 n2))
\end{verbatim}
\end{quote}
if the skeleton contains the structure specified by
\begin{quote}
\begin{verbatim}
(defstrand init 3 (a a) (b b) (n1 n1) (n2 n2)).
\end{verbatim}
\end{quote}

The antecedent in Figure~\ref{fig:ns init} contains two origination
assertions.  The formula \texttt{(non (privk b))} is extracted as
\texttt{(privk b)}.  A skeleton~$k$ satisfies the formula if
\texttt{b} maps to a message algebra term~$t$ in~$k$ such that~$k$
assumes that~$t$ is non-originating.  The unique origination formula for
\texttt{n1} is similarly extracted.

Putting it all together, the mapping
\[\{\mathtt{n1}\mapsto\mathtt{n1},
\mathtt{n2}\mapsto\mathtt{n2}, \mathtt{a}\mapsto\mathtt{a},
\mathtt{b}\mapsto\mathtt{b},\mbox{\tt z0}\mapsto0\}\] shows that
the shape in Figure~\ref{fig:ns init} satisfies the antecedent of the
security goal.

The \texttt{prec} predicate is used to assert a node precedes another
node.  The conclusion in Figure~\ref{fig:ns init} with \texttt{(prec
  z1 1 z0 2)} added is satisfied by the shape using the mapping
$\mbox{\tt z0}\mapsto0$ and $\mbox{\tt z1}\mapsto1$.

The \texttt{uniq-at} predicate is used to assert not only that an atom
uniquely originates, but also the node at which it originates.  In the
Figure~\ref{fig:ns init} goal, the \texttt{(uniq n1)} formula could
have been replaced by \texttt{(uniq-at n1 z0 0)}.  The extracted point
of view skeleton is the same.

Recall that our aim in analyzing a protocol is to find out what
security goals are true in all of its possible executions.  We are
interested in runs of {\cpsa} that show that when every shape
satisfies a goal, it is true in every execution.

When {\cpsa} performs a shape analysis, every shape it generates
refines the input skeleton.  Skeleton refinement is defined
in~\cite[Section~6]{cpsaprimer09}.  The definition makes precise the
notion of structure containment, as skeleton~$A$ refines skeleton~$B$
if and only if~$A$ contains the structure of skeleton~$B$.

The skeleton~$k_0$ extracted from the antecedent of a security goal
has the property that a skeleton refines~$k_0$ if and only if it
satisfies the antecedent.  A skeleton with this property is called the
\emph{characteristic skeleton} of the antecedent.

Given a goal~\(\Phi\), consider a shape analysis starting from the
characteristic skeleton~$k_0$ of its antecedent.  Assume {\cpsa} finds
shapes $k_1,\ldots,k_n$ and that {\cpsa} determines that each~$k_i$
satisfies~$\Phi$.  Consider the executions that contain the structure
in~$k_0$.  {\cpsa} tells us that each execution is in the executions
that contain the structure of some~$k_i$.  Furthermore, because~$k_0$
is a characteristic skeleton, each~$k_i$ satisfies the antecedent
of~$\Phi$.  Executions that do not contain the structure in~$k_0$ do
not satisfy the antecedent.  Therefore,~$\Phi$ is true in all
executions of the protocol and maximally informative.

\section{Examples}\label{sec:examples}

This section contains examples of both authentication and secrecy
goals.  The first example shows the feedback the user receives when a
shape does not satisfy a security goal.  The second example shows how
to use a listener to state a secrecy goal.

\subsection{Needham-Schroeder Responder}\label{sec:ns resp}

\begin{figure}
\begin{verbatim}
(defgoal ns                ; Goal
  (forall ((a b name) (n2 text) (z0 strd))
    (implies
      (and (p "resp" z0 3) (p "resp" "n2" z0 n2)
        (p "resp" "a" z0 a) (p "resp" "b" z0 b)
        (non (privk a)) (uniq n2))
      (exists ((z1 strd))
        (and (p "init" z1 2) (p "init" "b" z1 b))))))

(defskeleton ns            ; Point of view skeleton
  (vars (a b name) (n1 n2 text))
  (defstrand resp 3 (a a) (b b) (n1 n1) (n2 n2))
  (non-orig (privk a))
  (uniq-orig n2))
\end{verbatim}
\begin{center}
\includegraphics{cpsadiagrams-10.mps}
\end{center}
\begin{verbatim}
(defskeleton ns            ; Shape
  (vars (n1 n2 text) (a b b-0 name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (non-orig (privk a))
  (uniq-orig n2)
  (satisfies (no (a a) (b b) (n2 n2) (z0 0))))
\end{verbatim}
\caption{Needham-Schroeder Responder Point of View}
\label{fig:ns resp}
\end{figure}

Figure~\ref{fig:ns resp} contains an analysis of Needham-Schroeder
from the point of view of a complete run of the responder under the
assumption that the responder's private key is uncompromised and the
nonce it generates uniquely originates.

The conclusion of the goal asserts that in an execution compatible
with the point of view, there must be an initiator strand that agrees
with the responder strand on the name \texttt{b}.  The shape produced
by {\cpsa} is a counterexample to this assertion.  Because of this,
{\cpsa} annotates the shape with
\begin{quote}
\begin{verbatim}
(satisfies (no (a a) (b b) (n2 n2) (z0 0))).
\end{verbatim}
\end{quote}
The annotation includes a variable mapping for the shape that
satisfies the antecedent of the goal but does not satisfy its
conclusion.  The reason the shape does not satisfy the goal is because
the mapping \texttt{(b b)} maps the initiator's \texttt{b} parameter
to \texttt{b}, not \texttt{b-0} as is required to model the shape.

Galvin Lowe identified this authentication failure in
Needham-Schroeder and provided a fix.  In the Needham-Schroeder-Lowe
Protocol, the name \texttt{b} is included within the encryption in second
message of both roles.  With this modification, the shape found by
{\cpsa} satisfies the security goal in Figure~\ref{fig:ns resp}, so
Needham-Schroeder-Lowe achieves this authentication goal.

\subsection{A Needham-Schroeder Secrecy Goal}\label{sec:secrecy goal}

\begin{figure}
\begin{quote}
\begin{verbatim}
(defgoal ns
  (forall ((a b name) (n1 text) (z0 z1 strd))
    (implies
      (and (p "init" z0 3) (p "init" "n1" z0 n1)
        (p "init" "a" z0 a) (p "init" "b" z0 b)
        (p "" z1 1) (p "" "x" z1 n1)  ; Listener
        (non (privk a)) (non (privk b))
        (uniq n1))
      (false))))
\end{verbatim}
\end{quote}
\caption{Needham-Schroeder Secrecy Goal}\label{fig:ns secrecy}
\end{figure}

Figure~\ref{fig:ns secrecy} contains an analysis of Needham-Schroeder
from the point of view of a complete run of the initiator under the
assumption that the responder's and its peer's private keys are
uncompromised and the nonce~\texttt{n1} it generates uniquely
originates.  Futhermore, the point of view asserts that the nonce is
leaked using a listener.
\begin{quote}
\begin{verbatim}
(p "" z1 1) (p "" "x" z1 n1)    ; Listener
\end{verbatim}
\end{quote}

{\cpsa} finds no shapes, so Needham-Schroeder achieves this secrecy
goal and does not leak~\texttt{n1}.

\section{The Rest of the Story}\label{sec:whole story}

The examples in the previous section demonstrate the typical way
security goals are analyzed with {\cpsa}.  However, there are more
features that may be useful.

A \texttt{defgoal} form may contain more than one sentence.  See
Figure~\ref{fig:ns init goals} for an example.  When presented with
more than one sentence, {\cpsa} extracts the point of view skeleton
from the first sentence.

It is wise to ensure that the antecedent in every sentence is
identical.  When {\cpsa} performs satisfaction-checking on
sentence~$\Phi$, it only determines if each shape it finds is
satisfied.  If the point of view skeleton is not the characteristic
skeleton of the antecedent of~$\Phi$, the fact that all skeletons
satisfy~$\Phi$ cannot be used to conclude that~$\Phi$ is true in all
executions of the protocol.

\begin{figure}
\begin{quote}
\begin{verbatim}
(defgoal ns
  (forall ((a b name) (n text) (z0 strd))
    (implies
      (and (p "init" z0 2) (p "init" "n1" z0 n)
        (p "init" "a" z0 a) (p "init" "b" z0 b)
        (non (privk a)) (non (privk b)) (uniq n))
      (exists ((z1 strd))
        (and (p "resp" z1 2) (p "resp" "b" z1 b)))))
  (forall ((a b name) (n text) (z0 strd))
    (implies
      (and (p "init" z0 2) (p "init" "n1" z0 n)
        (p "init" "a" z0 a) (p "init" "b" z0 b)
        (non (privk a)) (non (privk b)) (uniq n))
      (exists ((z1 strd))
        (and (p "resp" z1 2) (p "resp" "a" z1 a))))))
\end{verbatim}
\end{quote}
\caption{Two Initiator Authentication Goals}\label{fig:ns init goals}
\end{figure}

{\cpsa} performs satisfaction-checking when an input skeleton in annotated
with one or more security goals.  The annotation uses the
\texttt{goals} key.

\begin{quote}
  \begin{alltt}
(defskeleton
   \ldots
   (goals \textsc{sent\ensuremath{+}}))
  \end{alltt}
\end{quote}

The program \texttt{cpsasas}, discussed in the next section, can be
used to generate a formula with an antecedent such that the input
skeleton is the characteristic skeleton of the antecedent.

\subsection{Shape Analysis Sentences}\label{sec:sas}

A shape analysis sentence expresses all that can be learned from a run
of {\cpsa} as a security goal.  If a security goal can be derived from
a shape analysis sentence, then the protocol achieves the security
goal, that is, the goal is true in all executions of the protocol.

The program \texttt{cpsasas} extracts shape analysis sentences from
the output of {\cpsa}.  Consider the first example in this paper
(Figure~\ref{fig:ns init}), which is in the sample file
\texttt{goals.scm}.  To generate a maximally informative security goal
from the initiator point of view with \texttt{ghci} and
\texttt{Make.hs}, type
\begin{quote}
\begin{verbatim}
$ ghci Make.hs
*Make> sas "goals"
\end{verbatim}
\end{quote}
When using GNU make, type ``\texttt{make goals\_sas.text}''.  The
resulting shape analysis sentence is displayed in Figure~\ref{fig:ns
  sas}.

\begin{figure}
\begin{verbatim}
(defgoal ns
  (forall ((n1 n2 text) (b a name) (z strd))
    (implies
      (and (p "init" z 3) (p "init" "n1" z n1)
        (p "init" "n2" z n2) (p "init" "a" z a)
        (p "init" "b" z b) (non (privk b)) (uniq-at n1 z 0))
      (exists ((n2-0 text) (z-0 strd))
        (and (p "resp" z-0 2) (p "resp" "n2" z-0 n2-0)
          (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b)
          (p "resp" "a" z-0 a) (prec z 0 z-0 0)
          (prec z-0 1 z 1))))))
\end{verbatim}
\caption{Initiator Shape Analysis Sentence}\label{fig:ns sas}
\end{figure}

A shape analysis sentences asserts that either a realized skeleton
does not satisfy its antecedent or it satisfies one or more of the
disjuncts in its conclusion.  {\cpsa} has been designed so that this
assertion is true.  Therefore, every shape analysis sentence is true
in all executions.

A security goal is true in all executions if it can be derived from a
shape analysis sentence~\cite{Ramsdell12}.  In practice,
theorem-proving using shape analysis sentences is rarely employed.
It's clumsy and it requires too much expertise.  The main use of
\texttt{cpsasas} is for generating a formula that is edited to become
a desired security goal.

\section{Rules}\label{sec: rules}

Support for rules was introduced in version 4.1 of {\cpsa}.

Each protocol includes a small collection of rules.  A rule is a
sentence in the goal language presented in Section~\ref{sec:syntax}.
Rules are defined after the roles of a protocol are defined.  The
syntax of a rule follows.

\begin{center}\scshape
  \begin{tabular}{rcl}
    rule&$\leftarrow$&(\sym{defrule} name sent comments)
  \end{tabular}
\end{center}

A rule is an axiom added to a protocol.  {\cpsa} uses the axiom as a
rewrite rule to derive zero or more new skeletons from a skeleton
produced during a step.  An example of a protocol with a rule is in
Figure~\ref{fig:doorsep} on Page~\pageref{fig:doorsep}.

The trust rule states that when CPSA finds a person strand of length
at least one, and the inverse of it's \texttt{p} parameter is
non-originating, CPSA should assume the inverse of it's \texttt{d}
parameter is non-originating.

\subsection{Facts}\label{sec:facts}
Each skeleton includes a small database of facts.  A fact is a named
relation among fact terms.  A fact term\index{fact term} is either a
strand of the skeleton or an algebra term.  A set of facts is
defined anywhere after strands are defined using the \sym{facts} form.
The syntax of facts follows.

\begin{center}\scshape
  \begin{tabular}{rcl}
    facts&$\leftarrow$&(\sym{facts} fact$\ast$) \\
    fact&$\leftarrow$&(symbol fterm$\ast$) \\
    fterm&$\leftarrow$&mesg $\mid$ nat
  \end{tabular}
\end{center}

For example, in a skeleton, a user may want to note that strand 0 owns
the private key for~\texttt{a} by assuming.

\begin{center}
  \verb|(facts (owns 0 (privk a)))|
\end{center}

Facts are most useful when combined with rules.  Here is an example of
their combination.  Suppose a point of view skeleton has two names,
\texttt{a} and~\texttt{b}, and the problem is modeling a situation in
which the two names are known to differ.  To enforce this constraint, add
\begin{center}
  \verb|(facts (neq a b))|
\end{center}
to the point of view skeleton and the \texttt{neq} rule below to the
protocol.

%below, eliminates skeletons that
%violate the constraint.
\begin{quote}
\begin{verbatim}
(defrule neq
  (forall ((a mesg))
    (implies
      (fact neq a a)
      (false))))
\end{verbatim}
\end{quote}

\subsection{DoorSEP}

\begin{sloppypar}
As a motivating scenario consider the Door Simple Example Protocol
(DoorSEP), derived from an expository protocol that was designed to
have a weakness.  Despite this, the protocol achieves the needs of an
application, given a trust assumption.
\end{sloppypar}

Imagine a door~$D$ which is equipped with a badge reader, and a
person~$P$ equipped with a badge.  When the person swipes the badge,
the protocol executes.  Principals such as doors or persons are
identified by the public parts of their key pairs, with \iv{D} and
\iv{P} being the corresponding private keys.  We write \enc{M}{K} for
the encryption of message~$M$ with key~$K$.  We represent digital
signatures $\enc{M}{\iv{P}}$ as if they were the result of encrypting
with $P$'s private key.

$P$ initiates the exchange by creating a fresh symmetric key~$K$,
signing it, and sending it to the door $D$ encrypted with the door's
public key.  $D$ extracts the symmetric key after checking the
signature, freshly generates a token~$T$, and sends it---encrypted
with the symmetric key---back to $P$.  $P$ demonstrates they are
authorized to enter by decrypting the token and sending it as
plaintext to the door.  The two roles of DoorSEP are shown in
Fig.~\ref{fig:doorsep protocol}, where each vertical column displays
the behavior of one of the roles.  The \cpsa4 encoding of the roles is
in Figure~\ref{fig:doorsep}.

\begin{figure}[tb]
  \[\begin{array}[c]{rc@{\qquad\qquad}cl}
      & \mbox{person}
      &\mbox{door}
      &\\
      \begin{array}[c]{r} ~ \\ ~ \\
        \mbox{Fresh: $K$}
      \end{array}
      & \xymatrix@R=2mm@C=7em{
      \bullet\ar@{=>}[d]\ar[r]^{\enc{\enc{K}{\iv{P}}}{D}}
      &\\
      \bullet\ar@{=>}[d]& \ar[l]_{\enc{T}{K}}\\
      \bullet \ar[r]^T & }
      &
        \xymatrix@R=2mm@C=7em{
        \ar[r]^{\enc{\enc{K}{\iv{P}}}{D}}    &\bullet\ar@{=>}[d]\\
      &\bullet\ar@{=>}[d] \ar[l]_{\enc{T}{K}}\\
      \ar[r]^T      &\bullet}
      &
        \begin{array}[c]{r} ~ \\ ~ \\
          \mbox{Fresh: $T$}
        \end{array}
  \end{array}\]
  \caption{DoorSEP Protocol}\label{fig:doorsep protocol}
\end{figure}

%   \[
%   \begin{array}{l@{{}:{}}l}
%     P\to D & \enc{\enc{K}{\iv{P}}}{D}\\
%     D\to P & \enc{T}{K}\\
%     P\to D & T.
%   \end{array}
%   \]

{\cpsa} finds an undesirable execution of DoorSEP.  Assume the
person's private key \iv{P} is uncompromised and the door has received
the token it sent out.  Then {\cpsa} finds that~$P$ freshly created
the symmetric key~$K$.  However, nothing ensures that the person meant
to open door $D$.  If $P$ ever initiates a run with a compromised
door~$C$, the adversary can perform a man-in-the-middle attack,
decrypting using the compromised key $C^{-1}$ and re-encrypting with
$D$'s public key, as elided in the $\cdots$ in Fig.~\ref{fig:doorsep
  first shape}.  To verify this result with \cpsa4, remove the trust
axiom in the doorsep protocol in \texttt{doc/rules.scm} and run \cpsa4.
%
\begin{figure}[tb]
  \[\xymatrix@R=2mm@C=7em{
    \txt{\strut person}&&\txt{\strut door}\\
    \bullet \ar[r]^{\enc{\enc{K}{\iv{P}}}{C}} & \cdots\ar[r]^{\enc{\enc{K}{\iv{P}}}{D}} &
    \bullet\ar@{=>}[d] \\
    & \null &   \bullet\ar@{=>}[d]\ar[l]_{\enc{T}{K}}\\
    &\null\ar[r]^T & \bullet}\]
  \begin{center}
    Uncompromised: $P\quad$ Fresh: $K, T$
  \end{center}
  \caption{DoorSEP Weakness}\label{fig:doorsep first shape}
\end{figure}
%
%   \[
%   \begin{array}{l@{{}:{}}l}
%     P\to A & \enc{\enc{K}{\iv{P}}}{C}\\
%     A\to D & \enc{\enc{K}{\iv{P}}}{D}\\
%     D\to A & \enc{T}{K}\\
%     A\to D & T.
%   \end{array}
%   \]
%
Thus, without additional assumptions, the door cannot authenticate the
person requesting entry.

\begin{figure}
\begin{verbatim}
(defprotocol doorsep basic
  (defrole person
    (vars (d p akey) (k skey) (t text))
    (trace
     (send (enc (enc k (invk p)) d))
     (recv (enc t k))
     (send t)))
  (defrole door
    (vars (d p akey) (k skey) (t text))
    (trace
     (recv (enc (enc k (invk p)) d))
     (send (enc t k))
     (recv t)))
  (defrule trust
    (forall ((z strd) (p d akey))
            (implies
             (and (p "person" z 1)
                  (p "person" "p" z p)
                  (p "person" "d" z d)
                  (non (invk p)))
             (non (invk d))))
    (comment "The trust rule"))
  (comment "Doorsep protocol using unnamed asymmetric keys"))

(defskeleton doorsep
  (vars (p akey))
  (defstrand door 3 (p p))
  (non-orig (invk p))
  (comment "Analyze from the doors's perspective"))
\end{verbatim}
\caption{Door Simple Example Protocol}\label{fig:doorsep}
\end{figure}

But possibly we can trust the person to swipe her badge only in front
of doors our organization controls.  And we can we ensure that our
doors have uncompromised private keys.  If so, then the adversary
cannot exercise the flaw.

We regard this as a \emph{trust assumption}, and we can express it as
an axiom:
%
\begin{axiom}\label{axiom:trust assumption}
  If an uncompromised signing key ${\iv{P}}$ is used to prepare an
  instance of the first DoorSEP message, then its owning principal has
  ensured that the selected door $D$ has an uncompromised private key.
\end{axiom}
%
The responsibility for ensuring the truth of this axiom may be split
between $P$ and the organization controlling $D$.  $P$ makes sure to
swipe her badge only at legitimate doors of the organization's
buildings.  The organization maintains a security posture that
protects the corresponding private keys.

\medskip\noindent\textbf{Is DoorSEP good enough}, assuming the trust
axiom?  Add the trust axiom back to the doorsep protocol in
\texttt{doc/rules.scm} and see.  You should find that the protocol
does its job; namely, ensuring that the door opens only when an
authorized person requests it to open.

\bibliography{cpsa}
\bibliographystyle{plain}

\end{document}