# Insecurity problem for assertions remains in NP

R Ramanujam
The Institute of Mathematical Sciences, Chennai (Retd.)
Homi Bhabha National Institute, Mumbai (Retd.)
Azim Premji University, Bengaluru (Visiting)
<EMAIL_ADDRESS>Vaishnavi Sundararajan
Visiting Post-Doctoral Fellow
Chennai Mathematical Institute
<EMAIL_ADDRESS>S P Suresh
Chennai Mathematical Institute
<EMAIL_ADDRESS>
###### Abstract

In the symbolic verification of cryptographic protocols, a central problem is
deciding whether a protocol admits an execution which leaks a designated
secret to the malicious intruder. [27] shows that, when considering finitely
many sessions and a protocol model where only terms are communicated, this
“insecurity problem” is NP-complete. Central to their proof strategy is the
observation that any execution of a protocol can be simulated by one where the
intruder only communicates terms of bounded size. However, when we consider
models where, in addition to terms, one can also communicate logical formulas,
the analysis of the insecurity problem becomes tricky. In this paper we
consider the insecurity problem for protocols with logical statements that
include equality on terms and existential quantification. Witnesses for
existential quantifiers may be of unbounded size, and obtaining small
witnesses while maintaining equality proofs complicates the analysis. We use a
notion of typed equality proofs, and extend techniques from [27] to show that
this problem is also in NP. We also show that these techniques can be used to
analyze the insecurity problem for systems such as the one proposed in [24].

##  1 Introduction

###  1.1 Background

The symbolic analysis of security protocols is a long-standing field of study,
with the Dolev-Yao model [15] being the standard. Here, messages in a protocol
are abstracted as elements in a _term algebra_ , which usually includes
operators for _pairing_ and _encryption_ , among others. _Proof rules_ govern
how to derive new terms from existing ones. This model also considers an
idealized intruder who is assumed to control the network, but cannot break
cryptography. This “all-powerful” intruder can see/block/inject/redirect
messages, as well as derive new terms from knowledge accumulated over the
execution of a protocol. In particular, every communication is split into a
send and a receive, with the sends being implicitly captured by the intruder,
and receives assumed to come from the intruder. A send need not be accompanied
by a corresponding receive, and vice versa. Building on this abstraction,
there have been tremendous advancements in the formal study of security
protocols. People have studied extensions of this basic model to express
richer classes of protocols and security properties [1, 6, 4, 11], and
associated decidability and complexity results [2, 8, 5, 10, 9, 21, 12, 25,
26, 16]. Various verification tools have also been built based on these formal
models [14, 6, 7, 23]. A tutorial introduction to this area with many more
references is [13].

###  1.2 The insecurity problem

A basic problem of interest is the _insecurity problem_ – is there an
execution of a given protocol that leaks a designated secret? Following the
abstract model of [27], protocols can be represented as a set of _roles_ ,
each of which is a sequence of pairs
${r_{1}}\\!\Rightarrow\\!{s_{1}},\ldots,{r_{n}}\\!\Rightarrow\\!{s_{n}}$. The
$r_{i}$s are messages received from the network/intruder, and each $s_{i}$ is
a message send (by an honest agent) in response to $r_{i}$. The $r_{i}$s and
$s_{i}$s can have variables occurring in them. Variables which occur in an
$s_{i}$ first are parameters of the protocol that are in the control of an
agent enacting the role. The agent instantiates them with concrete values to
obtain a _session_. Any variable remaining in a session will, therefore, first
occur in one of the $r_{i}$s, and represents an unknown value received from
the intruder. An execution (or _run_) of a protocol is a an interleaving of a
finite number of sessions, along with a mapping of all the variables occurring
in the run to concrete values. (We assume that variables occurring in a
session are distinct from those occurring in other sessions.) We further
require that all the messages received (resp. sent) can be derived from the
knowledge accumulated so far in the run by the intruder (resp. an honest
agent). A protocol is insecure if there is a run where the intruder can derive
a designated secret from their knowledge accumulated over the course of the
run.

A run can involve arbitrarily many sessions in parallel, each session may
introduce new fresh values (_nonces_), and the intruder can instantiate the
variables with arbitrarily large terms. Each of these sources of unboundedness
contributes to the intractability of the insecurity problem, rendering it
undecidable in general [3, 16, 19]. One way to obtain decidability is to
impose bounds on some of these parameters. In particular, [27] considers the
insecurity problem for finitely many sessions, i.e., is there a run of the
protocol consisting of at most $K$ sessions (for a fixed $K$) which leaks a
secret? Bounding the number of sessions automatically bounds the number of
fresh nonces used in a run, but the intruder can still instantiate variables
with arbitrarily large terms, as illustrated in the following example.

######  Example 1.1.

Consider a protocol given by the two roles:

$\displaystyle\eta_{1}$
$\displaystyle\coloneqq\quad{\ast}\\!\Rightarrow\\!{\\{(\mathit{pk}_{a},\\{m\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{b}}}$
$\displaystyle\eta_{2}(x,y)$
$\displaystyle\coloneqq\quad{\\{(x,\\{y\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{b}}}\\!\Rightarrow\\!{\\{y\\}_{x}}$

Here, $\ast$ is a dummy term triggering the start of $\eta_{1}$, $m$ is a
fresh name generated by $A$ intended to be kept secret, $\\{t\\}_{k}$ denotes
the encryption of $t$ with the key $k$, $(t,u)$ represents the pairing of
terms $t$ and $u$, and $\mathit{pk}_{a};\mathit{sk}_{a}$ and
$\mathit{pk}_{b};\mathit{sk}_{b}$ are the public-private key pairs of agents
$A$ and $B$.

However, the intruder can get $m$ via the run in Figure 1, obtained by
interleaving the sessions $\eta_{1}$, $\eta_{2}(x_{1},y_{1})$ and
$\eta_{2}(x_{2},y_{2})$ under the substitution $\sigma$. Here,
$A\rightarrow:t$ denotes a send of $t$ by $A$, and $\rightarrow A:t$ denotes a
receive of $t$ by $A$.

$A\rightarrow$ | : | $\\{(\mathit{pk}_{a},\\{m\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{b}}$
---|---|---
$\rightarrow B$ | : | $\\{(\mathit{pk}_{i},\\{(pk_{a},\\{m\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{b}}$
$B\rightarrow$ | : | $\\{(pk_{a},\\{m\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{i}}$
$\rightarrow B$ | : | $\\{(pk_{i},\\{m\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{b}}$
$B\rightarrow$ | : |  $\\{m\\}_{\mathit{pk}_{i}}$.

$\sigma\coloneqq[x_{1}\mapsto\mathit{pk}_{i},x_{2}\mapsto\mathit{pk}_{i},y_{1}\mapsto(\mathit{pk}_{a},\\{m\\}_{\mathit{pk}_{b}}),y_{2}\mapsto
m].$

Figure 1: Attack for Example 1.1

There are two points of interest in the above example. The first is that
$\sigma(y_{1})$ is a non-atomic term, and therefore the first term received by
$B$ has larger size than intended in the protocol. The second is that $y_{1}$
unifies under $\sigma$ with a non-atomic term mentioned in the protocol,
namely, $\sigma(y_{1})=\sigma(\mathit{pk}_{a},\\{m\\}_{\mathit{pk}_{b}})$.
This last fact is important – this pattern match is needed for the intruder to
get $B$ to believe that $\sigma(y_{1})$ is expected according to the protocol
specification, and elicit an appropriate response.

######  Example 1.2.

Consider the protocol from Example 1.1. Let $\sigma^{\prime}$ map $y_{1}$ to a
large term $t$ that does not have the same pattern as any term mentioned in
$\eta$, say
$((\mathit{pk}_{i},\mathit{pk}_{a}),(\mathit{pk}_{i},\mathit{pk}_{a}))$. This
is also a non-atomic term, but this does not “help” the intruder in any way.
Suppose $B$ receives
$\\{(\mathit{pk}_{i},\\{t\\}_{\mathit{pk}_{b}})\\}_{\mathit{pk}_{b}}$ and
responds with $\\{t\\}_{\mathit{pk}_{i}}$. What has $I$ gained? On decrypting
with $\mathit{sk}_{i}$, it can learn $t$, but that was already constructed by
$I$. Further, it cannot trick $B$ into looking inside $t$ and extracting some
embedded secret for it (like in the earlier attack $\sigma$), since $t$ does
not match any expected pattern. So, the intruder might as well take
$\sigma^{\prime}(y_{1})$ to be an atomic term.

Example 1.2 illustrates the core reasoning in [27]. Essentially, a variable
$x$ is good if it unifies with a non-variable pattern (from the protocol
specification) under $\sigma$, and bad otherwise. If there is an attack
$(\xi,\sigma)$ on the protocol which involves a bad variable, one can “zap” it
to an atomic value to obtain a “smaller” attack $(\xi,\sigma^{\prime})$, i.e.,
the sum of the sizes of $\sigma^{\prime}(x)$ (over all $x$) is smaller than
the corresponding sum for $\sigma$. By repeatedly zapping one bad variable
after another, one can obtain an attack $\sigma^{\\!*}$ where all variables
are good. One can now bound the size of each $\sigma^{\\!*}(x)$ by a
polynomial of the sizes of terms mentioned in the protocol specification, and
thus prove that insecurity is in NP. The technical challenge is to prove that
after each zap, all messages sent by the intruder in $\xi$ are still derivable
from $I$’s knowledge. The interested reader can consult [27] for further
details.

###  1.3 Our contribution

In this paper, we extend the techniques of [27] to protocols where agents can
communicate logical formulas in addition to terms. These formulas convey
properties of terms, and serve as an abstract vehicle to capture
certification. To highlight the essential proof ideas, we consider a syntax
consisting only of equality between terms (denoted ${{t}\bowtie{u}}$ to avoid
overloading the $=$ operator) and existential quantification.

When lifting the zapping procedure outlined above to formulas, equalities
between terms might be violated by a zap.

######  Example 1.3.

Consider a protocol which mentions $\\{x\\}_{k}$ in its specification, and
consider a run $(\xi,\sigma)$ where $x$ is bad and $y$ is good, with
$\sigma(x)=t$ and $\sigma(y)=\\{t\\}_{k}$. If we zap $x$ to an atomic value,
$y$ is no longer equal to $\\{x\\}_{k}$, and thus becomes bad. We could zap
$y$ in the next round, but the equality between $y$ and $\\{x\\}_{k}$ would be
lost.

Suppose the formula ${{y}\bowtie{\\{x\\}_{k}}}$ is also communicated. Then we
cannot zap $x$ without modifying $\\{y\\}_{k}$ appropriately.

Thus, formulas introduce an additional concern – the need to preserve
equalities. Zapping and derivability can also interact in more complicated
ways, as illustrated below.

######  Example 1.4.

Consider a run $(\xi,\sigma)$ of some protocol, with a bad variable $x$, where
$\sigma(x)=\\{n\\}_{k}$. Suppose the intruder derives $n$ by decrypting
$\sigma(x)$, perhaps as a pre-requisite to some message sent in this run. When
we zap $x$, we would like to be able to mimic all the derivations that happen
in the original run. But the zapped image of $x$ is now an atomic value, on
which decryption can no longer be applied.

Proof systems for equalities often include _projection_ , which lets one infer
${{m}\bowtie{n}}$ and ${{m^{\prime}}\bowtie{n^{\prime}}}$ from
${{(m,m^{\prime})}\bowtie{(n,n^{\prime})}}$. However, this means one cannot
zap “indiscriminately”.

######  Example 1.5.

Suppose $x$ is bad and $\sigma(x)=(m,m^{\prime})$, and we have a proof of
${{m}\bowtie{n}}$ by applying the projection rule on
${{\sigma(x)}\bowtie{(n,n^{\prime})}}$. If we zap $x$ to get a new
substitution $\sigma^{\prime}$, we see that we can no longer apply projection
on ${{\sigma^{\prime}(x)}\bowtie{(n,n^{\prime})}}$.

Thus, we cannot zap one variable in an equality independent of the other
component. We have to zap all bad variables in $\sigma$ to get a
$\sigma^{\\!*}$, without breaking any of the “relevant” equalities.

When a variable is good, it matches a pattern specified in the protocol. We
can view the pattern as a _type_ of the term. Note that, as in Example 1.1,
the intruder needs a variable to match a pattern from the protocol only in
situations where it wants an honest agent to look into the term and extract
some component. These variables need to be good, and therefore “typed”. We can
use this to get the notion of a _typed proof_. In a typed proof, all good
variables have a type, and any term that cannot be typed is built from its
components by the intruder.

Typed proofs seem to handle the problems introduced by equality formulas as
above. However, quantifiers complicate the situation further. Consider a
formula $\exists{x_{1}\ldots{}x_{k}}.{{t}\bowtie{u}}$. To derive such a
formula, one needs to apply existential quantification $k$ times. Each
occurrence of existential quantification is applied to an $\alpha(w_{i})$ to
get $\exists x_{i}.\alpha(x_{i})$. Collecting all such $(x_{i},w_{i})$ pairs
that occur in a derivation, we get a substitution $\mu$. Proving
$\exists{x_{1}\ldots{}x_{k}}.{{t}\bowtie{u}}$ thus reduces to proving
${{\mu(t)}\bowtie{\mu(u)}}$. In order to get a bound on the size of these
witnesses $w_{i}$, we might have to zap some of the values assigned by $\mu$
as well. Furthermore, there are complex interactions between $\sigma$ (which
provides meaning to variables occurring in a role) and $\mu$. We will see that
in order to obtain a correct classification of good and bad variables, we need
to consider both substitutions simultaneously. In fact, there are more than
two substitutions at play, and the interactions are even more complex. We
solve all these issues in Section 5, the heart of this paper. We then show how
to extend these results to the “assertions” used to model and analyze the FOO
e-voting protocol in [24].

###  1.4 Related Work: Equational Theories

A lot of work has been done in the field of symbolic verification for security
involving equalities of a different nature, namely those arising from
_equational theories_ [9, 10, 11]. In these theories, one considers terms
built using two kinds of operators – _constructors_ building up a term ${\sf
f}(t_{1},\ldots,t_{r})$ from its constituents $t_{1},\ldots,t_{r}$, and (zero
or more) _destructors_ corresponding to each constructor, that serve to break
down a complex term and obtain some part of it. These destructors are governed
by equations of the form ${\sf g}({\sf
f}(t_{1},\dots,t_{r}),u_{1},\dots,u_{s})=t_{i}$, for some $i\leqslant r$. For
instance, we might have the constructor ${\sf enc}$ and the corresponding
destructor ${\sf dec}$, with the equation ${\sf dec}({\sf
enc}(x,y),{y}^{-1})=x$. In fact, one usually converts these equations to
_rewrite rules_ , obtaining a rewrite system, and studies the convergence of
such a system. For example, one can convert the earlier equation to the
rewrite rule ${\sf dec}({\sf enc}(x,y),{y}^{-1})\rightarrow x$. Such rules are
implicitly universally quantified. Applying the above rule on a term $t$ boils
down to choosing any subterm of $t$ matching ${\sf dec}({\sf
enc}(x,y),{y}^{-1})$ (under some substitution $\sigma$) and replacing it by
$\sigma(x)$.

In fact, these rewrite rules correspond to inference rules. The above rewrite
rule says, for instance, that if one can derive ${\sf enc}(x,y)$ and
${y}^{-1}$, one can also derive $x$ (and ${\sf dec}$ is the name of the
inference rule). In contrast to the equations and rewrites as seen above
(which _operate_ on terms), the equalities that we consider in this paper have
the same status as terms – we start with an initial stock of terms and
equalities, and see which other equalities can be derived using inference
rules. One might, for instance, encode the standard rule for transitivity of
equalities into the following rewrite rule: ${\sf
trans}({{x}\bowtie{y}},{{y}\bowtie{z}})\rightarrow{{x}\bowtie{z}}$. Similarly,
one might encode the standard substitution rule for equalities as the rewrite
rule: ${\sf
subst}({{r(t)}\bowtie{s(t)}},{{t}\bowtie{u}})\rightarrow{{r(u)}\bowtie{s(u)}}$.
Here, we replace every occurrence of $t$ in ${{r(t)}\bowtie{s(t)}}$ (the same
$t$, and not a substitution instance like with ${\sf dec}$ and ${\sf enc}$
earlier) by $u$.

Thus, there is a clear distinction between the equalities we consider and
those in an equational theory. We view formulas as first-class objects
enjoying the same status as terms, which can be governed by equations in an
appropriate equational theory. We choose to work with inference systems (and
terms without destructors) here, but one can translate the system here into
the language of equational theories and rewrite rules.

###  1.5 Organization of the paper

In Section 2, we introduce the syntax and derivation systems for terms and
assertions. We deal with the _derivability problem_ for assertions in Section
3. In Section 4, we present a protocol model to introduce the insecurity
problem. In Section 5, we show how to properly zap all the bad variables
associated with a run. We thus prove that insecurity for a finite number of
sessions remains in NP, even after adding equalities and existential
quantification. In Section 6, we generalise the definitions to a richer syntax
in which we can model some widely-used protocols and specify useful security
properties, as presented in [24]. We discuss some possible avenues for future
work in Section 7.

##  2 The Dolev-Yao model: terms and formulas

###  2.1 Terms: Syntax and Derivation System

Each communicated message is modelled as a term in an algebra. New terms can
be derived from old ones using a proof system which specifies how these
operators behave. We have a set $\mathscr{N}$ of names (atomic terms, with no
further structure), and a set $\mathscr{V}$ of variables. We assume that
$\mathscr{V}_{q}\subset\mathscr{V}$ is the set of variables used for
quantification. We denote by $\mathscr{V}_{i}$ the set
$\mathscr{V}\setminus\mathscr{V}_{q}$. We assume a set of _keys_
$\mathscr{K}\subseteq\mathscr{N}$, and that every $k\in\mathscr{K}$ has an
inverse ${k}^{-1}\in\mathscr{K}$. $\mathscr{A}\subseteq\mathscr{N}$ is the set
of agents, with $I\in\mathscr{A}$ being the intruder. We consider the
following simple syntax for terms111Our main results are not dependent on the
exact choice of term algebra, so we can add other operators and proof rules,
as long as the system has normalization and subterm property, and derivability
is efficiently decidable., with operators for pairing and encryption.

$t\in\mathscr{T}:=x\mid m\mid(t,u)\mid{\sf enc}(t,k)$

where $x\in\mathscr{V}$, $m\in\mathscr{N}$, $k\in\mathscr{K}\cup\mathscr{V}$
and $t,u\in\mathscr{T}$. We use the shorthand $\\{t\\}_{k}$ for ${\sf
enc}(t,k)$. _Ground_ terms are those without variables. The set of subterms of
$t$ is denoted by ${\sf st}(t)$, and defined as usual. ${\sf vars}(t)$ denotes
the set of variables in $t$.

To derive new terms from existing ones, we use the proof system given in Table
1. ${\sf enc}$ and ${\sf pair}$ are constructor rules, while the others are
treated as destructors. We say $X\vdash_{\mathit{dy}}t$ if there is a proof of
$X\vdash t$ using these rules, and use $X\vdash_{\mathit{dy}}S$ to denote that
$X\vdash_{\mathit{dy}}t$ for every $t\in S$. For destructors, the leftmost
premise is the _major premise_.

tensy ${\sf ax}(t\in X)$ $\displaystyle X\vdash t$ |  tensy $\displaystyle\penalty 1X\vdash(t,u)$ ${\sf fst}$ $\displaystyle X\vdash t$ |  tensy $\displaystyle\penalty 1X\vdash(t,u)$ ${\sf snd}$ $\displaystyle X\vdash u$
---|---|---
tensy $\displaystyle\penalty 1X\vdash t\quad X\vdash u$ ${\sf pair}$ $\displaystyle X\vdash(t,u)$ |  tensy $\displaystyle\penalty 1X\vdash\\{t\\}_{k}\quad X\vdash{k}^{-1}$ ${\sf dec}$ $\displaystyle X\vdash t$ |  tensy $\displaystyle\penalty 1X\vdash t\quad X\vdash k$ ${\sf enc}$ $\displaystyle X\vdash\\{t\\}_{k}$
Table 1: Proof system for terms

For any proof $\pi$ of $X\vdash t$, we often refer to $X$ as ${\sf
axioms}(\pi)$, and we denote by ${\sf conc}(\pi)$ the term $t$, and by ${\sf
terms}(\pi)$ all terms occurring in $\pi$. $\pi$ is said to be _normal_ if no
constructor rule is the major premise of a destructor rule. The following
properties are standard (see [27], for example).

  * •

_Normalization_ : Every proof $\pi$ of $X\vdash t$ can be converted into a
normal proof $\varpi$ of the same.

  * •

_Subterm property_ : For any normal proof $\varpi$ of $X\vdash t$, ${\sf
terms}(\varpi)\subseteq{\sf st}(X\cup\\{t\\})$, and if $\varpi$ ends in a
destructor rule, ${\sf terms}(\varpi)\subseteq{\sf st}(X)$.

  * •

_Derivability problem_ : There is a PTIME algorithm to check whether
$X\vdash_{\mathit{dy}}t$, given $X$ and $t$.

###  2.2 Formulas

We consider a syntax which includes equality over terms (denoted by $\bowtie$)
and existential quantification. An _assertion_ is a formula of the form
$\exists{x_{1}\ldots{}x_{k}}.({{t}\bowtie{u}})$ where $k\geqslant 0$,
$\\{x_{1},\ldots,x_{k}\\}\subseteq\mathscr{V}_{q}$, and $t,u\in\mathscr{T}$.
If $k=0$, the assertion is just ${{t}\bowtie{u}}$.

We denote the free (resp. bound) variables occurring in an assertion $\alpha$
by ${\sf fv}(\alpha)$ and ${\sf bv}(\alpha)$. ${\sf vars}(\alpha)={\sf
fv}(\alpha)\cup{\sf bv}(\alpha)$. The set of subterms of terms occurring in
$\alpha$ is given by ${\sf st}(\alpha)$. The set of subformulas of $\alpha$ is
given by ${\sf sf}(\alpha)$. We can lift these notions to sets of assertions
as usual. For $\alpha=\exists{x_{1}\ldots{}x_{k}}.({{t}\bowtie{u}})$ and a
substitution $\lambda$,
$\lambda(\alpha)\coloneqq\exists{x_{1}\ldots{}x_{k}}.({{\lambda^{\prime}(t)}\bowtie{\lambda^{\prime}(u)}})$
where $\lambda^{\prime}=\lambda\restriction{\sf fv}(\alpha)$.

We define the _public terms_ of an assertion $\alpha$, denoted ${\sf
pubs}(\alpha)$, to be the set of maximal subterms of $\alpha$ that do not
contain any quantified variables. Formally, $t\in{\sf pubs}(\alpha)$ iff
$t\in{\sf st}(\alpha)$, ${\sf vars}(t)\cap\mathscr{V}_{q}=\varnothing$ and
there is no $u\in{\sf st}(\alpha)$ s.t. $t\neq u,t\in{\sf st}(u)$ and ${\sf
vars}(u)\cap\mathscr{V}_{q}=\varnothing$.

######  Example 2.1.

Suppose an assertion $\alpha=\exists{x}.{{t}\bowtie{\\{m\\}_{x}}}$ is
communicated. $\alpha$ states that $t$ is an encryption of $m$ with some key.
Thus $t$ and $m$ are revealed by $\alpha$, and $t,m\in{\sf pubs}(\alpha)$.

###  2.3 Proof System for Assertions

Before we present the proof system, we need to fix the conditions under which
one is allowed to derive a new assertion from existing ones. In a security
context, it becomes important to distinguish when a term is accessible inside
an assertion versus when it is not. To substitute a term $u$ (with, say, $x$)
inside a term $t$, an agent $A$ must essentially break the term down to that
position, replace $u$ with $x$, and construct the whole term back. This
depends on other terms $A$ has access to. We formalize this notion as
“abstractability”.

######  Definition 2.2.

The set of positions of a term $t$, denoted $\mathbb{P}(t)$, is a subset of
$\mathbb{N}^{*}$ defined as follows (where ${\sf f}$ is $(\cdot,\cdot)$ or
${\sf enc}$):

  * •

$\mathbb{P}(m)\coloneqq\\{\varepsilon\\}$, for
$m\in\mathscr{N}\cup\mathscr{V}$

  * •

$\mathbb{P}({\sf f}(t,u))\coloneqq\\{\varepsilon\\}\cup\\{0p\mid
p\in\mathbb{P}(t)\\}\cup\\{1p\mid p\in\mathbb{P}(u)\\}$

The term positions of an assertion
$\alpha=\exists{}x_{1}\ldots{}x_{k}.({{t}\bowtie{u}})$ are defined to be
$\mathbb{P}(\alpha)\coloneqq\\{0^{k}0p\mid
p\in\mathbb{P}(t)\\}\cup\\{0^{k}1p\mid p\in\mathbb{P}(u)\\}$.

For $t,r\in\mathscr{T}$, and $p\in\mathbb{P}(t)$, ${t}|_{p}$ is the subterm of
$t$ rooted at $p$. The set of positions where $r$ occurs in $t$ is given by
$\mathbb{P}_{r}({t})\coloneqq\\{p\in\mathbb{P}(t)\mid{t}|_{p}=r\\}$. For
$P\subseteq\mathbb{P}(t)$, ${t}[{r}]_{P}$ is the term obtained by replacing
the subterm of $t$ occurring at each $p\in P$ with $r$. We will use analogous
notation for assertions.

######  Definition 2.3.

Let $t\in\mathscr{T}$. The set of abstractable positions of $t$ w.r.t. $S$,
denoted $\mathbb{A}(S,t)$, is defined as follows. For $p\in\mathbb{P}(t)$, let
$\mathbb{Q}_{p}=\\{\varepsilon\\}\cup\\{qi\in\mathbb{P}(t)\mid q$ is a proper
prefix of $p\\}$. Then $\mathbb{A}(S,t)\coloneqq\\{p\in\mathbb{P}(t)\mid
S\vdash_{\mathit{dy}}{t}|_{q}$ for all $q\in\mathbb{Q}_{p}\\}$.

######  Example 2.4.

Let $t=(\\{\\{m\\}_{k}\\}_{k^{\prime}},(n,n^{\prime}))$.

$\mathbb{P}(t)=\\{\varepsilon,0,1,00,01,10,11,000,001\\}$

For $S=\\{\\{m\\}_{k},k^{\prime},n,n^{\prime}\\}$,
$\mathbb{A}(S,t)=\\{\varepsilon,0,1,00,01,10,11\\}$. For
$T=\\{m,k,k^{\prime},(n,n^{\prime})\\}$, $\mathbb{A}(T,t)=\mathbb{P}(t)$.

######  Definition 2.5 (Abstractable positions of an assertion).

The set of abstractable positions of
$\alpha=\exists{}x_{1}\ldots{}x_{k}.({{t}\bowtie{u}})$ w.r.t. $S$, is defined
to be the following, where $T=S\cup\\{x_{1},\ldots,x_{k}\\}$:

$\mathbb{A}(S,\alpha)\coloneqq\\{0^{k}0p\mid
p\in\mathbb{A}(T,t)\\}\cup\\{0^{k}1p\mid p\in\mathbb{A}(T,u)\\}$

######  Example 2.6.

Let $\alpha=\exists b.~{}\\{{{\\{m\\}_{b}}\bowtie{\\{m\\}_{k}}}\\}$. Suppose
we want to get $\exists ab.~{}\\{{{\\{a\\}_{b}}\bowtie{\\{m\\}_{k}}}\\}$ from
$\alpha$ w.r.t. the set $S=\\{m\\}$. That position of $m$ in $\alpha$ (i.e.
$000$) must be abstractable. This requires the sibling position $001$ to also
be abstractable, i.e. $S\vdash_{\mathit{dy}}b$. However, $S$ does not contain
the quantified variable $b$. Therefore, Definition 2.5 is set up to consider
derivability from $S\cup\\{b\\}$, not $S$. Thus,
$\mathbb{A}(S,\alpha)=\\{00,000,001\\}$. The tree for $\alpha$ is shown in
Figure 2, with the abstractable positions enclosed in boxes.

$\exists b$$\bowtie$ ${\sf enc}$$m$000$b$00100${\sf enc}$$m$010$k$01101 Figure
2: Assertion tree for Example 2.6

It can be seen that if we substitute variables occurring in some abstractable
positions with derivable terms, the abstractability of other positions does
not change. This is stated below and proved in Appendix A.

######  Lemma 2.7.

Let $S\cup\\{t,r\\}\subseteq\mathscr{T}$ s.t. $S\vdash_{\mathit{dy}}r$. If
$x\notin{\sf vars}(S)$ and
$P=\mathbb{P}_{x}({t})\subseteq\mathbb{A}(S\cup\\{x\\},t)$, then
$\mathbb{A}(S,{t}[{r}]_{P})\cap\mathbb{P}(t)=\mathbb{A}(S\cup\\{x\\},t)$.

${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 27.15108pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=54.30215pt\hbox{\kern 2.70003pt${\sf ax}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle S;A\cup\\{\alpha\\}\vdash\alpha$}}}}}$ |  ${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 10.145pt\hbox{$\displaystyle\penalty 1S\vdash_{\mathit{dy}}t$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=43.0375pt\hbox{\kern 2.70003pt${\sf eq}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle S;A\vdash{{t}\bowtie{t}}$}}}}}$ |  ${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash{{t}\bowtie{u}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=44.93962pt\hbox{\kern 2.70003pt${\sf sym}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle S;A\vdash{{u}\bowtie{t}}$}}}}}$
---|---|---
${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash{{t_{0}}\bowtie{u_{0}}}\quad S;A\vdash{{t_{1}}\bowtie{u_{1}}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=103.95927pt\hbox{\kern 2.70003pt${\sf cons}$}}}\hbox{\kern 7.76874pt\hbox{$\displaystyle S;A\vdash{{{\sf f}(t_{0},t_{1})}\bowtie{{\sf f}(u_{0},u_{1})}}$}}}}}$ |  ${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash{{{\sf f}(t_{0},t_{1})}\bowtie{{\sf f}(u_{0},u_{1})}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=88.42178pt\hbox{\kern 2.70003pt${\sf proj}_{i}^{\P}$}}}\hbox{\kern 21.25475pt\hbox{$\displaystyle S;A\vdash{{t_{i}}\bowtie{u_{i}}}$}}}}}$
${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1S;A\vdash{{t_{1}}\bowtie{t_{2}}}\quad\cdots\quad
S;A\vdash{{t_{k}}\bowtie{t_{k+1}}}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=122.87006pt\hbox{\kern 2.70003pt${\sf
trans}$}}}\hbox{\kern 35.29503pt\hbox{$\displaystyle
S;A\vdash{{t_{1}}\bowtie{t_{k+1}}}$}}}}}$
${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash{\alpha}[{t}]_{P}\quad S\vdash_{\mathit{dy}}t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=74.47807pt\hbox{\kern 2.70003pt$\exists\sf i^{{\ddagger}}$}}}\hbox{\kern 13.64474pt\hbox{$\displaystyle S;A\vdash\exists{x}.\alpha$}}}}}$ |  ${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash\exists{}{x}.\alpha\quad S\cup\\{x\\};A\cup\\{\alpha\\}\vdash\gamma$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=132.53683pt\hbox{\kern 2.70003pt$\exists\sf e^{\S}$}}}\hbox{\kern 50.29488pt\hbox{$\displaystyle S;A\vdash\gamma$}}}}}$
Table 2:  Derivation system $\vdash_{\mathit{a}}$ for assertions. ${\sf f}$ is
pairing or encryption. $\P$ states that
$S\vdash_{\mathit{dy}}\\{t_{0},t_{1},u_{0},u_{1}\\}$. ${\ddagger}$ stands for
$P=\mathbb{P}_{x}({\alpha})\subseteq\mathbb{A}(S\cup\\{x\\},\alpha)$. $\S$
states that $x\notin{\sf fv}(S)\cup{\sf fv}(A)\cup{\sf fv}(\gamma)$.

The assertion proof system is shown in Table 2. We say that
$(S;A)\vdash_{\mathit{a}}\alpha$ if there is a proof of $(S;A)\vdash\alpha$
using these rules. $(S;A)\vdash_{\mathit{a}}\Gamma$ means that
$(S;A)\vdash_{\mathit{a}}\gamma$ for every $\gamma\in\Gamma$. We say that
$(S;A)\vdash_{\mathit{eq}}\alpha$ if there is a proof of $(S;A)\vdash\alpha$
that does not use the $\exists\sf i$ and $\exists\sf e$ rules. We use the
notations ${\sf axioms}(\pi)$, ${\sf terms}(\pi)$ and ${\sf conc}(\pi)$, just
as with $\vdash_{\mathit{dy}}$ proofs.

###  2.4 Remarks about the proof rules

Since we reason about formulas in a security context, a few subtleties arise
in our proof system. We discuss these below.

  * •

“Standard” reasoning with equality would allow us to derive ${{m}\bowtie{x}}$
from ${{{\sf f}(m,k)}\bowtie{{\sf f}(x,y)}}$. But suppose ${\sf f}$ is
encryption. Security considerations dictate that one should not be able to
derive ${{m}\bowtie{x}}$ from ${{\\{m\\}_{k}}\bowtie{\\{x\\}_{y}}}$, unless
one can derive $m$. So, in general, one needs to reason with equalities in the
presence of a set of terms $S$. For the ${\sf proj}$ rule in particular, we
require that all immediate subterms are derivable from this set $S$. This,
however, does not rule out reasonable derivations, as illustrated in the next
example.

######  Example 2.8.

Let
$A=\bigl{\\{}{{x}\bowtie{\\{m\\}_{y}}},{{x}\bowtie{\\{z\\}_{k}}}\bigr{\\}}$
and $S=\\{m,k,y,z\\}$. One can derive ${{x}\bowtie{\\{m\\}_{k}}}$ from $S$ and
$A$, as in Figure 3. (For readability, we only present the RHS of every
sequent in the proof.)

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.08788pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=32.17575pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{x}\bowtie{\\{m\\}_{y}}}$}}}}\hskip 4.0pt plus
1.0fil\penalty 2\hskip 4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
0.06871pt\hbox{$\displaystyle\penalty 1S\vdash_{\mathit{dy}}m$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=24.49266pt\hbox{\kern 2.40002pt${\sf
eq}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{m}\bowtie{m}}$}}}}\hskip 4.0pt
plus 1.0fil\penalty 2\hskip 4.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.08788pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=32.17575pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{x}\bowtie{\\{m\\}_{y}}}$}}}}\hskip 4.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.77309pt\hbox{\kern 2.40002pt${\sf
sym}$}}}\hbox{\kern
17.79866pt\hbox{$\displaystyle{{\\{m\\}_{y}}\bowtie{x}}$}}}}\hskip 4.0pt plus
1.0fil\penalty 2\hskip 4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 14.67001pt\hbox{$\displaystyle\penalty
1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=29.34003pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{x}\bowtie{\\{z\\}_{k}}}$}}}}\hskip 4.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=174.13002pt\hbox{\kern 2.40002pt${\sf
trans}$}}}\hbox{\kern
66.10155pt\hbox{$\displaystyle{{\\{m\\}_{y}}\bowtie{\\{z\\}_{k}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=219.3496pt\hbox{\kern
2.40002pt${\sf proj}$}}}\hbox{\kern
100.1396pt\hbox{$\displaystyle{{y}\bowtie{k}}$}}}}\hskip 4.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=320.39247pt\hbox{\kern 2.40002pt${\sf
cons}$}}}\hbox{\kern
137.75684pt\hbox{$\displaystyle{{\\{m\\}_{y}}\bowtie{\\{m\\}_{k}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=430.69623pt\hbox{\kern
2.40002pt${\sf trans}$}}}\hbox{\kern
199.20216pt\hbox{$\displaystyle{{x}\bowtie{\\{m\\}_{k}}}$}}}}$

Figure 3: Proof tree for Example 2.8

  * •

As mentioned earlier, abstractability plays a crucial role in the application
of the $\exists\sf i$ rule. Note that the $\exists\sf i$ rule in Table 2
requires a _constructible witness_. We now explain this modification from the
“standard” $\exists\sf i$ rule.

Suppose $P$ is a set of positions in an assertion $\beta$ where a term $t$
occurs. Abstracting the occurrences of $t$ in these positions can be thought
of as obtaining $\exists{x}.{\beta}[{x}]_{P}$ from $\beta$. The above is
possible in the presence of a set of terms $S$ only when
$P\subseteq\mathbb{A}(S,\beta)$. Alternatively, suppose
$\alpha={\beta}[{x}]_{P}$. Then $\beta={\alpha}[{t}]_{P}$. Lemma 2.7
guarantees that $P\subseteq\mathbb{A}(S,\beta)$ iff
$P\subseteq\mathbb{A}(S\cup\\{x\\},\alpha)$, under the assumption
$S\vdash_{\mathit{dy}}t$, so we take that as a pre-requisite for $\exists\sf
i$.

  * •

A _substitution_ rule is standard for systems handling equality. For
$\vdash_{\mathit{a}}$, we consider the following ${\sf subst}$ rule, with the
abstractability side conditions
$P\subseteq\mathbb{P}_{x}({{{t}\bowtie{u}}})\cap\mathbb{A}(S\cup\\{x\\},{{t}\bowtie{u}})$
and $S\vdash_{\mathit{dy}}\\{r,s\\}$).

${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1(S;A)\vdash{({{t}\bowtie{u}})}[{r}]_{P}\quad(S;A)\vdash{{r}\bowtie{s}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=142.50253pt\hbox{\kern 3.00003pt${\sf
subst}$}}}\hbox{\kern
33.97678pt\hbox{$\displaystyle(S;A)\vdash{({{t}\bowtie{u}})}[{s}]_{P}$}}}}}$

We can simulate this rule using ${\sf eq}$, ${\sf sym}$, ${\sf trans}$ and
${\sf cons}$, as proved in Appendix A. Hence, we omit it from Table 2.

##  3 Derivability problem for $\vdash_{\mathit{a}}$

The derivability problem requires one to check if $\alpha$ is derivable from
$(S;A)$. To check whether an assertion of the form $\exists{x}.~{}\beta$ is
derivable, one would in general have to check if $\beta(t)$ is derivable for
some witness $t$. Here we show that if there is a witness at all, there is one
of small size.

One way to represent this is via a substitution $\mu$ which maps each
quantified variable $x$ to the corresponding $t$. In any proof, one can remove
quantifiers from the LHS (instantiated by “eigenvariables”) to move to an LHS
consisting solely of equality formulas. Any normal proof from such an LHS will
not involve $\exists\sf e$. One can also simplify the RHS – instead of proving
an assertion $\exists\vec{x}.{{t}\bowtie{u}}$, it suffices to prove
${{t}\bowtie{u}}$ in the $\vdash_{\mathit{eq}}$ system (the system without the
rules for quantification) with variables instantiated appropriately.

Hereon, in all assertions we consider, no variable appears both free and
bound. Further, whenever we use $(S;A)$, we mean that $S$ is a set of terms,
$A$ is a set of assertions, and $(S;A)$ is _sanitized_ , as defined below. We
use the notation ${\sf vars}(S;A)$ to mean ${\sf vars}(S)\cup{\sf vars}(A)$
and ${\sf fv}(S;A)$ to mean ${\sf vars}(S)\cup{\sf fv}(A)$.

######  Definition 3.1.

$(S;A)$ is sanitized if ${\sf fv}(S;A)\cap\mathscr{V}_{q}=\varnothing$ and
${\sf pubs}(\alpha)\in S$ for all $\alpha\in A$.

######  Definition 3.2 (Derivability problem for $\vdash_{\mathit{a}}$).

Given a set $S$ of terms, and a set $A\cup\\{\alpha\\}$ of assertions such
that $(S;A)$ is sanitized, check whether $S;A\vdash_{\mathit{a}}\alpha$.

######  Lemma 3.3.

Let $S,A,\exists x.\alpha$ and $\gamma$ be such that $x\notin{\sf
vars}(S)\cup{\sf vars}(A\cup\\{\gamma\\})$ and
$\mathbb{P}_{x}({\alpha})\subseteq\mathbb{A}(S\cup\\{x\\},\alpha)$. Then
$(S;A\cup\\{\exists x.\alpha\\})\vdash_{\mathit{a}}\gamma$ iff
$(S\cup\\{x\\};A\cup\\{\alpha\\})\vdash_{\mathit{a}}\gamma$.

With the help of this lemma (proved in Appendix A), we can transform any proof
to one where the LHS consists solely of atomic formulas. This leads us to a
notion of _kernel_.

######  Definition 3.4.

The kernel of $(S;A)$, denoted $\mathit{ker}(S;A)$, is defined to be
$(S\cup{\sf bv}(A);\\{{{t}\bowtie{u}}\mid\exists{\vec{x}}.{{t}\bowtie{u}}\in
A\\})$.

Each $x\in{\sf bv}(A)$ that is added to the kernel can be thought of as an
eigenvariable which stands for the witness for an existential assertion in
$A$. The following statement is an easy consequence of the way
$\mathit{ker}(S;A)$ is defined.

######  Lemma 3.5.

For any $\gamma$, $(S;A)\vdash_{\mathit{a}}\gamma$ iff
$\mathit{ker}(S;A)\vdash_{\mathit{a}}\gamma$ without using the $\exists\sf e$
rule.

We will refer to $\mathit{ker}(S;A)$ for any sanitized $(S;A)$ as _pure_. The
following property of pure $(T;E)$ is proved in Appendix A.

######  Observation 3.6.

Let $(T;E)$ be pure. If $(T;E)\vdash_{\mathit{a}}\alpha$ and $a\in{\sf
pubs}(\alpha)$, then $T\vdash_{\mathit{dy}}a$. If
$(T;E)\vdash_{\mathit{eq}}{{t}\bowtie{u}}$ then $T\vdash_{\mathit{dy}}t$ and
$T\vdash_{\mathit{dy}}u$.

Another property we desire of $(T;E)$ is _consistency_ – one should not be
able to prove absurdities like ${{(m,n)}\bowtie{\\{p\\}_{k}}}$ or
${{m}\bowtie{(m,n)}}$. This idea is formalised below.

######  Definition 3.7.

$(T;E)$ is consistent if there is a ground substitution $\lambda$ s.t.
$\lambda(t)=\lambda(u)$ for each ${{t}\bowtie{u}}\in E$.

Hereafter, we will only consider pure and consistent $(T;E)$.

A proof $\pi$ of $(T;E)\vdash\exists{}x_{1}\ldots{}x_{k}.({{t}\bowtie{u}})$
can be separated into a proof of ${{t}\bowtie{u}}$ with each $x_{i}$
instantiated by some witness, followed by $k$ applications of $\exists\sf i$.
This leads to the following theorem (whose proof is in Appendix A).

######  Theorem 3.8.

Let $\alpha=\exists{}x_{1}\ldots{}x_{k}.({{t}\bowtie{u}})$, and $(S;A)$ be
s.t. ${\sf bv}(\alpha)\cap{\sf vars}(S;A)=\varnothing$, with
$(T;E)=\mathit{ker}(S;A)$. $(S;A)\vdash_{\mathit{a}}\alpha$ iff there is a
substitution $\mu$ with ${\sf dom}(\mu)={\sf bv}(\alpha)$ s.t.:

  1. [1]

$\forall{}x\in{\sf dom}(\mu):T\vdash_{\mathit{dy}}\mu(x)$.

  2. [2]

$\forall{}x\in{\sf
dom}(\mu),r\in\\{t,u\\}:\mathbb{P}_{x}({r})\subseteq\mathbb{A}(T\cup{\sf
dom}(\mu),r)$.

  3. [3]

$(T;E)\vdash_{\mathit{eq}}{{\mu(t)}\bowtie{\mu(u)}}$.

To decide whether $(S;A)\vdash_{\mathit{a}}\alpha$, one can guess a $\mu$ and
check if the above conditions are satisfied. This amounts to guessing $\mu(x)$
for each $x\in{\sf bv}(\alpha)$, so it would be good to have a bound on the
size of $\mu(x)$. We choose the measure for size of a term to be the number of
distinct subterms.

######  Definition 3.9.

A substitution $\lambda$ is said to be $M$-bounded if $|{\sf
st}({\lambda(x)})|\leqslant M$, for all $x\in{\sf dom}(\lambda)$.

The following theorem, proved in Appendix B, is key to solving the
derivability problem.

######  Theorem 3.10.

If there is a $\mu$ satisfying the conditions in Theorem 3.8, there is an
$M$-bounded $\nu$ satisfying the same conditions, where $M=|{\sf
st}(S)\cup{\sf st}(A\cup\\{\alpha\\})|$.

After obtaining a small substitution $\nu$, we still have to check if
$(T;E)\vdash_{\mathit{eq}}{{\nu(t)}\bowtie{\nu(u)}}$. We solve this using
normalization and subterm property for $\vdash_{\mathit{eq}}$ (proved in
Appendix E).

######  Definition 3.11.

An $\vdash_{\mathit{eq}}$ proof $\pi$ of $T;E\vdash{{t}\bowtie{u}}$ is normal
if:

  * •

All $\vdash_{\mathit{dy}}$ subproofs are normal

  * •

The premise of ${\sf sym}$ can only be the conclusion of ${\sf ax}$

  * •

The premise of ${\sf eq}$ can only be the conclusion of a destructor

  * •

No premise of a ${\sf trans}$ is of the form ${{a}\bowtie{a}}$

  * •

The conclusion of a ${\sf trans}$ is not a premise of ${\sf trans}$

  * •

Adjacent premises of a ${\sf trans}$ are not conclusions of ${\sf cons}$

  * •

No subproof ending in ${\sf proj}$ contains ${\sf cons}$.

######  Theorem 3.12.

If $(T;E)\vdash_{\mathit{eq}}{{t}\bowtie{u}}$, then
$(T;E)\vdash_{\mathit{eq}}{{t}\bowtie{u}}$ via a normal proof.

######  Theorem 3.13 (Subterm property).

For any normal proof $\pi$ of $T;E\vdash_{\mathit{eq}}{{t}\bowtie{u}}$, then
${\sf terms}(\pi)\subseteq{\sf st}(T\cup\\{t,u\\})\cup{\sf st}(E)$. If ${\sf
cons}$ does not occur in $\pi$, then ${\sf terms}(\pi)\subseteq{\sf
st}(T)\cup{\sf st}(E)$.

To check whether $(T;E)\vdash_{\mathit{eq}}{{t}\bowtie{u}}$ we compute the set
$\mathscr{E}^{{t},{u}}_{{T},{E}}$ given by

$\bigl{\\{}{{r}\bowtie{s}}\mid r,s\in{\sf st}(T\cup\\{t,u\\})\cup{\sf
st}(E)\text{ and }(T;E)\vdash_{\mathit{eq}}{{r}\bowtie{s}}\bigr{\\}}$

and then check whether ${{t}\bowtie{u}}\in\mathscr{E}^{{t},{u}}_{{T},{E}}$.
The set $\mathscr{E}^{{t},{u}}_{{T},{E}}$ can be computed using a saturation-
based procedure that runs in polynomial time. The details are provided in
Appendix C.

##  4 Protocols and the insecurity problem

A _protocol_ is given by a finite set of roles corresponding to the actions of
_honest agents_. Each role consists of a finite sequence of alternating
receives and sends (each send triggered by a receive). Every sent message is
added to the intruder’s knowledge base. Each received message is assumed to
have come from the intruder, so it must be derivable by the intruder. Only
assertions are communicated – a term $t$ can be modelled via the assertion
${{t}\bowtie{t}}$, whose only public term is $t$.

######  Definition 4.1.

A protocol $\mathit{Pr}$ is a finite set of roles, each of the form
$({\beta_{1}},{\alpha_{1}})\ldots({\beta_{m}},{\alpha_{m}})$, where the
$\alpha_{i}$s and $\beta_{i}$s are assertions. An $x\in{\sf fv}(\mathit{Pr})$
is said to be an _agent variable_ if it occurs first in an $\alpha_{i}$;
otherwise it is an _intruder variable_.

######  Definition 4.2.

A session of a protocol $\mathit{Pr}$ is a sequence of the form
$u:{\beta_{1}}\\!\Rightarrow\\!{\alpha_{1}}\ \cdots\
u:{\beta_{\ell}}\\!\Rightarrow\\!{\alpha_{\ell}}$ where $u\in\mathscr{A}$ and
$(\beta_{1},\alpha_{1})\cdots(\beta_{\ell},\alpha_{\ell})$ is a prefix of a
role of $\mathit{Pr}$ with all the agent variables instantiated by values from
$\mathscr{N}$. A set of sessions $S$ of $\mathit{Pr}$ is coherent if ${\sf
fv}(\xi)\cap{\sf fv}(\xi^{\prime})=\varnothing$ for distinct
$\xi,\xi^{\prime}\in S$. One can always achieve coherence by renaming intruder
variables as necessary.

######  Observation 4.3.

Since agent variables are mapped to names, the only free variables in sessions
are intruder variables. Thus, for $i\leqslant\ell$ and any $x\in{\sf
fv}(\alpha_{i})$, there is a $j<i$ s.t. $x\in{\sf fv}(\beta_{j})$.

A run is an interleaving of sessions where each message sent by an agent
should be constructible from their knowledge. This is formalised by the notion
of _knowledge state_.

######  Definition 4.4.

A knowledge state is a pair $(X;\Phi)$ where $X$ is a finite set of terms and
$\Phi$ is a finite set of assertions. A knowledge function ${\sf k}$ is such
that ${\sf dom}({\sf k})=\mathscr{A}$ and for each $a\in\mathscr{A}$, ${\sf
k}(a)$ is a knowledge state.

Given a knowledge state $(X;\Phi)$ and an assertion $\alpha$, we define ${\it
update}((X;\Phi),\alpha)\coloneqq(X\cup{\sf
pubs}(\alpha),\Phi\cup\\{\alpha\\})$.

######  Definition 4.5.

A run of a protocol $\mathit{Pr}$ is a pair $(\xi,\sigma)$ where:

  * •

$\xi\coloneqq
u_{1}:{\beta_{1}}\\!\Rightarrow\\!{\alpha_{1}},\ldots,u_{n}:{\beta_{n}}\\!\Rightarrow\\!{\alpha_{n}}$
is an interleaving of a finite, coherent set of sessions of $\mathit{Pr}$.

  * •

$\sigma$ is a ground substitution with ${\sf dom}(\sigma)={\sf fv}(\xi)$.

  * •

There is a sequence ${\sf k}_{0}\ldots{\sf k}_{n}$ of knowledge functions
s.t.:

    * –

${\sf k}_{0}(a)=(X_{a};\varnothing)$, where $X_{a}$ is a finite set of initial
terms known to $a$ ($a$’s secret key, public keys, public names etc).

    * –

For all $i<n$,

${\sf k}_{i+1}(a)=\begin{cases}{\sf k}_{i}(a)&\mbox{if $a\neq u_{i},a\neq
I$}\\\ {\it update}({\sf k}_{i}(a),\beta_{i})&\mbox{if $a=u_{i}$}\\\ {\it
update}({\sf k}_{i}(a),\alpha_{i})&\mbox{if $a=I$}\end{cases}$

    * –

For $i\leqslant n$, ${\sf k}_{i}(u_{i})\vdash_{\mathit{a}}\alpha_{i}$ and
$\sigma({\sf k}_{i-1}(I))\vdash_{\mathit{a}}\sigma(\beta_{i})$.

The $\beta_{i}$s are implicit sends by $I$, and added to $u_{i}$’s state,
while the $\alpha_{i}$s are sent by $u_{i}$, and added to $I$’s state. Every
concrete message $\sigma(\beta_{i})$ should be derivable from the concrete
knowledge state of $I$, but it suffices for each $\alpha_{i}$ to be derived
from $u_{i}$’s state even without $\sigma$. This models the usual expectation
of protocols – that honest agent sends are enabled based on messages received
earlier in their role, and not on accidental unification with terms generated
by the intruder. We explicitly model honest agent derivability so as to allow
_conditional actions_ , i.e. to take some action only if an assertion is
derivable, and abort otherwise.

######  Definition 4.6.

A secrecy property is given by an assertion $\gamma$ which the intruder should
not know. A $K$-bounded attack which violates the secrecy of $\gamma$ is a run
of the protocol with at most $K$ sessions where $\sigma({\sf
k}_{n}(I))\vdash_{\mathit{a}}\sigma(\gamma)$.

######  Definition 4.7 ($K$-bounded insecurity problem).

Given a protocol $\mathit{Pr}$, an assertion $\gamma$, and $K\in\mathbb{N}$,
check if there exists a $K$-bounded attack on $\mathit{Pr}$ violating the
secrecy of $\gamma$.

##  5 Insecurity is in NP

Given a protocol $\mathit{Pr}$, a secrecy property specified by $\gamma$ and a
bound $K$, we now describe an NP algorithm to check if there is a $K$-bounded
attack. To do this, we need to guess a coherent set of sessions of size $K$
and an interleaving
$\xi=u_{1}:{\beta_{1}}\\!\Rightarrow\\!{\alpha_{1}},\ldots,u_{n}:{\beta_{n}}\\!\Rightarrow\\!{\alpha_{n}}$.
We also need to guess a substitution $\sigma$ with ${\sf dom}(\sigma)={\sf
fv}(\xi)$, and check that $(\xi,\sigma)$ satisfies the conditions in
Definition 4.5. We need to ensure that $\sigma$ is $M$-bounded for some $M$
which is polynomial in $K$ and the sizes of $\mathit{Pr}$ and $\gamma$. For
this, we apply Lemma 3.5 and Theorem 3.8 to each derivability of the form
$\sigma({\sf k}_{i-1}(I))\vdash_{\mathit{a}}\sigma(\beta_{i})$. Thus we have a
set of substitutions $\\{\sigma,\mu_{1},\dots,\mu_{n}\\}$ s.t.
$\mathit{ker}(\sigma({\sf
k}_{i-1}(I)))\vdash_{\mathit{eq}}{{\sigma\mu_{i}(r_{i})}\bowtie{\sigma\mu_{i}(s_{i})}}$
for each $i\leqslant n$ and $r_{i}$ and $s_{i}$ as appropriate.

We need to consider all these substitutions together and find $M$-bounded
equivalents $\sigma^{\\!*},\mu^{\\!*}_{1},\ldots,\mu^{\\!*}_{n}$ such that
$\sigma^{\\!*}({\sf
k}_{i-1}(I))\vdash_{\mathit{eq}}{{\sigma^{\\!*}\mu^{\\!*}_{i}(r_{i})}\bowtie{\sigma^{\\!*}\mu^{\\!*}_{i}(s_{i})}}$
for each $i\leqslant n$. Thus, it suffices to guess small substitutions and
check that these derivabilities hold for the intruder. For honest agent
derivations of the form ${\sf k}_{i}(u_{i})\vdash_{\mathit{a}}\alpha_{i}$, we
can use the NP algorithm to the derivability problem outlined in Section 3.
Thus we get an NP algorithm for insecurity.

An important difference between the derivability problem and the insecurity
problem is the following. In the derivability problem, the LHS is fixed, the
$\sigma$ is “already applied”, and we only need to show that if there is a
witness substitution $\mu$ that satisfies the conditions of Theorem 3.8, there
is a bounded substitution $\nu$ satisfying the same. However, for the
insecurity problem, $\sigma$ appears on the LHS of derivabilities, and
preserving them even after changing $\sigma$ to $\sigma^{\\!*}$ is a
challenge.

###  5.1 Preliminaries

We fix a protocol $\mathit{Pr}$ and a run $(\xi,\sigma)$ of $\mathit{Pr}$. By
renaming variables if necessary, we can ensure that ${\sf
fv}(\xi)\cap\mathscr{V}_{q}=\varnothing$. Since ${\sf dom}(\sigma)={\sf
fv}(\xi)$, we have $\sigma(x)=x$ for all $x\in\mathscr{V}_{q}$. It follows
that $\sigma(\mathit{ker}(S;A))=\mathit{ker}(\sigma(S;A))$, for any $(S;A)$.

For the rest of this section, we fix the following notation.

  * •

$(T_{i};E_{i})\coloneqq\mathit{ker}({\sf k}_{i}(I))$ and
$(U_{i};F_{i})\coloneqq\mathit{ker}({\sf k}_{i}(u_{i}))$.

  * •

$\mathit{IT}_{i}\coloneqq{\sf pubs}(\beta_{i})$ and
$\mathit{HT}_{i}\coloneqq{\sf pubs}(\alpha_{i})$

Note that $T_{i}\subseteq T_{i+1}$ and $E_{i}\subseteq E_{i+1}$ for every $i$.

######  Observation 5.1.

Any $t\in T_{i}$ is either a bound variable from $\beta_{j}$ (and hence in
$\mathscr{V}_{q}$) or in ${\sf pubs}(\beta_{j})$ for some $j$. In the latter
case, $t$ contains no variable from $\mathscr{V}_{q}$, and thus, ${\sf
vars}(t)\cap{\sf bv}(\xi)=\varnothing$, i.e. ${\sf vars}(t)\subseteq{\sf
fv}(\xi)={\sf dom}(\sigma)$. Reasoning similarly for $U_{i}$, we see that for
any $t\in T_{i}\cup U_{i}$, ${\sf vars}(t)\subseteq{\sf dom}(\sigma)$ or
$t\in\mathscr{V}_{q}$.

Applying Theorem 3.8 to the derivabilities in Definition 4.5, for every
$i\leqslant n$ we get substitutions $\mu_{i}$ and $\theta_{i}$ (with
respective domains ${\sf bv}(\beta_{i})$ and ${\sf bv}(\alpha_{i})$) s.t.:

  * •

for every $x\in{\sf dom}(\mu_{i})$,
$\sigma(T_{i-1})\vdash_{\mathit{dy}}\mu_{i}(x)$

  * •

$\sigma(T_{i-1};E_{i-1})\vdash_{\mathit{eq}}\sigma\mu_{i}({{r}\bowtie{s}})$
for ${{r}\bowtie{s}}\in{\sf sf}(\beta_{i})$

  * •

for every $x\in{\sf dom}(\theta_{i})$,
$\sigma(U_{i})\vdash_{\mathit{dy}}\theta_{i}(x)$

  * •

$\sigma(U_{i};F_{i})\vdash_{\mathit{eq}}\sigma\theta_{i}({{r}\bowtie{s}})$,
where ${{r}\bowtie{s}}\in{\sf sf}(\alpha_{i})$

Note that for $i\leqslant n$, ${\sf
k}_{i}(u_{i})\vdash_{\mathit{a}}\alpha_{i}$, and thus $\sigma({\sf
k}_{i}(u_{i}))\vdash_{\mathit{a}}\sigma(\alpha_{i})$. So we have a
$\theta_{i}$ for honest agent derivations.

Define $\mathscr{S}\coloneqq\\{\sigma,\theta_{i},\mu_{i}\mid i\leqslant n\\}$.
We can ensure that distinct $\lambda,\lambda^{\prime}\in\mathscr{S}$ have
disjoint domains. Assume that there is an ${\sf m}\in T_{0}\cap\mathscr{N}$
s.t. ${\sf m}\notin{\sf st}(\\{\alpha_{i},\beta_{i}\\})\cup{\sf st}({\sf
rng}(\theta_{i})\cup{\sf rng}(\mu_{i}))$ for all $i$. This can be thought of
as a fixed “spare name” that does not appear in the run.

######  Observation 5.2.

For every $i\leqslant n$ and for every $x\in{\sf dom}(\mu_{i})$,
$\sigma(T_{i-1})\vdash_{\mathit{dy}}\mu_{i}(x)$, and so any variable in
$\mu_{i}(x)$ must come from ${\sf
vars}(\sigma(T_{i-1}))\subseteq\bigcup_{j<i}({\sf dom}(\mu_{j})\cup{\sf
dom}(\theta_{j}))$. Similarly for any $x\in{\sf dom}(\theta_{i})$, ${\sf
vars}(\theta_{i}(x))\subseteq\bigcup_{j<i}({\sf dom}(\mu_{j})\cup{\sf
dom}(\theta_{j}))\cup{\sf dom}(\mu_{i})$.

Since each knowledge state arises from a sequence of updates to a sanitized
initial state, each $(T_{i};E_{i})$ and $(U_{i};F_{i})$ is pure. But we also
need them to be consistent (as in Definition 3.7). Towards this, we define a
substitution $\omega$, which is an appropriate composition of the
substitutions in $\mathscr{S}$. We motivate this by the following example.

######  Example 5.3.

Suppose $y\in{\sf bv}(\beta_{1})$, and $x\in{\sf bv}(\alpha_{2})$. Consider a
situation where $\theta_{2}(x)=\\{y\\}_{k}$ and $\mu_{1}(y)=(m_{0},m_{1})$.
Also suppose $(T_{2};E_{2})\vdash{{x}\bowtie{z}}$ for some $z\in{\sf
dom}(\sigma)$. For consistency, we need a ground $\lambda$ s.t.
$\lambda(x)=\lambda(z)$. We can take $\lambda$ to be
$\sigma\mu_{1}\theta_{2}$. We see that
$\lambda(x)=\sigma(\mu_{1}(\theta_{2}(x)))=\sigma(\mu_{1}(\\{y\\}_{k}))=\sigma(\\{(m_{0},m_{1})\\}_{k})=\\{(m_{0},m_{1})\\}_{k}$.
Observe that ${\sf dom}(\lambda)={\sf dom}(\sigma)\cup{\sf
dom}(\mu_{1})\cup{\sf dom}(\theta_{2})$, and since $z\notin{\sf
dom}(\mu_{1})\cup{\sf dom}(\theta_{2})$, $\lambda(z)=\sigma(z)$.

######  Definition 5.4.

$\omega\coloneqq\sigma\mu_{1}\theta_{1}\ldots\mu_{n}\theta_{n}$.

######  Observation 5.5.

$\omega$ is ground, and for
$\lambda\in\mathscr{S},\omega(\lambda(x))=\omega(x)$.

The next two lemmas show that each $E_{i}$ and $F_{i}$ is consistent and that
derivations preserve consistency. Any proofs omitted hereon can be found in
Appendix D.

######  Lemma 5.6.

Suppose $\lambda$ is such that $\lambda(r)=\lambda(s)$ for each
${{r}\bowtie{s}}\in E$, and $T;E\vdash_{\mathit{eq}}{{t}\bowtie{u}}$. Then
$\lambda(t)=\lambda(u)$.

######  Lemma 5.7.

For any $i\in\\{1,\ldots,n\\}$,

  1. 1.

if ${{t}\bowtie{u}}\in E_{i}\cup F_{i}$, then $\omega(t)=\omega(u)$.

  2. 2.

if
$\sigma(T_{i-1};E_{i-1})\vdash_{\mathit{eq}}\sigma\mu_{i}({{t}\bowtie{u}})$,
then $\omega(t)=\omega(u)$.

  3. 3.

if $\sigma(U_{i};F_{i})\vdash_{\mathit{eq}}\sigma\theta_{i}({{t}\bowtie{u}})$,
then $\omega(t)=\omega(u)$.

We developed this preliminary setup for both honest agent derivations as well
as intruder derivations in order to demonstrate the interplay between $\theta$
and $\mu$, as evidenced in the definition of $\omega$. However, the insecurity
problem itself is concerned only with intruder derivability, and therefore, in
the next few sections we will focus on
$\mathit{IT}_{i},\beta_{i},(T_{i};E_{i})$, and $\mu_{i}$.

###  5.2 Typed $\vdash_{\mathit{dy}}$ proofs

######  Definition 5.8 (Types).

We use the sets $\mathscr{C}$ (consisting of the terms occurring in $\xi$
before applying any substitution) and $\mathscr{D}$ (the same set, but without
variables) to type the terms appearing in any proof. They are defined as
follows.

$\mathscr{C}\coloneqq\bigcup_{i\leqslant n}\bigl{\\{}\bigl{(}{\sf
st}(T_{i}\cup U_{i})\cup{\sf st}(E_{i}\cup
F_{i})\bigr{)}\bigr{\\}}\quad\quad\mathscr{D}\coloneqq\mathscr{C}\setminus\mathscr{V}$

We show that under $\sigma$, any term $t$ with no type in $\mathscr{C}$
appears in a received assertion $\beta$ first, and is generated by the
intruder by putting information together, i.e. via a normal proof ending in a
constructor rule. Using this, we show that every proof from $\sigma(T_{i})$
can be turned into a “typed” proof. Typed proofs help preserve derivability
even after zapping variables.

Consider a proof $\pi$ of $\sigma(T_{i})\vdash t$ for some $t$. It is possible
that $\pi$ mentions terms from outside $\omega(\mathscr{C})$, even if
$t\in\omega(\mathscr{C})$. In a “typed” equivalent of $\pi$, every subproof
deriving such terms ends in a constructor rule. If a proof ends in a
destructor rule, however, one can anchor the conclusion to some term in
$\mathscr{C}$, i.e. provide a “type” from $\mathscr{C}$.

######  Definition 5.9.

[Typed $\vdash_{\mathit{dy}}$ proof] A $\vdash_{\mathit{dy}}$ proof $\pi$ is
typed if for each subproof $\pi^{\prime}$, either $\pi^{\prime}$ ends in a
constructor rule, or ${\sf
conc}(\pi^{\prime})\in\sigma(\mathscr{D})\cup\mathscr{V}_{q}$.

If a term $t$ does not match any pattern mentioned in the protocol, and
appears in the intruder’s knowledge set (even as a subterm of some term in the
set), then it must have appeared first in an intruder send. We formalize this
as follows.

######  Lemma 5.10.

Suppose $t\notin\sigma(\mathscr{D})\cup\mathscr{V}_{q}$. For $i\leqslant n$,
if $t\in{\sf st}(\sigma(T_{i}))$, then there is a $k<i$ such that $t\in{\sf
st}(\sigma(\mathit{IT}_{k}))$.

If a term as above is derived by the intruder at some stage $i$, the
derivation either ends in a construction rule, so $t$ is freshly put together
at this stage, or there is an earlier point at which the intruder derived $t$.
Thus, terms that cannot be provided a type from $\mathscr{D}$ do not originate
in an honest agent send.

######  Lemma 5.11.

Suppose $i\leqslant n$, $t\notin\sigma(\mathscr{D})\cup\mathscr{V}_{q}$ and
$\sigma(T_{i})\vdash_{\mathit{dy}}t$ via a normal proof $\pi$ ending in a
destructor rule. Then there is an $\ell<i$ such that
$\sigma(T_{\ell})\vdash_{\mathit{dy}}t$.

######  Theorem 5.12.

For all $t$ and all $i\in\\{0,\ldots,n\\}$, if
$\sigma(T_{i})\vdash_{\mathit{dy}}t$, then there is a typed normal proof
$\pi^{*}$ of the same.

  * Proof.

Assume the theorem holds for all $t$ and for all $j<i$. We show how to
transform any proof $\pi$ of $\sigma(T_{i})\vdash t$ into a typed normal proof
$\pi^{*}$ of the same.

    * –

$\pi$ ends in ax: $t\in\sigma(T_{i})\subseteq\sigma(\mathscr{C})$. If
$t\in\sigma(\mathscr{D})\cup\mathscr{V}_{q}$, we take $\pi^{*}$ to be $\pi$
itself. Otherwise, by Lemma 5.11, there is some $j<i$ such that
$\sigma(T_{j})\vdash_{\mathit{dy}}t$. Since $j<i$, we can get a typed normal
proof $\pi^{*}$ of $\sigma(T_{j})\vdash t$ and obtain the required result by
weakening the LHS.

    * –

$\pi$ ends in a constructor: We can find typed normal equivalents for all
immediate subproofs, and apply the same constructor rule to get the desired
$\pi^{*}$.

    * –

$\pi$ ends in a destructor: Let $\pi_{1}$ and $\pi_{2}$ be the immediate
subproofs of $\pi$, with ${\sf conc}(\pi_{1})=s$, where $t$ is an immediate
subterm of $s$. We can find typed normal equivalents $\pi^{*}_{1}$ and
$\pi^{*}_{2}$. If $\pi^{*}_{1}$ ends in a constructor, then we choose
$\pi^{*}$ to be the immediate subproof of $\pi^{*}_{1}$ s.t. ${\sf
conc}(\pi^{*})=t$. $\pi^{*}_{1}$ is typed normal, and so is $\pi^{*}$.

If $\pi^{*}_{1}$ does not end in a constructor,
$s\in\sigma(\mathscr{D})\cup\mathscr{V}_{q}$. Since a destructor rule ${\sf
r}$ was applied on $s$, $s\notin\mathscr{V}_{q}$. So
$s\in\sigma(\mathscr{D})$, and hence $t\in\sigma(\mathscr{C})$. If
$t\in\sigma(\mathscr{D})\cup\mathscr{V}_{q}$, we obtain a typed normal
$\pi^{*}$ by applying ${\sf r}$ on $\pi^{*}_{1}$. Otherwise, as with ${\sf
ax}$, by Lemma 5.11 and weakening, we get a typed and normal proof $\pi^{*}$
of $\sigma(T_{i})\vdash t$. ∎

###  5.3 Typed equality proofs

We now define a notion of “minimal variables”, which are variables that do not
unify with any non-atomic term mentioned in the protocol. The idea is that
images of minimal variables can be freely “zapped” to an atomic constant.

######  Definition 5.13 (Minimal variable).

$x\in{\sf dom}(\omega)$ is minimal if there is no $t\in\mathscr{D}$ such that
$\omega(x)=\omega(t)$.

######  Definition 5.14.

A term $t$ is zappable if there is a minimal $x$ such that
$\omega(t)=\omega(x)$.

######  Observation 5.15.

a

  * •

If a term $t$ is zappable, then $t\notin\mathscr{D}$.

  * •

If a term $t\in\omega(\mathscr{C})$ is not zappable, then
$t\in\omega(\mathscr{D})$.

  * •

For $t,u$ s.t. $\omega(t)=\omega(u)$, $t$ is zappable iff $u$ is zappable.

######  Definition 5.16 (Typed term).

A term $t$ is typed if
$t\in\sigma(\mathscr{D})\cup\omega(\mathscr{C})\cup\mathscr{V}_{q}$.

######  Example 5.17.

Note that we consider $\sigma(\mathscr{D})$ separately from
$\omega(\mathscr{C})$. Consider a term of the form $(m,x)\in\mathscr{D}$,
where $x\notin{\sf dom}(\sigma)$. $\sigma((m,x))=(m,x)$, but this cannot be in
$\omega(\mathscr{C})$, since $\omega(\mathscr{C})$ only contains ground terms.
Thus, $\sigma(\mathscr{D})\not\subseteq\omega(\mathscr{C})$.

We now consider a small example which will motivate our choices for the
definition of a _typed $\vdash_{\mathit{eq}}$ proof_.

######  Example 5.18.

Suppose $\sigma(x)=(t_{1},t_{2})$ for some minimal variable $x$, and
$\sigma(u)=(u_{1},u_{2})$ for some term $u$. Suppose we also have a proof
$\pi$ of ${{t_{1}}\bowtie{u_{1}}}$ obtained by applying ${\sf proj}_{1}$ to
${{\sigma(x)}\bowtie{\sigma(u)}}$, and we want to derive a “corresponding”
equality assertion under a small $\sigma^{\\!*}$. The most straightforward
strategy is to follow the structure of $\pi$. However, under $\sigma^{\\!*}$,
we would “zap” $x$ to an atomic value. We cannot apply ${\sf proj}$ to this,
so we can no longer preserve the structure of $\pi$.

To avoid such situations, we define a typed $\vdash_{\mathit{eq}}$ proof as
one whose structure can be preserved under zapping. We then show that any
$\vdash_{\mathit{eq}}$ proof can be simulated by a typed one.

######  Definition 5.19.

[Typed $\vdash_{\mathit{eq}}$ proof] A proof $\pi$ of
$X;A\vdash{{r}\bowtie{s}}$ is typed if for every subproof $\pi^{\prime}$ with
conclusion $X;A\vdash{{t}\bowtie{u}}$,

  * •

$\pi^{\prime}$ contains an occurrence of the ${\sf cons}$ rule, or

  * •

$t=u$, or

  * •

$t$ and $u$ are typed terms.

Observe that for any $t\in\sigma(\mathscr{C})$, we have
$t\in\sigma(\mathscr{D})$, or $t=\sigma(x)=x$ for some $x\notin{\sf
dom}(\sigma)$ (in which case $t\in\mathscr{V}_{q}$), or $t=\sigma(x)$ for
$x\in{\sf dom}(\sigma)$ (in which case $t=\omega(x)$, so
$t\in\omega(\mathscr{C})$). Thus
$\sigma(\mathscr{C})\subseteq\sigma(\mathscr{D})\cup\omega(\mathscr{C})\cup\mathscr{V}_{q}$,
i.e. every term in $\sigma(\mathscr{C})$ is typed. Using this, we can prove
the following lemma.

######  Lemma 5.20.

Suppose $t={\sf f}(t_{0},t_{1})$ and $u={\sf f}(u_{0},u_{1})$ are typed, and
$\omega(t)=\omega(u)$. One of the following is true:

  * •

$t$ and $u$ are not zappable, and $t_{0},t_{1},u_{0},u_{1}$ are typed, or

  * •

$t$ and $u$ are zappable, and $t=u$.

######  Theorem 5.21.

For all $i\leqslant n$, every normal $\vdash_{\mathit{eq}}$ proof from
$\sigma(T_{i};E_{i})$ is a typed proof.

  * Proof.

Let $\pi$ be a normal $\vdash_{\mathit{eq}}$ proof of
$\sigma(T_{i};E_{i})\vdash{{t}\bowtie{u}}$. Assume all proper subproofs of
$\pi$ are typed. We do a case analysis on the last rule of $\pi$. Most of the
cases are straightforward, so here we only show the case when $\pi$ ends in
${\sf proj}$. The full proof is presented in Appendix D.

Suppose there are $a={\sf f}(a_{0},a_{1})$ and $b={\sf f}(b_{0},b_{1})$ such
that $t=a_{0}$ and $u=b_{0}$ and the immediate subproof $\pi^{\prime}$ proves
${{a}\bowtie{b}}$. By Lemma 5.7 and Observation 5.5, $\omega(a)=\omega(b)$. By
normality, ${\sf cons}$ does not occur in $\pi$ or $\pi^{\prime}$, and since
$\pi^{\prime}$ is typed, two cases arise.

    * –

$a=b$: $t$ and $u$ are immediate subterms of $a$ and $b$, so $t=u$ and $\pi$
is typed.

    * –

$a$ and $b$ are typed: We have $\omega(a)=\omega(b)$. Hence, by Lemma 5.20,
either $a=b$ (so $t=u$ as above) or $t$ and $u$ are typed. In both cases,
$\pi$ is typed. ∎

###  5.4 Small substitutions $\sigma^{\\!*},\omega^{\\!*}$, and
$\mu^{\\!*}_{i}$

Recall that there is a fixed name $\displaystyle{\sf
m}\in\mathscr{C}\setminus{\sf st}(\bigcup_{\lambda\in\mathscr{S}}{\sf
rng}(\lambda))$.

######  Definition 5.22.

For any term $t$, we inductively define the zap of $t$, denoted
$\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}$, as follows:

$\displaystyle\overline{\mspace{1.0mu}{x}\mspace{1.0mu}}$
$\displaystyle\coloneqq x$
$\displaystyle\overline{\mspace{1.0mu}{n}\mspace{1.0mu}}$
$\displaystyle\coloneqq\begin{cases}{\sf m}&\qquad\hskip 5.69054pt\mbox{if $n$
is zappable}\\\ n&\qquad\hskip 5.69054pt\mbox{otherwise}\end{cases}$
$\displaystyle\overline{\mspace{1.0mu}{{\sf f}(t_{1},t_{2})}\mspace{1.0mu}}$
$\displaystyle\coloneqq\begin{cases}{\sf m}&\mbox{if ${\sf f}(t_{1},t_{2})$ is
zappable}\\\ {\sf
f}(\overline{\mspace{1.0mu}{t_{1}}\mspace{1.0mu}},\overline{\mspace{1.0mu}{t_{2}}\mspace{1.0mu}})&\mbox{otherwise}\end{cases}$

For a set of terms $X$,
$\overline{\mspace{1.0mu}{X}\mspace{1.0mu}}\coloneqq\\{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}\mid
t\in X\\}$. For a set of equalities $E$,
$\overline{\mspace{1.0mu}{E}\mspace{1.0mu}}\coloneqq\\{{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}\mid{{t}\bowtie{u}}\in
E\\}$.

######  Definition 5.23.

For $\lambda\in\\{\sigma,\omega,\mu_{i}\mid i\leqslant n\\}$, the small
substitution $\lambda^{\\!*}$ corresponding to $\lambda$ is defined as
$\lambda^{\\!*}(x)\coloneqq\overline{\mspace{1.0mu}{\lambda(x)}\mspace{1.0mu}}$.

######  Example 5.24.

Suppose $\mathscr{C}={\sf st}(\\{{\sf m},y,(y_{1},\\{y_{2}\\}_{k})\\})$, where
$y_{1},y_{2}$ are minimal, and $\mu_{2}(y)=(y_{1},\\{y_{2}\\}_{k})$. Then,
$\mu^{\\!*}_{2}(y)=(y_{1},\\{y_{2}\\}_{k})$, i.e. there is no zap even though
$y_{1}$ and $y_{2}$ are minimal (because
$\overline{\mspace{1.0mu}{y_{i}}\mspace{1.0mu}}=y_{i}\in\mathscr{V}$). The
pair itself is not zapped since it is in $\mathscr{C}$. The zap for $y_{1}$
and $y_{2}$ occurs when we consider $\omega^{\\!*}(y)$, which is $({\sf
m},\\{{\sf m}\\}_{k})$, since $\omega(y_{i})$ is a zappable term.

However, consider $\mathscr{C}={\sf st}(\\{{\sf m},y,y_{2},(y_{1},x)\\})$ and
the same $\mu_{2}$, with $x$ minimal and $\sigma(x)=\mu_{2}(\\{y_{2}\\}_{k})$.
Then, since $\\{y_{2}\\}_{k}\notin\mathscr{C}$, we see that
$\mu^{\\!*}_{2}(y)=(y_{1},{\sf m})$ and $\omega^{\\!*}(y)=({\sf m},{\sf m})$.

######  Example 5.25.

Let $t=\sigma(x)$ for a minimal $x$. So ${\sf vars}(t)=\varnothing$, and
$\sigma^{\\!*}(t)=t$. However,
$\overline{\mspace{1.0mu}{\sigma(t)}\mspace{1.0mu}}=\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}={\sf
m}$, since $t$ is zappable. Thus, it is not true that
$\lambda^{\\!*}(t)=\overline{\mspace{1.0mu}{\lambda(t)}\mspace{1.0mu}}$ for
all $t$.

However, the next lemma shows that this holds for all $t\in\mathscr{C}$.

######  Lemma 5.26.

For $i\leqslant n$ and $t\in\mathscr{C}$,
$\sigma^{\\!*}\mu^{\\!*}_{i}(t)=\overline{\mspace{1.0mu}{\sigma\mu_{i}(t)}\mspace{1.0mu}}$.

We now show that we can simulate any $\lambda$ using $\lambda^{\\!*}$ for
deriving both terms and equalities.

######  Observation 5.27.

$T_{i}\subseteq\mathscr{C}$, so by Lemma 5.26,
$\sigma^{\\!*}(T_{i})=\overline{\mspace{1.0mu}{\sigma(T_{i})}\mspace{1.0mu}}$,
and similarly
$\sigma^{\\!*}(E_{i})=\overline{\mspace{1.0mu}{\sigma(E_{i})}\mspace{1.0mu}}$,
for all $i\leqslant k$.

######  Lemma 5.28.

For $i\leqslant n$ and any term $t$, if $\sigma(T_{i})\vdash_{\mathit{dy}}t$
then
$\sigma^{\\!*}(T_{i})\vdash_{\mathit{dy}}\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}$.

  * Proof.

Let $X$ and $Y$ stand for $\sigma(T_{i})$ and $\sigma^{\\!*}(T_{i})$. By
Observation 5.27, $\overline{\mspace{1.0mu}{X}\mspace{1.0mu}}=Y$. Let $\pi$ be
a typed normal $\vdash_{\mathit{dy}}$ proof of $X\vdash t$ (ensured by Theorem
5.12). We prove that
$Y\vdash_{\mathit{dy}}\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}$. Consider
the last rule ${\sf r}$ of $\pi$. The following cases arise.

    * –

${\sf r}=\textsf{ax}$: $t\in X$, and therefore
$\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}\in Y$. Thus
$Y\vdash_{\mathit{dy}}\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}$ by ax.

    * –

${\sf r}$ is a constructor: Let $t={\sf f}(t_{1},t_{2})$ and let the immediate
subproofs of $\pi$ be $\pi_{1},\pi_{2}$, with ${\sf conc}(\pi_{i})=t_{i}$ for
$i\leqslant 2$. By IH, there is a proof $\varpi_{i}$ of
$Y\vdash\overline{\mspace{1.0mu}{t_{i}}\mspace{1.0mu}}$ for each $i\leqslant
2$. If $t$ is zappable, then $\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}={\sf
m}\in Y$ (${\sf m}\in T_{i}$ for all $i$, so ${\sf m}\in X$ and ${\sf m}\in
Y$), and we have
$Y\vdash_{\mathit{dy}}\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}$ using ax. If
$t$ is not zappable, then
$\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}=\overline{\mspace{1.0mu}{{\sf
f}(t_{1},t_{2})}\mspace{1.0mu}}={\sf
f}(\overline{\mspace{1.0mu}{t_{1}}\mspace{1.0mu}},\overline{\mspace{1.0mu}{t_{2}}\mspace{1.0mu}})$,
and we can apply ${\sf r}$ on the $\varpi_{i}$s to get
$Y\vdash_{\mathit{dy}}\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}$.

    * –

${\sf r}$ is a destructor: Let the immediate subproofs of $\pi$ be
$\pi_{1},\pi_{2}$, deriving $t_{1},t_{2}$ respectively, with $t_{1}$ being the
major premise, and $t$ an immediate subterm of $t_{1}$. Since $\pi$ is typed
normal, $\pi_{1}$ is also typed and ends in a destructor, so by Definition
5.9, $t_{1}\in\sigma(\mathscr{D})\cup\mathscr{V}_{q}$. Since we applied a
destructor on $t_{1}$, it is not in $\mathscr{V}_{q}$. Thus, there is some
$u_{1}\in\mathscr{D}$, with the same outermost operator as $t_{1}$, such that
$t_{1}=\sigma(u_{1})$. Hence, $\omega(t_{1})=\omega(u_{1})$.

If $t_{1}$ were zappable, there would be a minimal $x$ such that
$\omega(x)=\omega(t_{1})=\omega(u_{1})\in\omega(\mathscr{D})$, which
contradicts the minimality of $x$. Thus, $t_{1}$ is not zappable, and
$\overline{\mspace{1.0mu}{t_{1}}\mspace{1.0mu}}$ has the same outermost
structure as $t_{1}$. By IH, there is a proof $\varpi_{i}$ of
$Y\vdash\overline{\mspace{1.0mu}{t_{i}}\mspace{1.0mu}}$ for each $i\leqslant
2$. Since $\overline{\mspace{1.0mu}{t_{1}}\mspace{1.0mu}}$ is not atomic, we
can apply the destructor ${\sf r}$ on the $\varpi_{i}$s to get
$Y\vdash_{\mathit{dy}}\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}$. ∎

######  Lemma 5.29.

For $i\leqslant n$ and terms $t,u$, if
$\sigma(T_{i};E_{i})\vdash_{\mathit{eq}}{{t}\bowtie{u}}$ then
$\sigma^{\\!*}(T_{i};E_{i})\vdash_{\mathit{eq}}{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}$.

  * Proof.

Let $(X;A)$ and $(Y;B)$ denote $\sigma(T_{i};E_{i})$ and
$\sigma^{\\!*}(T_{i};E_{i})$ respectively. By Observation 5.27,
$\overline{\mspace{1.0mu}{X}\mspace{1.0mu}}=Y$ and
$\overline{\mspace{1.0mu}{A}\mspace{1.0mu}}=B$. Let $\pi$ be a typed normal
$\vdash_{\mathit{eq}}$ proof of $X;A\vdash{{t}\bowtie{u}}$ (guaranteed by
Theorem 5.21). We prove that
$Y;B\vdash_{\mathit{eq}}{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}$.
Most of the cases are straightforward, so here we only consider the cases when
$\pi$ ends in ${\sf proj}$ or ${\sf cons}$. The full proof is in Appendix D.

    * –

$\pi$ ends in ${\sf proj}$: Let the immediate subproof of $\pi$ be
$\pi^{\prime}$ deriving $X;A\vdash{{a}\bowtie{b}}$ where $a={\sf
f}(a_{0},a_{1})$, $b={\sf f}(b_{0},b_{1})$, and $t=a_{0}$ and $u=b_{0}$. By
IH, there is a proof $\varpi^{\prime}$ of
$Y;B\vdash{{\overline{\mspace{1.0mu}{a}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{b}\mspace{1.0mu}}}}$.
For ${\sf proj}$, we need
$X\vdash_{\mathit{dy}}\\{a_{0},a_{1},b_{0},b_{1}\\}$. By Lemma 5.28,
$Y\vdash_{\mathit{dy}}\\{\overline{\mspace{1.0mu}{a_{0}}\mspace{1.0mu}},\overline{\mspace{1.0mu}{a_{1}}\mspace{1.0mu}},\overline{\mspace{1.0mu}{b_{0}}\mspace{1.0mu}},\overline{\mspace{1.0mu}{b_{1}}\mspace{1.0mu}}\\}$.
By Lemma 5.7 and Observation 5.5, $\omega(a)=\omega(b)$. By normality, ${\sf
cons}$ cannot occur in $\pi$. $\pi$ is also typed, so either $a=b$ or $a$ and
$b$ are typed. If $a=b$, then $t=u$, and we have a proof of
$Y;B\vdash{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}$
ending in ${\sf eq}$. If $a$ and $b$ are typed, we apply Lemma 5.20 and
consider two cases.

      * *

$a$ and $b$ not zappable: Then $\overline{\mspace{1.0mu}{a}\mspace{1.0mu}}$
and $\overline{\mspace{1.0mu}{b}\mspace{1.0mu}}$ have the same outermost
structure as $a$ and $b$, and
$\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}=\overline{\mspace{1.0mu}{a_{0}}\mspace{1.0mu}}$
and
$\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}=\overline{\mspace{1.0mu}{b_{0}}\mspace{1.0mu}}$.
So we can apply ${\sf proj}$ on $\varpi^{\prime}$ to get
$Y;B\vdash_{\mathit{eq}}{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}$.

      * *

$a=b$: Then $t=u$ as well, and hence
$\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}=\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}$.
Since
$Y\vdash_{\mathit{dy}}\\{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}},\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}\\}$,
$Y;B\vdash_{\mathit{eq}}{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}$
with last rule ${\sf eq}$.

    * –

$\pi$ ends in ${\sf cons}$: Let $t={\sf f}(t_{0},t_{1})$ and $u={\sf
f}(u_{0},u_{1})$. Let $\pi$ have immediate subproofs $\pi_{0}$ and $\pi_{1}$,
each $\pi_{i}$ proving $X;A\vdash{{t_{i}}\bowtie{u_{i}}}$. By IH, there are
proofs $\varpi_{1},\varpi_{2}$, each $\varpi_{i}$ proving
$Y;B\vdash{{\overline{\mspace{1.0mu}{t_{i}}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u_{i}}\mspace{1.0mu}}}}$.
By Lemma 5.20, two cases arise.

      * *

$t$ and $u$ not zappable: Then
$\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}={\sf
f}(\overline{\mspace{1.0mu}{t_{1}}\mspace{1.0mu}},\overline{\mspace{1.0mu}{t_{2}}\mspace{1.0mu}})$
and $\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}={\sf
f}(\overline{\mspace{1.0mu}{u_{1}}\mspace{1.0mu}},\overline{\mspace{1.0mu}{u_{2}}\mspace{1.0mu}})$.
So
$Y;B\vdash_{\mathit{eq}}{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}$
using ${\sf cons}$ on the $\varpi_{i}$s.

      * *

$t$ and $u$ zappable: Then,
$\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}=\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}={\sf
m}\in Y$, so we have a proof of
$Y;B\vdash{{\overline{\mspace{1.0mu}{t}\mspace{1.0mu}}}\bowtie{\overline{\mspace{1.0mu}{u}\mspace{1.0mu}}}}$
ending in ${\sf eq}$. ∎

The following theorem is an immediate consequence of Lemmas 5.26, 5.28 and
5.29.

######  Theorem 5.30.

Let $t,u\in\mathscr{C}$ and $i\leqslant n$.

  * •

If $\sigma(T_{i-1})\vdash_{\mathit{dy}}\sigma\mu_{i}(t)$ then
$\sigma^{\\!*}(T_{i-1})\vdash_{\mathit{dy}}\sigma^{\\!*}\mu^{\\!*}_{i}(t)$.

  * •

If $\sigma(T_{i-1};E_{i-1})\vdash_{\mathit{eq}}\sigma\mu_{i}({{t}\bowtie{u}})$
then
$\sigma^{\\!*}(T_{i-1};E_{i-1})\vdash_{\mathit{eq}}\sigma^{\\!*}\mu^{\\!*}_{i}({{t}\bowtie{u}})$.

Having shown that the $\lambda^{\\!*}$s simulate the $\lambda$s, we next show
that they are all bounded.

######  Theorem 5.31.

For $\lambda\in\\{\sigma,\omega,\mu_{i}\mid i\leqslant n\\}$, $\lambda^{\\!*}$
is $|\mathscr{D}|$-bounded.

  * Proof.

For each $\lambda$ and any $x$,
$\omega^{\\!*}(\lambda^{\\!*}(x))=\omega^{\\!*}(x)=\overline{\mspace{1.0mu}{\omega(x)}\mspace{1.0mu}}$
(by Definition 5.23) and thus, $|{\sf st}({\lambda^{\\!*}(x)})|\leqslant|{\sf
st}({\omega^{\\!*}(x)})|$. So it suffices to prove a bound on $|{\sf
st}({\omega^{\\!*}(x)})|$. We show that for $t\in\mathscr{C}$, ${\sf
st}(\omega^{\\!*}(t))\subseteq\omega^{\\!*}(\mathscr{D})$. Note that if $t=x$
is non-minimal, there is an $r\in\mathscr{D}$ s.t.
$\omega^{\\!*}(t)=\omega^{\\!*}(r)$. Thus it suffices to prove the statement
for $t$ which is either a minimal variable or in $\mathscr{D}$.

The proof is by induction on $|\omega^{\\!*}(t)|$.

  * –

$|\omega^{\\!*}(t)|=1:$ $\omega^{\\!*}(t)\in\mathscr{N}$. So $t\in\mathscr{N}$
or a minimal variable. If $t\in\mathscr{N}$,
$\omega^{\\!*}(t)=t\in\mathscr{N}$. Otherwise, $\omega^{\\!*}(t)={\sf m}$. In
both these cases, ${\sf
st}(\omega^{\\!*}(t))\subseteq\omega^{\\!*}(\mathscr{D})$.

  * –

$|\omega^{\\!*}(t)|>1:$ Let $a\in{\sf st}(\omega^{\\!*}(t))$. If
$a=\omega^{\\!*}(u)$ for some $u\in{\sf st}(t)\setminus{\sf vars}(t)$, then
$a\in\omega^{\\!*}(\mathscr{D})$. If $a=\omega^{\\!*}(x)$ for some minimal
$x\in{\sf vars}(t)$, then $a={\sf m}=\omega^{\\!*}({\sf
m})\in\omega^{\\!*}(\mathscr{D})$. If $a\in{\sf st}(\omega^{\\!*}(x))$ for
non-minimal $x\in{\sf vars}(t)$, then $x\neq t$, and there is an
$r\in\mathscr{D}$ s.t. $\omega^{\\!*}(x)=\omega^{\\!*}(r)$, and $a\in{\sf
st}(\omega^{\\!*}(r))$. Since $|\omega^{\\!*}(r)|<|\omega^{\\!*}(t)|$, by IH,
${\sf st}(\omega^{\\!*}(r))\subseteq\omega^{\\!*}(\mathscr{D})$. Thus
$a\in\omega^{\\!*}(\mathscr{D})$.

Hence, $|{\sf
st}({\omega^{\\!*}(t)})|\leqslant|\omega^{\\!*}(\mathscr{D})|\leqslant|\mathscr{D}|$,
for $t\in\mathscr{C}$. ∎

###  5.5 NP algorithm for Insecurity: Sketch

After guessing a coherent set of sessions and an interleaving of these
sessions of length $n$, we guess bounded substitutions $\sigma^{\\!*}$ and
$\mu^{\\!*}_{1},\ldots,\mu^{\\!*}_{n}$, as well as a sequence of knowledge
functions such that the relevant equalities and terms (communicated in the
$\sigma^{\\!*}(\beta_{i})$s) are derivable from
$\sigma^{\\!*}(\mathit{ker}({\sf k}_{i-1}(I)))$. All these derivability checks
can be carried out in time polynomial in the size of the protocol description.

For the honest agent sends, we only require derivabilities of the form ${\sf
k}_{i}(u_{i})\vdash_{\mathit{a}}\alpha_{i}$, without applying any
substitution. This is the derivability problem, which we proved to be solvable
in NP. Finally, we check that $\sigma^{\\!*}({\sf
k}_{n}(I))\vdash_{\mathit{a}}\sigma^{\\!*}(\gamma)$, which can also be solved
in NP. Thus the $K$-bounded insecurity problem for assertions is in NP.

##  6 Applications and Extended Syntax

The Dolev-Yao model with formulas can be used for modelling real-world
protocols, as in [22] and [24]. We now introduce a variant of the model from
[24], and show how to encode the well-known FOO e-voting protocol [17] in that
system. Finally, we discuss how our results can be extended to this system.

###  6.1 Modelling the FOO protocol à la [24]

In [24], the authors allow principals to communicate a richer class of
assertions over an extended syntax. The syntax considered there includes
atomic predicates, equality, conjunction, existentially quantified assertions,
disjunction, and a$\ \mathit{says}\ $connective. We will consider the same
syntax, but instead of full disjunction, we will consider list membership
(denoted by $\twoheadleftarrow$), as this suffices for most examples. In the
following, $t,u\in\mathscr{T}$, $P$ is an $m$-ary predicate,
$u_{1},\ldots,u_{m},t_{0}\in\mathscr{N}\cup\mathscr{V}$, and
$t_{1},\ldots,t_{n}\in\mathscr{N}$, $x\in\mathscr{V}_{q}$, and
$\mathit{pk}_{A}$ denotes the public key of the agent $A\in\mathscr{A}$.

$\displaystyle\alpha$ $\displaystyle:={{t}\bowtie{u}}\mid
P(u_{1},\ldots,u_{m})\mid t_{0}\twoheadleftarrow[t_{1},\ldots,t_{n}]$
$\displaystyle\hskip 19.91692pt\mid\alpha_{0}\wedge\alpha_{1}\mid\exists
x.~{}\alpha(x)\mid\mathit{pk}_{A}\ \mathit{says}\ \alpha$

The extra rules required for this syntax are shown in Table 3.

One can model interesting protocols in this language, including the FOO
e-voting protocol [17, 20]. In this protocol, there is a voter $V$, an
authority $A$ who verifies the eligibility of voters but should not know their
votes, and a collector $C$ who should not know voters’ identities but counts
all votes.

To model this using only terms, a new operator called _blinding_ is used.
Signing a blinded object allows the signature to percolate through to the
object inside the blind. Formally, one can use $t$ and $b$ to make a blind
pair ${\sf blind}(t,b)$, and get ${\sf sign}(t,k)$ from ${\sf sign}({\sf
blind}(t,b),k)$ and $b$. The voter uses the blinding operation to hide their
vote from the authority but still get it certified as coming from an
authorized voter (as identified by their signing key $\mathit{sk}_{V}$). The
authority’s signature ${\sf sign}(\cdot,\mathit{sk}_{A})$ percolates through
to the vote when the voter removes the blind, and the voter can then
anonymously send (denoted by $\looparrowright$) this signed vote to the
collector for inclusion into the final tally. This specification is shown
below.

$\displaystyle V\rightarrow A$ $\displaystyle:{\sf sign}({\sf
blind}(\\{v\\}_{r},b),\mathit{sk}_{V})$ $\displaystyle A\rightarrow V$
$\displaystyle:{\sf sign}({\sf blind}(\\{v\\}_{r},b),\mathit{sk}_{A})$
$\displaystyle V\looparrowright C$ $\displaystyle:{\sf
sign}(\\{v\\}_{r},\mathit{sk}_{A})$

One can use assertions to model the voting phase of FOO as below, following
[24] (We use $\\{\alpha\\}^{A}$ to serve as shorthand for $\mathit{pk}_{A}\
\mathit{says}\ \alpha$). In fact, the use of assertions allows one to also
specify an eligibility check for voters via a conditional action ${\sf
assert}$, which allows the protocol to proceed only if the specified assertion
is derivable by the agent in question. Further, using list membership, voters
can also include a certificate that their vote is for an allowable candidate
from the list $\ell$. These are left implicit in the terms-only modelling.

$\displaystyle V\rightarrow A$ $\displaystyle:\\{v\\}_{p},\bigl{\\{}\exists
xr.{{\\{x\\}_{r}}\bowtie{\\{v\\}_{p}}}\wedge
x\twoheadleftarrow\ell\bigr{\\}}^{V}$ $\displaystyle A$ $\displaystyle:{\sf
assert}~{}{\sf el}(V)$ $\displaystyle A\rightarrow V$
$\displaystyle:\bigl{\\{}{\sf el}(V)\wedge\bigl{\\{}\exists
xr.{{\\{x\\}_{r}}\bowtie{\\{v\\}_{p}}}\wedge
x\twoheadleftarrow\ell\bigr{\\}}^{V}\bigr{\\}}^{A}$ $\displaystyle
V\looparrowright C$ $\displaystyle:\\{v\\}_{q},\exists Uys.\bigl{\\{}{\sf
el}(U)\wedge\bigl{\\{}\exists xr.{{\\{x\\}_{r}}\bowtie{\\{y\\}_{s}}}\wedge
x\twoheadleftarrow\ell\bigr{\\}}^{U}\bigr{\\}}^{A}$ $\displaystyle\hskip
14.22636pt\wedge\bigl{\\{}\exists
w.{{\\{y\\}_{w}}\bowtie{\\{v\\}_{q}}}\bigr{\\}}$

$V$ first sends to $A$ their encrypted vote along with an assertion claiming
that it is for a valid candidate from the list $\ell$. The authority checks
the voter’s eligibility via the ${\sf assert}$ action on the ${\sf el}$
predicate. If the check passes, the authority issues a certificate stating
that the voter is allowed to vote, crucially, without modifying the term
containing the vote. $V$ then existentially quantifies out their name from
this certificate, and anonymously sends to $C$ a re-encryption of the vote
authorized by $A$ along with a certificate to that effect. Thus, the intent
behind the various communications is made more transparent than in the model
with blind signatures. One can show that this satisfies anonymity [24].

We can also specify security properties in a more natural manner (as compared
to in the terms-only model). For instance, we say that _vote secrecy_ is
ensured in the above protocol if there is no run where the intruder can derive
$\exists{xy}:[\\{v\\}_{p}=\\{x\\}_{y}\wedge x=v]$. Note that this means that
while anyone can derive the value of $v$, which is public, they should not be
able to identify the value inside the encrypted vote $\\{v\\}_{p}$ as being a
particular public name. To express this in the terms-only formulation, one has
to check whether two runs that only differ in the vote $v$ can be
distinguished by the intruder [13]. It can be seen from [24] that the proving
such properties might involve considering multiple runs simultaneously, but
the specification itself does not refer to a notion of equivalence.

######  Example 6.1.

Consider a protocol where $V$ sends to $A$ the vote encrypted in a fresh key,
and an assertion that the vote belongs to an allowable list $\ell$ of
candidates. This looks as follows. $V\rightarrow A:\\{v\\}_{k},\exists
xr.\bigl{\\{}{{\\{x\\}_{r}}\bowtie{\\{v\\}_{k}}}\wedge
x\twoheadleftarrow\ell\bigr{\\}}$.

Suppose this same protocol is used for two elections that $V$ participates in
simultaneously, where the first election has candidates $0$ and $1$ (so
$\ell_{1}=[0,1]$) and the second has candidates $0$ and $2$ (so
$\ell_{2}=[0,2]$).

$V$ wants to vote for $0$ in both elections. Since the vote is for the same
candidate, $V$ (unwisely) decides to reuse the same term, instead of re-
encrypting in a fresh key. So we have a run where $V$ sends both $\exists
xr.\bigl{\\{}{{\\{x\\}_{r}}\bowtie{\\{v\\}_{k}}}\wedge
x\twoheadleftarrow[0,1]\bigr{\\}}$ and $\exists
ys.\bigl{\\{}{{\\{y\\}_{s}}\bowtie{\\{v\\}_{k}}}\wedge
y\twoheadleftarrow[0,2]\bigr{\\}}$. Now, since the same term $\\{v\\}_{k}$ is
involved in both assertions, an observer ought to be able to deduce that the
vote is actually for $0$.

Let $S$ be the set $\\{\\{v\\}_{k},0,1,2\\}$ and let $A$ consist of the above
two assertions sent out by $V$. $\mathit{ker}(S;A)=(T;E)$ where
$T=\\{\\{v\\}_{k},0,1,2,x,r,y,s\\}$ and
$E=\bigl{\\{}{{\\{x\\}_{r}}\bowtie{\\{v\\}_{k}}},x\twoheadleftarrow[0,1],{{\\{y\\}_{s}}\bowtie{\\{v\\}_{k}}},y\twoheadleftarrow[0,2]\bigr{\\}}$.
We present a proof of $T;E\vdash\exists
zw.\bigl{\\{}{{\\{z\\}_{w}}\bowtie{\\{v\\}_{k}}}\wedge{{z}\bowtie{0}}\bigr{\\}}$
in Figure 4. We omit the LHS as well as some $\vdash_{\mathit{dy}}$ proofs for
readability.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
19.67802pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=39.35605pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\\{x\\}_{r}}\bowtie{\\{v\\}_{k}}}$}}}}\hskip 4.0pt
plus 1.0fil\penalty 2\hskip 4.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.50835pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=33.0167pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
x\twoheadleftarrow[0,1]$}}}}\hskip 4.0pt plus 1.0fil\penalty 2\hskip 4.0pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.32689pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=32.65378pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
y\twoheadleftarrow[0,2]$}}}}\hskip 4.0pt plus 1.0fil\penalty 2\hskip 4.0pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
19.47375pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.94751pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\\{y\\}_{s}}\bowtie{\\{v\\}_{k}}}$}}}}\hskip 4.0pt
plus 1.0fil\penalty 2\hskip 4.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 19.67802pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=39.35605pt\hbox{\kern 2.40002pt${\sf
ax}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\\{x\\}_{r}}\bowtie{\\{v\\}_{k}}}$}}}}\hskip 4.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=74.95338pt\hbox{\kern
2.40002pt${\sf sym}$}}}\hbox{\kern
17.79866pt\hbox{$\displaystyle{{\\{v\\}_{k}}\bowtie{\\{x\\}_{r}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=190.9178pt\hbox{\kern
2.40002pt${\sf trans}$}}}\hbox{\kern
75.9453pt\hbox{$\displaystyle{{\\{y\\}_{s}}\bowtie{\\{x\\}_{r}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=236.13737pt\hbox{\kern
2.40002pt${\sf proj}$}}}\hbox{\kern
108.45572pt\hbox{$\displaystyle{{y}\bowtie{x}}$}}}}\hskip 4.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=345.78584pt\hbox{\kern 2.40002pt${\sf
subst}$}}}\hbox{\kern 156.38457pt\hbox{$\displaystyle
x\twoheadleftarrow[0,2]$}}}}\hskip 4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=456.0861pt\hbox{\kern 2.40002pt${\sf
int}$}}}\hbox{\kern 215.31248pt\hbox{$\displaystyle
x\twoheadleftarrow[0]$}}}}\hskip 4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=479.46118pt\hbox{\kern 2.40002pt${\sf
prom}$}}}\hbox{\kern 230.22226pt\hbox{$\displaystyle{{x}\bowtie{0}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=577.78964pt\hbox{\kern
2.40002pt$\wedge\sf i$}}}\hbox{\kern
257.0418pt\hbox{$\displaystyle{{\\{x\\}_{r}}\bowtie{\\{v\\}_{k}}}\wedge{{x}\bowtie{0}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=601.16472pt\hbox{\kern
2.40002pt$\exists\sf i^{2}$}}}\hbox{\kern
253.96408pt\hbox{$\displaystyle\exists
zw.\bigl{\\{}{{\\{z\\}_{w}}\bowtie{\\{v\\}_{k}}}\wedge{{z}\bowtie{0}}\bigr{\\}}$}}}}$

Figure 4: Proof for Example 6.1. $\exists\sf i^{2}$ indicates two applications
of $\exists\sf i$.

###  6.2 Adapting the results of Section 3 and Section 5

We can extend the definition of $\mathbb{P}(\alpha)$ in a straightforward
manner. The definition of $\mathbb{A}(S,\alpha)$ is given as follows.

  * •

$\mathbb{A}(S,{{t_{0}}\bowtie{t_{1}}})=\\{i\cdot p\mid i\in\\{0,1\\},\
p\in\mathbb{A}(S,t_{i})\\}$

  * •

$\mathbb{A}(S,P(u_{1},\ldots,u_{m}))=\\{i\mid 1\leqslant i\leqslant
m,S\vdash_{\mathit{dy}}u_{i}\\}$

  * •

$\mathbb{A}(S,t\twoheadleftarrow[t_{1},\ldots,t_{n}])=\\{0\\}$

  * •

$\mathbb{A}(S,\alpha_{0}\wedge\alpha_{1})=\\{i\cdot p\mid i\in\\{0,1\\},\
p\in\mathbb{A}(S,\alpha_{i})\\}$

  * •

$\mathbb{A}(S,\exists{x}.\alpha)=\\{0\cdot p\mid
p\in\mathbb{A}(S\cup\\{x\\},\alpha)\\}$

  * •

$\mathbb{A}(S,\mathit{pk}_{a}\ \mathit{says}\ \alpha)=\\{0\\}\cup\\{1\cdot
p\mid p\in\mathbb{A}(S,\alpha)\\}$

We now use $\vdash_{\mathit{eq}}$ to mean all the rules in Tables 2 and 3,
except $\wedge\sf i,\wedge\sf e,\exists\sf i,$ and $\exists\sf e$.

${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash t\twoheadleftarrow[n]$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=54.93964pt\hbox{\kern 2.70003pt${\sf prom}$}}}\hbox{\kern 4.87502pt\hbox{$\displaystyle S;A\vdash{{t}\bowtie{n}}$}}}}}$ | ${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 15.98415pt\hbox{$\displaystyle\penalty 1S;A\vdash{{t}\bowtie{n_{i}}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=78.89426pt\hbox{\kern 2.70003pt${\sf wk}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle S;A\vdash t\twoheadleftarrow[n_{1},\ldots,n_{k}]$}}}}}$
---|---
${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash t\twoheadleftarrow
l_{1}\quad\cdots\quad S;A\vdash t\twoheadleftarrow l_{m}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=126.49527pt\hbox{\kern 2.70003pt${\sf
int}$}}}\hbox{\kern 20.76877pt\hbox{$\displaystyle S;A\vdash
t\twoheadleftarrow(l_{1}\cap\ldots\cap l_{m})$}}}}}$
${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash t\twoheadleftarrow\ell\quad S;A\vdash{{t}\bowtie{u}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=102.22717pt\hbox{\kern 2.70003pt${\sf subst}$}}}\hbox{\kern 26.01877pt\hbox{$\displaystyle S;A\vdash u\twoheadleftarrow\ell$}}}}}$ | ${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash\alpha\quad S\vdash_{\mathit{dy}}\mathit{sk}_{a}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=72.50644pt\hbox{\kern 2.70003pt${\sf say}$}}}\hbox{\kern 2.22374pt\hbox{$\displaystyle S;A\vdash\mathit{pk}_{a}\ \mathit{says}\ \alpha$}}}}}$
${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash\alpha_{0}\quad S;A\vdash\alpha_{1}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=80.12965pt\hbox{\kern 2.70003pt$\wedge\sf i$}}}\hbox{\kern 14.14375pt\hbox{$\displaystyle S;A\vdash\alpha_{0}\wedge\alpha_{1}$}}}}}$ | ${{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1S;A\vdash\alpha_{0}\wedge\alpha_{1}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=51.84215pt\hbox{\kern 2.70003pt$\wedge\sf e_{i}$}}}\hbox{\kern 8.53049pt\hbox{$\displaystyle S;A\vdash\alpha_{i}$}}}}}$
Table 3:  Extra rules for $\wedge$, says and lists. For the ${\sf say}$ rule,
$(\mathit{pk}_{a},\mathit{sk}_{a})$ is the public-private key pair of
$a\in\mathscr{A}$.

The notion of kernel and the conditions in Theorem 3.8 also change. Earlier,
an assertion had the form $\exists{x_{1}\dots x_{k}}.{{t}\bowtie{u}}$, and we
reduced all reasoning to assertions of the form ${{t}\bowtie{u}}$, which were
maximal subformulas without a logical connective for the outermost operator.
We can think of those as the “atoms” of a formula, and we use this idea to
adapt the definition of $\mathit{ker}$. $(T;E)=\mathit{ker}(S;A)$ iff:

  * •

$T=S\cup{\sf bv}(A)$

  * •

$A=\\{\alpha\in{\sf sf}(A)\mid\alpha$ is of the form ${{t}\bowtie{u}}$ or
$t\twoheadleftarrow{l}$ or $\mathit{pk}(k)\ \mathit{says}\ \beta$ or
$P(u_{1},\ldots,u_{m})\\}$.

For Theorem 3.8, one would expect that deriving $\alpha$ reduces to deriving
substitution instances of all atoms of $\alpha$. But consider subformulas of
the form $\mathit{pk}_{a}\ \mathit{says}\ \beta$. We can derive those in two
ways – either by using ${\sf ax}$ (if the formula is already in the LHS) or by
using the ${\sf say}$ rule on $\beta$ and $\mathit{sk}_{a}$. In the latter
case, one would look to derive the atoms of $\beta$. We thus formalize the
atoms of a formula as below.

${\sf at}(\gamma)=\begin{cases}{\sf at}(\alpha)\cup{\sf at}(\beta)&\text{if
$\gamma=\alpha\wedge\beta$}\\\ {\sf at}(\alpha)&\text{if
$\gamma=\exists{x}.\alpha$}\\\ \left\\{\mathit{pk}(k)\ \mathit{says}\
\alpha\right\\}\cup{\sf at}(\alpha)&\text{if $\gamma=\mathit{pk}(k)\
\mathit{says}\ \alpha$}\\\ \\{\gamma\\}&\text{otherwise}\end{cases}$

Theorem 3.8 is modified as follows.

######  Theorem 6.2.

For a formula $\alpha$ s.t. ${\sf bv}(\alpha)\cap{\sf vars}(S;A)=\varnothing$,
and $(T;E)=\mathit{ker}(S;A)$, $(S;A)\vdash_{\mathit{a}}\alpha$ iff there is a
$\mu$ with ${\sf dom}(\mu)={\sf bv}(\alpha)$ and $X\subseteq{\sf at}(\alpha)$
s.t.:

  1. [1]

$\forall{}x\in{\sf bv}(\alpha):T\vdash_{\mathit{dy}}\mu(x)$.

  2. [2]

$\forall{}x\in{\sf bv}(\alpha),t\in{\sf st}(\alpha)$:
$\mathbb{P}_{x}({t})\subseteq\mathbb{A}(T\cup{\sf bv}(\alpha),t)$.

  3. [3]

For all $\beta\in X$, $(T;E)\vdash_{\mathit{eq}}\mu(\beta)$.

  4. [4]

$(T;\mu(X))\vdash_{\mathit{a}}\alpha$ via a proof with only introduction
rules.

We can extend the normalization and subterm properties appropriately (details
provided in Appendix E).

Very few changes are required to adapt the results of Section 5 to this new
system to show that insecurity for this extended system continues to be in NP.
In fact, one can obtain bounded substitutions for the passive and active
intruder problems exactly as for equality assertions. Only atomic terms occur
in assertions of the form $P(\cdots)$ and $t\twoheadleftarrow{l}$, thus no
variable standing for a term occurring in these assertions is zappable.
Similarly, for assertions of the form $\mathit{pk}_{a}\ \mathit{says}\
\alpha$, $\mathit{pk}_{a}$ is not zappable. However, there might be terms
inside $\alpha$ which are zappable, but these will be at the level of equality
subformulas of $\alpha$, and the says connective itself does not influence the
zapping procedure in any way.

So the extended syntax interferes very little with our proof strategy for
finding bounded substitutions. Thus, we have a practical language that can be
used to model protocols and properties, and which also enjoys nice
decidability properties.

A final note on atomic predicates of the form $P(\cdots)$: There are no rules
governing these, other than ${\sf ax}$. We can assume that depending on the
context, ground assertions of this kind are added and removed from agents’
knowledge states. For example, in a voting protocol, one can add to the
authority’s initial state all predicates of the form ${\sf el}(V)$ for
eligible voters $V$. As and when the authority receives a message from $V$ and
checks that ${\sf el}(V)$ is true, it removes ${\sf el}(V)$ from its knowledge
state, recording the fact that $V$ has voted and is no longer eligible. Our
decidability proofs are not affected by these modifications.

##  7 Future Work

An interesting feature of the language in [24] is the use of disjunction.
While our extended syntax uses list membership to express a limited form of
disjunction that seems to suffice for many protocols, it would be worthwhile
to explore the utility of full disjunction and its effect on the active
intruder problem.

In fact, with disjunction, we know that even the derivability problem becomes
more involved. To check if $(S;A)\vdash_{\mathit{a}}\gamma$, one can no longer
work with a single kernel of $(S;A)$. We can define a notion of “down-
closure”. For each disjunctive formula $\alpha\vee\beta$, one obtains two
down-closures – one containing $\alpha$, and the other $\beta$. In general,
many disjunctions could occur in $A$ and there are exponentially many down-
closures for any $(S;A)$. Using the standard left disjunction property
($\alpha\vee\beta$ derives $\gamma$ iff $\gamma$ is derivable from $\alpha$
and from $\beta$), we check if the kernels of all down-closures of $(S;A)$
derive $\gamma$. Thus the derivability problem is in $\Pi_{2}$. Some of these
down-closures need not even be consistent, and hence our solution for the
insecurity problem is not directly adaptable to full disjunction. Exploring
these issues is an interesting direction of research and is left for future
work.

It is also useful to add communicable assertions to the widely-used applied pi
calculus [1]. It would be especially interesting to see how this impacts the
notion of static equivalence, and then study expressibility and decidability.
These would also help us to extend tools like Proverif [7] with assertions.

As mentioned earlier, one can express certain “equivalence” properties in a
more natural manner with assertions as compared to the terms-only model. It is
another promising extension to study which equivalence properties can be
expressed as reachability properties in this manner, like the work in [18].

## References

  * [1] Martín Abadi, Bruno Blanchet, and Cédric Fournet.  The applied pi calculus: Mobile values, new names, and secure communication.  Journal of the ACM, 65(1):1:1–1:41, Oct 2017.
  * [2] Martín Abadi and Véronique Cortier.  Deciding knowledge in security protocols under equational theories.  Theor. Comput. Sci., 367:2–32, 2004.
  * [3] Roberto M. Amadio, Denis Lugiez, and Vincent Vanackère.  On the symbolic reduction of processes with cryptographic functions.  Theoretical Computer Science, 290(1):695–740, 2003.
  * [4] Michael Backes, Matteo Maffei, and Dominique Unruh.  Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol.  In IEEE Symposium on Security and Privacy, pages 202–215, 2008\.
  * [5] A. Baskar, R. Ramanujam, and S.P. Suresh.  A dexptime-complete Dolev-Yao theory with distributive encryption.  In Proceedings of MFCS 2010, volume 6281 of Lecture Notes in Computer Science, pages 102–113, August 2010.
  * [6] Bruno Blanchet.  An Efficient Cryptographic Protocol Verifier Based on Prolog Rules.  In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82–96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.
  * [7] Bruno Blanchet.  Modeling and verifying security protocols with the applied pi calculus and proverif.  Foundations and Trends in Privacy and Security, 1:1–135, 10 2016\.
  * [8] Bruno Blanchet and Andreas Podelski.  Verification of Cryptographic Protocols: Tagging Enforces Termination.  In Andrew D. Gordon, editor, Proceedings of FoSSaCS’03, volume 2620 of Lecture Notes in Computer Science, pages 136–152, 2003.
  * [9] Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, and Mathieu Turuani.  An NP decision procedure for protocol insecurity with XOR.  Theoretical Computer Science, 338(1–3):247–274, 2005.
  * [10] Hubert Comon-Lundh and Vitaly Shmatikov.  Intruder Deductions, Constraint Solving and Insecurity Decisions in Presence of Exclusive or.  In Proceedings of the 18th IEEE Synposium on Logic in Computer Science (LICS), pages 271–280, June 2003.
  * [11] Véronique Cortier, Stéphanie Delaune, and Pascal Lafourcade.  A survey of algebraic properties used in cryptographic protocols.  Journal of Computer Security, 14(1):1–43, 2006.
  * [12] Véronique Cortier, Stéphanie Delaune, and Vaishnavi Sundararajan.  A decidable class of security protocols for both reachability and equivalence properties.  Journal of Automated Reasoning, 65(4):479–520, 2021.
  * [13] Véronique Cortier and Steve Kremer.  Formal models and techniques for analyzing security protocols: A tutorial.  Found. Trends Program. Lang., 1(3):151–267, 2014.
  * [14] C.J.F. Cremers.  The Scyther Tool: Verification, falsification, and analysis of security protocols.  In Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, USA, Proc., volume 5123/2008 of Lecture Notes in Computer Science, pages 414–418. Springer, 2008.
  * [15] Danny Dolev and Andrew Yao.  On the Security of public-key protocols.  IEEE Transactions on Information Theory, 29:198–208, 1983.
  * [16] Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov.  Multiset rewriting and the complexity of bounded security protocols.  Journal of Computer Security, 12:247–311, 02 2004.
  * [17] Atsushi Fujioka, Tatsuaki Okamoto, and Kaazuo Ohta.  A practical secret voting scheme for large scale elections.  In ASIACRYPT, pages 244–251, 1992.
  * [18] Sébastien Gondron, Sebastian Mödersheim, and Luca Viganò.  Privacy as reachability.  In 2022 IEEE 35th Computer Security Foundations Symposium (CSF), pages 130–146, 2022.
  * [19] Nevin Heintze and Doug Tygar.  A model for secure protocols and their composition.  IEEE Transactions on Software Engineering, 22:16–30, 1996.
  * [20] Steve Kremer and Mark Ryan.  Analysis of an Electronic Voting Protocol in the Applied Pi Calculus.  In Proceedings of the European Symposium on Programming, volume 3444 of Lecture Notes in Computer Science, pages 186–200. Springer, 2005\.
  * [21] Pascal Lafourcade, Denis Lugiez, and Ralf Treinen.  Intruder deduction for the equational theory of abelian groups with distributive encryption.  Information and Computation, 205(4):581–623, April 2007.
  * [22] Matteo Maffei, Kim Pecina, and Mathieu Reinert.  Security and provacy by declarative design.  In 2003 IEEE 26th Computer Security Foundations Symposium, pages 81–96, 2003.
  * [23] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin.  The TAMARIN prover for the symbolic analysis of security protocols.  In Computer Aided Verification, pages 696–701. Springer Berlin Heidelberg, 2013.
  * [24] R. Ramanujam, Vaishnavi Sundararajan, and S. P. Suresh.  Existential assertions for voting protocols.  In Financial Cryptography and Data Security - FC 2017, volume 10323 of Lecture Notes in Computer Science, pages 337–352, 2017.
  * [25] R. Ramanujam and S. P. Suresh.  Decidability of context-explicit security protocols.  Journal of Computer Security, 13(1):135–165, 2005.
  * [26] R. Ramanujam and S. P. Suresh.  A (restricted) quantifier elimination for security protocols.  Theoretical Computer Science, 367:228–256, 2006.
  * [27] Michaël Rusinowitch and Mathieu Turuani.  Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete.  Theoretical Computer Science, 299:451–475, 2003.

##  Appendix A Proofs for Sections 2 and 3

See 2.7

  * Proof.

For any term $a$ and any set $Q\subseteq\mathbb{P}(a)$, we let ${a}|_{Q}$
denote $\\{{a}|_{q}\mid q\in Q\\}$. We now observe some general properties of
abstractability.

For any $T,a$ and $q\in\mathbb{A}(T,a)$ s.t. ${a}|_{q}$ is non-atomic, either
$\\{q0,q1\\}\subseteq\mathbb{A}(T,a)$ and
${a}|_{\\{q0,q1\\}}\vdash_{\mathit{dy}}{a}|_{q}$ via a constructor rule, or
$q$ is a maximal position in $\mathbb{A}(T,a)$ (it is not the prefix of any
other position in the set). We have the following two properties.

    1. 1.

Let $M=\\{q\in\mathbb{P}(a)\mid q$ is a maximal position in
$\mathbb{A}(T,a)\\}$. Then for every $p\in\mathbb{A}(T,a)$,
${a}|_{M}\vdash_{\mathit{dy}}{a}|_{p}$ via a proof consisting only of
constructor rules.

    2. 2.

Suppose $Q\subseteq\mathbb{P}(a)$ is prefix-closed (if $q\in Q$ and $p$ is a
prefix of $q$, then $p\in Q$) and sibling-closed (if $qi\in Q$ and
$qj\in\mathbb{P}(a)$, then $qj\in Q$). If $T\vdash_{\mathit{dy}}{a}|_{q}$ for
every maximal $q\in Q$, then $Q\subseteq\mathbb{A}(T,a)$.

We now prove the statement of the lemma. Let $u={t}[{r}]_{P}$, and let $A$ and
$B$ denote $\mathbb{A}(S\cup\\{x\\},t)$ and $\mathbb{A}(S,u)\cap\mathbb{P}(t)$
respectively. Note that $A$ and $B$ are both prefix-closed and sibling-closed.
Let $M$ (resp. $N$) be the set of maximal positions in $A$ (resp. $B$).

Since $P\subseteq A$ is the set of $x$-positions in $t$, $P\subseteq M$ and no
$q\in M$ is a prefix of a position in $P$. Thus, for every $q\in M$, either
${t}|_{q}=x$, or $x\notin{\sf vars}({t}|_{q})$. If ${t}|_{q}=x$, ${u}|_{q}=r$,
and $S\vdash_{\mathit{dy}}{u}|_{q}$ (since $S\vdash_{\mathit{dy}}r$). If
$x\notin{\sf vars}({t}|_{q})$, then ${u}|_{q}={t}|_{q}$ and
$S\vdash_{\mathit{dy}}{u}|_{q}$. This is because
$q\in\mathbb{A}(S\cup\\{x\\},t)$, so
$S\cup\\{x\\}\vdash_{\mathit{dy}}{t}|_{q}$, but $x$ does not occur in the
conclusion. Thus we have $S\vdash_{\mathit{dy}}{u}|_{q}$ for every $q\in M$.
Since $A$ is prefix-closed and sibling-closed, by 2, we get
$A\subseteq\mathbb{A}(S,u)$. Since $A\subseteq\mathbb{P}(t)$ as well, we get
$A\subseteq B$.

By similar reasoning as above, we can see that
$S\cup\\{x\\}\vdash_{\mathit{dy}}{t}|_{q}$ for each $q\in N$. (For some of
these positions $q$, $x$ does not occur at all in the subterm at that
position, and ${t}|_{q}={u}|_{q}$ is derivable from $S$. For other positions
$q$, ${t}|_{q}=x$ and is derivable from $S\cup\\{x\\}$.) Therefore $B\subseteq
A$. ∎

######  Lemma A.1.

The ${\sf subst}$ rule is admissible in $\vdash_{\mathit{a}}$.

  * Proof.

We first show that ${\sf subst}$ can be simulated by a series of applications
of ${\sf subst}_{1}$, defined below.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1S;A\vdash{({{t}\bowtie{u}})}[{r}]_{p}\quad S;A\vdash{{r}\bowtie{s}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=125.39137pt\hbox{\kern 3.00003pt${\sf
subst}_{1}$}}}\hbox{\kern 30.08786pt\hbox{$\displaystyle
S;A\vdash{({{t}\bowtie{u}})}[{s}]_{p}$}}}}$

The rule is enabled only if
$p\in\mathbb{P}_{x}({{{t}\bowtie{u}}})\cap\mathbb{A}(S\cup\\{x\\},{{t}\bowtie{u}})$
and $S\vdash_{\mathit{dy}}\\{r,s\\}$. ${\sf subst}_{1}$ replaces the $r$
occurring at $p$ by $s$.

Let $\alpha$ denote ${{t}\bowtie{u}}$ and suppose we have an instance of ${\sf
subst}$ with $(T;E)\vdash{\alpha}[{r}]_{P}$ and $(T;E)\vdash{{r}\bowtie{s}}$
as premises and $(T;E)\vdash{\alpha}[{s}]_{P}$ as conclusion, with
$P=\\{p_{1},\ldots,p_{\ell}\\}\subseteq\mathbb{P}_{x}({\alpha})\cap\mathbb{A}(T\cup\\{x\\},\alpha)$,
and $T\vdash_{\mathit{dy}}\\{r,s\\}$. The $p_{i}$s are $x$-positions, so none
of them is a prefix of another. Therefore, even after replacing the $x$s
occurring in the set of positions $P\setminus\\{p_{i}\\}$ with some terms,
$p_{i}$ remains an $x$-position.

For $0\leqslant i\leqslant\ell$, we define the following.
$P_{i}\coloneqq\\{p_{1},\ldots,p_{i}\\}$ and $Q_{i}\coloneqq P\setminus
P_{i}=\\{p_{i+1},\ldots,p_{\ell}\\}$ and
$\alpha_{i}\coloneqq{({\alpha}[{r}]_{Q_{i}})}[{s}]_{P_{i}}$. Note that
$\alpha_{0}={\alpha}[{r}]_{P}$ and $\alpha_{\ell}={\alpha}[{s}]_{P}$. We see
that $p_{i}$ is an $x$-position of
$\beta_{i}={({\alpha}[{r}]_{Q_{i}})}[{s}]_{P_{i-1}}$. By the equivalent of
Lemma 2.7 for assertions, $p_{i}\in\mathbb{A}(T\cup\\{x\\},\beta_{i})$, since
$P\subseteq\mathbb{A}(T\cup\\{x\\},\alpha)$, We also see that
$\alpha_{i-1}={\beta_{i}}[{r}]_{p_{i}}$ and
$\alpha_{i}={\beta_{i}}[{s}]_{p_{i}}$. Thus we can get from $\alpha_{i-1}$ to
$\alpha_{i}$ using the ${\sf subst}_{1}$ rule, and from $\alpha_{0}$ to
$\alpha_{\ell}$ using a series of ${\sf subst}_{1}$ rules.

Now we show that ${\sf subst}_{1}$ can be simulated in the
$\vdash_{\mathit{eq}}$ system. Suppose $\pi$ is a proof of
$(T;E)\vdash_{\mathit{eq}}{{r}\bowtie{s}}$, and let
$T\vdash_{\mathit{dy}}\\{r,s\\}$. For all $p$, and for all $t,u$ s.t.
$p\in\mathbb{P}_{x}({{{t}\bowtie{u}}})\cap\mathbb{A}(T\cup\\{x\\},{{t}\bowtie{u}})$,
we show that if $(T;E)\vdash_{\mathit{eq}}{({{t}\bowtie{u}})}[{r}]_{p}$, then
$(T;E)\vdash_{\mathit{eq}}{({{t}\bowtie{u}})}[{s}]_{p}$. The proof proceeds by
induction on the length of $p$.

    * –

$p=0$: We have a proof of ${{r}\bowtie{u}}$. By ${\sf sym}$, we get a proof of
${{u}\bowtie{r}}$. Combining this with $\pi$ using ${\sf trans}$, we get a
proof of ${{u}\bowtie{s}}$, from which we can get a proof of ${{s}\bowtie{u}}$
by applying ${\sf sym}$ again.

    * –

$p=1$: We have a proof of ${{t}\bowtie{r}}$. Combining this with $\pi$ using
${\sf trans}$, we get a proof of ${{t}\bowtie{s}}$, as desired.

    * –

$p=0q$ for some $q\neq\varepsilon$: Note that ${({{t}\bowtie{u}})}[{r}]_{p}$
is the same as ${{{t}[{r}]_{q}}\bowtie{u}}$. Suppose $q=1q^{\prime}$, w.l.o.g.
Then, $t={\sf f}(t_{0},t_{1})$ and ${t}[{r}]_{q}={\sf
f}(t_{0},{t_{1}}[{r}]_{q^{\prime}})$. Since $q\in\mathbb{A}(T\cup\\{x\\},t)$,
we have that $T\vdash_{\mathit{dy}}\\{t_{0},t_{1}\\}$, and by ${\sf eq}$,
$(T;E)\vdash_{\mathit{eq}}{{t_{j}}\bowtie{t_{j}}}$ for $j\in\\{0,1\\}$. From
$T\vdash_{\mathit{dy}}r$, and $q^{\prime}\in\mathbb{A}(T\cup\\{x\\},t_{1})$,
we have that $T\vdash_{\mathit{dy}}{t_{1}}[{r}]_{q^{\prime}}$. Thus, we have a
proof of
$(T;E)\vdash_{\mathit{eq}}{{{t_{1}}[{r}]_{q^{\prime}}}\bowtie{{t_{1}}[{r}]_{q^{\prime}}}}$
using ${\sf eq}$. Applying IH to the position $0q^{\prime}$, we have
$(T;E)\vdash_{\mathit{eq}}{{{t_{1}}[{s}]_{q^{\prime}}}\bowtie{{t_{1}}[{r}]_{q^{\prime}}}}$.
By applying ${\sf cons}$ to this and
$(T;E)\vdash_{\mathit{eq}}{{t_{0}}\bowtie{t_{0}}}$, we get
$(T;E)\vdash_{\mathit{eq}}{{{t}[{s}]_{q}}\bowtie{{t}[{r}]_{q}}}$. Applying
${\sf trans}$ to this and ${{{t}[{r}]_{q}}\bowtie{u}}$, we get a proof of
${{{t}[{s}]_{q}}\bowtie{u}}$, i.e. ${({{t}\bowtie{u}})}[{s}]_{p}$.

    * –

$p=1q$ for some $q\neq\varepsilon$: This is similar to the above. ∎

See 3.3

  * Proof.

For the left to right direction, let $\pi$ be a proof of
$S;A,\exists{x}.\alpha\vdash\gamma$. Note that we have a proof $\pi_{1}$ of
$\exists{x}.\alpha$ from $(S,x;A,\alpha)$, where the $\exists\sf i$ rule is
justified because the abstractability side condition
$\mathbb{P}_{x}({\alpha})\subseteq\mathbb{A}(S\cup\\{x\\},\alpha)$ is assumed.
We can then use the ${\sf cut}$ rule (which is admissible in
$\vdash_{\mathit{a}}$) on this proof along with the proof $\pi$ to get
$(S,x;A,\alpha)\vdash_{\mathit{a}}\gamma$.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
28.58092pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.16183pt\hbox{\kern 3.00003pt${\sf
ax}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
S,x;A,\alpha\vdash\alpha$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=101.65848pt\hbox{\kern
3.00003pt$\exists\sf i$}}}\hbox{\kern 14.39069pt\hbox{$\displaystyle
S,x;A,\alpha\vdash\exists{x}.\alpha$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\hskip 5.0pt plus 1.0fil{\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.1765pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 29.63774pt$\vbox to16.14578pt{\leaders\vbox
to5.38193pt{\vss\hbox{$\cdot$}\vss}\vfill}$\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle S;A,\exists{x}.\alpha\vdash\gamma$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=217.93056pt\hbox{\kern
3.00003pt${\sf cut}$}}}\hbox{\kern 80.9942pt\hbox{$\displaystyle
S,x;A,\alpha\vdash\gamma$}}}}$

For the other direction, let $\pi$ be a proof of $S,x;A,\alpha\vdash\gamma$.
We obtain a proof of $S;A,\exists{x}.\alpha\vdash\gamma$ as follows.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
39.49411pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=78.98822pt\hbox{\kern 3.00003pt${\sf
ax}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
S;A,\exists{x}.\alpha\vdash\exists{x}.\alpha$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 25.12094pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 26.58218pt$\vbox
to16.14578pt{\leaders\vbox
to5.38193pt{\vss\hbox{$\cdot$}\vss}\vfill}$\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle S,x;A,\alpha\vdash\gamma$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=189.427pt\hbox{\kern
3.00003pt$\exists\sf e$}}}\hbox{\kern 63.68687pt\hbox{$\displaystyle
S;A,\exists{x}.\alpha\vdash\gamma$}}}}$

∎

See 3.6

  * Proof.

Suppose $(T;E)=\mathit{ker}(S;A)$, for sanitized $(S;A)$. So ${\sf
fv}(S;A)\cap\mathscr{V}_{q}=\varnothing$, ${\sf pubs}(\beta)\in S$ for all
$\beta\in A$, and $T=S\cup{\sf bv}(A)$ and
$E=\\{{{t}\bowtie{u}}\mid\exists{\vec{x}}.{{t}\bowtie{u}}\in A\\}$. Thus ${\sf
pubs}(\gamma)\in T$ for every $\gamma\in E$, and ${\sf
vars}(E)\cap\mathscr{V}_{q}\subseteq T$.

Let $\pi$ be a proof of $(T;E)\vdash_{\mathit{a}}\alpha$. Note that $\pi$ has
no occurrence of $\exists\sf e$. We assume that all premises of ${\sf eq}$ are
normal $\vdash_{\mathit{dy}}$ proofs ending in a destructor (by repeatedly
turning all $\text{constructor}+{\sf eq}$ patterns into ${\sf eq}+{\sf
cons}$). We show by induction that $T\vdash_{\mathit{dy}}{\sf pubs}(\alpha)$.
Let ${\sf r}$ denote the last rule of $\pi$.

    * –

${\sf r}={\sf ax}$: $\alpha\in E$. So $T\vdash_{\mathit{dy}}{\sf
pubs}(\alpha)$, by purity.

    * –

${\sf r}={\sf eq}$: $\alpha$ is ${{t}\bowtie{t}}$ with
$T\vdash_{\mathit{dy}}t$ via a proof ending in destructor. Since any term in
$T$ is either in $\mathscr{V}_{q}$ or contains no variables from
$\mathscr{V}_{q}$, and since $t\in{\sf st}(T)$, we see that ${\sf
pubs}(\alpha)$ is $\\{t\\}$ or $\varnothing$, and $T\vdash_{\mathit{dy}}{\sf
pubs}(\alpha)$ in both cases.

    * –

${\sf r}\in\\{{\sf sym},{\sf trans}\\}$: Any $t\in{\sf pubs}(\alpha)$ is in
${\sf pubs}(\beta)$ for one of the premises $\beta$, and the result follows.

    * –

${\sf r}={\sf cons}$: $\alpha$ is of the form ${{t}\bowtie{u}}$, where $t={\sf
f}(t_{0},t_{1})$ and $u={\sf f}(u_{0},u_{1})$, and the immediate subproofs of
$\pi$ derive ${{t_{0}}\bowtie{u_{0}}}$ and ${{t_{1}}\bowtie{u_{1}}}$. Now, any
term in ${\sf pubs}(\alpha)$ is a public term of one of the premises (and we
can apply IH), unless it is $t$ or $u$. Say it is $t$. Then, $t$ is a maximal
subterm of $\alpha$ which avoid $\mathscr{V}_{q}$, and thus it must be that
$t_{0}$ and $t_{1}$ are also public terms of the premises. Thus
$T\vdash_{\mathit{dy}}\\{t_{0},t_{1}\\}$ by IH, and hence
$T\vdash_{\mathit{dy}}t$. Similarly for $u$.

    * –

${\sf r}={\sf proj}$: $\alpha$ is ${{t}\bowtie{u}}$, and any public term of
$\alpha$ is a public term of the premise (and we can apply IH), unless it is
$t$ or $u$. But by abstractability, $T\vdash_{\mathit{dy}}\\{t,u\\}$, and we
are done.

    * –

${\sf r}=\exists\sf i$: $\alpha$ is of the form $\exists{x}.\beta$, with
premise $\gamma={\beta}[{r}]_{P}$, where $P=\mathbb{P}_{x}({\beta})$. We also
have, by the other requirements for the rule, $T\vdash_{\mathit{dy}}r$ and
$P\subseteq\mathbb{A}(T\cup\\{x\\},\beta)$. By Lemma 2.7,
$P\subseteq\mathbb{A}(T,\gamma)$. Consider any $a={\alpha}|_{q}\in{\sf
pubs}(\alpha)$. If $a\in{\sf pubs}(\gamma)$, then we can apply IH. Otherwise,
$q$ has to be a sibling of some position in $p\in P$. In other words, $a$ is
public in $\alpha$ because its sibling is $x$, but in $\gamma$, the $x$ is
replaced by $r$ (and ${\sf vars}(r)\cap\mathscr{V}_{q}=\varnothing$), so $a$
is no longer a _maximal_ subterm avoiding $\mathscr{V}_{q}$. Since the set of
abstractable positions is sibling-closed, $q\in\mathbb{A}(T,\alpha)$, and
since subterms at abstractable positions are derivable,
$T\vdash_{\mathit{dy}}a$.

Now consider an $\vdash_{\mathit{eq}}$ proof of $(T;E)\vdash{{t}\bowtie{u}}$.
It has been shown above that $T\vdash_{\mathit{dy}}{\sf
pubs}({{t}\bowtie{u}})$. Consider $t$. Either $t\in{\sf
pubs}({{t}\bowtie{u}})$, in which case we are done. Otherwise, every maximal
subterm of $t$ which avoids $\mathscr{V}_{q}$ is derivable from $T$, and every
$x\in{\sf vars}(t)\cap\mathscr{V}_{q}$ is in $T$. From these, we can “build
up” $t$ using constructor rules only, thereby proving that
$T\vdash_{\mathit{dy}}t$. Similarly we can show that $T\vdash_{\mathit{dy}}u$.
∎

See 3.8

  * Proof.

a [$1\Rightarrow 2$:] Suppose $(S;A)\vdash_{\mathit{a}}\alpha$. Then
$(T;E)\vdash_{\mathit{a}}\alpha$ via a proof which has no occurrence of the
$\exists\sf e$ rule. Let $\pi$ be a normal proof of $(T;E)\vdash\alpha$. Since
$E$ only has equalities, $\pi$ ends with a series of applications of
$\exists\sf i$. For each $i\leqslant k$, define $\mu(x_{i})\coloneqq w_{i}$,
where $w_{i}$ is the witness used by the $\exists\sf i$ rule introducing
$\exists{x_{i}}$ in $\alpha$. The side condition for $\exists\sf i$ guarantees
that $T\vdash_{\mathit{dy}}\mu(x)$ for each $x\in dom(\mu)$, thus satisfying
condition [1] of the theorem. It is easy to see that ${\sf dom}(\mu)\cap{\sf
vars}({\sf rng}(\mu))=\varnothing$, since each $\mu(x)$ is derivable from $T$,
which has no occurrence of any $y\in{\sf dom}(\mu)$.

There is a maximal subproof $\pi^{\prime}$ of $\pi$ with no occurrence of
$\exists\sf i$. The conclusion of this is ${{t}\bowtie{u}}$, but with $w_{i}$
replacing $x_{i}$ for every $i\leqslant k$. In other words, ${\sf
conc}(\pi^{\prime})$ is $\mu({{t}\bowtie{u}})$. So [3] is also satisfied.

We now prove [2]. It suffices to consider $k=3$ to convey the essential idea.
For $i\leqslant 3$, let $\alpha_{i}$ be the formula
$\exists{x_{i+1}\ldots{}x_{3}}.({{t}\bowtie{u}})$. Note that
$\mu(\alpha_{0})=\alpha_{0}=\alpha$ and $\alpha_{3}={{t}\bowtie{u}}$. The
proof $\pi$ can be viewed as successively proving
$\mu(\alpha_{3}),\mu(\alpha_{2}),\mu(\alpha_{1})$ and $\mu(\alpha_{0})$.

We now assume that $\mathbb{P}_{x_{3}}({t})\subseteq\mathbb{A}(T\cup{\sf
dom}(\mu),t)$, and show the same for $x_{2}$. Letting
$\mu^{\prime}={\mu\upharpoonright\\{x_{1}\\}}$, we see that
$\mu(\alpha_{2})={(\mu^{\prime}(\alpha_{3}))}[{w_{2}}]_{P}$, where
$P=\mathbb{P}_{x_{2}}({\mu^{\prime}(\alpha_{3})})$. The side condition for
$\exists\sf i$ obtaining $\mu(\alpha_{1})$ from
${(\mu^{\prime}(\alpha_{3}))}[{w_{2}}]_{P}$ says that
$\mathbb{P}_{x_{2}}({\mu^{\prime}(\alpha_{3})})\subseteq\mathbb{A}(T\cup\\{x_{2}\\},\mu^{\prime}(\alpha_{3}))$.
We see that $p\in\mathbb{P}_{x_{2}}({\mu^{\prime}(t)})$ iff
$00p\in\mathbb{P}_{x_{2}}({\mu^{\prime}(\alpha_{3})})$, and
$p\in\mathbb{A}(T\cup\\{x_{2},x_{3}\\},\mu^{\prime}(t))$ iff
$00p\in\mathbb{A}(T\cup\\{x_{2}\\},\mu^{\prime}(\alpha_{3}))$. So the side
condition is equivalent to
$\mathbb{P}_{x_{2}}({\mu^{\prime}(t)})\subseteq\mathbb{A}(T\cup\\{x_{2},x_{3}\\},\mu^{\prime}(t))$.

Since $x_{2}\notin{\sf vars}({\sf rng}(\mu^{\prime}))$,
$\mathbb{P}_{x_{2}}({\mu^{\prime}(t)})=\mathbb{P}_{x_{2}}({t})$. Further,
$T\vdash_{\mathit{dy}}\mu^{\prime}(x_{1})$, so by Lemma 2.7,
$\mathbb{A}(T\cup\\{x_{2},x_{3}\\},\mu^{\prime}(t))=\mathbb{A}(T\cup\\{x_{1},x_{2},x_{3}\\},t)$.
Thus we see that $\mathbb{P}_{x_{2}}({t})\subseteq\mathbb{A}(T\cup{\sf
dom}(\mu),t)$. We can similarly prove the same for $x_{1}$, and obtain a proof
of [2] for $t$. The proof for $u$ is similar.

[$2\Rightarrow 1$:] Given the proof of $(T;E)\vdash\mu({{t}\bowtie{u}})$ we
can apply $\exists\sf i$ successively to get a proof of $\alpha$. We just need
to show that the abstractability side conditions are satisfied. Using the same
notation as in the proof of [$1\Rightarrow 2$] above, we consider the passage
from ${(\mu^{\prime}(\alpha_{3}))}[{w_{2}}]_{P}$ to $\mu(\alpha_{2})$. As
above, we need to show that
$\mathbb{P}_{x_{2}}({\mu^{\prime}(t)})\subseteq\mathbb{A}(T\cup\\{x_{2},x_{3}\\},\mu^{\prime}(t))$
and similarly for $u$. But we saw above that this is equivalent to
$\mathbb{P}_{x_{2}}({t})\subseteq\mathbb{A}(T\cup{\sf dom}(\mu),t)$, which is
guaranteed by [2]. ∎

##  Appendix B Proof of Theorem 3.10

We recommend reading this appendix after reading the main paper, since we
reuse some notions from Section 5 here.

Let $(S;A)$ be sanitized, and
$\alpha=\exists{x_{1}\ldots{}x_{k}}.({{t^{0}}\bowtie{u^{0}}})$ be an assertion
with ${\sf bv}(\alpha)\cap{\sf vars}(S;A)=\varnothing$. Let
$(T;E)=\mathit{ker}(S;A)$. By Theorem 3.8, $(S;A)\vdash_{\mathit{a}}\alpha$
iff there is a substitution $\mu$ with ${\sf dom}(\mu)={\sf bv}(\alpha)$ s.t.:

  1. [1]

$\forall{}x\in{\sf dom}(\mu):T\vdash_{\mathit{dy}}\mu(x)$.

  2. [2]

$\forall{}x\in{\sf dom}(\mu),r\in\\{t^{0},u^{0}\\}$:
$\mathbb{P}_{x}({r})\subseteq\mathbb{A}(T\cup{\sf bv}(\alpha),r)$.

  3. [3]

$(T;E)\vdash_{\mathit{eq}}\mu({{t^{0}}\bowtie{u^{0}}})$.

In this section, we prove that if there is a $\mu$ satisfying the above
conditions, there is also a small $\nu$ satisfying the same. We use $Z$ to
refer to ${\sf dom}(\mu)$. Let $\mathscr{C}={\sf st}(T)\cup{\sf
st}(E\cup\\{\alpha\\})$, and let $\mathscr{D}=\mathscr{C}\setminus Z$. For all
$x\in Z$, $T\vdash_{\mathit{dy}}\mu(x)$. So all variables occurring in
$\mu(x)$ must also be in ${\sf vars}(T)$. But ${\sf vars}(T;E)\cap
Z=\varnothing$, so ${\sf vars}(\mu(x))\cap Z=\varnothing$ for any $x\in Z$.

Define $t\approx u$ iff $T;E\vdash_{\mathit{eq}}\mu({{t}\bowtie{u}})$. It is
easy to see that $\approx$ is a partial equivalence relation (on the subset of
terms $t$ such that $T\vdash_{\mathit{dy}}\mu(t)$).

We say that $x\in Z$ is _minimal_ if there is no $t\in\mathscr{D}$ with
$x\approx t$. Let $\mathscr{V}_{m}$ denote the set of all minimal variables.
Our strategy for finding a small $\nu$ is to “zap” minimal variables, and
propagate the change to (interpretations of) non-minimal variables. For this,
it is convenient to translate every term to an “equivalent” one with only
minimal variables. This notion of equivalence is based on unifiability under
$\mu$. The set of terms which are equivalent to terms in $\mathscr{C}$ is
defined as follows.

######  Definition B.1.

$\widehat{\mathscr{C}}\coloneqq\\{t\mid{\sf vars}(t)\cap
Z\subseteq\mathscr{V}_{m}$, either $t\in\mathscr{V}_{m}$ or
$\exists{u}\in\mathscr{D}:t\approx u\\}$.

######  Lemma B.2.

For every $t\in\mathscr{C}$ with $T\vdash_{\mathit{dy}}\mu(t)$, there is
${t}^{*}\in\widehat{\mathscr{C}}$ such that:
$T\vdash_{\mathit{dy}}\mu({t}^{*})$; $t\approx{t}^{*}$; and for all
$x\in\mathscr{V}_{m}$, $\mathbb{P}_{x}({{t}^{*}})\subseteq\mathbb{A}(T\cup
Z,{t}^{*})$.

  * Proof.

For $x,y\in Z$, $x\prec y$ iff $\exists{r}\in\mathscr{D}:x\in{\sf st}(r)\text{
and }r\approx y$.

We now show that $\prec$ is acyclic. Towards this, we claim that if $x\prec y$
and $y\prec z$, then there is some term $a$ (not necessarily in $\mathscr{C}$)
s.t. $\mu(x)$ is a proper subterm of $\mu(a)$ and $a\approx z$. Extending this
reasoning, we see that if $x\prec^{+}x$, we have some term $a$ such that
$\mu(x)$ is a proper subterm of $\mu(a)$ and
$(T;E)\vdash_{\mathit{eq}}{{\mu(a)}\bowtie{\mu(x)}}$. But $E$ is consistent,
which means that there is some $\lambda$ s.t.
$\lambda(\mu(a))=\lambda(\mu(x))$. But this is incompatible with $\mu(x)$
being a proper subterm of $\mu(a)$. Thus $\prec$ is acyclic.

We now prove the claim. Suppose $x\prec y$ and $y\prec z$. Then there exist
$r,s\in\mathscr{D}$ such that the following hold:

    * –

$x\in{\sf st}(r)$ and $(T;E)\vdash_{\mathit{eq}}{{\mu(r)}\bowtie{\mu(y)}}$

    * –

$y\in{\sf st}(s)$ and $(T;E)\vdash_{\mathit{eq}}{{\mu(s)}\bowtie{\mu(z)}}$

Let $a={s}[{r}]_{\mathbb{P}_{y}({s})}$, i.e. the term obtained by replacing
each $y$ in $s$ by $r$. Since $\mu(x)\in{\sf st}(\mu(r))$, $\mu(x)$ is a
proper subterm of $\mu(a)$. One can derive
$(T;E)\vdash{{\mu(a)}\bowtie{\mu(z)}}$ via ${\sf subst}$ on
${{\mu(s)}\bowtie{\mu(z)}}$ and ${{\mu(r)}\bowtie{\mu(y)}}$. Thus $a\approx
z$.

Since $\prec$ is acyclic, we can define a notion of _rank_ for variables:
$\mathit{rank}(x)=\max\\{\mathit{rank}(y)\mid y\prec^{+}x\\}+1$. For a term
$u\in\mathscr{D}$, we define $\mathit{rank}(u)=\max\\{\mathit{rank}(x)\mid