
\section{Introduction} \label{s-intro}

YET TO CHANGE FROM TPHOLS 2009 PAPER
In most symbolic techniques for reasoning about security protocols, 
certain assumptions are often made concerning the capability of
an intruder that tries to compromise the protocols. 
A well-known model of intruder is the so-called Dolev-Yao 
model~\cite{dolevyao}, which assumes perfect crytography. We consider here a formal
account of Dolev-Yao intruder model, formalised as some sort
of deduction system. 
This deductive formulation is used in formalisations of various
``environment-sensitive'' bisimulations (see e.g., \cite{boreale-siam}) 
for process calculi designed
for modeling security protocols, such as the spi-calculus~\cite{abadi99ic}.
An environment-sensitive bisimulation is a bisimulation relation which
is indexed by a structure representing the intruder's knowledge, which
we call an {\em observer theory.}
%% \footnote{We have chosen a rather neutral term `observer' in place of
%%   `intruder' to reflect the fact that we are not focusing on security
%%   protocol verification, but bisimulation.}

An important line of work related to the spi-calculus, or process calculi
in general, is that of automating bisimulation checking. 
The transition semantics of these calculi often involve processes
with infinite branching (e.g., transitions for input-prefixed processes
in the $\pi$-calculus~\cite{milner92icII}), and therefore a {\em symbolic
method} is needed to deal with potential infinite branches lazily.
The resulting bisimulation, called {\em symbolic bisimulation}, has 
been developed for the spi-calculus \cite{borgstrom04concur}. The work reported
in \cite{borgstrom04concur} is, however, only aimed at finding an effective approximation 
of environment-sensitive bisimulation, and there has been no metatheory 
developed for this symbolic bisimulation so far. A recent work by the second author
\cite{tiu-trace-based-bisim-abs} attempts just that: to establish a symbolic bisimulation that has
good metatheory, in particular, a symbolic bisimulation which is also a congruence.
The latter is also called {\em open bisimulation}~\cite{sangiorgi96acta}. 
One important part of the formulation of open bisimulation for the spi-calculus 
is a symbolic representation of observer theories, which needs to
satisfy certain consistency properties, in addition to closure under
a certain notion of ``respectful substitutions'', as typical in formulations
of open bisimulation. 

A large part of the work on open bisimulation in \cite{tiu-trace-based-bisim-abs} 
deals with establishing properties of observer theories and 
their symbolic counterparts. This paper is essentially about formally verifying 
the results of \cite{tiu-trace-based-bisim-abs} 
concerning properties of (symbolic) observer theories in Isabelle/HOL. 
In particular, it is concerned with proving decidability of the deduction 
system for observer theory, correctness of a finite
characterisation of consistency of observer theories (hence decidability of consistency
of observer theories), and preservation of consistency under respectful substitutions.
Additionally, we also verify some key steps towards a decision procedure for
checking consistency of symbolic observer theories, which is needed in automation
of open bisimulation. A substantial formalisation work described here concerns 
decidability proofs. Such proofs are difficult to formalise in Isabelle/HOL,
as noted in \cite{ucb-mech-LF}, due to the fact that Isabelle/HOL is based on classical logic.
We essentially follow \cite{ucb-mech-LF} in that decidability in this case can be inferred
straightforwardly by inspection on the way we define total functions corresponding to
the decidability problems in question. That is, we show, by meta-level inspection, 
that the definitions of the functions do not introduce any infinite aspect and are 
therefore are finitely computable.

There is a recent work \cite{kahsai08} in formalising the spi-calculus
and a notion of environment-sensitive bisimulation (called the {\em hedged
bisimulation} \cite{borgstrom05}) in Isabelle/HOL. However, this notion of bisimulation
is a ``concrete'' bisimulation (as opposed to symbolic), which means that 
the structure of observer theories is less involved and much easier to deal
with compared to its symbolic counterpart. 
Our work on observer theories is mostly orthogonal to their work, and
it can eventually be integrated into their formalisation 
to provide a completely formalised open bisimulation for the spi-calculus.
% Such an integration is perhaps not too difficult,
Such an integration may not be too difficult,
given that much % a large part
of their work, e.g., formalisation of the operational semantics of the spi-calculus,
can be reused without modifications. 

\newpage
NEW TO THIS PAPER

In \cite{dawson-tiu-observer-theory} we discussed 
respectful substitutions for bi-traces,
defined as follows.
A {\em bi-trace} is a {\em list} of message pairs marked with
$i$ (indicating input) or $o$ (output),
with the restriction that any variable appears first in an input pair.
A substitution pair $\vec\theta = (\theta_1, \theta_2)$
replaces free names $x \in \mathcal N$ by messages,
using substitutions $\theta_1 (\theta_2)$ for the first (second)
component of each pair.
For a bi-trace $h$, $\vec\theta$ \emph{respects} $h$, or is $h$-respectful
\cite[Definition~34]{tiu-trace-based-bisim-full},
if for every free name $x$ in an input pair $(M,N)^i$,
$\{h'\}\vec\theta \vdash x\theta_1 \eqm x\theta_2$,
where $h'$ is the part of $h$ preceding $(M,N)^i$.
This is expressed in Isabelle by $h \in$ \texttt{bt\_resp} $\vec\theta$.

Since a bitrace is a sequence of pairs of messages (marked as input or output),
we projected this notion to a similar trace of single messages (which we will
henceforth call a \emph{trace}).
This gave the notion of a ``respectful substitution'' for a trace.
We reproduce \cite[Theorem~20]{dawson-tiu-observer-theory} here.

\begin{theorem}[\texttt{subst\_exists, subst\_unique}]
\label{t-subst-exists-unique}
Given a consistent bi-trace $h$
whose projections to a single message trace are 
$s_1 = \pi_1(h)$ and $s_2 = \pi_2(h)$,
and a substitution $\theta_1$ which respects $s_1$,
there exists $\theta_2$ such that $\vec\theta = (\theta_1, \theta_2)$
respects $h$,
and $\theta_2$ is ``unique'' in the sense that any two such $\theta_2$
act the same on names in $s_2$
\end{theorem}

We also reproduce (in part) the definition of a \emph{consistent} bi-trace.

\begin{definition} \label{d-bt-cons}
\cite[Definition~35]{tiu-trace-based-bisim-full}
The set of {\em consistent bi-traces} are defined inductively (on
the length of bi-traces) as follows:
\begin{enumerate}
\item The empty bi-trace is consistent.
\item If $h$ is a consistent bi-trace then $h.(M,N)^i$ is also a consistent
bi-trace, provided that $h \vdash M \eqm N$.
\item If $h$ is a consistent bi-trace,
then $h' = h.(M,N)^o$ is a consistent bi-trace, \\
provided that for every $h$-respectful substitution pair $\vec \theta$, %\\
% \underline{if $h\vec \theta$ is a consistent bi-trace then}
$\{h'\vec \theta \}$ is a consistent theory.
\end{enumerate}
\end{definition}

Thus, to determine whether $h' = h.(M,N)^o$ is a consistent bi-trace,
we need to consider \emph{all} $h$-respectful substitution pairs $\vec \theta$.
By Theorem~\ref{t-subst-exists-unique} it is enough to consider all 
respectful substitutions of a trace $s_1$;
for each such substitution we can get the respectful substitution of the
bi-trace. 

Now we could produce a finite set of substitutions
$\Theta_1$ such that each respectful substitution 
$\theta_1$ of $s_1 = \pi_1(h)$ is of the form
$\theta_1' \circ \rho_1$ for some $\theta_1' \in \Theta_1$.
Then $\theta_1'$ gives rise to a ``unique'' $h$-respectful substitution 
$\theta$.
We would then need to check whether % $\{h\theta'\}$ is a consistent theory
$\{h(\theta' \circ \rho)\}$ 
\footnote{Here, $(\theta' \circ \rho)$ means $\theta'$ followed by $\rho$.}
is consistent for all $\rho$.

Now we can check whether $\{h\theta'\}$ is a consistent theory,
using the finitely checkable criterion for a consistent theory,
given by Tiu \cite[Proposition~20]{tiu-trace-based-bisim-full}
see also \cite[Proposition~11, Theorem~13]{dawson-tiu-observer-theory}.
But this does not give us consistency of $\{h(\theta' \circ \rho)\}$ 
for all $\rho$.

Instead, from the criteria for a consistent theory we can get a 
finite set $\Sigma$ of most general substitutions $\sigma$
which may make $\{h\theta\}$ inconsistent.
That is, if we can substitute in $\{h\}$ to get an inconsistent theory,
it is of the form $\{h\}\sigma\theta$ for some $\theta$,
and some $\sigma \in \Sigma$.
Then, for each such $\sigma$ we can find the finite set of most general
substitutions which can be composed
with $\sigma_1$ or $\sigma_2$ to get a respectful substitution,
as described above.
Then we can test each of these $\sigma_i \circ \theta$
to see if they do in fact lead to an inconsistent theory.
In this case, if any less general substitution
$\sigma_i \circ \theta \circ \rho$ gives an inconsistent theory
then so does $\sigma_i \circ \theta$.

Note that in our results and proofs we either consider only substitutions which 
do not touch variables which do not appear, or, as in
Theorem~\ref{t-subst-exists-unique}, regards substitutions as the same when
they differ only on variables which are not present.
END OF NEW STUFF

%The paper is set out as follows.
We assume that the reader is familar with Isabelle proof assistant, its
object logic HOL and logical frameworks in general. 
In the remainder of this section we briefly describe relevant Isabelle notations
used throughout the paper.
%In the remainder of this section we briefly describe relevant aspects of the theorem prover Isabelle.
In Section~\ref{s-obsv}, we give an overview of observer theories and an intuition
behind them. We also give a brief description of two problems that will be
the focus of subsequent sections, namely, those that concern decidability
of consistency checking for (symbolic) observer theories.  
In Section~\ref{s-otd} we consider formalisation of a notion of theory reduction
and decidability of consistency checking for observer theories.
%% give a more detailed account of observer theories, 
%% showing their reduction as defined in \cite{tiu-trace-based-bisim-abs},
%% which we use to prove that reduction is finitely computable.
%% We then discuss theory consistency and an a finite characterisation of
%% consistency, which is finitely computable. 
In Section~\ref{s-bt} we discuss a symbolic representation of observer theories
using pairs of symbolic traces~\cite{boreale}, called {\em bi-traces}, their
consistency requirements and a notion of {\em respectful substitutions}.  
We prove a key lemma which relates a symbolic technique for
trace refinement \cite{boreale} to bi-traces, and discuss how this may
lead to a decision procedure for testing bi-trace consistency.
Section~\ref{s-concl-fw} concludes.  


%% We devise a concept of a substitution being respectful of a theory 
%% (rather than of a bi-trace), 
%% which property is preserved by theory reduction. 
%% We show how (in a sense) a ``respectful'' single trace substitution
%% can be uniquely completed to form a respectful bi-trace substitution, 
%% and discuss how this may lead to a finite procedure for testing bi-trace
%% consistency using ideas of symbolic trace refinement by Boreale \cite{boreale},
%% and prove some results in this direction.
%% % In Section~\ref{s-concl-fw} we conclude.  
%% Section~\ref{s-concl-fw} concludes.  

% \section{Isabelle} \label{s-isa}
%% \subsubsection{Isabelle}
%% Isabelle is an automated proof assistant \cite{isabelle-ref}.  Its
%% meta-logic is an intuitionistic typed higher-order logic, sufficient
%% to support the built-in inference steps of higher-order unification
%% and term rewriting.  Isabelle accepts inference rules of the form
%% ``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''
%% where the $\alpha_i$ and $\beta$ are expressions of the Isabelle
%% meta-logic, or are expressions using a new syntax, defined by the
%% user, for some ``object logic''. Most users build on one of the
%% comprehensive ``object logics'' already supplied, like Isabelle/HOL
%% \cite{IsLogHOL}, which is an Isabelle theory based on the higher-order
%% logic of Church % \cite{church-types} and the HOL system of Gordon
%% \cite{HOL-introduction}.  HOL offers inductively defined sets, and
%% recursive datatypes, which we use extensively.  We assume the reader
%% is familiar with ML and logical frameworks in general.

\paragraph{Isabelle notation}
The Isabelle codes for the results of this paper can be found at
\url{http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/spi/}.  
In the statement of lemma or theorem, a name given in \texttt{typewriter}
font indicates the name of the relevant theorem in our Isabelle development.
We show selected theorems and definitions in the text,
and more in the Appendix.
A version of the paper, including the Appendix, is in 
\url{http://users.rsise.anu.edu.au/~jeremy/pubs/spi/fotesb/}.  
% In many cases where the Isabelle code contains no specific features of
% interest, it is relegated to the Appendix.
So now we indicate some key points of the Isabelle notation.
\begin{itemize}
\item A name preceded by \texttt{?} indicates a variable: other names are 
entities which have been defined as part of the theory
\item Conclusion $\beta$ depending on assumptions $\alpha_i$ is
\texttt{[|}
$\alpha_1 \texttt{;} \alpha_2 \texttt{;} \ldots \texttt{;} \alpha_n$
\texttt{|] ==> } $\beta$
\item $\forall$, $\exists$ are written as \texttt{ALL}, \texttt{EX} 
\item $\subseteq$, $\supseteq$, $\in$ are written as
  \texttt{<=}, \texttt{>=}, \texttt{:} 
%\item TO DO - add as necessary
\end{itemize}

