
\documentclass{beamer}
% \documentclass[handout]{beamer} % for handout

\usetheme{Frankfurt}
\usecolortheme{seahorse}
\usepackage{proof}

% \usetheme{split}

\newcommand\comment[1]{} 
\comment% \AtBeginSection[]%
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection]
   \end{frame}
}
\comment% \AtBeginSubsection[]%
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection,currentsubsection]
   \end{frame}
}

\title{Formalising Observer Theory for Environment-Sensitive Bisimulation}
\author{Jeremy Dawson and Alwen Tiu}
\institute{
Logic and Computation Group
\\School of Computer Science
\\College of Engineering and Computer Science
\\ Australian National University
\\ Canberra ACT 0200, Australia
\\ \url{http://users.rsise.anu.edu.au/~jeremy/}
\ \ \url{http://users.rsise.anu.edu.au/~tiu/}
}

\begin{document}

\newcommand\spr[2]{\langle #1, #2 \rangle}
\newcommand\enc[2]{\{#1\}_{#2}}
\newcommand\pairM{\ensuremath{\langle M_a, M_b \rangle}}
\newcommand\pairN{\ensuremath{\langle N_a, N_b \rangle}}
\newcommand\encM{\ensuremath{\{ M_p \}_{M_k}}}
\newcommand\encN{\ensuremath{\{ N_p \}_{N_k}}}

\newcommand\GammaR{\ensuremath{\Gamma {\Downarrow}}}

\def\eqm{\leftrightarrow}
\def\rna{{\mathbf a}}
\def\rnb{{\mathbf b}}
\def\rnc{{\mathbf c}}
\def\rnd{{\mathbf d}}

\frame{\titlepage}

% \section[Outline]{}
\frame
{
  \frametitle{Outline}
  \tableofcontents}

% \section{Section title} 
% \subsection{Subsection title} 
% \frame
% {
  % \frametitle{Frame title}
  % \framesubtitle{Frame subtitle}
% }

\section{Observer theories}
\frame
{
  \frametitle{Observer theories}
We consider a formalisation of a notion of \alert{observer theories}.
\begin{itemize}
\item used in various ``environment-sensitive'' bisimulation for
process calculi, e.g., the spi-calculus.
\item describes the knowledge and capabilities of an observer
\item given a formal account using deductive systems
\end{itemize}
Two critical notions:
\begin{itemize}
\item \alert{decidability} of message deduction by the observer 
\item \alert{consistency} of a given theory
\end{itemize}
We formalise a theory in Isabelle/HOL,
encoding observer theories as pairs of symbolic traces.
  }

\subsection{Messages} 
\begin{frame}[fragile]
  \frametitle{Messages}
  Messages are formed from
  \begin{itemize}
  \item ``names'' (or flexible names), $a$, $x$, $y$ : like variables
  \item rigid names, $\rna$, $\rnb$ : like constants
  \item pairs of messages, $\spr{M}{N}$,
  \item symmetric encryption, $\enc M K$, (key $K$, message $M$) 
\end{itemize}
\begin{verbatim}
datatype msg = Name nat 
             | Rigid nat 
             | Mpair msg msg 
             | Enc msg msg
\end{verbatim}
\end{frame}

\subsection{Message indistinguishability} 
\frame
{
  \frametitle{Message indistinguishability}

  Can an observer differentiate two processes
  based on the messages output by the processes? \\[1ex]

  With encryption, indistinguishability is not just syntactic equality
  (one encrypted message looks ``just like'' another).  \\[1ex]

  For $\Gamma$ an observer theory (a finite set of pairs of messages),
  $ \Gamma \vdash M \eqm N $ 
  means the observer cannot distinguish between $M$ and $N$,
  given the {\em indistinguishability assumption} $\Gamma$ \\[1ex]

In Isabelle, $(\Gamma, M, N) \in \texttt{indist}$
\\[1ex]
Data structures involving pairs of messages 
can be projected to the first (or second) component. 
Thus $\pi_i(X)$, $i = 1,2$, for $X$ a pair, theory, bi-trace, sequent, etc.
  }

\frame
{
  \frametitle{Proof system for message indistinguishability}

$$
\infer[(var)]
{\Gamma \vdash x \eqm x}
{x \in \mathcal N}
\qquad
\infer[(id)]
{\Gamma \vdash M \eqm N}
{(M, N) \in \Gamma}
$$
$$
\infer[(pr)]
{\Gamma \vdash \pairM \eqm \pairN}
{\Gamma \vdash M_a \eqm N_a & \Gamma \vdash M_b \eqm N_b}
$$
$$
\infer[(er)]
{\Gamma \vdash \encM \eqm \encN}
{\Gamma \vdash M_p \eqm N_p & \Gamma \vdash M_k \eqm N_k}
$$
$$
\infer[(pl)]
{\Gamma, {(\pairM,\pairN)} \vdash M \eqm N}
{\Gamma, (M_a, N_a), (M_b, N_b) \vdash M \eqm N}
$$
$$
\infer[(el)]
{\Gamma, {(\encM,\encN)} \vdash M \eqm N}
{\Gamma \vdash M_k \eqm N_k &
\Gamma, (M_p, N_p), (M_k, N_k) \vdash M \eqm N}
$$
Cut-admissibility and some invertibility results hold

}
  
\comment{
\frame
{
  \frametitle{Lemmas regarding the proof system (Tiu, 2007) OMIT ??}
\begin{lemma}[Cut-admissibility]
If $\Gamma \vdash M \eqm N$ and $\Delta, (M,N) \vdash R \eqm T$
then $\Gamma \cup \Delta \vdash R \eqm T$ \\[1ex]
\end{lemma}

\begin{lemma}[Partial invertibility of rules] 
\begin{itemize}
\item
$\Gamma, (\spr {M_a} {M_b}, \spr {N_a} {N_b}) \vdash M \eqm N$
$\Longleftrightarrow$ % if and only if
$\Gamma, (M_a, N_a), (M_b, N_b) \vdash M \eqm N$  \\[1ex]

\item
If $\Gamma, (\enc {M_p} {M_k}, \enc {N_p} {N_k}) \vdash M_k \eqm N_k$,
then
$\Gamma, (\enc {M_p} {M_k}, \enc {N_p} {N_k}) \vdash M \eqm N$
$\Longleftrightarrow$ % if and only if
$\Gamma, (M_p, N_p), (M_k, N_k) \vdash M \eqm N$  \\[1ex]

\item
  $\Gamma \vdash \spr {M_a} {M_b} \eqm \spr {N_a} {N_b}$ 
  $\Longleftrightarrow$ \\ % if and only if 
  $\Gamma \vdash M_a \eqm N_a$ and
  $\Gamma \vdash M_b \eqm N_b$ \\[1ex]

\item
  If $\Gamma \vdash M_k \eqm N_k$ then \\
  $\Gamma \vdash \enc {M_p} {M_k} \eqm \enc {N_p} {N_k}$ 
  $\Longleftrightarrow$ % if and only if 
  $\Gamma \vdash M_p \eqm N_p$ 
  \end{itemize}
  \end{lemma}
  }
  }


\subsection{Observer theory consistency} 
\frame
{
  \frametitle{Observer theory consistency}
  Intuitively, is the theory plausibly a set of pairs of messages which the
  observer would see as indistinguishable ? \\[1ex]

  For example, % the theory
  $
  \{ (\textcolor{blue}{\enc \rna \rnb}, 
      \textcolor{green}{\enc \rnc \rnd}),
  (\textcolor{blue}\rnb, \textcolor{green}\rnc)
  \}
  $
  is not consistent, since
  \begin{itemize}
  \item 
 %  on the first projection (i.e., the set $\{\enc \rna \rnb, \rnb\}$),
  one can decrypt %the first message
  \textcolor{blue}{$\enc \rna \rnb$} using % the second message
  \textcolor{blue}{$\rnb$}, but
  \item
  % the same operation cannot be done on the second projection.
  one cannot decrypt %the first message
  \textcolor{green}{$\enc \rnc \rnd$} using % the second message
  \textcolor{green}{$\rnc$}
  \end{itemize}
  
\comment{
\begin{definition}[consistent] % (equivalent, see Definition 9, Lemma 10(a))
  A theory $\Gamma$ is {\em consistent} if for every $M$ and $N$, if
  $\Gamma \vdash M \eqm N$ then the following hold:
  \begin{itemize}
  \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 for every $M', N', M_p, N_p$
  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{itemize}
\end{definition}
end of comment }

\begin{definition}[consistent] %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{itemize}
\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{itemize}
\end{definition}

  }

\section{Decidability of $\vdash$}
\frame
{
\frametitle {Decidability of $\vdash$}

want consistency to be decidable --- involves
deciding $\Gamma \vdash M \eqm N$

\begin{itemize}
\item
Naive approach to testing $\Gamma \vdash M \eqm N$
can loop: \\ in $(el)$ rule, left premise can equal the conclusion

\item
Finiteness argument shows decidability since backwards proof only
introduces sub-messages of messages in conclusion

\item
but we want a more focussed procedure than exhaustive search

\item
\alert{theory reduction}: we ``reduce'' a theory to its ``simplest'' form
\end{itemize}
  }

\frame
{
\frametitle {Theory reduction}
As originally defined (Tiu, 2007)
\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 } \alert{\Gamma, (\encM,\encN) \vdash M_k \leftrightarrow N_k}
\end{eqnarray*}
(assume $(\pairM,\pairN) \not\in \Gamma$\ ;   
$(\encM,\encN) \not\in \Gamma$)  
% (otherwise reduction would not terminate)

This involves deciding whether
$ {\Gamma, (\encM,\encN) \vdash M_k \leftrightarrow N_k}$

Alternative definition:
\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 } \alert{\Gamma \vdash M_k \leftrightarrow N_k}
\end{eqnarray*}
This involves deciding 
$ {\Gamma \vdash M_k \leftrightarrow N_k}$
(a \emph{smaller} theory $\Gamma$).
}

\subsection{Theory reduction} 
\frame
{
  \frametitle{Results about theory reduction}

\begin{lemma}
\begin{enumerate}
\item \label{indist-nc}
If $\Gamma \longrightarrow \Gamma'$
then $\Gamma \vdash M \eqm N$ if and only if
$\Gamma' \vdash M \eqm N$
\item 
$\longrightarrow$ is well-founded (total size reduces)
\item
As $\longrightarrow'\ \subseteq\ \longrightarrow$,
the above hold for $\longrightarrow'$ also.
\item \label{red-confl}
$\longrightarrow$ is confluent 
\end{enumerate}
\end{lemma}


Proof of (\ref{red-confl}): By (\ref{indist-nc}),
side condition $\Gamma \vdash M_k \eqm N_k$
iff $\Gamma' \vdash M_k \eqm N_k$
% so confluence seems easy.
(Isabelle proof difficult, number of cases explodes).

\begin{theorem}
\begin{itemize}
\item
$\Gamma$ has a $\longrightarrow$-normal form $\GammaR$
\item
$\Gamma \vdash M \eqm N$ if and only if $\GammaR\ \vdash M \eqm N$
\end{itemize}
\end{theorem}

\begin{theorem}
$\GammaR\ \vdash M \eqm N$ if and only if $\GammaR\ \vdash_R M \eqm N$
\end{theorem}
}

\frame
{
  \frametitle{Use of theory reduction}

  We define a \alert{right} derivation 
$\textcolor{black}{\vdash_R}$
$$
\infer[(var)]
{\Gamma\ \textcolor{black}{\vdash_R}\ x \eqm x}
{x \in \mathcal N}
\qquad
\infer[(id)]
{\Gamma\ \textcolor{black}{\vdash_R}\ M \eqm N}
{(M, N) \in \Gamma}
$$
$$
\infer[(pr)]
{\Gamma\ \textcolor{black}{\vdash_R}\ \pairM \eqm \pairN}
{\Gamma\ \textcolor{black}{\vdash_R}\ M_a \eqm N_a & \Gamma\
\textcolor{black}{\vdash_R}\ M_b \eqm N_b}
$$
$$
\infer[(er)]
{\Gamma\ \textcolor{black}{\vdash_R}\ \encM \eqm \encN}
{\Gamma\ \textcolor{black}{\vdash_R}\ M_p \eqm N_p & \Gamma\
\textcolor{black}{\vdash_R}\ M_k \eqm N_k}
$$

Now $\Gamma\ \textcolor{black}{\vdash_R}\ M \eqm N$
is obviously decidable (just keep decomposing the right-hand side,
and testing for $(id)$ rule).

\begin{theorem} % Isabelle: [reduce_nc, virt_reduce RS sym] MRS trans ;
$\GammaR\ \vdash M \eqm N$ if and only if $\GammaR\ \vdash_R M \eqm N$
\end{theorem}

  }

\subsection{The alternative theory reduction} 
\frame
{
  \frametitle{The alternative theory reduction $\longrightarrow'$}

\begin{theorem}
\begin{itemize}
\item
If $\Gamma$ is $\longrightarrow$-reducible,
then it is $\longrightarrow'$-reducible,
(though the same reduction may not be available)
(long proof in paper)
\item
Thus (as $\longrightarrow'\ \subseteq\ \longrightarrow$)
$\GammaR$ is also the $\longrightarrow'$-normal form of $\Gamma$
\end{itemize}
\end{theorem}

\begin{theorem}
$\Gamma \vdash M \leftrightarrow N$ is decidable
\end{theorem}

% Now we get decidability:
% to decide whether $\Gamma \vdash M \leftrightarrow N$:
Procedure: calculate $\GammaR$ and determine whether
$\GammaR\ \vdash_R M \leftrightarrow N$. \\[1ex]
Calculating $\GammaR$ (\emph{using $\longrightarrow'$)}
requires deciding questions of the form
$\Gamma' \vdash M_k \leftrightarrow N_k$, 
where $\Gamma'$ is \emph{smaller} than $\Gamma$
(because a pair (\encM,\encN) is omitted). \\[1ex]
Thus this procedure terminates.
  }

\comment{
\subsection{Another proof: normal derivations} 
\frame
{
  \frametitle{Another proof: normal derivations OMIT ??}
Recall the \alert{right} derivation $\textcolor{green}{\vdash_R}$;
  we define a \alert{normal} derivation $\textcolor{blue}{\vdash_N}$
$$
\infer[(virt)]
{\Gamma \ \textcolor{blue}{\vdash_N}\ M \eqm N}
{\Gamma\ \textcolor{green}{\vdash_R}\ M \eqm N}
$$
$$
\infer[(pl)]
{\Gamma, {(\pairM,\pairN)}\ \textcolor{blue}{\vdash_N}\ M \eqm N}
{\Gamma, (M_a, N_a), (M_b, N_b)\ \textcolor{blue}{\vdash_N}\ M \eqm N}
$$
$$
\infer[(el)]
{\Gamma, {(\encM,\encN)}\ \textcolor{blue}{\vdash_N}\ M \eqm N}
{\Gamma\ \textcolor{green}{\vdash_R}\ M_k \eqm N_k &
\Gamma, (M_p, N_p), (M_k, N_k)\ \textcolor{blue}{\vdash_N}\ M \eqm N}
$$
  }

\frame
{
  \frametitle{Using normal derivations OMIT ??}
\begin{theorem}[normal derivation]
${\Gamma \vdash_N M \eqm N}$ iff ${\Gamma \vdash M \eqm N}$
\end{theorem}

So we define yet another reduction relation $\longrightarrow_R$,
like $\longrightarrow'$, but with side condition 
     ${\Gamma \vdash_R M_k \leftrightarrow N_k}$:
so clearly $\longrightarrow_R\ \subseteq\ \longrightarrow$.\\[1ex]

Then we can get a similar result to that for $\longrightarrow'$ 
\begin{theorem}
\begin{itemize}
\item
If $\Gamma$ is $\longrightarrow$-reducible,
then it is $\longrightarrow_R$-reducible,
(though the same reduction may not be available)
\item
Thus (as $\longrightarrow_R\ \subseteq\ \longrightarrow$)
$\GammaR$ is also the $\longrightarrow_R$-normal form of $\Gamma$
\item
As ${\Gamma \vdash_R M \eqm N}$ is decidable,
so $\GammaR$ is computable.
\end{itemize}
\end{theorem}


% Also ${\Gamma, (\encM,\encN) \vdash_R M_k \leftrightarrow N_k}$ iff
% ${\Gamma \vdash_R M_k \leftrightarrow N_k}$, trivially, since 
% $M_k$ is \emph{smaller} than \encM.

}
end of comment }

\subsection{Theory reduction and consistency}
\frame
{
  \frametitle{Theory reduction and consistency (Tiu, 2007)}
  \begin{lemma}  % Isabelle: reduce_cons
  \begin{itemize}
  \item 
If $\Gamma \longrightarrow \Gamma'$
then $\Gamma$ is consistent if and only if $\Gamma'$ is consistent
  \item 
$\Gamma$ is consistent if and only if $\GammaR$ is consistent
  \end{itemize}
  \end{lemma}
 \begin{lemma}
 There is a simpler, finitely checkable,
  characterisation of consistency for a reduced theory $\Gamma$:
  \begin{description}
  \item[using]
  ``for every $(M,N) \in \Gamma$ \ldots''
  \item[not]
  ``for every $M$ and $N$, if $\Gamma \vdash M \eqm N$ then \ldots''
  \end{description}
 \end{lemma}

Thus theory consistency is decidable 
  
  }

\section{Proving decidability or computability}
\frame
{
  \frametitle{Proving decidability or computability}
  To prove computability \alert{formally} 
  requires modelling the computation process, but
  we can prove it \alert{``semi-formally''}: \\[1ex]

  We have a definition of ${\Gamma \vdash_R M \eqm N}$
  in Isabelle as an \alert{inductively defined set} (rules above);
  % We have set out rules above for ${\Gamma \vdash_R M \eqm N}$,
  we gave another corresponding definition as a \alert{recursive function}
  % \texttt{is\_der\_virt} (here, $\vdash_f$), eg
   (here, $\vdash_f$), eg
  \begin{eqnarray*}
  \lefteqn{\Gamma \vdash_f \spr {M_a} {M_b} \eqm \spr {N_a} {N_b}  
  \Longleftrightarrow} \\ % if and only if 
  & & (\spr {M_a} {M_b}, \spr {N_a} {N_b}) \in \Gamma\  \lor\ 
  (\Gamma \vdash_f M_a \eqm N_a \land
  \Gamma \vdash_f M_b \eqm N_b)
  \end{eqnarray*}

  \begin{itemize}
  \item
  Isabelle \alert{makes us prove} that the recursive 
  definition of $\vdash_f$ terminates.
  % function \texttt{is\_der\_virt} terminates. \\[1ex]

  \item
  We can \alert{inspect} to see the absence of any further ``infinite'' features
  (eg testing for membership of an infinite set,
  quantification over an infinite set) \\[1ex]

  \item
  We then \alert{proved} ${\Gamma \vdash_R M \eqm N}$ iff
  ${\Gamma \vdash_f M \eqm N}$  
  \end{itemize}
}

\frame
{
  \frametitle{Decidability of reduction}
  
  For theory reduction using $\longrightarrow'$,
  \begin{itemize}
  \item
  reducing $\Gamma$ (calculating $\GammaR$)
  required deciding ${\Gamma' \vdash M_k \eqm N_k}$,
  for some $\Gamma'$ \alert{smaller} than $\Gamma$,
  \item
  deciding ${\Gamma' \vdash M_k \eqm N_k}$ required calculating 
  ${\Gamma' {\Downarrow}}$ (and then testing
  ${\Gamma' {\Downarrow} \vdash_R M_k \eqm N_k}$)
  \end{itemize}
  
 ~ \\[-1ex]
  
  Definition of reduction as a function is further complicated by the fact that
  the single-step reduction relation is not deterministic. \\[1ex]

  We defined a function \texttt{reduce} which chooses a possible reduction,
 %  (this is recursive as explained above)
  performs it, and then reduces the result. \\[1ex]

  Isabelle wasn't able to prove the termination conditions automatically,
  so we had to use \texttt{recdef (permissive)}.
}

\frame
{
  \frametitle{The reduction function --- using \texttt{recdef (permissive)}}

  We had to prove that the measure function gets smaller,
  and thereby simplify the simplification rules produced by Isabelle \\[1ex]

  That is, with a definition (measure function $m$) :
  $\texttt{reduce}\ S = \ldots \mbox{ if } m(F(S)) < m(S) \mbox{ then } F(S) 
  \mbox{ else arbitrary } \ldots $
  we had to prove that the \mbox{arbitrary} clause never applied \\[1ex]

  Finally we proved that \texttt{reduce} gives the $\longrightarrow'$-normal
  form. \\[1ex]

  Then, by inspection of the text of the definition,
  we asserted that there was no part of it whose computation would not be
  finite.
  }

\section{Bi-traces and respectful substitutions}
\frame
{
  \frametitle{Bi-traces and respectful substitutions}
  \begin{definition}
  \begin{itemize}
  \item 
  A \emph{bi-trace} is an \emph{ordered} set (a list) of message pairs,
  each marked as $i$ (input) or $o$ (output),
  where any free name first appears in an input pair.
  \item A \emph{substitution pair} is a pair of mappings 
  $\vec\theta = (\theta_1, \theta_2)$ from free names to messages,
  where $\theta_1 (\theta_2)$ applies to the first (second) message of any pair.
  \item
  a \emph{respectful} substitution is (roughly) 
  a substitution where for each variable $x$ in an input pair, 
  $\Gamma\vec\theta \vdash x\theta_1 \eqm x\theta_2$
  where $\Gamma$ is the set of previous pairs
  (that is, input messages are only those which an outsider is capable of
  creating)
  \end{itemize}
  \end{definition}
  }

\section{Consistent bi-traces}
\frame
{
  \frametitle{Consistent bi-traces}
  \begin{definition}[Consistent bi-trace]
  A bi-trace is \emph{consistent} if \\
  \ldots for \emph{every} respectful substitution
  pair $\vec\theta$, $\Gamma\vec\theta$ is a consistent theory
  \end{definition}

The quantification makes deciding this difficult (work in progress).

But note, the definition of respectful substitution involves the \alert{order}
of pairs; deciding whether a theory is consistent involves reducing it,
which requires an \alert{unordered} theory.

So we defined a variant of respectfulness:
  \begin{definition}[\texttt{thy\_strl\_resp}]
  A substitution pair $\vec\theta$ satisfies 
  \texttt{thy\_strl\_resp} for $\Gamma$ and $p$ if, for each $x$ in $\Gamma$,
  $(\Gamma|{p(x)})\ \vec\theta \vdash x\theta_1 \eqm x\theta_2$ 
  where $\Gamma|{p(x)}$ is got by removing message pairs containing
  free names other than those in ${p(x)}$ from $\Gamma$
  \end{definition}
  }

\frame
{
  \frametitle{Theory reduction and \texttt{thy\_strl\_resp}}

  \begin{lemma}
  % Isabelle strl_resp_oth_red
  % Isabelle thy_strl_resp_reduce
  For given $\theta$ and $p$ (see below),
  if $\Gamma$ satisfies \texttt{thy\_strl\_resp}
  \begin{itemize}
  \item
  if $\Gamma \longrightarrow \Gamma'$,
  then $\Gamma'$ satisfies \texttt{thy\_strl\_resp}
  \item
  $\GammaR$ satisfies \texttt{thy\_strl\_resp}
  \end{itemize}
  \end{lemma}
   We use this result where $p(x)$ is
  the set of free names which appeared prior to $x$ in the bi-trace
  from which $\Gamma$ was obtained. \\[1ex]
  This definition and result enabled us to combine the ideas of 
  reduction of an \alert{unordered} theory with the respectfulness of a
  substitution pair with respect to an \alert{ordered} bi-trace.
  }

\section{Unique Completion of a Respectful Substitution}
\frame
{
  \frametitle{Unique Completion of a Respectful Substitution}
In analysing bi-trace consistency (``for \emph{all} respectful substitutions''), 
the following result is useful.


\begin{theorem} \label{t-subst-exists-unique}
Given a consistent bi-trace $h$
whose projections to a single message trace are $s_1$ and $s_2$,
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 $\pi_2(h)$
\end{theorem}

Given $\theta_1$ we want to compute $\theta_2$.
  }

\frame
{
  \frametitle{Computing the Unique Completion}


First we defined a function \texttt{match\_rc1} which,
given a theory $\Gamma$ and a message $M$,
``attempts'' to determine a message $N$ such that $\Gamma \vdash M \eqm N$.
($N$ is unique if $\Gamma$ is consistent).

\begin{theorem} 
If $\Gamma$ is consistent, then \\ $\Gamma \vdash M \eqm N$ iff
\texttt{match\_rc1} $\GammaR\ M = \texttt{Some}\ N$
\end{theorem}

Then we defined a function \texttt{second\_sub}, using \texttt{match\_rc1},
to find the appropriate value of $x \theta_2$ for
each new $x$ in the bi-trace
\begin{theorem} 
If $h$ is a consistent bi-trace, and $\theta_1$ satisfies the respectfulness
condition for $\pi_1(h)$, and $\theta_2 = \texttt{second\_sub}\ h\ \theta_1$,
then $(\theta_1, \theta_2)$ respects $h$
\end{theorem}

Informal arguments show that \texttt{match\_rc1} and \texttt{second\_sub}
are finitely computable.  
  }

\section{Conclusion}
\frame
{
  \frametitle{Conclusion : value of the formalisation}
  
\begin{itemize}
\item theories very intricate, with low-level detail 
\item details can be overlooked in paper proofs, we have found bugs
\item symbolic decision procedures (on-going work)
  are often very technical and complicated;
  no-one has verified any symbolic techniques for process calculi
  as far as we know: this is a first attempt
\item it has helped us find better proofs about reduction and respectful
  substitutions
\item theorem proving system helps keep track of results proved 
  (numerous when several different definitions of reduction and sets of
  rules for deriving $\Gamma \vdash M \eqm N$)
\end{itemize}


}
\end{document}
\comment{
  }

