\section{Observer theory reduction and consistency}
\label{s-otd}

We now discuss our formalisation of observer theory and 
its consistency properties in Isabelle/HOL. 

The datatype for messages is represented in Isabelle/HOL as follows.
\begin{verbatim}
datatype msg = Name nat | Rigid nat | Mpair msg msg | Enc msg msg
\end{verbatim}
A observer theory, as already noted, is a finite set of pairs of messages.
In Isabelle, we just use a set of pairs, so the finiteness condition appears 
in the Isabelle statements of many theorems. 
The judgment $\Gamma \vdash M \eqm N$ is represented by $(\Gamma, (M, N))$,
or, equivalently in Isabelle, $(\Gamma, M, N)$.

In Isabelle we define, inductively, a set of sequents \texttt{indist}
which is the set of sequents derivable in the proof system for
message equivalence (Figure~\ref{f-msg-ind}). Subsequently we found it 
helpful to define the corresponding set of rules explicitly, 
calling them \texttt{indpsc}.
The rules for message synthesis, given in Figure~\ref{f-msg}, 
are just a projection to one component of the rule set 
\texttt{indpsc}; we call this projection \texttt{smpsc}.
It is straightforward to extend the notion of a projection
on rule sets, so we can define the rules for message synthesis
as simply \texttt{smpsc} = $\pi_1$(\texttt{indpsc}).
%% In mathematical notation we can just
%% write $\pi_1$ or $\pi_2$ to denote the projection to the first or second
%% component, for pairs, theories, sequents and rules,
%% and also the marked message pairs and bi-traces introduced in \S\ref{s-bt};
%% thus we could write \texttt{smpsc} = $\pi_1$(\texttt{indpsc}), i.e.,
%% the rule set \texttt{smpsc} is the first projection of the rule set \texttt{indpsc}.
The formal expression in Isabelle is more complex: see Appendix~\ref{v-smpsc}.
% But the definition in Isabelle, \texttt{smpsc\_def}, uses
% \texttt{seqmap fst}, which applies \texttt{fst} (ie, $\pi_1$)
% to each member of the antecedent and to the consequent of a sequent,
% and \texttt{pscmap} $f$, which applies $f$ to each premise and to the
% conclusion of a rule.
Likewise, we write \textit{pair}$(X)$ to turn each message $M$ into the pair 
$(M,M)$ in a theory, sequent, rule or bi-trace $X$.

The following lemma relates message synthesis and message equivalence. 
%% Our definition for message synthesis rules is \texttt{smpsc} = $\pi_1$(\texttt{indpsc}),
%% but Lemma~\ref{l-smpsc}\ref{smpsc-alt} provides an alternative definition.
Lemma \ref{l-smpsc}\ref{smpsc-ex-indpsc-der} depends on theory consistency, 
to be introduced later.

% where $R'$ is obtained from $R$ by
% converting every message $M$ to a pair $(M, M)$.
% This uses \texttt{pair}, where $\texttt{pair}\ x = (x,x)$.
%% Similarly we have Lemma~\ref{l-smpsc}\ref{slice-derrec-smpsc-empty} and
%% \ref{derrec-smpsc-eq};
%% \ref{smpsc-ex-indpsc-der} is non-trivial
%% and depends on the assumption of theory consistency, to be introduced later.
% The theorem \texttt{slice\_derrec\_smpsc\_empty} reflects the fact that
% an entire proof can be projected to the first component of each pair.
% A converse result, \texttt{smpsc\_ex\_indpsc\_der},
% is complicated by the $(el)$
% rule, and requires the condition of theory consistency (introduced later).

\begin{lemma} \label{l-smpsc}
\begin{enumerate}
\item \texttt{\upshape(smpsc\_alt)} \label{smpsc-alt}
Rule $R \in \texttt{smpsc}$ iff
$\textit{pair} (R) \in \texttt{indpsc}$ 
\item \texttt{\upshape(slice\_derrec\_smpsc\_empty)}
\label{slice-derrec-smpsc-empty}
if $\Gamma \vdash M \eqm N$ then $\pi_1 (\Gamma) \vdash M$ 
\item \texttt{\upshape(derrec\_smpsc\_eq)} \label{derrec-smpsc-eq}
$\Sigma \vdash M$ if and only if $\textit{pair} (\Sigma) \vdash M \eqm M$ 
\item \texttt{\upshape(smpsc\_ex\_indpsc\_der)} \label{smpsc-ex-indpsc-der}
if $\pi_1 (\Gamma) \vdash M$ and $\Gamma$ is consistent, then 
there exists $N$ such that $\Gamma \vdash M \eqm N$
\end{enumerate}
\end{lemma}

\subsection{Decidability of $\vdash$ and computability of theory reduction}
\label{s-dec-red}

The first step towards deciding theory consistency is to define a notion
of {\em theory reduction}. Its purpose is to extract a ``kernel'' of the theory
with no redundancy, that is, no pairs in the kernel are derivable from
the others.  
We need to establish the decidability of $\vdash$, and 
then termination of the theory reduction. 
In \cite{tiu-trace-based-bisim-abs}, Tiu observes that 
$\Gamma \vdash M \leftrightarrow N$ is decidable, because the right rules 
(working upwards) make the right-hand side messages smaller, and the left rules
saturate the antecedent theory with more pairs of smaller messages.
Hence for a given end sequent, there are only finitely many possible
sequents which can appear in any proof of the sequent.
%
%% However, since the first premise of the $(el)$ rule (in the original
%% version) may be larger than the conclusion,
%% we found that some attempts to formalise the proof would fail.
%% A correct approach is to argue that for a given end-sequent, 
%% there are only finitely many possible sequents which can appear 
%% in any proof of that end-sequent.
Some results relevant to this argument for decidability are presented in
Appendix~\ref{app-vdash-decidable}.
Here we present an alternative proof for the decidability
of $\vdash$ and termination of theory reduction.

%% Here we present an alternative approach which also provides a more
%% practical means of efficiently deciding $\vdash$, in conjunction with 
%% theory reduction, which is also needed for the decidability of theory
%% consistency (\S\ref{s-thy-cons}).

Tiu \cite[Definition~4]{tiu-trace-based-bisim-abs} defines a reduction relation
of observer theories:
\begin{eqnarray*}
{\Gamma, (\pairM,\pairN)} & \longrightarrow &
  {\Gamma, (M_a, N_a), (M_b, N_b)} \\
{\Gamma, (\encM,\encN)} & \longrightarrow & {\Gamma, (M_p, N_p), (M_k, N_k)}
 \\
 && \mbox{ if } {\Gamma, (\encM,\encN) \vdash M_k \leftrightarrow N_k}
\end{eqnarray*}
%It is to be understood that 
We assume that $\Gamma$ does not contain
(\pairM,\pairN) and (\encM,\encN) respectively (otherwise reduction
would not terminate). 
This reduction relation is terminating and confluent, 
and so every theory $\Gamma$ reduces to a unique normal form \GammaR.
It also preserves the entailment $\vdash$.

\begin{lemma} \label{l-red-nc}
\begin{enumerate}
\item \cite[Lemma~15]{tiu-trace-based-bisim-full} \texttt{\upshape(red\_nc)}
\label{red-nc}
If $\Gamma \longrightarrow \Gamma'$
then $\Gamma \vdash M \eqm N$ if and only if
$\Gamma' \vdash M \eqm N$
\item \texttt{\upshape(nf\_nc)} \label{nf-nc}
Assuming that $\GammaR$ exists,
$\Gamma \vdash M \leftrightarrow N$ if and only if
$\GammaR\ \vdash M \leftrightarrow N$ 
\end{enumerate}
\end{lemma} 
%\subsubsection{Isabelle proof of confluence of reduction}
%Now $\longrightarrow$ is terminating and confluent.  
It is easy to show that $\longrightarrow$ is well-founded, 
since the sum of the sizes of [the first member of each of] the message pairs
reduces each time.
Confluence is reasonably easy to see since the side condition for the second
rule is of the form
$ {\Gamma' \vdash M_k \leftrightarrow N_k} $
where $\Gamma'$ is exactly the theory being reduced, and,
from Lemma~\ref{l-red-nc}, this condition (for a particular $M_k,N_k$) 
will continue to hold, or not, when other reductions have changed $\Gamma'$.
Actually, proving confluence in Isabelle was not so easy, and
we describe the difficulty and our proof in Appendix~\ref{or-confl}.
Then it is a standard result, and easy in Isabelle,
that confluence and termination give normal forms.
% satisfying these properties.  

\begin{theorem}[\texttt{nf\_oth\_red}] \label{t-nf-oth-red}
Any theory $\Gamma$ has a $\longrightarrow$-normal form $\GammaR.$ 
\end{theorem}

\subsubsection{A different reduction relation}
As a result of Lemma~\ref{l-red-nc},
to decide whether $\Gamma \vdash M \leftrightarrow N$ one might calculate
\GammaR\ and determine whether 
$\GammaR\ \vdash M \leftrightarrow N$, which is easier 
(see Lemma~\ref{l-nf-no-left}).
However to calculate \GammaR\ requires determining whether 
$\Gamma \vdash M_k \leftrightarrow N_k$, 
so the decidability of this procedure is not obvious.

We defined an alternative version, $\longrightarrow'$,
of the reduction relation, by changing the condition in the second rule,
so our new relation is:
\begin{eqnarray*}
{\Gamma, (\pairM,\pairN)} & \longrightarrow' &
  {\Gamma, (M_a, N_a), (M_b, N_b)} \\
{\Gamma, (\encM,\encN)} & \longrightarrow' & {\Gamma, (M_p, N_p), (M_k, N_k)}
 \quad \mbox{if } {\Gamma \vdash M_k \leftrightarrow N_k}
\end{eqnarray*}

This definition does not give the same relation, but we are able to show that
the two relations have the same normal forms.
Using this reduction relation, the procedure 
to decide whether $\Gamma \vdash M \leftrightarrow N$ is:
calculate $\GammaR$ and determine whether
$\GammaR\ \vdash M \leftrightarrow N$.
Calculating $\GammaR$ requires deciding questions of the form
$\Gamma' \vdash M_k \leftrightarrow N_k$, where 
$\Gamma'$ is smaller than $\Gamma$ (because a pair (\encM,\encN) is omitted).
Thus this procedure terminates.

Note that Lemma~\ref{l-red-nc} also holds for $\longrightarrow'$ since
$\longrightarrow'\ \subseteq\ \longrightarrow$.

To show the two relations have the same normal forms,
we first show (in Theorem~\ref{t-red-alt}\ref{oth-red-alt-lem})
that if $\Gamma$ is $\longrightarrow$-reducible,
then it is $\longrightarrow'$-reducible,
even though the same reduction may not be available.
\begin{theorem} \label{t-red-alt}
\begin{enumerate}
\item \texttt{\upshape(red\_alt\_lem)}
If $\Gamma \vdash M_k \leftrightarrow N_k$ then either \\
$\Gamma \setminus \{(\encM,\encN)\} \vdash M_k \leftrightarrow N_k$
or there exists $\Gamma'$ such that $\Gamma \longrightarrow' \Gamma'$
\item \texttt{\upshape(oth\_red\_alt\_lem)} \label{oth-red-alt-lem}
If $\Gamma \longrightarrow \Delta$ then there exists $\Delta'$ such that
$\Gamma \longrightarrow' \Delta'$
\item \texttt{\upshape(rsmin\_or\_alt)}
If $\Gamma$ is $\longrightarrow'$-minimal (i.e., cannot be reduced further) then
$\Gamma$ is $\longrightarrow$-minimal
\item \texttt{\upshape(nf\_acc\_alt)}
$\Gamma \longrightarrow' \GammaR$
(where $\GammaR$ is the $\longrightarrow$-normal form of $\Gamma$)
\item \texttt{\upshape(nf\_alt, nf\_same)} \label{nf-same}
$\GammaR$ is also the $\longrightarrow'$-normal form of $\Gamma$
\end{enumerate}
\end{theorem}
\begin{proof}
We show a proof of $(a)$ here. We prove a stronger result namely:
% \begin{center}
If $\Gamma \vdash M \leftrightarrow N$ and
$\textit{size}\ M \leq \textit{size}\ Q_k$ then either
$\Gamma' = \Gamma \setminus \{(\encQ,\encR)\} \vdash M \leftrightarrow N$
or there exists $\Delta$ such that $\Gamma \longrightarrow' \Delta$.
% \end{center}

We prove it by induction on the derivation of
$\Gamma \vdash M \leftrightarrow N$.
If the derivation is by the ($var$) rule, ie, $(M,N) = (x,x)$,
then clearly $\Gamma' \vdash M \leftrightarrow N$ by the ($var$) rule.
If the derivation is by the ($id$) rule, ie, $(M,N) \in \Gamma$,
then the size condition shows that $(M,N) \in \Gamma'$,
and so $\Gamma' \vdash M \leftrightarrow N$ by the ($id$) rule.

If the derivation is by either of the right rules ($pr$) or ($er$),
then we have $\Gamma \vdash M' \leftrightarrow N'$
and $\Gamma \vdash M'' \leftrightarrow N''$, according to the rule used,
with $M'$ and $M''$ smaller than $M$.
Then, unless $\Gamma \longrightarrow' \Delta$ for some $\Delta$,
we have by induction
$\Gamma' \vdash M' \leftrightarrow N'$ and 
$\Gamma' \vdash M'' \leftrightarrow N''$, 
whence, by the same right rule, $\Gamma' \vdash M \leftrightarrow N$.

If the derivation is by the left rule ($pl$), then
$\Gamma \longrightarrow' \Delta$ for some $\Delta$.

If the derivation is by the left rule ($el$), then
we apply the inductive hypothesis to the \emph{first} premise of the rule.
Let the ``principal'' message pair for the rule be $(\encM,\encN)$,
so the first premise is $\Gamma \vdash M_k \leftrightarrow N_k$.
Note that we apply the inductive hypothesis to 
a possibly \emph{different} pair of encrypts in $\Gamma$,
namely $(\encM,\encN)$ instead of $(\encQ,\encR)$.

By induction, either $\Gamma \longrightarrow' \Delta$ for some $\Delta$
or (since $\textit{size}\ M_k \leq \textit{size}\ M_k$), we have 
$\Gamma \setminus \{(\encM,\encN)\} \vdash M_k \leftrightarrow N_k$.
Then we have $\Gamma \longrightarrow' \Delta$, as required,
where $\Delta = \Gamma \setminus \{(\encM,\encN)\}, (M_p, N_p), (M_k, N_k)$. 
\qed
% Then we can set $\Delta = $ \\
% $\Gamma \setminus \{(\encM,\encN)\}, (M_p, N_p), (M_k, N_k)$, 
% and $\Gamma \longrightarrow' \Delta$, as required. \qed
%
%Then \\ $\Gamma \longrightarrow' \Gamma \setminus \{(\encM,\encN)\},
  %(M_p, N_p), (M_k, N_k)$, as required. \qed
\end{proof}
 
Since the process of reducing a theory essentially replaces pairs of compound
messages with more pairs of simpler messages, this suggests that to show 
that $\Gamma \vdash M \leftrightarrow N$ for a reduced $\Gamma$,
one need only use the rules which build up pairs of compound messages on the
right. 
That is, one would use 
the right rules $(pr)$ and $(er)$, but not the left rules $(pl)$ and $(el)$.
Let us define $\Gamma \vdash_r M \leftrightarrow N$ to mean that 
$\Gamma \vdash M \leftrightarrow N$ can be derived using 
the rules $(var), (id), (pr)$ and $(er)$ of Figure~\ref{f-msg-ind}.
 % \emph{except} rules $(pl)$ and $(el)$.
We call the set of these rules \texttt{indpsc\_virt}. 

We define a function \texttt{is\_der\_virt} which shows how to test
$\Gamma \vdash_r M \leftrightarrow N$, 
and, in Lemma~\ref{l-nf-no-left}\ref{virt-dec}, % \texttt{virt\_dec},
prove that it does this.
It terminates because at each recursive call,
the size of $M$ gets smaller.
When we define a function in this way, 
Isabelle requires termination to be \emph{proved} (usually it can do this
automatically).
Then \emph{inspection} of the function definition shows that, 
{assuming} the theory \texttt{oth} is finite,
the function is finitely computable.
We discuss this idea further later.
We also define a simpler function \texttt{is\_der\_virt\_red},
as an alternative to \texttt{is\_der\_virt}, 
which gives the same result when $\Gamma$ is reduced, see
Appendix~\ref{v-is-der-virt-red}.

{\small
\begin{verbatim}
recdef "is_der_virt" "measure (%(oth, M, N). size M)"
  "is_der_virt (oth, Name i, Name j) = ((Name i, Name j) : oth | i = j)"
  "is_der_virt (oth, Mpair Ma Mb, Mpair Na Nb) =
    ((Mpair Ma Mb, Mpair Na Nb) : oth |
      is_der_virt (oth, Ma, Na) & is_der_virt (oth, Mb, Nb))"
  "is_der_virt (oth, Enc Mp Mk, Enc Np Nk) =
    ((Enc Mp Mk, Enc Np Nk) : oth |
      is_der_virt (oth, Mp, Np) & is_der_virt (oth, Mk, Nk))"
  "is_der_virt (oth, M, N) = ((M, N) : oth)"
\end{verbatim}
}

\begin{lemma} \label{l-nf-no-left}
\begin{enumerate}
\item \texttt{\upshape(nf\_no\_left)} \label{nf-no-left}
If $\Gamma$ is reduced 
and $\Gamma \vdash M \!\eqm\! N$ then 
$\Gamma \vdash_r M \!\eqm\! N$ 
\item \texttt{\upshape(virt\_dec)} \label{virt-dec}
$\Gamma \vdash_r M \leftrightarrow N$ if and only if 
\texttt{is\_der\_virt} $(\Gamma, (M,N))$
\end{enumerate}
\end{lemma}

We can now define a function \texttt{reduce} which computes a
$\longrightarrow'$-normal form.
{\small
\begin{verbatim}
recdef (permissive) "reduce" "measure (setsum (size o fst))"
  "reduce S = (if infinite S then S else
    let P = (%x. x : Mpairs <*> Mpairs & x : S) ;
      Q = (%x.  (if x : Encs <*> Encs & x : S then
          is_der_virt (reduce (S - {x}), keys x) else False))
    in if Ex P then reduce (red_pair (Eps P) (S - {Eps P}))
      else if Ex Q then reduce (red_enc (Eps Q) (S - {Eps Q}))
      else S)"
\end{verbatim}
}
To explain this:
$P\ (M,N)$ means $(M,N) \in S$ and $M,N$ are both pairs;
$Q\ (M,N)$ means $(M,N) \in S$ and $M,N$ are both encrypts, say
$\encM,\encN$, where
\mbox{$S \setminus\{(M,N)\} \vdash_r (M_k,N_k)$;}
\texttt{red\_pair} and \texttt{red\_enc} do a single step reduction
based on the message pairs or encrypts given as their argument,
\texttt{Ex P} means $\exists x.\ P\ x$, and
\texttt{Eps P} means some $x$ satisfying $P$, if such exists.
% (similarly \texttt{Ex Q}, \texttt{Eps Q}).
% and \texttt{keys} (\encM, \encN) = $(M_k, N_k)$.
% \texttt{Eps P} is also written \texttt{SOME x. P x}, or 
% $\epsilon x.\ P\ x$.
% and \texttt{is\_der\_virt} $\Gamma\ (M,N)$
% is a function which tells whether
% $\Gamma \vdash M \leftrightarrow N$ for a reduced $\Gamma$.
Thus the function selects arbitrarily 
a pair of message pairs or encrypts
suitable for a single reduction step, performs that step, 
and then reduces the result.

The expression \texttt{measure (setsum (size o fst))}
is the termination measure, the sum of the sizes of the first member of each
message pair in a theory.
The function \texttt{reduce} is recursive,
and necessarily terminates since at each iteration 
this measure function, applied to the argument, is smaller.
However this function definition is sufficiently complicated that 
Isabelle cannot automatically prove that it terminates ---
thus the notation \texttt{(permissive)} in the definition.

Isabelle produces a complex definition dependent on conditions 
that if we change a theory by applying 
\texttt{red\_pair} or \texttt{red\_enc}, or by deleting a pair,
then we get a theory which is smaller according to the measure function.
Since in the HOL logic of Isabelle all functions are total, 
we have a function \texttt{reduce} in any event; 
we need to prove the conditions to prove that \texttt{reduce} 
conforms to the definition given above.
% produces $\longrightarrow$-normal forms.
We then get Theorem~\ref{t-reduce}\ref{reduce-nf} and \ref{virt-reduce},
which show how to test $\Gamma \vdash M \eqm N$
as a manifestly finitely computable function.
% Since those conditions hold we get Theorem~\ref{t-reduce}\ref{reduce-nf}.
% Recall from Theorem~\ref{t-red-alt}\ref{nf-same} that 
% $\GammaR$ is the normal form of $\Gamma$ under
% $\longrightarrow$ and under $\longrightarrow'$.
% Then combining this with previous results easily gives
% Theorem~\ref{t-reduce}\ref{virt-reduce},
% which expresses the way to test $\Gamma \vdash M \eqm N$ 
% as a manifestly finitely computable function.
We also prove a useful characterisation of $\GammaR$.
% motivated by the $\mathbf I(\sigma)$ of \cite[Definition~10]{boreale},
% which we discuss later.

\begin{theorem} \label{t-reduce} % [\texttt{reduce\_nf, reduce\_nf\_alt}] 
\begin{enumerate}
\item \texttt{\upshape(reduce\_nf, reduce\_nf\_alt)} \label{reduce-nf}
\texttt{reduce} $\Gamma = \GammaR$
\item \texttt{\upshape(virt\_reduce, idvr\_reduce)} \label{virt-reduce}
$\Gamma \vdash M \eqm N$ if and only if 
\texttt{is\_der\_virt} $(\GammaR, (M, N))$, equivalently, if and only if
\texttt{is\_der\_virt\_red} $(\GammaR, (M, N))$
\item \texttt{\upshape(reduce\_alt)} \label{reduce-alt}
For $(M, N) \not\in \Ne$, $(M, N) \in \GammaRNe$ iff 
\begin{enumerate}
\item $\Gamma \vdash M \eqm N$,
 \item $M$ and $N$ are not both pairs, and
 \item if % $M$ and $N$ are both encrypts,
 $M = \encM, N = \encN$, then 
 $\Gamma \not\vdash M_k \eqm N_k$
\end{enumerate}
\end{enumerate}
\end{theorem}

As Urban et al point out in \cite{ucb-mech-LF}
formalising decidability --- or computability --- is difficult.  
It would require formalising the computation process, 
as distinct from simply defining the quantity to be computed.
However, as is done in \cite[\S 3.4]{ucb-mech-LF}, it is possible to 
define a quantity in a certain way which makes it reasonable to assert that it
is computable.
This is what we have aimed to do in defining the function \texttt{reduce}.
It specifies the computation to be performed (with a caveat mentioned later).
Isabelle requires us to show that this computation is terminating, 
and we have shown that it produces 
the $\longrightarrow'$-normal form.
To ensure termination, we needed to base the definition of 
\texttt{reduce} on $\longrightarrow'$, not on $\longrightarrow$, 
but by Theorem~\ref{t-red-alt}\ref{nf-same},
$\longrightarrow'$ and $\longrightarrow$ have the same normal forms.

Certain terminating functions are not obviously computable,
for example $f\ x = (\exists y.\ P\ y)$ (even where $P$ is computable).
So our definition of \texttt{reduce} requires inspection to ensure that
it contains nothing which makes it not computable.
It does contain existential quantifiers, but they are in essence quantification
over a finite set. 
The only problem is the subterms \texttt{Eps P} and \texttt{Eps Q},
that is $\epsilon x.\ P\ x$ and $\epsilon x.\ Q\ x$.
These mean ``some $x$ satisfying $P$'' (similarly $Q$).
In Isabelle's logic, this means \emph{some} $x$, 
but we have no knowledge of which one 
(and so we cannot perform precisely this computation).
But our proofs went through without any knowledge of which $x$ is denoted
by $\epsilon x.\ P\ x$.
Therefore it would be safe to implement a computation which makes any choice of 
$\epsilon x.\ P\ x$, and we can safely assert that our proofs would still hold
for that computation.\footnote{
In general a repeated choice must be made consistently;
the HOL logic \emph{does} imply $\epsilon x.\ P\ x = \epsilon x.\ P\ x$.
This point clearly won't arise for the \texttt{reduce} function.
}
That is, in general we assert that if a function involving $\epsilon x.\ P\ x$
can be proven to have some property, then a function which replaces $\epsilon
x.\ P\ x$ by some other choice of $x$ 
(satisfying $P$ if possible) would also have that property.
Based on this assertion we say that our definition of \texttt{reduce}
shows that the $\longrightarrow$-normal form is computable, 
and so that $\Gamma \vdash M \leftrightarrow N$ is decidable.

We found that although the definition of \texttt{reduce} gives the
function in a computable form, many proofs are much easier using
the characterisation as the normal form.
For example Lemma~\ref{l-red-nc}\ref{nf-nc} is much easier 
using Lemma~\ref{l-red-nc}\ref{red-nc} than using the definition of 
\texttt{reduce}.
We found this with some other results, such as:
if $\Gamma$ is finite, then so is $\GammaR$, 
% and the result \texttt{reduce\_paired} (below),
and if $\Gamma$ consists of identical pairs then so does $\GammaR$.

\comment{ red_comps - omitted

\subsubsection{Message set reduction, and decidability of message synthesis}
Just as we described the rules for message synthesis in terms of those for
message equivalence, we can obtain similar results for deciding message
synthesis.
So we define \texttt{reduce\_ss} and \texttt{idv\_ss} 
by applying \texttt{reduce} and \texttt{is\_der\_virt} respectively 
to observer theories consisting of ``identical pairs'' $(M,M)$,
% (as $\texttt{pair}\ x = (x,x)$),
Then we get the expected result \texttt{idv\_reduce\_ss},
that if $S$ is reduced then $\textit{idv\_ss}\ (S, M)$ iff $S \vdash M$,
the single message analogue of Theorem~\ref{t-reduce}\ref{virt-reduce}.
The proof of this depends on the result \texttt{reduce\_paired}, that
if $\Gamma$ consists of identical pairs then so does $\GammaR$.

In \cite{boreale} Boreale considers ``marked symbolic traces'', 
which are like a sequence of input or output messages.
In Definition~10 and Proposition~11 he formulates 
a test for $\Gamma \vdash M$,
which could be adapted to observer theories, as we now describe.

Given the definition of \texttt{is\_der\_virt},
Theorem~\ref{t-reduce}\ref{virt-reduce}
suggests a characterisation of $\Gamma \vdash M \eqm N$ of the form
``(some set derived from $(M,N)) \subseteq \GammaR$''.
With Theorem~\ref{t-reduce}\ref{reduce-alt},
this suggests a result for theories
analogous to \cite[Proposition~11]{boreale}.

A related idea is that $\Gamma \vdash M \eqm N$ iff
$\GammaRNe = \RNe{(\Gamma \cup \{(M,N)\})}$
which follows from Theorem~\ref{l-Ne}\ref{nf-equiv-der} below,
giving a criterion for $\Gamma \vdash M \eqm N$.

However we need this result only for sets of single messages.
%We formalise this only for sets of single messages.
So we define the ``reduced components'' of a message, 
given a reduced message set $S$, as follows.
\begin{align*}
\textit{red\_comps}\ S\ x & = \{\} \qquad \qquad
\textit{red\_comps}\ S\ \mathbf a = \{\mathbf a\} \\[-0.5ex]
\textit{red\_comps}\ S\ \pairM & = 
  \textit{red\_comps}\ S\ M_a \cup \textit{red\_comps}\ S\ M_b \\[-0.5ex]
\textit{red\_comps}\ S\ \encM & = \textit{red\_comps}\ S\ M_p 
  && \mbox{if } \textit{idv\_ss}\ (S, M_k) \\[-0.5ex]
\textit{red\_comps}\ S\ \encM & = \{\encM\} && \mbox{otherwise}
%  \\
% \textit{red\_comps}\ S\ \encM & = \left\{
% \begin{array}{l@{\qquad}l}
% \textit{red\_comps}\ S\ M_p & \mbox{if } \textit{idv\_ss}\ (S, M_k) \\
 % \{\encM\} & \mbox{otherwise}
% \end{array}\right.
\end{align*}
\comment{
\begin{verbatim}
"red_comps S (Name x) = {}"
"red_comps S (Rigid x) = {Rigid x}"
"red_comps S (Mpair Ma Mb) = red_comps S Ma Un red_comps S Mb"
"red_comps S (Enc Mp Mk) = 
  (if idv_ss (S, Mk) then red_comps S Mp else {Enc Mp Mk})" 
\end{verbatim}
}
Recall that if $S$ is reduced then 
$\textit{idv\_ss}\ (S, M_k)$ iff $S \vdash M_k$.
We therefore obtain the following result,
which is similar to \cite[Proposition~11]{boreale}.
% but it is in the form we need subsequently,
 % to adapt Boreale's work to deciding bi-trace consistency.

\begin{lemma}[\texttt{rc\_reduce}] \label{l-rc-reduce}
$S \vdash M$ if and only if
$\textit{red\_comps}\ \irred S\ M \subseteq \irred S$
\end{lemma}

end of comment (red_comps - omitted) }

% For deciding message synthesis, using \texttt{rc\_reduce}
 % is very similar to using \texttt{idv\_reduce\_ss},
% but it is in the form we need subsequently,
% to adapt Boreale's work to deciding bi-trace consistency.

% \subsubsection{Pairs of the same name}
% These results follow from the ($var$) rule.

Since also $\Gamma$ and $\GammaR$ entail the same message pairs, 
% and so each entails all the pairs in each other, 
it is reasonable to ask which theories,
other than those with the same normal form as $\Gamma$,
entail the same message pairs as $\Gamma$.
Now it is clear, due to the ($var$) rule, 
that deleting $(x,x)$ from a theory does not
change the set of entailed message pairs or the reductions available.
However we find that the condition is that theories entail the same pairs iff 
their normal forms are equal, modulo \Ne.

We could further change $\longrightarrow'$ by deleting the $(M_k,N_k)$ from the
second rule.  
Lemma~\ref{l-red-nc}\ref{red-nc} holds for this new relation.
% and it gives the same (ir)reducible theories. 
For further discussion see Appendix~\ref{v-red-alt}.

\begin{theorem}  \label{l-Ne}
\begin{enumerate}
\item \texttt{\upshape(rsmin\_names)} \label{l-rsmin-names}
$\Gamma$ is reduced if and only if $\Gamma \setminus \Ne$ is reduced
\item \cite[Lemma~8]{tiu-trace-based-bisim-full} \texttt{\upshape(name\_equivd)}
$\Gamma \vdash M \eqm N$ if and only if
$\Gamma \setminus\ \Ne\ \vdash M \eqm N$
\item \texttt{\upshape(nf\_equiv\_der)} \label{nf-equiv-der}
Theories $\Gamma_1$ and $\Gamma_2$ entail the same message pairs
if and only if $\RNe{\Gamma_1} = \RNe{\Gamma_2}$
\end{enumerate}
\end{theorem}

\subsection{Theory consistency} \label{s-thy-cons}

%% Tiu \cite[Definition~11]{tiu-trace-based-bisim-full}
%% defines a \emph{consistent} observer theory,
%% and we give a slightly different definition
%% not referring to message synthesis,
%% in our predicate \texttt{thy\_cons},
%% and in Lemma~\ref{l-tc-equiv}\ref{l-thy-cons-equiv} prove it is equivalent. 
%% % to Tiu's definition in \texttt{thy\_cons\_equiv}.

\begin{definition} %Alwen's definition
\cite[Definition~11]{tiu-trace-based-bisim-full}
\label{def:theory-consistency}
A theory $\Gamma$ is {\em consistent} if for every $M$ and $N$, if
$\Gamma \vdash M \eqm N$ then the following hold:
\begin{enumerate}
\item $M$ and $N$ are of the same type of expressions, i.e., $M$ is
a pair (an encrypted message, a (rigid) name) if and only if $N$ is.
\item If $M = \enc {M_p} {M_k}$ and $N = \enc {N_p}{N_k}$ then
$\pi_1(\Gamma) \vdash M_k$ implies $\Gamma \vdash M_k \eqm N_k$ and
$\pi_2(\Gamma) \vdash N_k$ implies $\Gamma \vdash M_k \eqm N_k$.
\item For any $R$, $\Gamma \vdash M \eqm R$ implies $R = N$
and $\Gamma \vdash R \eqm N$ implies $R = M.$
\end{enumerate}
\end{definition}
This definition of consistency involves infinite quantification.
% The point of this section is to eliminate this quantification by
We want to eliminate this quantification by
finding a finite characterisation on {\em reduced theories}.
But first, let us define another equivalent notion of consistency,
which is simpler for verification, as it does not use
the deduction system for message synthesis.

\begin{definition} %our definition
\label{d-thy-cons}
A theory $\Gamma$ satisfies the predicate \texttt{thy\_cons}
if for every $M$ and $N$, if
$\Gamma \vdash M \eqm N$ then the following hold:
\begin{enumerate}
\item $M$ and $N$ are of the same type of expressions, i.e., 
as in Definition~\ref{def:theory-consistency}(a)
\item for every $M', N', M_p, N_p$  %typo in published version
if $\Gamma \vdash M' \eqm N'$ or
$\Gamma \vdash \enc {M_p} {M'} \eqm \enc {N_p}{N'}$,
then $M' = M$ iff $N' = N$
\end{enumerate}
\end{definition}

%The two definitions are equivalent, as stated in the following lemma.
\begin{lemma} \label{l-tc-equiv}
\begin{enumerate}
\item \texttt{\upshape(thy\_cons\_equiv)} \label{l-thy-cons-equiv}
$\Gamma$ is consistent % (Definition~\ref{def:theory-consistency})
iff it satisfies Definition~\ref{d-thy-cons}
\item \texttt{\upshape(thy\_cons\_equivd)} \label{l-thy-cons-equivd}
$\Gamma$ is consistent if and only if $\Gamma \setminus\ \Ne$ is consistent 
\item \cite[Lemma~19]{tiu-trace-based-bisim-full}
\texttt{\upshape(nf\_cons)} \label{l-nf-cons}
$\Gamma$ is consistent if and only if $\GammaR$ is consistent 
\item \texttt{\upshape(cons\_der\_same)} \label{l-cons-der-same}
If $\Gamma_1$ and $\Gamma_2$ entail the same message pairs then 
$\Gamma_1$ is consistent if and only if $\Gamma_2$ is consistent 
\end{enumerate}
\end{lemma}

Tiu \cite[Proposition~20]{tiu-trace-based-bisim-full}
gives a characterisation of consistency (reproduced
below in Proposition~\ref{prop:characterisation-of-consistency})
which is finitely checkable.
In Definition~\ref{d-thy-cons-red} we define a predicate
\texttt{thy\_cons\_red} which is somewhat similar.
In Theorem~\ref{t-thy-cons-red} we show that, for a reduced theory, 
that our \texttt{thy\_cons\_red} is equivalent to consistency and to 
the conditions in Proposition~\ref{prop:characterisation-of-consistency}.
%% First we reproduce Tiu's Proposition~20, 
%% but note that our proof of it is that
%% it follows from Theorem~\ref{t-thy-cons-red}. 
Decidability of consistency then follows from decidability of $\vdash$,
and termination of normal form computation.

\begin{proposition} %Alwen's 
\label{prop:characterisation-of-consistency}
\cite[Proposition~20]{tiu-trace-based-bisim-full}
A theory $\Gamma$ is consistent if and only if $\irred{\Gamma}$ satisfies
the following conditions: if $(M,N) \in \irred{\Gamma}$ then
\begin{enumerate}
\item $M$ and $N$ are of the same type of expressions, in particular,
if $M = x$, for some name $x$, then $N = x$ and vice versa,
\item if $M = \enc {M_p} {M_k}$ and $N = \enc {N_p}{N_k}$ then
$\pi_1(\irred \Gamma) \not \vdash M_k$ and
$\pi_2(\irred \Gamma) \not \vdash N_k$.
\item for any $(U,V) \in \irred{\Gamma}$, $U = M$ if and only if $V = N$.
\end{enumerate}
\end{proposition}

\begin{definition} %ours
\label{d-thy-cons-red}
A theory $\Gamma$ satisfies the predicate \texttt{thy\_cons\_red} if
\begin{enumerate}
\item for all $(M, N) \in \Gamma$,
  $M$ and $N$ satisfy Proposition~\ref{prop:characterisation-of-consistency}(a) 
\item \label{eq-iff-eq}
  for all $(M, N)$ and $(M', N') \in \Gamma$, $M' = M$ iff $N' = N$
\item for all $(\enc {M_p} {M_k}, \enc {N_p}{N_k}) \in \Gamma$,
for all $M,N$ such that $\Gamma \vdash M \eqm N$, \\
\mbox{$M \not= M_k$ and $N \not= N_k$}
\end{enumerate}
\end{definition} 

\begin{theorem} \label{t-thy-cons-red}
\begin{enumerate}
\item
\texttt{\upshape(tc\_red\_iff)} \label{l-tc-red-iff}
$\Gamma$ is consistent iff $\GammaR$ satisfies \texttt{thy\_cons\_red}
% ie the conditions of Definition~\ref{d-thy-cons-red}
\item \texttt{\upshape(thy\_cons\_red\_equiv)} \label{l-thy-cons-red-equiv}
$\GammaR$ satisifes 
Proposition~\ref{prop:characterisation-of-consistency}(a) to (c)
iff it satisfies \texttt{thy\_cons\_red},
ie, Definition~\ref{d-thy-cons-red}(a) to (c)
\end{enumerate}
\end{theorem}