\section{Respectful Substitutions and Bi-trace Consistency} \label{s-bt}

We now consider a symbolic representation of observer theories
from \cite{tiu-trace-based-bisim-abs}, given below. 
We denote with $fn(M)$ the set of names in $M$. 
This notation is extended straightforwardly to pairs of messages,
lists of (pairs of) messages, etc.

\begin{definition}
\label{def:bi-traces}
A {\em bi-trace} is a {\em list} of message pairs marked with
$i$ (indicating input) or $o$ (output), i.e., elements 
in a bi-trace have the form $(M,N)^i$ or $(M,N)^o$.
Bi-traces are ranged over by $h$. We denote with $\pi_1(h)$ the list obtained
from $h$ by taking the first component of the pairs in $h$.
The list $\pi_2(h)$ is defined analogously.
Bi-traces are subject to the following restriction: 
if $h = h_1.(M,N)^o.h_2$ then $fn(M,N) \subseteq fn(h_1).$
We write $\{h\}$ to denote the set of message pairs
obtained from $h$ by forgetting the marking and the order.
\end{definition}

Names in a bi-trace represent {\em symbolic values} which are
input by a process at some point. This explains the requirement 
that the free names of an output pair in a bi-trace 
must appear before the output pair.
We express this restriction on name occurrences by defining 
a predicate \texttt{validbt} on lists of marked message pairs, 
and we do not mention it in the statement of each result, 
although it does appear in their statements in Isabelle.  
In our Isabelle representation the list is reversed, so that the latest
message pair is the first in the list.
The theory $\{h\}$ obtained from a bi-trace $h$
is represented by \texttt{oth\_of} $h$.
Likewise for a list $s$ of marked messages (which can be seen
as a symbolic trace \cite{boreale}), 
we can define the set $\{s\}$ of messages by  
forgetting the annotations and ordering.

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$.

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

Given Lemma~\ref{l-pres-bt-cons}\ref{l-cons-subs-bt} below,
it may appear that leaving out the underlined words of 
Definition~\ref{d-bt-cons} would make no difference.
This minor fact can indeed be proved formally: details are given in
Appendix~\ref{vd-bt-cons}.
 

The following are significant lemmas from 
\cite{tiu-trace-based-bisim-full} which we proved in Isabelle.
As an illustration of the value of automated theorem proving, 
we found that the original proof of \ref{l-bt-resp-comp} in a draft of
\cite{tiu-trace-based-bisim-full} contained an error 
(which was easily fixed).

\begin{lemma} \label{l-pres-bt-cons}
\begin{enumerate}
\item \cite[Lemma~24]{tiu-trace-based-bisim-full}
  \texttt{\upshape(subst\_indist)} \label{l-subst-indist}
Let $\Gamma \vdash M \eqm N$ and let $\vec \theta = (\theta_1,\theta_2)$
be a substitution pair such that 
for every free name $x$ in $\Gamma$, $M$ or $N$,
$\Gamma\vec\theta \vdash \theta_1(x) \eqm \theta_2(x)$.
Then $\Gamma\vec\theta \vdash M\theta_1 \eqm N\theta_2$.

\item \cite[Lemma~40]{tiu-trace-based-bisim-full}
  \texttt{\upshape(bt\_resp\_comp)} \label{l-bt-resp-comp}
Let $h$ be a consistent bi-trace,
let $\vec\theta = (\theta_1,\theta_2)$ be an $h$-respectful substitution pair,
and let $\vec\gamma = (\gamma_1,\gamma_2)$
be an $h\vec\theta$-respectful substitution pair. 
Then $\vec\theta \circ \vec\gamma$ is also $h$-respectful.

\item \cite[Lemma~41]{tiu-trace-based-bisim-full}
\texttt{\upshape(cons\_subs\_bt)} \label{l-cons-subs-bt}
If $h$ is a consistent bi-trace and $\vec \theta = (\theta_1,\theta_2)$
respects $h$, then $h \vec \theta$ is also a consistent bi-trace.
\end{enumerate}
\end{lemma}

\subsubsection{Respectfulness of a substitution relative to a theory}
Testing consistency of bi-traces 
involves testing whether a theory $\Gamma$ is consistent after applying any
respectful substitution pair $\vec\theta$ to it.
We will present some results that (under certain conditions)
if we reduce $\{h\}$ first, and then apply an $h$-respectful substitution,
then the result is a reduced theory,
to which the simpler test for consistency, \texttt{thy\_cons\_red}, applies. 

The complication here is that reduction applies to a theory 
%(an unordered set of pairs of messages) 
whereas the definition of bi-trace
consistency crucially involves the ordering of the pairs of messages.
We overcome this by devising the notion, \texttt{thy\_strl\_resp},
of a substitution being respectful 
with respect to an (unordered) theory and an ordered list of sets of
variable names. 
%
Importantly,
this property holds for $\{h\}$ where $\vec\theta$ is $h$-respectful,
and it is preserved by reducing a theory.
We use this to prove some later results 
involving $\irred{\{h\}}$ and $h$-respectful substitutions,
such as Theorem~\ref{t-bit-con}.
Details are in Appendix~\ref{v-thy-resp}.
% We define \texttt{fn\_bt} $h$,
% the list of sets of free names of a bi-trace $h$, in the natural way,
% see Appendix~\ref{v-fn-bt}.


\subsubsection{Simplifying testing consistency after substitution}
\label{s-test-bt-cons}
Recall that a theory $\Gamma$ is consistent
if and only if $\GammaR$ is consistent
(Lemma~\ref{l-tc-equiv}\ref{l-nf-cons}),
and if and only if $\Gamma \setminus \Ne$ is consistent 
(Lemma~\ref{l-tc-equiv}\ref{l-thy-cons-equivd}).
Thus, to determine whether $\Gamma$ is consistent,
one may calculate $\GammaR$ or $\GammaRNe$ 
(which is reduced, by Lemma~\ref{l-Ne}\ref{l-rsmin-names}),
and use the function \texttt{thy\_cons\_red} 
(by virtue of Theorem~\ref{t-thy-cons-red}\ref{l-tc-red-iff}).
Therefore, the naive approach to testing bi-trace consistency
is to apply $\theta$ to $\Gamma$ and then reduce the result,
and delete pairs $(x,x) \in \Ne$.
We can derive results which permit a simpler approach.

\begin{theorem} \label{t-bit-con}
Let $h$ be a bi-trace, and let $\Gamma = \{h\}$.
Let $\vec\theta$ be an $h$-respectful substitution pair,
and denote its action on $\Gamma$ by $\vec\theta$ also.
\begin{enumerate}
\item \texttt{\upshape(nf\_subst\_nf\_Ne)} \label{nf-subst-nf-Ne}
$\RNe{\Gamma\vec\theta} = \RNe{(\GammaRNe)\vec\theta}$
\item \texttt{\upshape(subst\_nf\_Ne\_tc)} \label{subst-nf-Ne-tc}
$ \Gamma \vec\theta$ is consistent if and only if 
$(\GammaRNe)\vec\theta$ is consistent
\end{enumerate}
\end{theorem}
%% \begin{proof}
%% \ref{subst-nf-Ne-tc} follows from \ref{nf-subst-nf-Ne} using 
%% Theorem~\ref{l-Ne}\ref{nf-equiv-der} and
%% Lemma~\ref{l-tc-equiv}\ref{l-cons-der-same}
%% \end{proof}

This, given a bi-trace $h$ and a respectful substitution pair $\vec\theta$,
if one wants to test whether
$\Gamma\vec\theta = \{h\vec\theta\}$ is consistent, 
it makes no difference to the consistency of the resulting theory if one
  reduces the theory and deletes pairs $(x,x)$ before substituting.
This means that we need only consider substitution in a theory which is reduced
and has pairs $(x,x)$ removed.

If we disallow encryption where keys are themselves pairs or encrypts,
then further simplification is possible.
Thus we will require that keys are atomic 
(free names or rigid names, \texttt{Name} $n$ or \texttt{Rigid} $n$),
both initially and after substitution.

\begin{theorem}[\texttt{subs\_not\_red\_ka}] \label{t-subs-not-red-ka}
Let $\Gamma$ be reduced, consistent and have atomic keys. 
Then $(\Gamma \setminus \Ne) \vec\theta$ is reduced.
\end{theorem}

Thus, if keys are atomic, the effect of 
Theorem~\ref{t-subs-not-red-ka} is to
simplify the consistency test thus:
to test the consistency of the substituted theory $\Gamma\vec\theta$,
one reduces $\Gamma$ to $\GammaR$ and deletes pairs $(x,x)$ to get 
$\Gamma' = \GammaRNe$.
One then considers substitution pairs $\vec\theta$ of $\Gamma'$,
knowing that any $\Gamma'\vec\theta$ is reduced 
and so the simpler criterion for theory consistency,
\texttt{thy\_cons\_red}, applies to it.
Thus we get:
% Consequently we get the following theorem.

\begin{theorem} \label{t-nfs-comm}
Let $h$ be a bi-trace, and let $\Gamma = \{h\}$,
where $\Gamma$ is consistent with atomic keys. 
Let $\vec\theta$ be an $h$-respectful substitution pair,
and write $\Gamma\vec\theta = \{h\vec\theta\}$. % Then 
% and denote its action on $\Gamma$ by $\vec\theta$ also.
\begin{enumerate}
\item \texttt{\upshape(nfs\_comm)} \label{nfs-comm}
$\RNe{\Gamma \vec\theta} = (\GammaRNe) \vec\theta \setminus \Ne$ 
\item \texttt{\upshape(nfs\_comm\_tc)} \label{nfs-comm-tc}
$\Gamma \vec\theta$ is consistent iff
\texttt{thy\_cons\_red} holds of 
 $(\GammaRNe) \vec\theta \setminus \Ne$ 
\end{enumerate}
\end{theorem}
%% \begin{proof}
%% \begin{enumerate}
%% \item
%%  follows from Theorem~\ref{t-subs-not-red-ka} and
%% Theorem~\ref{t-bit-con}\ref{nf-subst-nf-Ne}
%% \item
%% follows from \ref{nfs-comm},
%% Lemma~\ref{l-tc-equiv}\ref{l-thy-cons-equivd} and \ref{l-nf-cons},
%% Lemma~\ref{l-Ne}\ref{l-rsmin-names} and
%% Theorem~\ref{t-thy-cons-red}\ref{l-tc-red-iff}
%% \end{enumerate}
%% \end{proof}

 \subsubsection{Unique Completion of a Respectful Substitution}
A bi-trace can be projected into the fist or second component of each pair,
giving lists of marked messages.
We can equally project the definition of a respectful substitution pair,
so that for a list $s$ of marked messages,
substitution $\theta_i$ respects $s$,
$s \in$ \texttt{sm\_resp} $\theta_i$, iff 
for every free name $x$ in an input message $M^i$,
$\{s'\}\theta_i \vdash x\theta_i$,
where $\vdash$ is here the message synthesis relation, 
and $\{s'\}$ is the set of marked messages prior to $M^i$.
%
Given $h$, whose projections are $s_1, s_2$, 
if $\vec\theta$ respects $h$ then clearly $\theta_i$ respects $s_i$
(proved as \texttt{bt\_sm\_resp}, see Appendix~\ref{v-bt-sm-resp}).
Conversely, given $\theta_i$ which respects $s_i$ ($i = 1$ \emph{or} 2),
can we complete $\theta_i$ to an $h$-respectful pair $\vec\theta$?

\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$ 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}

We defined a function which, given $\theta_1$ in this situation,
returns $\theta_2$.
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$.
By Theorem~\ref{t-subst-exists-unique} 
and Lemma~\ref{l-tc-equiv}\ref{l-thy-cons-equiv} % added since LNCS version
such a message is unique if $\Gamma$ is consistent.

The definition of \texttt{match\_rc1} (Appendix~\ref{vd-match-rc1})
follows that of \texttt{is\_der\_virt\_red} (Appendix~\ref{v-is-der-virt-red}),
so Theorem~\ref{t-match-rc1}\ref{match-rc1-iff-idvr} 
holds whether or not $\Gamma$ is actually reduced. 

It will be seen that it involves testing for membership of a finite set,
and corresponding uses of the $\epsilon$ operator,
(as in the case of \texttt{reduce}, as discussed earlier).
% in connexion with the finite computability of \texttt{reduce}.
Therefore we assert that \texttt{match\_rc1} is finitely computable.

The return type of \texttt{match\_rc1} is $message$ \texttt{option},
which is \texttt{Some} $res$ if the result $res$ is successfully found,
or \texttt{None} to indicate failure.
% Applying this result to a reduced consistent theory $\GammaR$ shows that 
% $\Gamma \vdash M \eqm N$ iff
  % \texttt{match\_rc1} $\GammaR\ M = \texttt{Some}\ N$
% uses \texttt{tc\_red\_iff} and \texttt{idvr\_reduce}
\begin{theorem} \label{t-match-rc1}
\begin{enumerate}
\item \texttt{\upshape(match\_rc1\_iff\_idvr)} \label{match-rc1-iff-idvr}
If $\Gamma$ satisfies \texttt{thy\_cons\_red}, then \\
  \texttt{is\_der\_virt\_red} $(\Gamma, M, N)$ iff 
  \texttt{match\_rc1} $\Gamma\ M = \texttt{Some}\ N$ 
\item \texttt{\upshape(match\_rc1\_indist)} \label{match-rc1-indist}
If $\Gamma$ is consistent, then \\ $\Gamma \vdash M \eqm N$ iff 
\texttt{match\_rc1} $\GammaR\ M = \texttt{Some}\ N$ 
\end{enumerate}
\end{theorem}
%% \begin{proof}
%% \ref{match-rc1-indist} follows from \ref{match-rc1-iff-idvr} using
%% Theorems~\ref{t-thy-cons-red}\ref{l-tc-red-iff}
%% and \ref{t-reduce}\ref{virt-reduce}.
%% \end{proof}

Then we defined a function \texttt{second\_sub} which uses \texttt{match\_rc1}
to find the appropriate value of $x \theta_2$ for 
each new $x$ which appears in the bi-trace, and
we proved that \texttt{second\_sub}
does in fact compute the $\theta_2$ of Theorem~\ref{t-subst-exists-unique}.
See Appendix~\ref{v-second-sub} for
the definition of \texttt{second\_sub} and this result.
The function \texttt{second\_sub} tests membership of a finite set,
and uses \texttt{reduce} and \texttt{match\_rc1},
so we assert that \texttt{second\_sub} is also finitely computable.