bcasyntax.tex

The complete syntax for the analyzer using the Basic Crypto Algebra is
shown in Tables~\ref{tab:syntax} and~\ref{tab:goal}.  The start
grammar symbol is \textsc{file}, and the terminal grammar symbols
are: \textsc{(, ), symbol, string, integer,} and the constants set in
typewriter font.  The language used for stating security goals is in
Table~\ref{tab:goal}.  The goal language adds the sort
symbol \texttt{node}.

The \textsc{alist}, \textsc{prot-alist}, \textsc{role-alist},
\textsc{skel-alist}, and \textsc{goal-alist} productions are
Lisp style association lists, that is, lists of key-value pairs, where
every key is a symbol.  Key-value pairs with unrecognized keys are
ignored, and are available for use by other tools.  On output,
unrecognized key-value pairs are preserved when printing protocols,
but elided when printing skeletons.

\begin{table}
\newcommand{\sym}[1]{\textup{\texttt{#1}}}
\begin{center}\scshape
\begin{tabular}{rcl}
file&$\leftarrow$&herald?~form+
\\herald&$\leftarrow$&
(\sym{herald}~title~alist)
\\title&$\leftarrow$&$\mbox{symbol}\mid\mbox{string}$
\\form&$\leftarrow$&
$\mbox{comment}\mid\mbox{protocol}\mid\mbox{skeleton}\mid\mbox{goal}$
\\ comment&$\leftarrow$&
(\sym{comment}~\ldots)
\\ protocol&$\leftarrow$&
(\sym{defprotocol} id alg role+ rule$\ast$ prot-alist)
\\ id&$\leftarrow$&symbol
\\ alg&$\leftarrow$&symbol
\\ role&$\leftarrow$&
(\sym{defrole} id vars trace role-alist)
\\ vars&$\leftarrow$&
(\sym{vars} decl$\ast$)
\\ decl&$\leftarrow$&
(id+ sort)
\\ sort&$\leftarrow$&
$\sym{text} \mid \sym{data} \mid \sym{name} \mid \sym{skey}
\mid \sym{akey}\mid\sym{mesg}\mid\sym{chan}$
\\ trace&$\leftarrow$&(\sym{trace} event+)
\\ event&$\leftarrow$&
$(\sym{send}\mbox{ id? term})\mid(\sym{recv}\mbox{ id? term})$
\\ term&$\leftarrow$&
$\mbox{id}\mid\mbox{akey}\mid(\sym{ltk}\mbox{ id id})\mid\mbox{string}\mid(\sym{cat}\mbox{ term+})$
\\ &$\mid$&$(\sym{enc}\mbox{ term+ term})\mid(\sym{hash}\mbox{ term+})$
\\ akey&$\leftarrow$&
$\mbox{id}\mid(\sym{invk}\mbox{ id})
\mid(\sym{pubk}\mbox{ id})
\mid(\sym{privk}\mbox{ akey})$
\\ &$\mid$&$(\sym{pubk}\mbox{ id}\mbox{ string})
\mid(\sym{privk}\mbox{ id}\mbox{ string})$
\\ role-alist&$\leftarrow$&$
(\sym{non-orig}\mbox{ ht-term}\ast)\mbox{ role-alist}$
\\ &$\mid$&$(\sym{pen-non-orig}\mbox{ ht-term}\ast)\mbox{ role-alist}$
\\ &$\mid$&$(\sym{uniq-orig}\mbox{ term}\ast)\mbox{ role-alist}$
\\ &$\mid$&$(\sym{conf}\mbox{ id}\ast)\mbox{ role-alist}$
\\ &$\mid$&$(\sym{auth}\mbox{ id}\ast)\mbox{ role-alist}$
\\ ht-term&$\leftarrow$&term${}\mid{}$(integer term)
\\ rule&$\leftarrow$&
(\sym{defrule} id sentence rule-alist)
\\ rule-alist&$\leftarrow$&$\ldots$
\\ prot-alist&$\leftarrow$
&$(\sym{lang}\mbox{ ldecl}\ast)\mbox{ prot-alist}\mid{}$\ldots
\\ ldecl&$\leftarrow$&$(\sym{symbol}{\mathord +}\mbox{ kind})$
\\ kind&$\leftarrow$&$\sym{atom}\mid\sym{akey}\mid\sym{hash}\mid
(\sym{tupl}\mbox{ integer})$
\\ &&$\sym{enc}\mid\sym{senc}\mid\sym{aenc}\mid\sym{sign}$
\end{tabular}
\end{center}
\caption{{\cpsa} Syntax}\label{tab:syntax}
\end{table}

\begin{table}
\newcommand{\sym}[1]{\textup{\texttt{#1}}}
\begin{center}\scshape
\begin{tabular}{rcl}
   skeleton&$\leftarrow$&
(\sym{defskeleton} id vars
\\ &&\qquad strand+ skel-alist)
\\ strand&$\leftarrow$&
(\sym{defstrand} id integer maplet$\ast$)
\\ &$\mid$&(\sym{deflistener} term)
\\ maplet&$\leftarrow$&
(term term)
\\ skel-alist&$\leftarrow$&$(\sym{non-orig}\mbox{ term}\ast)\mbox{ skel-alist}$
\\ &$\mid$&$(\sym{pen-non-orig}\mbox{ term}\ast)\mbox{ skel-alist}$
\\ &$\mid$&$(\sym{uniq-orig}\mbox{ term}\ast)\mbox{ skel-alist}$
\\ &$\mid$&$(\sym{conf}\mbox{ id}\ast)\mbox{ skel-alist}$
\\ &$\mid$&$(\sym{auth}\mbox{ id}\ast)\mbox{ skel-alist}$
\\ &$\mid$&$(\sym{facts}\mbox{ fact$\ast$})\mbox{ skel-alist}$
\\ &$\mid$&$(\sym{precedes}\mbox{ node-pair}\ast)\mbox{ skel-alist}\mid\ldots$
\\ node-pair&$\leftarrow$&
(node node)
\\ node&$\leftarrow$&
(integer integer)
\\ fact&$\leftarrow$&(id fterm$\ast$)
\\ fterm&$\leftarrow$&term $\mid$ integer
\\
\\ goal&$\leftarrow$&
(\sym{defgoal} id sentence+ goal-alist)
\\ sentence&$\leftarrow$&(\sym{forall} (decl$\ast$) implication)
\\ implication&$\leftarrow$&
(\sym{implies} \mbox{antecedent} \mbox{conclusion})
\\ conclusion&$\leftarrow$&(\sym{false})
   $\mid$ existential $\mid$ (\sym{or} existential$\ast)$
\\ existential&$\leftarrow$&(\sym{exists}
(decl$\ast$) antecedent) $\mid$ antecedent
\\ antecedent&$\leftarrow$& atomic $\mid$ (\sym{and} atomic$\ast$)
\\ atomic&$\leftarrow$&(\sym{p} roleid svar hgt)
\\ &$\mid$&(\sym{p} roleid param svar term)
\\ &$\mid$&(\sym{prec} svar pos svar pos)
\\ &$\mid$&(\sym{non} term) $\mid$ (\sym{pnon} term)
\\ &$\mid$&(\sym{uniq} term) $\mid$ (\sym{uniq-at} term svar pos)
\\ &$\mid$&(\sym{conf} id) $\mid$ (\sym{auth} id)
\\ &$\mid$&(\sym{fact} id term$\ast$) $\mid$ (= term term)
\\ roleid&$\leftarrow$& string
\\ hgt&$\leftarrow$& integer
\\ pos&$\leftarrow$& integer
\\ svar&$\leftarrow$& id
\\ param&$\leftarrow$& string
\end{tabular}
\end{center}
\caption{{\cpsa} Syntax Continued}\label{tab:goal}
\end{table}

The contents of a file can be interpreted as a sequence of
S-expressions.  The S-expressions used are restricted so that most
dialects of Lisp can read them, and characters within symbols and
strings never need quoting.  Every list is proper.  An S-expression
atom is either a \textsc{symbol}, an \textsc{integer}, or
a \textsc{string}.  The characters that make up a symbol are the
letters, the digits, and the special characters in
``\verb|-*/<=>!?:$%_&~^+|''.  A symbol may not begin with a digit or a
sign followed by a digit.  The characters that make up a string are
the printing characters omitting double quote and backslash, except
when double quote and backslash are escaped using the backslash
character.  Double quotes delimit a string.  A comment\index{comments}
begins with a semicolon, or is an S-expression list at top-level that
starts with the \texttt{comment} symbol.