\section{Conclusions and Further Work}
\label{s-concl-fw}

We have modelled observer theories and bi-traces 
in the Isabelle theorem prover, and have confirmed, by proofs in Isabelle, 
the results of a considerable part of \cite{tiu-trace-based-bisim-abs}.
This work constitutes a significant step formalising 
open bisimulation for the spi-calculus in Isabelle/HOL, and ultimately
towards a logical framework for proving process equivalence.

%% We have focussed on the decidability of equivalence relative to an observer
%% theory ($\Gamma \vdash M \eqm N$)
%% and of theory and bi-trace consistency.
%% Tiu describes reductions of observer theories and shows that
%% where $\Gamma$ reduces to $\GammaR$, $\Gamma$ is consistent iff $\GammaR$ is
%% and $\Gamma \vdash M \eqm N$ iff $\GammaR\ \vdash M \eqm N$,
%% and these latter questions are easily decidable.
%% We completed this picture by defining a different theory reduction relation,
%% which we showed leads to the same reduced theories as Tiu's definition,
%% and is, moreover, easily seen to be finitely computable.
% As part of this we formally proved 
% that normal forms exist for the reduction relations. 
% and described how we handled what would otherwise have been an exceedingly
% tedious proof.

We discussed the issue of showing finite computability in Isabelle/HOL,
using a mixed formal/informal argument, and building upon the discussion
in Urban et al \cite{ucb-mech-LF}.
We defined a function \texttt{reduce} in Isabelle, 
and showed that it computes $\GammaR$.
Isabelle required us to show that the function terminates.  
We asserted, with relevant discussion, 
that inspection shows that the definition does not introduce
any infinite aspect into the computation and so asserted that therefore the 
function is finitely computable.
Similarly, we provided a finitely computable function \texttt{is\_der\_virt}
and proved that it tests $\Gamma \vdash M \eqm N$ for a reduced theory $\Gamma$.


We then considered bi-traces and bi-trace consistency.
The problem here is that, to test bi-trace consistency, it is
necessary to test whether $\Gamma\theta$ is consistent for all $\theta$
satisfying certain conditions.
We proved a number of lemmas which simplify this task, 
and appear to lead to a finitely computable algorithm for this.
In particular, our result on the unique completion of 
respectful substitutions that relates symbolic trace
and bi-trace  opens up the possibility to use 
symbolic trace refinement algorithm \cite{boreale} to
compute a notion of {\em bi-trace refinement}, which will
be useful for bi-trace consistency checking.

Another approach to representating observer theories is to use
equational theories, instead of deduction rules, e.g., as in the applied-pi 
calculus~\cite{abadi01popl}. In this setting, 
the notion of consistency of a theory is replaced by the notion of {\em static equivalence}
between knowledge of observers~\cite{abadi01popl}.
Baudet has shown that static equivalence between
two symbolic theories is decidable~\cite{baudet07phd}, 
for a class of theories called subterm-convergent theories (which
subsumes the Dolev-Yao model of intruder). It will be interesting to 
work out the precise correspondence between static equivalence and
our notion of bi-trace consistency, as such correspondence may transfer
proof techniques from one approach to the other.


%% These include the significant results that where keys are atomic,
%% one can \emph{first} reduce a theory and remove free name pairs, 
%% \emph{then} substitute using a respectful substitution,
%% and the resulting theory is reduced.
%% Then the only difficult part of testing consistency is
%% Definition~\ref{d-thy-cons-red}\ref{eq-iff-eq}.
%% There are finitely many choices for the pair $M, M'$ of that criterion,
%% and for each choice one could find 
%% the most general subsitution $\theta_1$ which makes $M\theta_1 = M'\theta_1$.

%% We showed that to get a respectful substitution $(\theta_1, \theta_2)$,
%% if $\theta_1$ exists satisfying a single-trace analogue of respectfulness,
%% then $\theta_2$ exists and is determined by $\theta_1$, and vice versa.
%% % except for their action on free names which don't appear
%% %
%% This suggests that having determined the most general $\theta_1$
%% which gives $M\theta_1 = M'\theta_1$,
%% we simply determine the corresponding $\theta_2$,
%% using Theorems \ref{t-subst-exists-unique} and \ref{t-match-rc1}
%% and the function \texttt{second\_sub}, 
%% and see whether $N\theta_2 = N'\theta_2$.

%% The problem here is that this $\theta_1$ may not satisfy 
%% the single-trace respectfulness condition. % \texttt{sm\_resp}.
%% Here we hope to use a technique similar to that of Boreale
%% (see \cite[Proposition~11]{boreale}, and following).
%% % This motivated our definition of \texttt{red\_comps} 
%% % and Lemma~\ref{l-rc-reduce}.
%% The procedure would be to unify further pairs of message
%% components, of which there would be finitely many choices,
%% leading to a finite procedure for computing bi-trace consistency.
%% We propose to work out the details of using this method,
%% and to check them using Isabelle.

\paragraph{Acknowledgment} We thank the anonymous referees for their comments
on an earlier draft.
This work is supported by the Australian Research Council through the Discovery 
Projects funding scheme (project number DP0880549).