cpsa-2.2.3: doc/bcasyntax.tex

The complete syntax for the analyzer using the Basic Crypto Algebra is
shown in Table~\ref{tab:syntax}.  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 \textsc{alist}, \textsc{prot-alist}, \textsc{role-alist},
and \textsc{skel-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}$
\\ comment&$\leftarrow$&
(\sym{comment}~\ldots)
\\ protocol&$\leftarrow$&
(\sym{defprotocol} id alg role+ 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}$
\\ trace&$\leftarrow$&(\sym{trace} event+)
\\ event&$\leftarrow$&
$(\sym{send}\mbox{ term})\mid(\sym{recv}\mbox{ term})$
\\ term&$\leftarrow$&
$\mbox{id}\mid(\sym{pubk}\mbox{ id})
\mid(\sym{privk}\mbox{ id})
\mid(\sym{invk}\mbox{ id})$
\\ &$\mid$&$(\sym{pubk}\mbox{ id}\mbox{ string})
\mid(\sym{privk}\mbox{ id}\mbox{ string})$
\\ &$\mid$&$(\sym{ltk}\mbox{ id id})\mid\mbox{string}\mid(\sym{cat}\mbox{ term+})$
\\ &$\mid$&$(\sym{enc}\mbox{ term+ term})$
\\ role-alist&$\leftarrow$&$
(\sym{non-orig}\mbox{ ht-term}\ast)\mbox{ role-alist}$
\\ &$\mid$&$(\sym{uniq-orig}\mbox{ term}\ast)\mbox{ role-alist}\mid\ldots$
\\ ht-term&$\leftarrow$&term${}\mid{}$(integer term)
\\ prot-alist&$\leftarrow$&$\ldots$
\\ 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{uniq-orig}\mbox{ term}\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)
\end{tabular}
\end{center}
\caption{{\cpsa} Syntax}\label{tab:syntax}
\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.  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.