cpsa-2.5.3: doc/cpsagoals.tex

\documentclass[12pt]{article}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{graphicx}
\usepackage{alltt}
\input{macros}

\newcommand{\sym}[1]{\textup{\texttt{#1}}}

\title{CPSA and Formal Security Goals}
\author{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 node))
    (implies
     (and (p "init" 2 z0)
      (p "init" "n1" z0 n1) (p "init" "b" z0 b)
      (non (privk b)) (uniq n1))
     (exists ((z1 node))
      (and (p "resp" 1 z1) (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$\ast$)
  \end{tabular}
\end{center}

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

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 position and role
parameter predicates.  Protocol specific predicates are distinguished
from protocol independent predicates by being composed of three
tokens, the first of which is \texttt{p}.

The first line of the table gives the syntax of a role position
predicate.  It contains three tokens, \texttt{p}, a string that names
a role, and an integer that specifies a position within the trace of
the role.  That is, for role~$r$ with a trace of length~$n$, there
are~$n$ role position predicates, \mbox{\texttt{p} $r$ $i$}, for
$0\leq i < n$.  Thus \verb|(p "init" 2 z0)| is an atomic formula using
the role position predicate for position 2 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{node} occurs in a formula, its position
must be specified using a role position 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 pos & \dom{node} & \mbox{Role position} \\
    \scshape\sym{p} role param & $\dom{node}\times\dom{mesg}$
    & \mbox{Role parameter} \\
    \sym{str-prec}& $\dom{node}\times\dom{node}$
    & \mbox{Precedes on strand} \\
    \sym{prec}& $\dom{node}\times\dom{node}$
    & \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{node}$
    & \mbox{Unique origination at node} \\
    $=$ & $\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" 2 z0)
  (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" 2 z0)} is called a role position
formula.  A skeleton~$k$ satisfies the formula if \texttt{z0} maps to
a node $n=(s,2)$ 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" 2 z0)} when \texttt{z0} maps to $(0,2)$.

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 a node $n=(s,i)$ in~$k$ 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,2)$ and \texttt{n1} maps to the
message algebra term \texttt{n1}.

Collectively, a skeleton satisfies the formula
\begin{quote}
\begin{verbatim}
(and (p "init" 2 z0)
     (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}\mapsto(0,2)\}\] 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 z0)} added is satisfied by the shape using the mapping $\mbox{\tt
  z0}\mapsto(0,2)$ and $\mbox{\tt z1}\mapsto(1,1)$.

The \texttt{str-prec} predicate is used to assert a node precedes another
node and that both are on the same strand.

The \texttt{uniq-at} predicate is used to assert not only that an atom
uniquely originates, but also the node at which it originates.  It is
typically used in conjunction with a \texttt{str-prec} formula.  In
the Figure~\ref{fig:ns init} goal, the \texttt{(uniq n1)} formula
could have been replaced by
\begin{quote}
\begin{verbatim}
(p "init" 0 z2) (str-prec z2 z0) (uniq-at n1 z2),
\end{verbatim}
\end{quote}
where \texttt{z2} has sort \texttt{node}.  The extracted point of view
skeleton is the same.  Of course, an error is raised if the role
position formula is replaced by \texttt{(p "init" 1 z2)}.

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 node))
    (implies
     (and (p "resp" 2 z0) (p "resp" "n2" z0 n2)
      (p "resp" "a" z0 a) (p "resp" "b" z0 b)
      (non (privk a)) (uniq n2))
     (exists ((z1 node))
      (and (p "init" 1 z1) (p "init" "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 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 2))))
\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 2))).
\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 node))
    (implies
     (and (p "init" 2 z0) (p "init" "n1" z0 n1)
      (p "init" "a" z0 a) (p "init" "b" z0 b)
      (p "" 0 z1) (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 "" 0 z1) (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}.

\subsection{Unilateral Authentication}\label{sec:unilateral}

This example focuses on unilateral authentication.  To best visualize
this example, process the sample file \texttt{goal.scm} with {\cpsa}
and display its output in a browser.

The protocol and its goal are shown in Figure~\ref{fig:unilateral}.
The goal asserts that if a realized skeleton contains a full length
initiator strand that uniquely generates \texttt{n1}, and
peer~\texttt{a}'s private key is uncompromised, then the skeleton will
contain a responder strand that agrees with the initiator on the
name~\texttt{a}.  When given as input, {\cpsa} verifies that the goal
is true in all executions of the protocol.

\begin{figure}
\begin{minipage}{2.7in}
\begin{verbatim}
(defprotocol unilateral basic
  (defrole init
    (vars (a name) (n text))
    (trace
     (send (enc n (pubk a)))
     (recv n)))
  (defrole resp
    (vars (a name) (n text))
    (trace
     (recv (enc n (pubk a)))
     (send n))))
\end{verbatim}
\end{minipage}\hfil
\begin{minipage}{3.0in}
\begin{verbatim}
(defgoal unilateral
  (forall ((a name) (n text)
           (z0 node))
   (implies
    (and (p "init" 1 z0)
     (p "init" "n" z0 n)
     (p "init" "a" z0 a)
     (non (privk a)) (uniq n))
    (exists ((z1 node))
     (and (p "resp" 1 z1)
      (p "resp" "a" z1 a))))))
\end{verbatim}
\end{minipage}
\caption{Unilateral Protocol and Authentication Goal}\label{fig:unilateral}
\end{figure}

\begin{figure}
\begin{quote}
\begin{verbatim}
(defgoal ns
  (forall ((a name) (n text) (z0 node))
   (implies
    (and (p "init" 1 z0) (p "init" "n1" z0 n)
     (p "init" "b" z0 a) (non (privk a)) (uniq n))
    (exists ((z1 node))
     (and (p "resp" 1 z1) (p "resp" "b" z1 a))))))
\end{verbatim}
\end{quote}
\caption{Translated Unilateral Goal for the
  Initiator}\label{fig:unilateral ns init}
\end{figure}

\begin{figure}
\begin{quote}
\begin{verbatim}
(defgoal ns
  (forall ((a name) (n text) (z0 node))
   (implies
    (and (p "resp" 2 z0) (p "resp" "n2" z0 n)
     (p "resp" "a" z0 a) (non (privk a)) (uniq n))
    (exists ((z1 node))
     (and (p "init" 2 z1) (p "init" "a" z1 a)))))
\end{verbatim}
\end{quote}
\caption{Translated Unilateral Goal for the
  Responder}\label{fig:unilateral ns resp}
\end{figure}

In Section~\ref{sec:ns resp}, a goal written for the Needham-Schroeder
Protocol was reused to analyze the Needham-Schroeder-Lowe Protocol.
We now use the unilateral authentication goal to analyze
Needham-Schroeder.

Consider the goal in Figure~\ref{fig:unilateral ns init}.  This goal
is the result of translating the Unilateral role position and
parameter predicates as follows.
\begin{center}
\begin{tabular}{l@{$\quad\rightarrow\quad$}l}
  \texttt{p "init" "n"}&\texttt{p "init" "n1"}\\
  \texttt{p "init" "a"}&\texttt{p "init" "b"}\\
  \texttt{p "resp" "a"}&\texttt{p "resp" "b"}
\end{tabular}
\end{center}
When given Figure~\ref{fig:unilateral ns init} as input, {\cpsa}
verifies that the goal is true in all executions of the protocol.

There is another way to translate the Unilateral goal.
\begin{center}
\begin{tabular}{l@{$\quad\rightarrow\quad$}l}
  \texttt{p "init" 1}&\texttt{p "resp" "2"}\\
  \texttt{p "init" "n"}&\texttt{p "resp" "n2"}\\
  \texttt{p "init" "a"}&\texttt{p "resp" "a"}\\
  \texttt{p "resp" "1"}&\texttt{p "init" "2"}\\
  \texttt{p "resp" "a"}&\texttt{p "init" "a"}
\end{tabular}
\end{center}
When given Figure~\ref{fig:unilateral ns resp} as input, {\cpsa}
verifies that the goal is true in all executions of the protocol.

{\cpsa} has demonstrated two ways in which Needham-Schroeder achieves
the goals of the Unilateral Protocol.

\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 node))
    (implies
     (and (p "init" 1 z0) (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 node))
      (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))
  (forall ((a b name) (n text) (z0 node))
   (implies
     (and (p "init" 1 z0) (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 node))
      (and (p "resp" 1 z1) (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 z-0 node))
    (implies
      (and (p "init" 0 z) (p "init" 2 z-0)
        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
        (p "init" "a" z-0 a) (p "init" "b" z-0 b)
        (str-prec z z-0) (non (privk b)) (uniq-at n1 z))
      (exists ((n2-0 text) (z-1 z-2 z-3 node))
        (and (p "init" 1 z-1) (p "resp" 0 z-2)
          (p "resp" 1 z-3) (p "resp" "n2" z-3 n2-0)
          (p "resp" "n1" z-3 n1) (p "resp" "b" z-3 b)
          (p "resp" "a" z-3 a) (prec z z-2) (prec z-3 z-1)
          (str-prec z z-1) (str-prec z-1 z-0)
          (str-prec z-2 z-3))))))
\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}.  {\cpsa} comes with a
Prolog program that translates shape analysis sentences into Prover9
syntax~\cite{prover9}.  Prover9 can then be used to perform the
required theorem-proving.

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.

\bibliography{cpsa}
\bibliographystyle{plain}

\end{document}