troubleshooting.tex

\chapter {Troubleshooting}
\label{ch:troubleshooting}

The {\cpsa} tool is a complicated one and many errors are possible in
its use.  In this chapter we discuss these errors, from the simplest
to the most complex, and offer suggestions as to how to resolve them.

\section{Non-termination}
\label{sec:bounds}

The {\cpsa} tool is not guaranteed to complete its search on all
well-formed inputs.  The problem space {\cpsa} attempts to perform
includes some Turing-undecidable problems.

Because of this, the tool has two bail-out conditions that users should be
aware of:

\begin{itemize}

\index{strand bound}
\item The {\bf strand bound} causes the tool to abort its analysis if any
skeleton it analyzes has more strands than the bound.  By default, the strand
bound is 12.

\index{step limit}
\item The {\bf step limit} causes the tool to abort its analysis if during
the analysis of a single input \texttt{defskeleton} or \texttt{defgoal}, the
number of skeletons it processes exceeds the limit.  By default, the step limit
is 2000.

\index{depth limit}
\item The {\bf depth limit} causes the tool to not analyze skeletons
  more steps away from the initial point of view than the bound.
  There is no depth limit by default.  Skeletons that are unrealized and not
  analyzed due to the depth limit are marked with ``\texttt{(fringe)}''.

\end{itemize}

If you execute an analysis and the tool says ``Strand bound exceeded''
or ``Step limit reached,'' then that bail-out condition has come into play.
This may indicate an analysis that would never terminate, but it may also be
the case that the strand bound or step limit is too small, and a larger one will
enable the analysis to complete.

Unlike the strand bound and the step limit, the depth limit never
triggers an error condition, and can thus be useful for multi-skeleton
analyses in which one of the earlier skeletons would otherwise have a
non-terminating analysis.

The step limit, depth limit, and strand bound can be adjusted through the
\texttt{limit}, \texttt{depth}, and \texttt{bound} options, respectively.  See
Section~\ref{sec:options}.

\index{interrupting}
Note that sometimes, a user may become impatient waiting for an
analysis to either complete or bail out.  When this happens, the user should
not hesitate to interrupt the tool; the tool will output a partial result that can
be graphed so the user can examing the analysis done so far.

An analysis that doesn't terminate does not necessarily represent an
insecure protocol, it may just indicate a protocol where a more clever
analysis is required than {\cpsa}'s automated one.

\subsection{Configuring the search}
There are cases in which the default {\cpsa} analysis does not
terminate, but a non-default analysis would terminate.  The tool has
several default settings that influence the search but can be
configured:

\begin{itemize}
\index{try-old-strands option}
\index{reverse-nodes option}
\index{options!try-old-strands}
\index{options!reverse-nodes}
\item {\bf Node precedence.}  In a skeleton with multiple unrealized
  receptions, the tool will, by default, focus on the topmost
  unrealized node of the rightmost strand that contains an unrealized
  node.  If you find that an analysis gets into a large search space
  due to exploring those unrealized receptions first, you could alter
  this order with the \texttt{reverse-nodes} or
  \texttt{try-old-strands} options.  The latter will prioritize the
  leftmost strands over the rightmost, while the former will
  prioritize the bottom-most unrealized node in the strand rather than
  the topmost. These can be used individually or jointly, yielding
  three extra non-default search strategies.

\index{check-nonces option}
\index{options!check-nonces}
\item {\bf Critical term precedence.}  Occasionally, a reception will
  arise that is unrealized and multiple critical terms are available.
  In particular, there are cases where a term contains both a
  hard-to-explain encryption and a restricted nonce.  For instance, in
  the Kerberos protocol, the ticket $\enc{k,a,b}{SK(b,s)}$ can serve
  as both a critical encryption (because $SK(b,s)$ may be declared
  non-originating) and a critical term (because $k$ is uniquely
  originating).  By default, {\cpsa} will treat the encryption as the
  critical term because this tends to lead to learning more in fewer
  steps, but this choice can be reversed by using the
  \texttt{check-nonces} option.

\index{priority}
\item {\bf Priority.}  The tool contains an ability to declare a
  priority for certain receptions that differs from the default.
  Priority takes precedence over all other search orderings.  See
  Section~\ref{sec:decl_syntax} for the format requirements for
  declaring priorities, and the \texttt{priority\_test.scm} example in the
  examples directory.

  Note that the default priority is 5, and priority 0 indicates that
  the tool should never bother solving tests at those nodes.  This may
  be of use, for instance, if solving one particular node leads to
  infinite analysis, but other nodes would result in a quick
  determination that a skeleton is dead.
\end{itemize}

\section{Error messages}
\label{sec:errors}

In this section, we provide an alphabetical listing of error messages
/ failures that may arise during {\cpsa} execution.  If you get an error
message not included here, it likely represents a bug and should be reported
to the tool maintainers.

\begin{itemize}
\item \textbf{``[ASSERT FAILED] [...]''}.  This kind of error should
  not occur.  If you see this happen, please contact the tool maintainers
  and make a bug report!

\item \textbf{``Aborting after applying 500 rules and more are
  applicable''}.  This most likely indicates a circular use of rules.

\item \textbf{``Algebra.absenceSubst: bad absence assertion''} or
  \textbf{``Algebra.nullifyOne: unexpected pattern''} The
  \texttt{absent} declaration must be declared on a pair where the
  first element is an \scap{rndx} variable and the second element is 
  an exponent.
  % or a \scap{base} term.
  %
  These errors should not occur if you did not give {\cpsa} an input
  with an absent declaration.

\item \textbf{``Algebra.inv: Cannot invert a variable of sort mesg''}.
  Variables of the \texttt{mesg} sort should never be used as the key
  in an encryption.  {\cpsa} uses a single function symbol to represent
  both symmetric and asymmetric encryption, and when the key is a variable
  of sort \texttt{mesg}, it is ambiguous which is meant.  As a result,
  it is unclear what the decryption key would be for such a message.  When
  {\cpsa} tries to calculate the decryption key when the encryption key
  is a variable of sort \texttt{mesg}, this error is produced.

\item \textbf{``Atom not unique at node''}.  This occurs when a
  formula has been specified including a \texttt{uniq-at} predicate in
  the antecedent that is untrue.

\item \textbf{``Bad char [...]''}.  This error message comes from a
  low-level parser trying to understand S-expressions.  When parsing
  an S-expression, any non-whitespace that isn't a parenthesis is an
  ``atom'' but we expect atoms to be symbols, numbers, or quoted
  strings, and only certain characters are allowed in these.  An atom
  that starts with a digit is expected to be a number, for instance, so
  subsequent non-digits will cause an error of this kind.  The characters
  allowed in symbols include all alphanumeric characters and the following
  punctuation marks: \verb|+, -, *, /, <, =, >, !, ?, :, $,|  \verb|%, _, &, ~, ^|.

\item \textbf{``Bad height'' / ``Bad position in role'' / ``Negative
  position in role''}.  A \texttt{defstrand} includes a specification
  of a height (the length of the instance) but that height must be
  positive and must not exceed the length of the role.

\item \textbf{``Bad str-prec''}.  Your goal included a
  \texttt{str-prec} predicate among node variables associated with
  different roles.  In other words, your formula has attempted to make
  a single strand that includes events from distinct roles.

\item \textbf{``Close of unopened list''}.  Your input has an erroneous
  close-paren.

\item \textbf{``Disallowed bare exponent''}.  See
  Section~\ref{sec:dh}.  The tool requires that within roles and
  skeletons, any exponent occurring outside an exponentiation
  function must be of sort \texttt{rndx}.

\item \textbf{``Domain does not match range''}.  This error message
  occurs when {\cpsa} is trying to understand the variable assignment
  you have specified in a \texttt{defstrand}.  You may have defined
  the value of a parameter more than once, or your definition may have
  a type mismatch.  For instance if $a$ is a parameter role expected
  to be of the name type, and you declare $t$ to be a text variable,
  then including \texttt{(a t)} in a defstrand will produce this
  error.

\item \textbf{``Duplicate role [...] in protocol [...]''}.  The roles
  in a protocol must have distinct names.  This error occurs if you
  have two protocols with the same name.

\item \textbf{``Duplicate variable declaration for [...]''}.  Within
  any \texttt{vars} statement, any symbol may be used for a variable
  name, but each variable name can be declared only once.

\item \textbf{``End of input in string''}.  You included a quote-delimited
  string but didn't close it before the end of the input file.

\item \textbf{``Equals not allowed in antecedent''}.  The \texttt{equals}
  predicate may only be used on the conclusion side of a \texttt{defgoal}.

\item \textbf{``Expansion limit exceeded''}.  This most likely indicates
  a circular use of macros.  The limit of expansion of a macro within a macro is
  hard-coded in the tool as depth 1000.

\item \textbf{``Expecting [...] to be [a/an ...]''}.  You have a type
  error in your use of a function symbol.  For instance if
  \texttt{(pubk a)} is to be loaded within a particular variable
  declaration scope, the $a$ variable should be of the $\scap{name}$
  sort.

\item \textbf{``Expecting a node variable'' / ``Expecting an algebra
  term''}.  Certain predicates within a \texttt{defgoal} expect one of
  their inputs to be a declared node variable (or to be a non-node
  variable).  If a variable used in such an input is declared
  otherwise, this error message is produced.

\item \textbf{``Expecting an atom''}.  Certain declarations, in particular
  the \texttt{uniq-orig}, \texttt{uniq-gen}, and \texttt{non-orig} ones,
  are expected to be used on atomic terms rather than compound ones.

\item \textbf{``Expecting terms in algebra [...]''}. This is a
  historical artifact resulting from the fact that the algebra has two
  names. If you specify one name as a runtime parameter (or in the
  herald) that is different from the name used in the
  \texttt{defprotocol} form, this error will result.

\item \textbf{``Expts must first be received, rndxs first
    sent''}. If the first occurrence of a variables of the
  \texttt{expt} sort is in a transmission, it could resolve to any
  multiplication of exponents and so is underspecified. When receiving
  an exponent, there is no way to ensure it was not chosen to be some
  multiplication of other exponents, so we can assume its sort is
  \texttt{rndx}. Hence the rule described by the error. 
% \item \textbf{``Role not well formed: variable [...] not
%     obtained''}.  Variables of the %$\scap{base}$ or
%   $\scap{expr}$ sort must be ``obtained'' when used in roles, meaning
%   that the first occurrence must be in a reception.
  
\item \textbf{``Identifier [...] unknown''}.  This is a relatively common
  user-caused error that occurs when you try to use a variable not declared
  in your \texttt{vars} declaration.

\item \textbf{``Include depth exceeded with file [...]''}.  Most
  likely, this indicates a circular use of the \texttt{include}
  command.  The limit of inclusion within an included file is depth
  16.

\item \textbf{``Keyword [...] unknown''}.  The tool was expecting the symbol
  to specify an algebra function symbol, but it didn't match any of the available
  ones.  This most commonly indicates that the user forgot to include a
  function symbol name at the beginning of a list when describing a term.  One of
  the most common forms of this mistake is to include \texttt{(send (a b))} in
  a trace of a role, when the user intended to model the sending of the pair $(a,b)$.
  The proper input would be \texttt{(send (cat a b))}.

  Because of this type of mistake, it is recommended to avoid using variables
  in your model that are the same as function symbol names such as
  ``ltk'' or ``pubk''.

\item \textbf{``In a rule equality check, cannot find a binding for
  some variable''}.  An equality in a rule is receiving a variable
  that has not been bound by a length or parameter predicate.  Try
  moving the equality to the end of the conjunction in which it
  occurs.

\item \textbf{``In rule [...], parameter predicate for [...] did not
  get a strand''}.  This message occurs when a strand variable is not
  bound by a length predicate.

\item \textbf{``In rule [...], [...] did not get a strand''}.
  This message occurs when a strand variable is not bound by a length
  predicate.

\item \textbf{``In rule [...], [...] did not get a term}.  This
  message occurs when an algebra variable is not bound by a parameter
  predicate.

\item \textbf{``Malformed [...]''}.  Generally speaking, this indicates
  a syntax error.  Consult the grammar in Chapter~\ref{ch:input} for the
  syntax requirements for the type of object the tool claims was malformed.
  Double-check that you have spelled required keywords correctly, and that
  your parentheses are matched.

\item \textbf{``Malformed association list''}.  This refers to one of
  the ``-alist'' symbols in the grammar; these may occur in skeletons,
  goals, protocols, or roles.

  Association lists are lists of S-expressions, each of which is a
  list that starts with a symbol.  This error would occur if you had,
  for instance, a symbol or a number, or an S-expression starting with
  a number as an input to a \texttt{defrole} or \texttt{defskeleton}.

\item \textbf{``Malformed input''}.  Top level S-expressions in your
  input file must be one of the following: \texttt{defprotocol,
    defskeleton, defgoal, comment,} or \texttt{herald}.  The tool also
  recognizes \texttt{defpreskeleton} as a synonym for
  \texttt{defskeleton}.  If you have an S-expression at the top level
  that is other than one of these, this is the error message you will
  see.

\item \textbf{``Malformed pair -- nodes in same strand''}.  In a
  \texttt{defskeleton} you are prohibited from specifying orderings
  between nodes in the same strand.

  This is not the case for \texttt{leadsto} relationships.

\item \textbf{``No strands''}.  Your \texttt{defskeleton} did not include
  any strands at all; it must include at least one.

\item \textbf{``Node occurs in more than one role predicate''}.  Node
  variables in a goal must occur within a role position predicate, but
  should not occur within more than one within their defined scope.

\item \textbf{``Priority declaration disallowed on [...]''}.
  Prioritization has no effect except on events that need an
  explanation.  If you try to change the default priority of a
  \texttt{send} or \texttt{stor} event, this is assumed to be a
  mistake and the tool produces this error.

\item \textbf{``Protocol [...] unknown''}.  This error occurs when you
  have a \texttt{defskeleton} or \texttt{defgoal} with a protocol name
  not matching any \texttt{defprotocol} so far present in the file.

\item \textbf{``Role [...] not found in [...]''}.  You included a
  \texttt{defstrand} referencing a role that does not exist in the
  protocol definition.

\item \textbf{``Role in parameter pred differs from role position
  pred''}.  A node variable in a formula should occur in a role
  position predicate but may also occur in node parameter predicates.
  However, node parameter predicates for a given node variable should
  match the role of the role position predicate the variable occurs
  in.

\item \textbf{``Role not well formed: role trace is a prefix of a
    listener''}.  {\cpsa} disallows the use of roles that begin with
  the reception of some message followed by the transmission of that
  same message, because there is an ambiguity as to whether an
  instance is a listener or an instance of a protocol role.  This
  should not be a problem because beginning a role in this manner is
  quite unusual, but if it is necessary for you to do so we recommend
  the reception be paired with a tag constant such as \texttt{(cat
    "regular role" [...])}.

\item \textbf{``Role not well formed: non-orig [...] carried''}.  The
  \texttt{non-orig} declaration specifies that a certain atomic value
  not be carried (see Section~\ref{sec:secrecy_assumptions}).  You
  have made such a declaration but a plain (full-height) instance of
  your role violates the rule.

\item \textbf{``Role not well formed: uniq-orig/uniq-gen [...] doesn't
    originate/generate''}. The \texttt{uniq-orig} declaration in a
  role requires the declared value to originate, i.e., its first
  carried occurrence is in a transmission. The role probably has an
  earlier carried reception of the value. Similarly \texttt{uniq-gen}
  requires the first occurrence (whether carried or not) to be in a
  transmission. See Section~\ref{sec:secrecy_assumptions} for an
  explanation of ``carried.''
  % The \texttt{uniq-orig} declaration states not only that the
  % declared value originates on a regular strand uniquely (see
  % Section~\ref{sec:secrecy_assumptions}), but also states that the
  % apparent origination point is the unique origination point of that
  % value.  As such, you may only use the \texttt{uniq-orig}
  % declaration on a value that does originate somewhere.  If you
  % declare a value \texttt{uniq-orig} on a role but it does not
  % originate on that role, you get this error. Similarly for
  % \texttt{uniq-gen}

\item \textbf{``Role not well formed: variable [...] not acquired''}.
  Variables of the $\scap{mesg}$ sort must be ``acquired'' when used
  in roles.  This means that the first occurrence of the variable must
  be a \emph{carried} occurrence in a reception event.  See
Section~\ref{sec:secrecy_assumptions} for an explanation of
``carried.''


\item \textbf{``[Role / Skeleton] not well formed: inequality
    conditions violated''}.  A \texttt{neq} declaration is false where
  it is first declared: in a role or skeleton definition.

\item \textbf{``[Role / Skeleton] not well formed: lt declarations
    form a cycle''}.  The \texttt{lt} declarations present in a role
  or in a skeleton are already violated in the role or skeleton
  definition.

\item \textbf{``[Role / Skeleton] not well formed: subsort
    requirements violated''}.  The \texttt{subsort} declarations
  present in the role or skeleton being defined are already violated.

\item \textbf{``Skeleton not well formed: a variable in [...] is not in some trace''}.
  A \texttt{defskeleton} causes this error when a variable used in a declaration
  does not appear in any of the traces.

\item \textbf{``Skeleton not well formed: cycle found in ordered pairs''}.
  The ordering edges (strand succession plus ordered pairs) of a skeleton should form
  an acyclic graph.  A cycle represents circular causality which should not be possible in
  any real execution.

\item \textbf{``Skeleton not well formed: non-orig [...] carried''}.  The \texttt{non-orig}
  declaration specifies that a certain atomic value not be carried
  (see Section~\ref{sec:secrecy_assumptions}).  You have made such a declaration but your
  \texttt{defskeleton} violates the rule.

\item \textbf{``Skeleton not well formed: ordered pairs not well formed''}.
  This error occurs when an ordering is specified between the wrong types of events.
  In {\cpsa}, an ordering must be such that the earlier node has an outgoing type, so
  for instance an ordering directly between two reception events is disallowed.

% \item \textbf{``Skeleton not well formed: uniq-orig [...] doesn't
%     originate''}.  The \texttt{uniq-orig} declaration states not only
%   that the declared value originates on a regular strand uniquely (see
%   Section~\ref{sec:secrecy_assumptions}), but also states that the
%   apparent origination point is the unique origination point of that
%   value.  As such, you may only use the \texttt{uniq-orig} declaration
%   on a value that does originate somewhere.  If you declare a value
%   \texttt{uniq-orig} on a skeleton but it does not originate in the
%   skeleton, you get this error.

%   Similarly, \textbf{``...: uniq-gen [...] doesn't generate''}
%   represents a detected error in that \texttt{uniq-gen} states that
%   not only does the given value generate (see
%   Section~\ref{sec:secrecy_assumptions}) uniquely, but that its apparent
%   generation point is that generation point.  As such, a generation
%   point is expected.

\item \textbf{``Sort [...] not recognized''}.  You attempted to declare a variable
  to be of a sort not present in the algebra. There is likely a typo
  in one of the sorts.

\item \textbf{``Terms in [role/skeleton] not well formed''}.  This error occurs
  when you have constructed a term using a function symbol that
  expects inputs of a certain sort, but your inputs are not of that
  sort.  For instance, in \texttt{(ltk a b)}, \texttt{a} and
  \texttt{b} must be variables of the \texttt{name} sort, or they are not
  well-formed.  To resolve: double-check your variable declarations and
  your use of function symbols.

  % This may also occur if you use the \texttt{node} sort in a role or skeleton; that
  % sort should only be used in a goal declaration.

\item \textbf{``Too many locations in declaration''}.  You have a
  native declaration that appears to include two or more
  locations in it.  All native declarations allow at most one
  location.

\item \textbf{``Type mismatch in equals''}.  The \texttt{equals} predicate
  in a \texttt{defgoal} can be used to compare node variables or to compare
  algebra variables, but cannot be used to compare node variables to algebra
  variables.

\item \textbf{``Unbound variable in [...]''}.  In a \texttt{defgoal},
  variables must meet specific binding requirements.  See Chapter~\ref{ch:goals}
  for details.  This error indicates that you have provided a formula that the
  tool rejects for this reason.

\item \textbf{``Unexpected end of input in list''}.  One of the most frequent
  user errors---you didn't include close parens for all your S-expressions.

\end{itemize}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "cpsa4manual"
%%% End: