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

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. 


%% \paragraph{Spi calculus has been formalised before; what's new here?}
%% This work is new because:
%% \begin{itemize}
%% \item It's about open bisimulation; no-one has even attempted
%%   formalizing open bisimulation for spi-calculus (or even the
%%   $\pi$-calculus, although there is a recent work in encoding open
%%   bisimulation in a logical framework (\cite{tiu09tocl}), but no
%%   metatheory is proved within the framework).  Besides, the notion of
%%   bi-traces here is new, and is significantly different from the
%%   notion of ``frames'' (as in frame bisimulation) or ``hedges'' (in
%%   hedged bisimulation).  One important different is that these other
%%   bisimulations are basically {\em concrete bisimulation} (as opposed
%%   to symbolic), so they do not consider problems such as: what is a
%%   good notion of consistency that is stable under substitutions, etc.

%% \item We are interested in decidability proofs. Previous
%%   formalisations were only concerned with proving some meta theory,
%%   such as, reflexitivity, transitivity of bisimulation etc.  Also note
%%   that in general, decidability proofs are difficult to formalize in
%%   Isabelle/HOL without a significant library on computability theory,
%%   which, as far as we know, does not exist yet.

%% \item Formalising decidability is difficult.. [INSERT SOME COMMENTS
%%   ABOUT URBAN'S LICS PAPER]

%% \end{itemize}

%% \paragraph{Why bother formalizing the intruder theory? Aren't they obvious?}
%% Symbolic techniques for process calculi are in general very dense and
%% technical (see, for instance, descriptions of symbolic bisimulation in
%% \cite{borgstrom04concur,briais07tcs,delaune07fsttcs}), and as far as
%% we know, there is currently no formalisation of various notions of
%% symbolic bisimulations found in the literature, although a few have
%% been implemented.  Our formalisation has also helped us uncover some
%% mistakes in proofs of some important lemmas.

%%%

%% NOTE - TPHOLs LENGTH LIMIT IS 16pp

%% ADD INTRO TO THE SUBJECT MATTER 

%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}