
\section{A finite set of most general respectful substitutions} \label{s-fsrs}

A common requirement of our substitutions will be (as it would ordinarily be
expressed) that the variables in the domain
(that is, those variables which are substituted)
do not appear in any of the messages in the range
(that is, the messages which are subsituted for the variables in the domain).
In fact, since we formalise a substitution in Isabelle as a total function,
we formalise the domain of a substitution as
those variables which are not simply mapped to themselves.
This requirement is expressed by the predicate \texttt{dr\_disj}.

Another requirement is that no new variables appear in the domain or 
in any of the range messages. 
We assume a definition of ``most general unifier'' which produces
substitutions satisfying this criterion.

Then we call a substitution \emph{null} if it is the identity function on
messages, equivalently, if its domain is empty.

Given the form of the definition of a respectful substitution, 
we can express it as a number of constraints of the form
$\Sigma \vdash M$, meaning that to be respectful,
a substitution $\theta$
must satisfy $\Sigma\theta \vdash M\theta$.
% that is, finding a substitution pair $\vec\theta = (\theta_1, \theta_2)$ 
% such that $\Gamma\theta \vdash M\theta_1 \eqm N\theta_2$.

Figure~\ref{f-msg} shows the proof rules for deriving $\Sigma \vdash M$.
Note that we abbreviate $\Sigma \cup \{M,N\}$ as $\Sigma,M,N$.

\begin{figure}[t]
$$
\infer[(var)]
{\Sigma \seqsym x}
{x \in {\mathcal{N}}}
\qquad
\infer[(id)]
{\Sigma, M \seqsym M}
{}
\qquad
\infer[(pr)]
{\Sigma \seqsym \spr M N}
{\Sigma \seqsym M & \Sigma \seqsym N}
$$
$$
\infer[(er)]
{\Sigma \seqsym \enc M N}
{\Sigma \seqsym M & \Sigma \seqsym N}
\qquad
\infer[(pl)]
{\Sigma, \spr M N \seqsym R}
{\Sigma, M, N \seqsym R}
\qquad
\infer[(el)]
{\Sigma, \enc M N \seqsym R}
{\Sigma \seqsym N & \Sigma, M, N \seqsym R}
$$
\caption{A proof system for message synthesis}
\label{f-msg}
\end{figure}

\subsection{Satisfying a single constraint for a respectful substitution}

We look at how we get the ways of
satisfying a given single constraint of the form $\Sigma \vdash M$.

Given a constraint $\Sigma \vdash M$ % $\Gamma \vdash M \eqm N$
we define possible ways of ``reducing it'' to (usually simpler) 
constraint(s) which have a suitable property.
In general a constraint $C = \Sigma \vdash M$
can be reduced in several ways,
but each reduction produces one ``main''
constraint $C' = \Sigma' \vdash M$
and a set of ``right'' constraints $\mathcal C'_R$.
Repeated reductions act on the ``main'' constraint and accumulate an
ever-increasing set of ``right'' constraints.
Thus we could say $C \rightarrow (C', \mathcal C'_R)$
(and, for convenience, we may write this),
but since all the reductions leave $M$ untouched in the main constraint,
our formalisation uses a reduction 
$\Sigma \rightarrow (\Sigma', \mathcal C'_R)$.
Then, to express the accumulation of ``right'' constraints, 
we define $\longrightarrow$.
The second formulation shows the notation we may sometimes use,
where $C = \Sigma \vdash M$ and $C' = \Sigma' \vdash M$, 
but the first follows our Isabelle formalisation.
$$
\frac {\Sigma \rightarrow (\Sigma', \mathcal C'_R)}
{(\Sigma, \mathcal C_R) \longrightarrow 
  (\Sigma', \mathcal C_R \cup \mathcal C'_R)}
\qquad
\frac {C \rightarrow (C', \mathcal C'_R)}
{(C, \mathcal C_R) \longrightarrow 
  (C', \mathcal C_R \cup \mathcal C'_R)}
$$

This idea appears in a different form in Tiu\cite{??},
and the reduction rules also have an obvious resemblance to the observer
theory reduction of \cite[??]{dawson-tiu-fotesb}.
%
\begin{eqnarray*}
% {\Gamma, (\pairM,\pairN) \vdash M \eqm N} & \rightarrow &
% ({\Gamma, (M_a, N_a), (M_b, N_b) \vdash M \eqm N}, \{\}) \\
% {\Gamma, (\encM,\encN) \vdash M \eqm N} & \rightarrow & 
% ({\Gamma, (M_p, N_p), (M_k, N_k) \vdash M \eqm N}, 
  % \{\Gamma, (\encM,\encN) \vdash M_k \leftrightarrow N_k\})
{\Sigma, \pairM} & \rightarrow &
(({\Sigma, M_a, M_b}), \{\}) \\
{\Sigma, \encM} & \rightarrow & 
(({\Sigma, M_p, M_k}), 
  \{\Sigma, \encM \vdash M_k\})
\end{eqnarray*}
%It is to be understood that
We assume that $\Gamma$ does not contain
% (\pairM,\pairN) and (\encM,\encN) respectively (otherwise reduction
 \pairM and \encM respectively (otherwise reduction
would not terminate).

In our Isabelle formalisation, $\rightarrow$ is \texttt{orkvs} and 
$\longrightarrow$ is \texttt{orkvss}.

% \footnote{In defining \texttt{orkvs} and \texttt{orkvss},
 % the ``$~\vdash M$'' (which is left unchanged) is omitted.}

For such a constraint set $(C, \mathcal C_R)$, we say it is satisfied if
the constraint $C$ holds, and the constraints in $\mathcal C_R$ can 
be derived only using \emph{right} derivations.
A right derivation is essentially one in which the right-hand side can be
built up from messages on the left-hand side using the pairing and encryption
operators.  
More formally, it is a derivation which uses only the 
rules $(var)$, $(id)$, $(pr)$ and $(er)$ of Figure~\ref{f-msg}.
We write $\Sigma \vdash_R M$ to indicate right derivability. 
Now it is decidable whether or not a constraint
$\Sigma \vdash_R M$ is derivable (see \cite[??]{dawson-tiu-fotesb}).
This follows from the fact that in a backwards proof using only these rules,
the right-hand side gets smaller at each rule application.

\begin{proposition}\label{p-orkvss}
\begin{enumerate}
\item \texttt{\upshape(subst\_orkvss\_if)}
If ${(C, \mathcal C_R) \longrightarrow (C', \mathcal C'_R)}$,
then, for any substitution $\theta$, 
if $(C', \mathcal C'_R)$ are satisfiable after substitution by $\theta$,
then so are $(C, \mathcal C_R)$.
\item \texttt{\upshape(idv\_orkvs)}
If $C$ is derivable but not right derivable, 
then there exists $(C', \mathcal C'_R)$, which are derivable,  
such that $C \rightarrow (C', \mathcal C'_R)$.
\item $\longrightarrow$ is well-founded
 (as the main constraint gets smaller at each step). 
\item \texttt{\upshape(orkvss\_iff)} \label{l-orkvss-iff}
$C$ is derivable if and only if 
there exists $(C', \mathcal C'_R)$,
where $C'$ as well as $\mathcal C'_R$ are right derivable,
such that $C \longrightarrow^* (C', \mathcal C'_R)$.
\end{enumerate}
\end{proposition}

The reduction relation is also finitely branching,
as there is at most one reduction for
each member of $\Sigma$ (recall that we assume $\Sigma$ is finite: 
it is a set of messages which have actually been sent).
Therefore this gives a decision procedure for $C = \Sigma \vdash M$: 
obtain all $(C', \mathcal C'_R)$, and test whether, for any of them,
$C'$ and $ \mathcal C'_R$ are all right derivable.

Note that many of our Isabelle results are for observer theories 
(sets of \emph{pairs} of messages) rather than for message sets,
and for pairs of substitution functions;
we use such results for this work by putting a pair of identical messages in
place of a single message.
\begin{verbatim}
subst_orkvss_if : "[| (?Tvs, ?Svs) : orkvss;
    satvss (subst_vs ?fg ?Tvs) ?MN |] ==>
  satvss (subst_vs ?fg ?Svs) ?MN"),

idv_orkvs : "[| (?G, ?MN) : indist; ~ is_der_virt (?G, ?MN) |] ==>
  EX G' Cs. ((G', Cs), ?G) : orkvs & satvss (G', Cs) ?MN"

orkvss_iff : "finite ?S -->
  satvss (?S, ?Us) ?MN = (EX S' Us'. is_der_virt (S', ?MN) &
    ((S', Us'), ?S, ?Us) : orkvss^* & satvss (S', Us') ?MN)" 
\end{verbatim}

In fact we defined a function \texttt{idv\_ss\_sets},
where \texttt{idv\_ss\_sets} $M$ is a set of sets of messages.
We defined \texttt{idv\_ss\_sets}
in a way makes it clear that it is finitely computable 
(see the discussion on this topic in \cite[??]{dawson-tiu-fotesb}).
% which has the following property (which we proved) that 

\begin{lemma}[\texttt{idv\_ss\_sets}]\label{l-idv-ss-sets}
$\Sigma \vdash_R M$ if and only if
$\Sigma$ contains a member $S$ of \texttt{idv\_ss\_sets} $M$.
\end{lemma}

\begin{verbatim}
idv_ss_sets : "idv_ss (?S, ?M) = (EX sp:idv_ss_sets ?M. sp <= ?S)"
\end{verbatim}

At this point we have a decision procedure for $C = \Sigma \vdash M$:
\begin{enumerate}
\item Find all $(C', \mathcal C'_R)$ such that
$C \longrightarrow^* (C', \mathcal C'_R)$,
and test whether \emph{any} of them satisfies the following
\item Test whether \emph{all} constraints $\Sigma' \vdash M'$ in 
$\{C'\} \cup \mathcal C'_R$
satisfy the following
\item Calculate \texttt{idv\_ss\_sets} $M'$
(which is a set of sets of messages) and see if
among them there is \emph{any} one, $S$,
which satisfies the following
\item Find all functions $f$ from $S$ into $\Sigma'$,
and test whether \emph{any} of them satisfies the following
\item Test whether for \emph{all} $s \in S$, $s = f(s)$
\end{enumerate}

Now the last two items here are just a long-winded way of saying
$S \subseteq \Sigma'$.
But here our task is to find substitutions $\theta$
such that $\Sigma\theta \vdash M\theta$ is satisfied.
The last step of the decision procedure could be replaced by:
let $\theta$ be the most general unifier of $\{(s, f(s))\,|\, s \in S\}$.
This leaves us with the problem that the earlier steps of the decision
procedure given were performed with respect to the constraint 
$\Sigma \vdash M$, not $\Sigma\theta \vdash M\theta$.
We now have to address this issue.

Firstly, we look at the effect of calculating \texttt{idv\_ss\_sets} $M$
\emph{before} applying $\theta$ to $M$, when we are interested in 
$\Sigma\theta \vdash M\theta$.
(We will use this lemma with $\Pi = \Sigma\theta$.) 
we get two results which are not converses ---
note that the conclusion of \ref{l-idv-sets-sub-indist} uses $\vdash$, not
$\vdash_R$ ---
but which will be sufficient for
deriving an equivalence later, in Theorem~\ref{t-smder-unif-ch1}.

\begin{lemma} \label{l-idv-sets-sub}
\begin{enumerate}
\item (\texttt{idv\_sets\_sub\_idv}) \label{l-idv-sets-sub-idv}
If $\Pi \vdash_R M\theta$ then
there exists $S \in \texttt{idv\_ss\_sets}\ M$
such that $S\theta \subseteq \Pi$
\item (\texttt{idv\_sets\_sub\_indist}) \label{l-idv-sets-sub-indist}
If $S \in \texttt{idv\_ss\_sets}\ M$
and $\Sigma$ satisfies the respectfulness condition, 
and the variables in $M$ are all in $\Sigma$
% \footnote{the Isabelle result is slightly more general than this}
and $S\theta \subseteq \Sigma\theta$, then 
$\Sigma\theta \vdash M\theta$
\end{enumerate}
\end{lemma}

\begin{verbatim}
idv_sets_sub_idv : "is_der_virt (?G, subst_pr ?fg (?a, ?a)) ==>
  EX sp:idv_sets (?a, ?a). subst_pr ?fg ` sp <= ?G" 

idv_sets_sub_indist : "[| ?sp : idv_sets ?MN; thy_strl_resp ?fg ?ns ?G;
    fn_oth (insert ?MN ?G) <= Union (set ?ns);
    subst_pr ?fg ` ?sp <= subst_pr ?fg ` ?G |] ==>
  (subst_pr ?fg ` ?G, subst_pr ?fg ?MN) : indist"
\end{verbatim}

Note that Lemma~\ref{l-idv-sets-sub}\ref{l-idv-sets-sub-idv}, 
unlike Lemma~\ref{l-idv-ss-sets}, is not an equivalence,
but gives necessary conditions for a constraint to be satisfied.
That is, it gives us \emph{some}, if not \emph{all},
pairs of messages which need to be identified by a proposed substitution.
% On the other hand, if Lemma~\ref{l-idv-sets-sub}\ref{l-idv-sets-sub-idv}
% gives us no (new) pairs of messages which need to be identified,
% then Lemma~\ref{l-idv-ss-sets} gives that the relevant constraint is already
% satisfied.
For the converse result, Lemma~\ref{l-idv-sets-sub}\ref{l-idv-sets-sub-indist},
we need to consider that there may be variables in $M$
which are affected by $\theta$: here the respectfulness condition ensures that
in such a case $\Sigma\theta \vdash x\theta$.
This is the key to the outcome we arrive at below, which is that we need to 
obtain and compose several substitutions until we get a respectful one.
It is also the reason why the results we describe next are formulated in
terms of two substitutions: one already determined and one yet to be
determined.

Secondly we look at the effect of calculating $\longrightarrow^*$
\emph{before} applying $\theta$ to $M$.
The problem here is that we may find a variable $x$ among the messages in
$\Sigma$, where $x\theta$ is a message formed by the pairing or 
the encryption operators, providing a reduction for $\Sigma\theta$
where there is no corresponding reduction for $\Sigma$.

Here we rely on the fact that we are looking for a respectful substitution
$\theta$, so, under this assumption we get $\Sigma\theta \vdash x\theta$.

We define an inference system for deriving 
$\Sigma\theta \vdash M\theta$ without ever using any $x\theta$ as the 
principal formula for any of the left rules.
It also gives a \emph{normal} derivation (no left rule above a right rule or
above the left premise of $(el)$) without redundant steps.
This inference system is shown in Figure~\ref{fig:sub-syn-msg}.
Clearly $\Sigma \vdash_\theta M$ implies $\Sigma\theta \vdash M$.

\begin{figure}
$$
\infer[virt]
{\Sigma \seqsym_\theta M}
{(\Sigma \setminus \mathcal N)\ \theta \seqsym_R M}
$$
$$
\infer[pl \quad
\mbox{ if }\spr M N \not\in \Sigma
]
{\Sigma, \spr M N \seqsym_\theta R}
{\Sigma, M, N \seqsym_\theta R}
$$
$$
\infer[el \quad
\mbox{ if }\enc M N \not\in \Sigma
]
{\Sigma, \enc M N \seqsym_\theta R}
{(\Sigma \setminus \mathcal N)\ \theta
\seqsym_R N\theta & \Sigma, M, N \seqsym_\theta R}
$$
\caption{A proof system for substituted message synthesis}
\label{fig:sub-syn-msg}
% in Isabelle, this is single message version of indist_nsv_excl
\end{figure}

Now the relation $\rightarrow$ (on the constraints before substitution)
is naturally related to this proof system,
similarly to Proposition~\ref{p-orkvss}\ref{l-orkvss-iff},
although Lemma~\ref{l-indist-nsv-ex-orkvss} is not an equivalence.
Let $\mathcal N$ be the set of all message variables.

\begin{lemma}[\texttt{indist\_nsv\_ex\_orkvss}]\label{l-indist-nsv-ex-orkvss}
If $\Sigma \seqsym_\theta M\theta$ and $C$ is $\Sigma \seqsym M$
then there exists 
$(C', \mathcal C'_R)$ such that $C \rightarrow^* (C', \mathcal C'_R)$
and, for all the constraints $\Sigma' \vdash M'$ in $(C', \mathcal C'_R)$,
we have $(\Sigma' \setminus \mathcal N)\theta \vdash_R M'\theta$.
\end{lemma}

Now since respectfulness of $\theta$ essentially means  
that the (remainder of) $\Sigma\theta$ entails $x\theta$,
we can get that omitting $\mathcal N$ from $\Sigma$ before applying $\theta$ 
does not matter.  Or, precisely:
\begin{lemma}[\texttt{indist\_ne\_nsv\_excl}]\label{l-indist-ne-nsv-excl}
If $\Sigma\theta \seqsym M$ and $\theta$ satisfies 
the appropriate respectfulness condition for $\Sigma$,
then $\Sigma \seqsym_\theta M$.
\end{lemma}

The ``appropriate respectfulness condition''
uses \texttt{thy\_strl\_resp}, and is described in detail in
\cite[Appendix~A.19]{dawson-tiu-fotesb}.
Briefly, from the notion of a respectful substitution of a bi-trace (or a trace)
we get a ``respectful'' substitution of 
an observer theory (or message set) with respect to an ordered list of sets of
variables.
Then, a respectful substitution of a trace becomes a respectful substitution
of the underlying message set, and also of the sets that we see after applying
the reduction $\longrightarrow$.

We tried to improve 
Lemma~\ref{l-indist-nsv-ex-orkvss} to a stronger result of the form
``Given $\Sigma$ and $\theta$, there exists $(C', \mathcal C'_R)$ such that
for all $M$, if $C = \Sigma \seqsym_\theta M$ then \ldots''.
Taking advantage of this would make a decision procedure more efficient.  
We did not succeed in this.
However we did succeed in improving in this way the combination of Lemmas 
\ref{l-indist-nsv-ex-orkvss} and \ref{l-indist-ne-nsv-excl}.
Thus we know that there is one of the finite set of possibilities for 
$(C', \mathcal C'_R)$ which applies for all $M$.

\begin{lemma}[\texttt{indist\_resp\_ex\_orkvss\_red}]
\label{l-indist-resp-ex-orkvss-red}
If $\theta$ satisfies the appropriate respectfulness condition for $\Sigma$,
then there exist $\Sigma'$ and $\mathcal C'_R$
such that
\begin{enumerate}
\item \label{l-eora} $\Sigma \rightarrow^* (\Sigma', \mathcal C'_R)$
\item \label{l-eorb} 
  for all the constraints $\Sigma'' \vdash M'$ in $\mathcal C'_R$,
$(\Sigma'' \setminus \mathcal N)\theta \vdash_R M'\theta$
\item \label{l-eorc} $(\Sigma' \setminus \mathcal N)\theta$ is reduced, and
\item \label{l-eord} for all $M$, $\Sigma\theta \seqsym M$ is derivable if and only if 
$(\Sigma' \setminus \mathcal N)\theta \vdash_R M$ is derivable
\end{enumerate}
\end{lemma}

Note that by \cite[Theorem~7(c)]{dawson-tiu-fotesb},
and \ref{l-eorc} and \ref{l-eord} above, 
$\Sigma\theta\!\!\Downarrow \setminus \mathcal N =
  (\Sigma' \setminus \mathcal N)\theta \setminus \mathcal N$.

\begin{verbatim}
indist_nsv_ex_orkvss : "(?G, ?MN) : indist_nsv_excl ?fg ==>
  EX H Vs. ((H, Vs), ?G, {}) : orkvss^* &
  is_der_virt (subst_pr ?fg ` (H - Ne), ?MN) &
  (ALL (K, X):Vs. is_der_virt (subst_seq ?fg (K - Ne, X)))" 

indist_ne_nsv_excl : "[| finite ?G; (?H, ?MN) : indist_norm_excl;
  ?H = subst_pr ?fg ` ?G; ?G <= range pair; thy_strl_resp ?fg ?ns ?G;
  fn_oth ?G <= Union (set ?ns) |] ==> (?G, ?MN) : indist_nsv_excl ?fg"

indist_resp_ex_orkvss_red : "[| finite ?G; ?G <= range pair; 
    thy_strl_resp ?fg ?ns ?G; fn_oth ?G <= Union (set ?ns) |] ==>
  EX H Vs.  ((H, Vs), ?G, ?Us) : orkvss^* &
    ((ALL (K, X):?Us. is_der_virt (subst_seq ?fg (K - Ne, X))) -->
      (ALL (K, X):Vs. is_der_virt (subst_seq ?fg (K - Ne, X)))) &
    min_orkvs_Ne ?fg H &
    (ALL MN. ((subst_pr ?fg ` ?G, MN) : indist) =
      is_der_virt (subst_pr ?fg ` (H - Ne), MN))" 
\end{verbatim}

We can now combine Lemmas \ref{l-indist-ne-nsv-excl},
\ref{l-indist-nsv-ex-orkvss} and \ref{l-idv-sets-sub}.
To find a substitution $\theta$ satisfying $\Sigma \vdash M$
(one of the respectfulness constraints!),
where $\theta$ is respectful (so we can use Lemma~\ref{l-indist-ne-nsv-excl}),
we select one $(C', \mathcal C'_R)$ as in Lemma~\ref{l-indist-nsv-ex-orkvss}.

Let us index the constraints in the selected $(C', \mathcal C'_R)$ 
by $i \in I$.
Since Lemma~\ref{l-idv-sets-sub-idv} 
gives a necessary condition for a substitution $\theta$
to make each of the constraints $\Sigma_i \vdash_R M_i$
in $(C', \mathcal C'_R)$ to be satisfied.
We attempt to satisfy all those conditions.
Each condition is of the form:
there exists $S \in \texttt{idv\_ss\_sets}\ M_i$
such that $S\theta \subseteq \Sigma_i\theta$.
Since $S\theta \subseteq \Sigma_i\theta$ is equivalent to:
there exists a function $f_i$ from $S$ into $\Sigma_i$ such that 
$\theta$ unifies the set of pairs $\mathcal P_i = \{(s, f_i(s))\,|\, s \in S\}$.
So for each way of choosing a function $f_i$ for each $i \in I$,
we take the union $\mathcal P = \bigcup_{i \in I} \mathcal P_i$.
(We would then want $\theta$ to unify all the pairs in $\mathcal P$.)

The function \texttt{sat\_unifs} does this.
The theorem \texttt{sat\_unifs\_iff} expresses its relevant properties,
but its definition is considerably more complicated.
Thus \texttt{sat\_unifs} \ldots obtains a set of possible 
$\mathcal P$, one of which should be unified by $\theta$.
Then \texttt{unif\_ch1} takes the union of these over all possible choices of
$(C', \mathcal C'_R)$.

\begin{verbatim}
sat_unifs_iff : "(EX unif':sat_unifs ?F ?G ?smcs. unif' <= ?unif) =
  (ALL ssn:?smcs. EX A:?F ssn. EX M<=?unif. fst ` M = A & snd ` M <= ?G ssn)" 

unif_ch1_def : "unif_ch1 ?f ?G ?M ==
  UN (H, Vs):{x. (x, ?G, {}) : orkvss^*}.
  sat_unifs (idv_sets o subst_pr ?f o snd)
  (%(K, X). subst_pr ?f ` (K - Ne)) (insert (H, ?M, ?M) Vs)"
\end{verbatim}

\begin{theorem}[\texttt{smder\_unif\_ch1}]\label{t-smder-unif-ch1}
% [\texttt{resp\_ork\_comp\_unif}]\label{l-resp-ork-comp-unif}
If $\gamma \circ \delta$ is a respectful substitution 
(for the trace whose message set is $\Sigma$)
and the variables in $M$ are all in $\Sigma$
then $\Sigma\gamma\delta \vdash M\gamma\delta$ is derivable iff
there exists
a set $\mathcal P$ of pairs in \texttt{unif\_ch1} $\gamma\ \Sigma\ M$
such that for each $(M', M'') \in \mathcal P$, $M'\delta = M''\delta$.
\end{theorem}

\begin{verbatim}
smder_unif_ch1 : "[| validst ?st; ?st : sm_resp (comp_subst ?g ?f);
         fn_msg ?M <= (UN mm:set ?st. fn_msg (rem_io mm)) |] ==>
   ((subst_msg (comp_subst ?g ?f) ` rem_io ` set ?st,
     subst_msg (comp_subst ?g ?f) ?M) : derrec smpsc {}) =
   (EX unif:unif_ch1_ss ?f (rem_io ` set ?st) ?M.
      ALL (a, b):unif. subst_msg ?g a = subst_msg ?g b)" 
\end{verbatim}

Thus, given $\Sigma$ and $M$, if we are looking for a respectful substitution
$\theta$ such that $\Sigma\theta \vdash M\theta$,
the first step is to apply Theorem~\ref{t-smder-unif-ch1}
with $\gamma = id$, that is, calculate 
\texttt{unif\_ch1} $id\ \Sigma\ M$,
and take the most general unifier of each resulting set of pairs.
This gives a finite set of substitutions $\gamma_i$, $i \in I$,
with the property that (although they need not be respectful),
any respectful substitution $\theta$ such that $\Sigma\theta \vdash M\theta$
is a specialisation of some $\gamma_i$.
We now therefore need to look at specialising each such $\gamma_i$ to a
respectful substitution.

\subsection{Moving towards a respectful substitution: the function
\texttt{umgrs1}}

We define a function \texttt{umgrs1} which proceeds towards finding a
respectful substitution.
For a trace $s$ and a substitution $\gamma$, 
\texttt{umgrs1} $s\ \gamma$ is a finite set of substitutions $\delta$ which 
could be composed with $\gamma$ to be the next step towards a 
respectful substitution.

Some of the Isabelle code relates to pairs of messages (as found in an observer
theory) rather than single messages.  
In part, we reuse this code, simply applying it to identical pairs of messages
in place of single messages.
Thus \texttt{unif\_ch} applies to pairs of messages just as 
\texttt{unif\_ch\_st} applies to single messages.
This accounts for the definition of \texttt{unif\_ch\_st}
in terms of \texttt{unif\_ch}, where 
$(a,b) \in \texttt{slice\_unif}\ r$ iff $((a,a), (b,b)) \in r$,
and \texttt{pair} $x = (x,x)$.

The function \texttt{bt\_constrs} gives the list of constraints for
a substitution to be $h$-respectful for a bi-trace $h$.
Each constraint is, in general, of the form $\Gamma \vdash M \eqm N$,
but here we will have $M = N$ and $\Gamma$ consists of identical pairs.

We omit the definition of \texttt{UN\_choices}, 
but show the theorem, \texttt{UN\_choices\_iff},
which characterises it.

For each constraint, \texttt{unif\_ch1} gives a set of sets of pairs:
for the constraint to be satisfied by a substitution, 
one of the sets of pairs must be unified by the substitution.
%
With several constraints, each one may be satisfied by unifying one of
several sets of pairs: \texttt{UN\_choices} takes all possible ways of making
this choice for each constraint, and, for each such way, takes the union of the 
sets of pairs which are to be unified.

\begin{verbatim}
unif_ch_st_def : "unif_ch_st ?g ?st == 
  slice_unif ` unif_ch ?g (map (map_io pair) ?st)" 

unif_ch_def : "unif_ch ?g ?bt ==
  UN_choices (bt_constrs ?bt) (%(ss, m, n). unif_ch1 (?g, ?g) ss n)"

UN_choices_iff : "(EX U':UN_choices ?A ?B. U' <= ?U) =
	                (ALL a:?A. EX b:?B a. b <= ?U)"
\end{verbatim}

\subsection{Using \texttt{umgrs1} in a complete search for
respectful substitutions}

\texttt{unif\_ch\_st} $\gamma\ s$ gives a ``necessary'' 
set of sets of pairs of messages;
that is, to get a $s$-respectful substitution $\zeta$
which is a further substitution after $\gamma$, 
we must compose $\gamma$ with a substitution which unifies all message pairs in
one of the sets given by \texttt{unif\_ch\_st} $\gamma\ s$.

\begin{lemma}[\texttt{sm\_resp\_unif\_ch}]\label{l-sm-resp-unif-ch}
If $\gamma \circ \delta$ respects $s$ then $\delta$ unifies 
one of the sets of pairs in \texttt{unif\_ch\_st} $\gamma\ s$.
\end{lemma}

\begin{verbatim}
sm_resp_unif_ch :
  "[| validst ?st; ?st : sm_resp (comp_subst ?h ?g) |] ==>
  EX unif:unif_ch_st ?g ?st. 
    ALL (a, b):unif. subst_msg ?h a = subst_msg ?h b")]

umgrs1_def : "umgrs1 ?st ?g == Some -` mgu ` unif_ch_st ?g ?st" 
\end{verbatim}

Now we get the same result expressed in terms of the most general unifiers of
the several sets of pairs.

\begin{lemma}[\texttt{ex\_umgrs1}]\label{l-ex-umgrs1}
If $\gamma \circ \delta$ is an $s$-respectful substitution,
then there exists $\sigma \in \texttt{umgrs1}\ s\ \gamma$ and $\rho$
such that $\delta = \sigma \circ \rho$
\end{lemma} 

\begin{verbatim}
ex_umgrs1 : "[| validst ?st; ?st : sm_resp (comp_subst ?h ?g) |] ==>
  EX k:umgrs1 ?st ?g. EX j. ?h = comp_subst j k" 
\end{verbatim}

We find that if $\texttt{umgrs1}\ s\ \gamma$ contains the null substitution,
we are done: we do not need that $\texttt{umgrs1}\ s\ \gamma$ consists of
only the null substitution.

\begin{lemma}[\texttt{umgrs1\_id}]\label{l-umgrs1-id}
If any $\delta \in \texttt{umgrs1}\ s\ \gamma$ is the identity substitution,
then $\gamma$ is $s$-respectful.
\end{lemma}

\begin{verbatim}
umgrs1_id : "[| ?d : umgrs1 ?st ?g; validst ?st;
  subst_msg ?d = id |] ==> ?st : sm_resp ?g" 
\end{verbatim}

Let us sum up to this point: given a substitution $\gamma$,
every $s$-respectful substitution of the form $\gamma \circ \ldots$ 
is also of the form $\gamma \circ \delta \circ \ldots$, 
for some $\delta \in \texttt{umgrs1}\ s\ \gamma$.
So the procedure is to proceed towards a $s$-respectful substitution
by calculating and composing more substitutions $\delta$.
Also, we know that we are done when \texttt{umgrs1} $s\ \gamma$
gives a null substitution.

So now we specify this accumulation of substitutions $\delta$.

We define a result of a single step:
for non-null $\delta \in \texttt{umgrs1}\ s\ \gamma$,
our next attempt towards a respectful substitution is $\gamma \circ \delta$,
and then \texttt{umgrs1cp} $s$ is the set of all such
$(\gamma \circ \delta, \gamma)$.
Here, although \texttt{umgrs1cp} is not recursive,
it is defined in Isabelle as an inductively defined set.

\begin{verbatim}
umgrs1cp.intros : "[| ?d : umgrs1 ?st ?g; domain ?d ~= {}; 
    ?h = comp_subst ?d ?g |] ==> (?h, ?g) : umgrs1cp ?st" 
\end{verbatim}

Then \texttt{umgrs\_resp} $s\ \gamma$ gives the result of continuing this
process as far as it will go: we keep on producing $\gamma \circ \delta$
from $\gamma$, as above, until (by Lemma~\ref{l-umgrs1-id}) we have
a respectful substitution.

\begin{verbatim}
umgrs_resp_def : "umgrs_resp ?st ?g ==
  {h. (h, ?g) : (umgrs1cp ?st)^* & (EX k:umgrs1 ?st h. domain k = {})}"
\end{verbatim}

To show that this procedure actually reaches all desired respectful
substitutions, we need that it terminates.  
From this it also follows that the set of these substitutions is finite.

\begin{lemma}\label{l-wfp-umgrs1cp-finite}
Assuming $\gamma$ satisfies \texttt{dr\_disj} $\gamma$
and involves only variables in $s$,
\begin{enumerate}
\item \texttt{\upshape(umgrs\_wfp)}
The relation \texttt{umgrs1cp} $s$ is well-founded.
\item \texttt{\upshape(finite\_umgrs\_resp)}
\texttt{finite\_umgrs\_resp} $s\ \gamma$ contains 
only finitely many substitutions.
\end{enumerate}
\end{lemma}
\begin{proof}
At each step, the (finite) set of variables in $s$ but not involved in 
the substitution gets smaller.
This uses some ancillary results mentioned below.
\qed \end{proof}
\begin{verbatim}
umgrs_wfp : 
  "[| domain ?g Un range_names ?g <= UNION (rem_io ` set ?st) fn_msg;
             dr_disj ?g |] ==> ?g : wfp (umgrs1cp ?st)" 

finite_umgrs_resp :
  "[| domain ?g Un range_names ?g <= UNION (rem_io ` set ?st) fn_msg;
	     dr_disj ?g |] ==> finite (umgrs_resp ?st ?g)"
\end{verbatim}

This gives us our desired result, showing how to construct a finite
set of most general respectful substitutions which specialise
a given substitution $\gamma$.
\begin{theorem}[\texttt{ex\_umgrs\_resp}] \label{t-umgrs-resp}
\begin{enumerate}
\item \texttt{\upshape({ex\_umgrs\_resp})}
If $\gamma \circ \delta$ is an $s$-respectful substitution,
then there exists $\sigma \in \texttt{umgrs\_resp}\ s\ \gamma$ and $\rho$
such that $\gamma \circ \delta = \sigma \circ \rho$
\item \texttt{\upshape(umgrs\_resp\_id)}
If $\sigma \in \texttt{umgrs\_resp}\ s\ \gamma$ then 
$\sigma$ is an $s$-respectful substitution
\end{enumerate}
\end{theorem}

\begin{verbatim}
ex_umgrs_resp : "[| validst ?st; dr_disj ?g;
  domain ?g Un range_names ?g <= UNION (rem_io ` set ?st) fn_msg;
  ?st : sm_resp (comp_subst ?h ?g) |] ==>
  EX k:umgrs_resp ?st ?g. EX j. comp_subst ?h ?g = comp_subst j k"

umgrs_resp_id : "[| ?h : umgrs_resp ?st ?g; validst ?st |] ==>
  ?st : sm_resp ?h" 
\end{verbatim}

Recall that Theorem~\ref{t-smder-unif-ch1}
gives a set of substitutions $\gamma_i$, $i \in I$, and we needed to
find all respectful substitutions specialising some $\gamma_i$.
Now Theorem~\ref{t-umgrs-resp} gives, for each $\gamma_i$,
a set of substitutions $\sigma_{ij}$, $j \in J$, such that 
each respectful substitution specialising $\gamma_i$
is a specialisation of some $\sigma_{ij}$,
and each $\sigma_{ij}$ is respectful.

Therefore, putting Theorems \ref{t-smder-unif-ch1} and
\ref{t-umgrs-resp} together, we get, given $\Sigma$ and $M$,
a set $\sigma_{ij}$ of respectful substitutions such that 
\begin{enumerate}
\item $\Sigma\sigma_{ij} \vdash M\sigma_{ij}$
\item  if $\theta$ is respectful and $\Sigma\theta \vdash M\theta$
the $\theta$ is a specialisation of some $\sigma_{ij}$
\end{enumerate}

\begin{theorem}[\texttt{smder\_sub\_resp}]\label{l-smder-sub-resp}
Let $\Theta$ be the set of respectful substitutions $\theta$ 
(for the trace whose message set is $\Sigma$)
such that $\Sigma\theta \vdash M\theta$ is derivable.
Let $\Phi = \bigcup \{ \texttt{umgrs\_resp}\ s\ \gamma \,|\, 
  \gamma \in \texttt{unif\_ch1}\ id\ \Sigma\ M\}$. 
Then 
\begin{enumerate}
\item $\Phi \subseteq \Theta$
\item if $\theta \in \Theta$ 
then there exists $\sigma \in \Phi$ and $\rho$
such that $\theta = \sigma \circ \rho$
\end{enumerate}
\end{theorem}

We now mention some of the more minor technical results used above.

\begin{lemma}
Assuming \texttt{dr\_disj} $\gamma$ then 
for each step $(\zeta, \gamma) \in \texttt{umgrs1cp}\ s$, 
$\texttt{domain}\ \zeta \supset \texttt{domain}\ \gamma$
\end{lemma}
\begin{verbatim}
dom_umgrs1c "[| dr_disj ?g; (?h, ?g) : umgrs1cp ?st |] ==>
  domain ?g < domain ?h"
\end{verbatim}

This is combined with results such as 
\begin{lemma}
for $(\zeta, \gamma) \in \texttt{umgrs1cp}\ s$,
\begin{enumerate}
\item \texttt{\upshape(drs\_umgrs1cp)}
if $\gamma$ involves only variables which are in $s$, then so does $\zeta$ 
% if only variables in $s$ are involved in $\gamma$, 
% then this also holds for $\zeta$ 
\item \texttt{\upshape(dr\_disj\_1cp\_u)}
if \texttt{dr\_disj} $\gamma$ then 
\texttt{dr\_disj} $\zeta$
\end{enumerate}
\end{lemma}
to show that, starting from a given $\gamma$ and continuing to obtain
substitutions in this way, (every branch of) this process terminates, and
we obtain only finitely many substitutions.
That is, it gives Lemma~\ref{l-wfp-umgrs1cp-finite}.

\begin{verbatim}
\end{verbatim}

\begin{verbatim}
\end{verbatim}

