A decision procedure and typing result for alpha-beta privacy

Abstract

We present a decision procedure for verifying whether a protocol respects privacy goals, given a bound on the number of transitions. We consider multi message-analysis problems, where the intruder does not know exactly the structure of the messages but rather knows several possible structures and that the real execution corresponds to one of them. This allows for modeling a large class of security protocols, with standard cryptographic operators, non-determinism, branching and statefulness. Our first contribution is the definition of a decision procedure for a fragment of alpha-beta privacy. Moreover, we have implemented a prototype tool as a proof-of-concept and a first step towards automation. Our second contribution is to show that, for a class of protocols satisfying certain syntactic conditions, it is sound to restrict the intruder model to a typed model, where the intruder only sends well-typed messages. Our typing result holds for an unbounded number of transitions.

Keywords

Privacy security protocols unlinkability formal methods automated verification

1. Introduction

The concept of $(α, β)$ -privacy was introduced as an alternative way to define privacy-type properties in security protocols.^1,2 The most widespread models of privacy use an equivalence notion between two processes to describe the goal that the intruder cannot distinguish between two possible realities. In contrast, $(α, β)$ -privacy considers states that each represent one possible reality, and what the intruder knows about the reality in that state. This knowledge is not only in form of messages as in classic intruder models, but also in form of relations between messages, agents, and so on. Together with a notion of what the intruder is allowed to know in a given state, we define a privacy violation if the intruder in any reachable state knows more than allowed. Privacy is then a question of reachability—a safety property—which is often easier to reason about and to specify than classical equivalence notions. First, one does not have to boil the privacy goal down to a distinction between two situations, which is often unnatural for more complicated properties. Second, one specifies goals positively by what the intruder is allowed to know rather than what they are not allowed to know (and thus unable to distinguish). This essentially means that in the worst case one is erring on the safe side, that is, allowing less than the protocol actually reveals, and thus can be alerted by a counterexample. The expressive power of equivalence notions and of $(α, β)$ -privacy is actually hard to relate in general, due to the different nature of the approaches. However, on concrete examples it seems one can always give reasonable adaptations from one approach to the other.^1,2

1.1. A decision procedure

$(α, β)$ -privacy shifts the problem from a notion of equivalence (that is a challenge for automation) to a simple reachability problem where however the privacy check for each reached state is more involved. So far, there is only one work³ that considers a solution to checking a given state in $(α, β)$ -privacy. However, that work is only applicable to specifications without conditional branching and it is based on an exploration of all concrete messages that the intruder can send, which are infinitely many unless one bounds the intruder.

Our first contribution in this article is a decision procedure for the full notion of transaction processes defined by Gondron et al.¹ for constructor/destructor theories.^4–8 This notion in fact entails that the intruder performs a symbolic execution of the transaction that in general yields several possibilities (due to conditional branching if the intruder does not know the truth value of the condition) and the intruder can then contrast this with all observations and experiments (constructing different messages and comparing them) to potentially rule out some possibilities. The core of our work is in a procedure to model this intruder analysis without bounding the number of steps that the intruder can make in this process. To that end, we use a popular constraint-based technique to represent the intruder symbolically, that is, without exploring infinite sets of possibilities, which we call here the lazy intruder. In fact, we use several layers of symbolic representation to make the approach feasible.

Our decision procedure tells us whether from a given state we can reach a state that violates privacy for a fixed bound on the number of transitions. Our procedure is limited to such a bound on transitions, corresponding to the restriction to a bounded number of sessions in many approaches.⁹ This is similar to the bounds needed in tools like APTE,¹⁰ AKiSs,¹¹ SPEC^12,13 and DeepSec.⁷ In fact, this article draws from the techniques used in these approaches, such as the symbolic representation of the intruder, a notion of an analyzed intruder knowledge, and methods for deciding the equivalence of frames. There are, however, several basic differences and generalizations. In particular, we use a symbolic handling of privacy variables (that in the equivalence-based approaches are simply one binary choice) and this is linked to logical formulas about relations between elements of the considered universe. In fact, in the prototype implementation of our decision procedure that we provide as a further contribution, we employ the SMT solver cvc5¹⁴ to handle these logical evaluations. Moreover, we have multiple frames with constraints for the different possibilities resulting from conditional branching and we analyze if the intruder can rule out any possibilities in any instance.

In contrast, the tools ProVerif⁵ and Tamarin¹⁵ do handle unbounded sessions but require the restriction to so-called diff-equivalence,^8,16 which drastically limits the use of branching in security protocols, though Cheval and Rakotonirina¹⁷ recently relax these restrictions a bit. It seems thus in general that one has to choose between expressive power and unbounded sessions, and our approach is decidedly on the side of expressive power.

1.2. A typing result

Type-flaw attacks occur when a security protocol uses several messages that have different meanings but have a similar shape so that an intruder can exploit it and send a message of one type where a message of another type is expected. For example, one message of the protocol is a signature on a nonce for challenge-response, say $s i g n (i n v (p k (x)), N)$ (where $i n v$ denotes the private key to the public key $p k (x)$ of agent $x$ ), and another message is a signature on an encrypted message like $s i g n (i n v (p k (y)), c r y p t (p k (z), M, R))$ . It is actually easy to prevent type-flaw attacks by good protocol design: messages should not sign or encrypt raw data, but rather include a few bits of information that specify the meaning of the message. In the example, the signatures should contain at least some kind of tag that distinguishes the different types of signed statements. Such a countermeasure is not only almost for free, it is completely in line with prudent engineering principles.^18,19

Formal verification of security protocols generally gets easier if we can rule out type-flaw attacks and analyze everything in a typed model where the intruder is restricted to sending well-typed messages. Then, many security problems become decidable (and, e.g., one can guarantee termination of tools like ProVerif²⁰).

This motivates a relative soundness result of the form: “if a protocol that obeys certain type-flaw resistance requirements has an attack, then it has a well-typed attack.” It is then sound to verify such a protocol in the typed model. This is particularly relevant in practice, if many existing protocols without modification already satisfy type-flaw requirements.

Most of the existing typing results, for example, Almousa et al.,²¹ Arapinis and Duflot,²² Arapinis and Duflot,²³ Cortier and Delaune,²⁴ and Hess and Mödersheim,^25,26 use a constraint-based method for analyzing security protocols that is based on a symbolic approach: this technique avoids exploring all the messages that the intruder could generate at a given point, but instead uses a variable with the constraint that this variable represents any message that the intruder can generate from their current knowledge. This variable is only instantiated when the choice matters for the attack. One can then show that in a type-flaw resistant protocol, these instantiations are always well-typed, and that all remaining variables (that do not matter for the attack in the end) can be instantiated with something well-typed as well. Thus, if an attack exists, there exists a well-typed one. Although this method yields a decision procedure only for a bounded number of sessions, since the argument applies to an attack of arbitrary length, the typing result is not bounded to a fixed number of sessions and can be used in approaches/tools that do not use the lazy intruder (like ProVerif).

A trend in protocol verification is the support for privacy-type properties such as unlinkability or vote-secrecy, that is, secrecy of a choice over a small domain of intruder-known values. This is challenging for verification tools and thus many tools require a restriction like diff-equivalence where, roughly speaking, conditions—and thus control flow—cannot depend on the private choice. It is thus very desirable to simplify the tools’ lives by a typing result, but that is harder to obtain for privacy as well. For instance, a typing result needs to exclude that the intruder can gain any insight about a condition (and thus possibly private choices) by sending an ill-typed message. This is in fact related again to the problem of control flow (that classical diff-equivalence sidesteps): the intruder may not know in general what exactly is happening in the protocol, while in standard protocol verification the intruder is only unclear about the concrete value of some cryptographically strong secrets.

Our second contribution in this article is a typing result for $(α, β)$ -privacy: “if there is an attack, then there is a well-typed one.” We define a set of requirements for protocols and algebraic theories we can support, and prove that under these requirements the procedure performs only well-typed instantiations of variables and well-typed intruder experiments. As in previous typing results, this is independent of the number of transitions considered. This result is, to our knowledge, not only more general than previous typing results for privacy, since the requirements are less restrictive and a larger class of protocols is considered, but it also has a more declarative proof.

1.3. Outline

In Section 2, we present the notion of $(α, β)$ -privacy in transition systems and define the problem that our procedure decides. In Section 3, we define how we symbolically represent messages sent by the intruder and how to solve constraints with the lazy intruder rules. In Section 4, we introduce the notion of symbolic states with their semantics. In Section 5, we explain how the intruder can perform experiments and make logical deductions relevant for privacy by comparing messages in their knowledge. In Section 6, we define the algebraic theories supported and how they are handled in the procedure. In Section 7, we discuss the prototype tool that we have developed and the case studies we have applied it to. In Section 8, we define the class of type-flaw resistant protocols that our typing result supports. In Section 9, we present the typing result for an unbounded number of transitions. In Section 10, we discuss related and future work. The Supplemental Appendix contains additional technical details and all the proofs of correctness.

This journal article is based on the conference paper,²⁷ which presented the decision procedure. Our main new contributions are the support for stateful protocols and, most importantly, the typing result.

2. Preliminaries and problem definition

Mödersheim and Viganò² introduce $(α, β)$ -privacy as a reachability problem in a state transition system, where each state contains two formulas $α$ and $β$ . Intuitively, $α$ represents what the intruder may know (e.g. the result of an election) and $β$ what the intruder has observed (e.g. the encrypted votes). Then, a state $(α, β)$ violates privacy iff some model of $α$ can be excluded by the intruder knowing $β$ , that is, the intruder in that state can rule out more than allowed. The transition system violates $(α, β)$ -privacy iff some reachable state does.

2.1. ( $α, β$ )-privacy for a state

Mödersheim and Viganò² focus on how to define $(α, β)$ pairs for a fixed state, and describes a state-transition relation only briefly by an example. Let us also start with a fixed state. The formulas $α$ and $β$ are by Herbrand logic,²⁸ a variant of first-order logic (FOL), with the difference that the universe is the quotient algebra of the Herbrand universe (the set of all terms that can be built with the function symbols) modulo a congruence relation $\approx$ . This congruence specifies algebraic properties of cryptographic operators. For concreteness, we use the congruence defined in Figure 1; the class of properties supported by our result is in Definition 6.1. The quotient algebra consists of the $\approx$ -equivalence classes of terms.

Figure 1.

The congruence used in this article: $c r y p t$ and $d c r y p t$ are asymmetric encryption and decryption, $s c r y p t$ and $d s c r y p t$ are symmetric encryption and decryption, $s i g n$ and $o p e n$ are signing and verification/opening, $p a i r$ is a transparent function and the ${p r o j}_{i}$ are the projections, $i n v$ gives the private key corresponding to a public key, and $p u b k$ gives the public key from a private key. Here $k$ , $t$ , $r$ , and the $t_{i}$ are variables standing for arbitrary messages. When the conditions are not met, the functions give $f f$ , which is a constant indicating failure of decryption or parsing. If $c r y p t$ and $s c r y p t$ are used as binary functions, we consider their deterministic variants where the random factor $r$ has been fixed and is omitted for simplicity.

Given an alphabet $Σ$ , a $Σ$ -interpretation $I$ interprets variable and relation symbols as usual in the Herbrand universe induced by $Σ$ and $\approx$ ; the interpretation of the function symbols is determined by the Herbrand universe. We have a model relation $╞_{Σ}$ as expected. By construction, $I ╞_{Σ} s ≐ t$ iff $I (s) \approx I (t)$ . We say that $ϕ$ entails $ψ$ , and write $ϕ ╞_{Σ} ψ$ , when every $Σ$ -interpretation that is a model of $ϕ$ is also a model of $ψ$ . We write $ϕ \equiv_{Σ} ψ$ when $ϕ ╞_{Σ} ψ$ and $ψ ╞_{Σ} ϕ$ . We also use $\equiv_{Σ}$ to define formulas.

We now fix the alphabet $Σ$ that contains all symbols we use, namely cryptographic functions, a countable set of constants representing agents, nonces and so on, and some relation symbols. We also have the set of variable symbols $V$ . Each protocol specification will fix a sub-alphabet $Σ_{0} \subset Σ$ of payload symbols; we call $Σ ∖ Σ_{0}$ the technical symbols. All $α$ formulas use only symbols in $Σ_{0}$ and variables. In the rest of the article, we often omit the alphabet and just write $╞$ to mean $╞_{Σ_{0}}$ , and $\equiv$ to mean $\equiv_{Σ_{0}}$ .

The main idea of $(α, β)$ -privacy is that we distinguish between the actual privacy goal (e.g. an unlinkability goal talking only about agents) and the means to achieve it (e.g. the cryptographic messages exchanged).

Definition 2.1 (Adapted from Mödersheim and Viganò²)

Given two formulas $α$ over $Σ_{0}$ and $β$ over $Σ$ with $f v (α) \subseteq f v (β)$ , where $f v$ denotes the free variables, we say that $(α, β)$ -privacy holds iff for every $Σ_{0}$ -interpretation $I ╞_{Σ_{0}} α$ there exists a $Σ$ -interpretation $I^{'} ╞_{Σ} β$ such that $I$ and $I^{'}$ agree on the variables in $f v (α)$ and on the relation symbols in $Σ_{0}$ .

We call the formula $α$ the payload, defining the privacy goal. For example, for unlinkability in an RFID-tag protocol, we may have a fixed set ${t_{1}, t_{2}, t_{3}}$ of tags and in a concrete state, the intruder has observed that two tags have run a session. Then $α$ in that state may be $x_{1}, x_{2} \in {t_{1}, t_{2}, t_{3}}$ , meaning that the intruder is only allowed to know that both $x_{1}$ and $x_{2}$ are indeed tags, but not, for instance, whether $x_{1} ≐ x_{2}$ . In our approach, the formulas $α$ that can occur fall into a fragment where we can always compute a finite representation of all models, in particular the variables like the $x_{i}$ in the example will always be from a fixed finite domain.

For the formula $β$ , we employ the concept of frames: a frame has the form $F = l_{1} \mapsto t_{1} . \dots . l_{n} \mapsto t_{n}$ , where the $l_{i}$ are distinguished variables called labels and the $t_{i}$ are messages (that do not contain labels). This represents that the intruder has observed (or initially knows) messages $t_{1}, \dots, t_{n}$ and we give each message a unique label. We call the set ${l_{1}, \dots, l_{n}}$ the domain of $F$ . A frame can be used as a substitution, mapping labels to messages.

To describe intruder deductions, we define a subset $Σ_{p u b}$ of the function symbols to be public: they represent operations the intruder can perform on known messages. For instance, all symbols used in Figure 1 are public except for $i n v$ , since getting the private key is not an operation that everyone can do themselves.^a A recipe (in the context of a frame $F$ ) is any term that consists of only labels (in the domain of $F$ ) and public function symbols, so it represents a computation that the intruder can perform on $F$ . We write $F (r)$ for the message generated by the recipe $r$ with the frame $F$ .

Two frames $F_{1}$ and $F_{2}$ with the same domain are statically equivalent, written $F_{1} \sim F_{2}$ , iff for every pair $(r_{1}, r_{2})$ of recipes, we have $F_{1} (r_{1}) \approx F_{1} (r_{2}) \Leftrightarrow F_{2} (r_{1}) \approx F_{2} (r_{2})$ . This means that the intruder cannot distinguish $F_{1}$ and $F_{2}$ , since any experiment they can make (i.e. comparing the outcome of two computations $r_{1}, r_{2}$ ) either gives in both frames the same result or in both frames not.

Static equivalence can be encoded in Herbrand logic² and so for instance we can have as part of $β$ formulas like $c o n c r \sim s t r u c t$ , where $s t r u c t$ is a frame with variables and $c o n c r = I (s t r u c t)$ for some model $I ╞ α$ is the concrete frame of intruder observations. As an example, let $α \equiv x_{1}, x_{2} \in {0, 1}$ , $s t r u c t = l_{1} \mapsto h (k, x_{1}) . l_{2} \mapsto h (k, x_{2})$ and $c o n c r = l_{1} \mapsto h (k, 0) . l_{2} \mapsto h (k, 1)$ . Observe that $α$ has four models, but in the two models where $I (x_{1}) = I (x_{2})$ we have $I ⧸ ╞ c o n c r \sim s t r u c t$ , because for these models $l_{1}$ and $l_{2}$ give the same message in $s t r u c t$ but different messages in $c o n c r$ . Since in this example $c o n c r \sim s t r u c t$ is part of $β$ , $β$ allows the intruder to rule out two models of $α$ , thus $(α, β)$ -privacy does not hold.

2.2. ( $α, β$ )-privacy for a transition system

So far we have been talking about only a single $(α, β)$ pair, that is, a single state of a larger transition system. Gondron et al.¹ define a language for specifying transition systems where the reachable states and their $(α, β)$ pairs are defined by executing atomic transactions. We present their formalization with some minor adaptations to ease our further development.

We distinguish two sorts of variables: the privacy variables $V_{p r i v a c y}$ , which are denoted with lower-case letters like $x$ and are all introduced in the form $x \in D$ for a finite domain $D$ of public constants from $Σ_{0}$ , and the intruder variables $V_{i n t r u d e r}$ , which are denoted with upper-case letters like $X$ for messages received and cell reads in a transaction.

We also distinguish destructor and constructor function symbols. In Figure 1, we have that $d c r y p t$ , $d s c r y p t$ , $o p e n$ , $p u b k$ , ${p r o j}_{1}$ , and ${p r o j}_{2}$ are destructors whereas the rest are constructors. Moreover, we call $p a i r$ and $i n v$ transparent functions, because one can get all their arguments without any key (but recall that $i n v$ is not a public function).

Definition 2.2 (Protocol specification)

A protocol specification consists of

a number of transaction processes $P_{i}$ , where the $P_{i}$ are left processes according to the syntax below, describing the atomic transactions that participants in the protocol can execute;

a number of memory cells, for example, $c e l l [\cdot]$ , together with a ground context $C [\cdot]$ for each memory cell defining the initial value of the memory, so that initially $c e l l [t] = C [t]$ ;

a $Σ_{0}$ -formula $γ_{0}$ that fixes the interpretation of the relation symbols.

We define left, center, and right processes as follows:

\begin{array}{llll} P_{l} & Left process \\ ::= & m o d e x \in D . P_{l} & Non-deterministic choice \\ ∣ & r c v (X) . P_{l} & Receive \\ ∣ & P_{c} & Center process \\ P_{c} & Center process \\ ::= & t r y X := d (t, t) i n P_{c} c a t c h P_{c} & Destructor application \\ ∣ & X := c e l l [t] . P_{c} & Cell read \\ ∣ & i f ϕ t h e n P_{c} e l s e P_{c} & Conditional statement \\ ∣ & ν n_{1}, \dots, n_{k} . P_{r} & Fresh constants \\ P_{r} & Right Process \\ ::= & s n d (t) . P_{r} & Send \\ ∣ & c e l l [t] := t . P_{r} & Cell write \\ ∣ & ⋆ ϕ . P_{r} & Release \\ ∣ & 0 & Terminate (nil process) \end{array}

where

m o d e

is either

⋆

⋄

ϕ

is a quantifier-free Herbrand formula, and

d

is a destructor. Destructors are not allowed to occur elsewhere in terms. For simplicity, we have denoted destructors as binary functions, but we may similarly use unary destructors (like

{p r o j}_{i}

and

p u b k

in the example).

We require that a transaction $P$ is a closed left process, that is, $f v (P) = \emptyset$ —we define the free variables $f v (P)$ of a process $P$ as expected, where the non-deterministic choices, receives, cell reads and fresh constants are binding. Moreover, for destructor applications:

f v (t r y X := d (k, t) i n P_{1} c a t c h P_{2}) = f v (d (k, t)) \cup (f v (P_{1}) ∖ {X}) \cup f v (P_{2})

Finally, a bound variable cannot be instantiated a second time.

Example 2.1. (Running example)

Let us consider the following transaction where a server non-deterministically chooses an agent $x$ and a yes/no-decision $y$ , receives a message, tries to decrypt it with their own private key and then sends the decision encrypted with the public key of $x$ :

\begin{aligned} ⋆ x \in A g e n t . ⋆ y \in {y e s, n o} . \\ r c v (M) . \\ t r y N := d c r y p t (i n v (p k (s)), M) i n \\ i f y ≐ y e s t h e n \\ ν r . s n d (c r y p t (p k (x), p a i r (y e s, N), r)) . 0 \\ e l s e ν r . s n d (c r y p t (p k (x), n o, r)) . 0 \\ c a t c h 0 \end{aligned}

Here the

⋆

means that the choice of

x

and

y

is privacy relevant and the intruder may (at least for now) only learn that

x \in A g e n t

and

y \in {y e s, n o}

. The outgoing message has a different form depending on

y

: in the positive case the server also includes the content

N

of the encrypted message

M

they received (and if the message is not of the right format, then the transaction simply terminates); in either case the encryption is randomized with a fresh

r

. We may omit

r

if we want to model non-randomized encryption.

p k

is a public function (modeling a fixed public-key infrastructure known to everybody).

Much of these processes follows standard process calculus constructs. The special constructs of $(α, β)$ -privacy are the non-deterministic choice and release. Choice comes in two flavors: $⋆$ if the choice is privacy relevant (as in the example), and $⋄$ if not. The release is used to declare that a certain fact $ϕ$ may now be known to the intruder; we discuss this construct and what formulas can be released a bit later.

Observe that privacy variables are introduced only by non-deterministic choices $m o d e x \in D$ . If the $m o d e$ is $⋆$ , the transaction augments $α$ by $x \in D$ , thus specifying that the intruder may not know more about $x$ unless we also explicitly release some information about $x$ . If the $m o d e$ is $⋄$ , the transaction augments $β$ by $x \in D$ . In this case, it is not in itself a violation of privacy if the intruder learns more about $x$ , but it may lead to a privacy violation if this allows for finding out more about the variables in $α$ . This is useful if one wants to keep the privacy specification independent of some rather technical secret. In our model, the intruder knows which transaction is executed, but in general does not know which branch is taken. Using, for example, $⋄ z \in {1, 2} . i f z ≐ 1 t h e n P_{1} e l s e P_{2}$ , one can reduce the visibility of processes $P_{1}$ and $P_{2}$ by putting them in a single transaction. In some execution the intruder may find out, for example, $z ≐ 1$ , and it is not a privacy violation in itself.

Semantics. The semantics follows Gondron et al.,¹ with small adaptations. It is defined as a state transition system where each transition corresponds to the execution of one transaction. Thus, transactions are atomic: they cannot run concurrently with another transaction. In particular, when reading from and writing to memory cells, no race conditions can occur and we thus do not need locking mechanisms. A transaction thus consists in receiving input, checking this input (possibly reading from memory), then making a decision (possibly updating the memory), and finally sending an output and releasing information.

The atomicity of transactions has an advantage: we can easily formalize how the intruder can reason about what is happening. In particular, we assume that the intruder at each point knows which transaction is executed and what process a transaction contains. What the intruder does not know in general are the concrete values of the variables and the truth values of conditions, and thus in which branch of an $i f$ - $t h e n$ - $e l s e$ or $t r y$ - $c a t c h$ we are. However, the intruder can always contrast this knowledge with the observations about incoming and outgoing messages: if an observed sent message does not fit with one branch of the transaction, then the intruder knows that branch was not taken, and thus they also learn something about the truth value of the corresponding conditions. In other cases, the intruder may know what is in a received message and thus know the truth value of some condition. The intruder thus performs a symbolic execution of the transaction, leaving open what they do not know, keeping a list of possibilities, and in fact the semantics of transactions formally models this symbolic execution by the intruder.

Let a possibility be a tuple $(P, ϕ, s t r u c t, δ)$ , where $P$ is the transaction being executed, $ϕ$ is the conditions under which this possibility was reached, $s t r u c t$ is a frame that we call the structural knowledge about the messages in this possibility and $δ$ is a sequence of memory updates. A state is a tuple $(α, β_{0}, γ, P)$ , where $α$ , $β_{0}$ , and $γ$ are $Σ_{0}$ -formulas, and $P$ is a non-empty finite set of possibilities $P = {(P_{1}, ϕ_{1}, {s t r u c t}_{1}, δ_{1}), \dots, (P_{n}, ϕ_{n}, {s t r u c t}_{n}, δ_{n})}$ , where one of the possibilities is marked by underlining as the possibility that is actually the case in the real execution (but the intruder does not know which one, in general). In this article, we consider only well-formed states, where a state is well-formed iff all ${s t r u c t}_{i}$ have the same domain, $γ ╞ γ_{0}$ describes a unique model of $α \land β_{0}$ and the $ϕ_{i}$ both are mutually exclusive, that is, $╞ \neg (ϕ_{j} \land ϕ_{k})$ , for $j \neq k$ , and cover all models, that is, $α \land β_{0} ╞ ⋁_{i = 1}^{n} ϕ_{i}$ . We define the concrete frame $c o n c r$ as the instantiation of the ${s t r u c t}_{j}$ from the possibility underlined by $γ$ .

Definition 2.3 (Multi-message-analysis problem)

Given a well-formed state $S = (α, β_{0}, γ, P)$ , let $c o n c r = γ ({s t r u c t}_{j})$ where $(P_{j}, ϕ_{j}, {s t r u c t}_{j}, δ_{j})$ is the marked possibility in $P$ . Define

β (S) \equiv_{Σ} α \land β_{0} \land ⋁_{i = 1}^{n} ϕ_{i} \land c o n c r \sim {s t r u c t}_{i}

We say that

S

satisfies privacy iff

(α, β (S))

-privacy holds.

The semantics models that the intruder can symbolically execute transactions, but at branchings they do not know in general whether the condition is true; the possibilities reflect the different possible truth values of the conditions and what would have happened in that case. The underlined possibility is the one that really happened. Contrasting $c o n c r$ and each ${s t r u c t}_{i}$ , the intruder may be able to exclude some possibility (because $c o n c r$ and ${s t r u c t}_{i}$ are distinguishable) and thus learn about the truth value of conditions $ϕ_{i}$ . Vice-versa, what the intruder knows about variables may allow them to exclude some possibilities.

To model the symbolic execution of a transaction $P$ , we start in a state where all possibilities contain that process $P$ . The semantics defines an evaluation relation $\to$ on states that works off the processes in each possibility until in all possibilities, the process is $0$ . We call such a state finished. The branching of $\to$ represents the non-deterministic choices of the process as well as choices of messages by the intruder.

To give a gentle introduction to $(α, β)$ -privacy in transition systems, we present the symbolic execution at hand of the running example from Example 2.1. The complete definition of the rules is in Table 1. Notation: $δ_{| c e l l}$ is the largest subsequence of $δ$ that only contains memory updates on $c e l l$ and $⊎$ is the disjoint union of sets.

As a starting point for the symbolic execution, we use the singleton set of possibilities ${\underline{(P, t r u e, [], [])}}$ , where $P$ is the process from the running example. Let $α$ , $β_{0}$ , and $γ$ be $t r u e$ ; $[]$ denotes the empty frame and empty memory. We list in Table 2 the successive states that are reached when executing $P$ and we explain below the transitions.

Non-deterministic choice. The first steps in the running example are two non-deterministic choices of privacy variables. In general, there are several successor states, one for each possible choice of the variables. Let us follow the case where $x = a$ and $y = y e s$ ; this is added to $γ$ , and we add to $α$ that $x \in A g e n t$ and $y \in {y e s, n o}$ . We reach states $2$ then $3$ . Note that $x$ and $y$ are not replaced in the remaining process—this is a symbolic execution by the intruder. Also note that the general rule assumes that all possibilities start with the same $m o d e$ ; this is ensured since this choice can only occur in the left part of the transaction, before any branching on conditions and tries can occur.

Table 1.
Semantics of the execution for states.

Choice $(α, β_{0}, γ, {(m o d e x \in D . P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$

$\to (α^{'}, β_{0}^{'}, γ \land x ≐ c, {(P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$

for every $c \in D$

where $α^{'} \equiv α \land x \in D$ and $β_{0}^{'} \equiv β_{0}$ if $m o d e = ⋆$ , and $α^{'} \equiv α$ and $β_{0}^{'} \equiv β_{0} \land x \in D$ if $m o d e = ⋄$

Receive $(α, β_{0}, γ, {(r c v (X) . P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$

$\to (α, β_{0}, γ, {(P_{i} [X \mapsto {s t r u c t}_{i} (r)], ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$

for every recipe $r$ over the domain of the ${s t r u c t}_{i}$

Cell read $(α, β_{0}, γ, {(X := c e l l [s] . P, ϕ, s t r u c t, δ)} ⊎ P) \to (α, β_{0}, γ, {(P^{'}, ϕ, s t r u c t, δ)} \cup P)$

where $δ_{| c e l l} = c e l l [s_{1}] := t_{1} . \dots . c e l l [s_{k}] := t_{k}$ , the initial value of $c e l l$ is given by ground context $C [\cdot]$

and $P^{'} = i f s ≐ s_{1} t h e n P [X \mapsto t_{1}] e l s e \dots i f s ≐ s_{k} t h e n P [X \mapsto t_{k}] e l s e P [X \mapsto C [s]]$

Cell write $(α, β_{0}, γ, {(c e l l [s] := t . P, ϕ, s t r u c t, δ)} ⊎ P) \to (α, β_{0}, γ, {(P, ϕ, s t r u c t, c e l l [s] := t . δ)} \cup P)$

Conditional $(α, β_{0}, γ, {(i f ψ t h e n P_{1} e l s e P_{2}, ϕ, s t r u c t, δ)} ⊎ P)$

$\to (α, β_{0}, γ, {(P_{1}, ϕ \land ψ, s t r u c t, δ), (P_{2}, ϕ \land \neg ψ, s t r u c t, δ)} \cup P)$

Release $(α, β_{0}, γ, {(⋆ ψ . P, ϕ, s t r u c t, δ)} ⊎ P) \to (α^{'}, β_{0}, γ, {(P, ϕ, s t r u c t, δ)} \cup P)$

where $α^{'} \equiv α \land ψ$ if $γ ╞ ϕ$ , and $α^{'} \equiv α$ otherwise

Eliminate $S = (α, β_{0}, γ, {(P, ϕ, s t r u c t, δ)} ⊎ P) \to (α, β_{0}, γ, P)$

if $β (S) ⧸ ╞ ϕ$

Send $(α, β_{0}, γ, {(s n d (t_{i}) . P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}} ⊎ P)$

$\to (α, β_{0} \land ⋁_{i = 1}^{n} ϕ_{i}, γ, {(P_{i}, ϕ_{i}, {s t r u c t}_{i} . l \mapsto t_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$

if $γ ╞ ⋁_{i = 1}^{n} ϕ_{i}$ and every process in $P$ is $0$ , where $l$ is a fresh label

Terminate $(α, β_{0}, γ, {(0, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}} ⊎ P)$

$\to (α, β_{0} \land ⋁_{i = 1}^{n} ϕ_{i}, γ, {(0, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$

if $γ ╞ ⋁_{i = 1}^{n} ϕ_{i}$ , $P$ is non-empty and every process in $P$ starts with $s n d (\cdot)$

Table 2.

States of the running example.

State	$α$	$β_{0}$	$γ$	$P$
$1$	$t r u e$	$t r u e$	$t r u e$	${\underline{(⋆ x \in A g e n t . ⋆ y \in {y e s, n o} \dots, t r u e, [], [])}}$
$2$	$x \in A g e n t$	$t r u e$	$x ≐ a$	${\underline{(⋆ y \in {y e s, n o} . r c v (M) \dots, t r u e, [], [])}}$
$3$	$α_{2} \land y \in {y e s, n o}$	$t r u e$	$γ_{2} \land y ≐ y e s$	${\underline{(r c v (M) . t r y \dots, t r u e, [], [])}}$
$4$	$α_{3}$	$t r u e$	$γ_{3}$	${\underline{(t r y N := \dots, t r u e, [], [])}}$
$5$	$α_{3}$	$t r u e$	$γ_{3}$	${(0, f a l s e, [], []), \underline{(i f y ≐ y e s \dots, t r u e, [], [])}}$
$6$	$α_{3}$	$t r u e$	$γ_{3}$	${\underline{(i f y ≐ y e s t h e n s n d (\dots) .0 e l s e s n d (\dots) .0, t r u e, [], [])}}$
$7$	$α_{3}$	$t r u e$	$γ_{3}$	${\underline{(s n d (c r y p t (p k (x), p a i r (y e s, a), r_{1})) .0, y ≐ y e s, [], [])},$
				$(s n d (c r y p t (p k (x), n o, r_{1}) .0, y ≐̸ y e s, [], [])}$
$8$	$α_{3}$	$y ≐ y e s$	$γ_{3}$	${\underline{(0, y ≐ y e s, l \mapsto c r y p t (p k (x), p a i r (y e s, a), r_{1}), [])},$
		$\lor y ≐̸ y e s$		$(0, y ≐̸ y e s, l \mapsto c r y p t (p k (x), n o, r_{1}), [])}$

Receive. The next step is now $r c v (M)$ . Again the construction ensures that every process in the possibilities starts with a receive step (with the same variable). Here, the intruder can choose an arbitrary recipe $r$ (over the domain of the ${s t r u c t}_{i}$ ) for the message that should be received as $M$ . In fact, in general, we have here infinitely many possible $r$ and thus infinitely many successors. (Our decision procedure uses a constraint-based approach to handle this in a finite way.) Note that the message that is being received depends on the possibility: it is ${s t r u c t}_{i} (r)$ in the $i$ th possibility, that is, whatever the recipe $r$ yields in the respective intruder knowledge ${s t r u c t}_{i}$ . As the intruder knowledge at this point is empty in the example, $r$ can only be a recipe built from public constants and functions. Let us consider $r = c r y p t (p k (s), a, h (a))$ , which then replaces $M$ in the process. This leads to state $4$ .

Cell read and write. The running example does not use memory cells, and we describe briefly the rules here. When reading from the memory, we add conditional statements to substitute in the process the appropriate value from the memory (that depends on the argument term). When writing to the memory, the update is simply prepended to the sequence of memory updates $δ$ .

Conditional statement. The process is now $t r y N := \dots i n i f \dots c a t c h 0$ . For the sake of this semantics, we can just consider $t r y X := t i n P_{1} c a t c h P_{2}$ as a syntactic sugar for $i f t ≐ f f t h e n P_{2} e l s e P_{1} [X \mapsto t]$ (for the decision procedure it is important that destructors only occur in this $t r y$ - $c a t c h$ form, however). We have to evaluate the condition $d c r y p t (i n v (p k (s)), c r y p t (p k (s), a, h (a))) ≐ f f$ , which we can simplify to $f a l s e$ , that is, the intruder knows that the received message will decrypt correctly. We thus have in state $5$ two possibilities of which the second is underlined and where $N$ has been substituted with the content of the encryption, that is, the constant $a$ . The Eliminate rule allows removing possibilities with the condition $f a l s e$ , so we reach state $6$ . The underlined possibility is what really happened (which is here obvious). We apply a second time the Conditional rule, again splitting into two possibilities and leading to state $7$ . The first possibility is what really happens (as stated by $γ$ ) and is thus underlined, and here the intruder does not know which one is the case.

Fresh constants. The $ν$ operator can be implemented by replacing the placeholder with a fresh non-public constant, say $r_{1}$ . We can in fact do this as a preparation before executing the transaction.

Send. When all the rules for the other constructs have been applied as far as possible, each of the remaining processes must be either a send or $0$ . If the intruder observes that a message is sent, this rules out all possibilities where the remaining process is $0$ (the counterpart is the transition for Terminate). For all others, each ${s t r u c t}_{i}$ is augmented by the message sent in the respective possibility. Moreover, $β_{0}$ is updated with the disjunction of the $ϕ_{i}$ that are consistent with the intruder observations. In our example, we reach state $8$ , where $c o n c r (l) = c r y p t (p k (a), p a i r (y e s, a), r_{1})$ . We have reached a finished state, and the intruder has thus completed the symbolic execution of this transaction.

Example 2.2

Let us point out a few more interesting features of our running example. At the finished state, without further knowledge, the intruder is unable to tell which of the two possibilities is the case. This would be different if the encryption were not randomized: suppose we drop the third argument of $c r y p t$ . Then the intruder could now construct $c r y p t (p k (x^{'}), n o)$ for each value $x^{'} \in A g e n t$ and compare the result with the observed message. Since this does not succeed in any case, the intruder learns that the second possibility is excluded, thus $y ≐ y e s$ , violating $(α, β)$ -privacy. Even worse, if we look at the state where the non-deterministic choice was $y = n o$ , the intruder would find out $x$ because exactly one of the guesses succeeds.

Reverting to randomized encryption, suppose that there had been an earlier transaction where the intruder observed $l^{'} \mapsto c r y p t (p k (z), n o, r_{2})$ for some privacy variable $z \in A g e n t$ . If the intruder uses this as input for the next transaction, then the decryption works iff $z ≐ s$ . Thus, we have a third possibility at the final sending step, namely $(0, z ≐̸ s, l^{'} \mapsto c r y p t (p k (z), n o, r_{2}), [])$ . Then from the fact that a message was sent, the intruder can rule out this third possibility and thus deduce that $z ≐ s$ , again violating $(α, β)$ -privacy.

Release. This construct is used to declare information that the intruder is now allowed to learn, for instance in some cases we may let the intruder learn the true value of a privacy variable. In our running example, we did not use the release. However, in case the server is replying to the intruder, then the intruder can decrypt the message and observe what was the decision. Thus they would learn both the value of $x$ (i.e. the agent was the intruder) and $y$ (i.e. they know the server’s decision), which would violate $(α, β)$ -privacy. We could thus add a release if $x$ is the intruder to allow this deduction.

We consider it a specification error if when applying the Release rule, the formula $ϕ$ released contains symbols which are in $Σ ∖ Σ_{0}$ and variables not in $f v (α)$ . Thus, the specification can use symbols from the technical level in a release as long as the evaluated terms use only symbols in $Σ_{0}$ and $f v (α)$ (i.e. the payload level) when executing the protocol. This means that releasing technical information in the payload is not allowed. Additionally for our decision procedure below, the same requirement applies to a relational formula $R (t_{1}, \dots, t_{n})$ in the symbolic execution of conditional statements. This kind of specification error can be detected during the symbolic execution and means that insufficient checks are made over the terms before the release or conditional statement.

2.3. Privacy as reachability

We have defined in Table 1 the relation $\to$ that works off the steps of a transaction, modeling an intruder’s symbolic execution of a transaction $P$ . We now define a transition relation $⟶$ on finished states (i.e. the process in every possibility is $0$ ) such that $S ⟶ S^{'}$ iff there is a transaction $P$ such that $s t a r t (P, S) \to^{*} S^{'}$ , where $s t a r t (P, S)$ denotes replacing the $0$ -process in every possibility of $S$ with process $P$ . Then one transition with relation $⟶$ means executing exactly one transaction. Let the initial state be $S_{0} = (t r u e, t r u e, γ_{0}, {\underline{(0, t r u e, [], [])}})$ .

Definition 2.4 (The reachability problem)

Let $k \geq 0$ . A protocol specification satisfies privacy until bound $k$ iff $(α, β)$ -privacy holds for every $S$ and $i \in {0, \dots, k}$ such that $S_{0} ⟶^{i} S$ .

A protocol specification satisfies privacy iff for every $k \geq 0$ , it satisfies privacy until bound $k$ .

The first contribution of the present article is a procedure to solve the reachability problem given a bound $k$ , that is, whether a violation is reachable in at most $k$ transitions, under the restriction of the algebraic properties to constructor/destructor theories of Definition 6.1.

3. FLICs: Framed lazy intruder constraints

The semantics of the transition system says that, in a state where the processes are receiving a message, the intruder can choose any recipe built on the domain of $c o n c r$ (respectively, the ${s t r u c t}_{i}$ : they all have the same domain). The problem is that there are in general infinitely many recipes the intruder can choose from. A classic technique for deciding such infinite spaces of intruder possibilities is a constraint-based approach that we call the lazy intruder^9,29,30: it is lazy in that it avoids, as long as possible, instantiating the variables of receive steps like $r c v (X)$ . The concrete intruder choice at this point does not matter; only when we check a condition that depends on $X$ , we consider possible instantiations of $X$ as far as needed to determine the outcome of the condition. Note that this is another symbolic layer of our approach: a symbolic state with variable $X$ represents all concrete states where $X$ is replaced with a message that the intruder can construct. In fact what the intruder can construct depends on the messages the intruder knew at the time when the message represented by $X$ was sent. Due to the symbolic execution, in a state there are in general several ${s t r u c t}_{i}$ , and thus we need to represent not only the messages sent by the intruder with variables but also the recipes that they have chosen, because a given recipe can produce different messages in each ${s t r u c t}_{i}$ .

To keep track of this, we define an extension of frames called framed lazy intruder constraints (FLICs): the entries of a standard frame represent messages that the intruder received and we write them now with a minus sign: $- l \mapsto t$ . We extend this by also writing entries for messages the intruder sends with a plus sign: $+ R \mapsto t$ , where $R$ is a recipe variable (disjoint from privacy and intruder variables). When solving the constraints, $R$ may be instantiated with a more concrete recipe, but only using labels that occurred in the FLIC before this receive step; the order of the entries is thus significant. The messages $t$ can contain variables representing intruder choices that we have not yet made concrete. We require that the intruder variables first occur in positive entries as they represent intruder choices made when sending a message.

Since we deal with several possibilities in parallel, we will have several FLICs in parallel, replacing the ${s t r u c t}_{i}$ in the ground model. Each FLIC has the same sequence of incoming labels and outgoing recipes. The intruder does not know in general which possibility is the case, but knows how they constructed messages from their knowledge, that is, the same recipe may result in a different message in each possibility.

A FLIC is a constraint, namely that the intruder can indeed produce messages of the form needed to reach a particular state of the execution. We show that we can solve such FLICs, that is, find a finite representation of all solutions (as said before, there are in general infinitely many possible concrete choices) using the lazy intruder technique, similarly to other works doing constraint-based solving with frames such as Cheval et al.^7,31 In the rest of this section, we focus on defining and solving constraints by considering just one FLIC and not the rest of the possibilities, and we will explain in Section 4 how the lazy intruder is used for the transition system with several possibilities.

3.1. Defining constraints

Definition 3.1 (FLIC)

A framed lazy intruder constraint (FLIC) $A$ is a sequence of mappings of the form $- l \mapsto t$ or $+ R \mapsto t$ , where each label $l$ and recipe variable $R$ occurs at most once, each term $t$ is built from function symbols, privacy variables, and intruder variables. The first occurrence of each intruder variable must be in a message sent.

We write $- l \mapsto t \in A$ if $- l \mapsto t$ occurs in $A$ , and similarly $+ R \mapsto t \in A$ . The domain $d o m (A)$ is the set of labels of $A$ and $v a r s (A)$ are the privacy and intruder variables that occur in $A$ ; similarly, we write $r v a r s (A)$ for the recipe variables.

The message $A (r)$ produced by $r$ in $A$ is: $A (l) = t$ if $- l \mapsto t \in A$ , $A (R) = t$ if $+ R \mapsto t \in A$ and $A (f (r_{1}, \dots, r_{n})) = f (A (r_{1}), \dots, A (r_{n}))$ .

For recipes that use labels or recipe variables not defined in the FLIC, the result is undefined. We also define an ordering between recipes and labels: $r <_{A} l$ iff every label $l^{'}$ in $r$ occurs before $l$ in $A$ .

Example 3.1
Consider the transaction from Example 2.1, step $r c v (M)$ . Using FLICs, we add $+ R \mapsto M$ to the FLIC (where both $R$ and $M$ are fresh variables). We are lazy in the sense that we do not explore at this point what $R$ and $M$ might be, because any value would do. Now the server checks whether $M$ can be decrypted with the private key $i n v (p k (s))$ . This is the case iff $M$ has the form $c r y p t (p k (s), \cdot, \cdot)$ (we will show in Section 4 how exactly the $t r y$ - $c a t c h$ construct works in the presence of the lazy intruder). In the positive case, $M$ is instantiated with $c r y p t (p k (s), X, Y)$ for two fresh intruder variables $X$ and $Y$ , thus requiring that $R$ indeed yields a message of this form. The constraint solving in Section 3.2 computes a finite representation of all solutions for $R$ . The negative case is considered separately, where we remember the negated equality $M ≐̸ c r y p t (p k (s), \cdot, \cdot)$ .
Definition 3.2 (Semantics of FLICs)

Let $A$ be a FLIC such that $v a r s (A) = \emptyset$ , that is, the messages in $A$ are ground, so $A$ has only recipe variables. $A$ is constructible iff there exists a ground substitution of recipe variables $ρ_{0}$ such that $A_{1} (ρ_{0} (R)) \approx t$ for every recipe variable $R$ , where $A = A_{1} . + R \mapsto t . A_{2}$ (this implies that only labels from $d o m (A_{1})$ can occur in $ρ_{0} (R)$ ). We then say that $ρ_{0}$ constructs $A$ .

Let $A$ be an arbitrary FLIC and $I$ be an interpretation of all privacy and intruder variables. We say that $I$ is a model of $A$ , written $I | \equiv A$ , iff $I (A)$ is constructible. $A$ is satisfiable iff it has a model.

A FLIC is thus satisfiable if there exist a suitable interpretation for the variables in messages and a suitable intruder choice for the variables in recipes such that all the constraints are satisfied.

Example 3.2
Suppose that Alice sent a signed message $m$ to the intruder $i$ and the constraint is to send some signed message to Bob. This is recorded in the following FLIC $A$ :
${- l}_{1} \mapsto i n v (p k (i)) . {- l}_{2} \mapsto c r y p t (p k (i), s i g n (i n v (p k (a)), m)) . + R \mapsto c r y p t (p k (b), s i g n (i n v (p k (X)), Y))$
Here $I_{1} = [X \mapsto a, Y \mapsto m]$ is a model, because $I_{1} (A)$ is constructible using the recipe $R = c r y p t (p k (b), d c r y p t (l_{1}, l_{2}))$ . For every ground recipe $r$ over $d o m (A)$ also $I_{r} = [X \mapsto i, Y \mapsto A (r)]$ is a model, using $R = c r y p t (p k (b), s i g n (l_{1}, r))$ ; note there are infinitely many such $r$ .
3.2. Solving constraints

We now present how to solve constraints when the intruder does not have access to destructors, that is, as if all destructors were private functions and thus cannot occur in recipes. Hence the only place where destructors can occur are in transactions using $t r y$ - $c a t c h$ . This allows us to work in the free algebra for now and with only destructor-free terms. To achieve the correctness of our procedure for the full intruder model with access to destructors, we show in Section 6 how all intruder applications of destructors can be handled by special analysis steps. This allows us to keep the core of the method free of destructors and algebraic reasoning.

Definition 3.3 (Simple FLIC)

A FLIC $A$ is called simple iff every message sent is an intruder variable, and each intruder variable is sent only once, that is, every message sent is of the form $+ R_{i} \mapsto X_{i}$ and the $X_{i}$ are pairwise distinct.

Simple FLICs are always satisfiable, since there are no more constraints on the messages, and the intruder can choose any recipes they want. In order to solve constraints in a non-simple FLIC, we instantiate privacy, intruder and recipe variables until we reach a simple FLIC. Computing a finite representation of all solutions is then done by keeping track of the substitutions applied to instantiate the variables.

Definition 3.4
Let $σ$ be a substitution that does not contain recipe variables. We define $σ (- l \mapsto t . A) = - l \mapsto σ (t) . σ (A)$ and $σ (+ R \mapsto t . A) = + R \mapsto σ (t) . σ (A)$ .

However, we cannot directly define the instantiation of recipe variables for an arbitrary FLIC, because we always need to make sure we instantiate both the recipe and the intruder variables according to the constraints. We thus define how to apply a substitution of recipe variables for simple FLICs.
Definition 3.5 (Choice of recipes)

A choice of recipes for a simple FLIC $A$ is a substitution $ρ$ mapping recipe variables to recipes, where $d o m (ρ) \subseteq r v a r s (A)$ .

Let $[R \mapsto r]$ be a choice of recipes for $A$ that maps only one recipe variable, where $A = A_{1} . + R \mapsto X . A_{2}$ . Let $R_{1}, \dots, R_{n}$ be the fresh variables in $r$ , that is, ${R_{1}, \dots, R_{n}} = r v a r s (r) ∖ r v a r s (A)$ , taken in a fixed order (e.g. the order in which they first occur in $r$ ). Let $X_{1}, \dots, X_{n}$ be fresh intruder variables. The application of $[R \mapsto r]$ to the FLIC $A$ is defined as $[R \mapsto r] (A_{1} . + R \mapsto X . A_{2}) = A^{'} . σ (A_{2})$ where $A^{'} = A_{1} . + R_{1} \mapsto X_{1} . \dots . + R_{n} \mapsto X_{n}$ and $σ = [X \mapsto A^{'} (r)]$ .

For the general case, let $ρ$ be a choice of recipes for $A$ . We define $ρ (A)$ recursively where one recipe variable is substituted at a time, and we follow the order in which the recipe variables occur in $A$ : if $ρ = [R \mapsto r] ρ^{'}$ , where $R$ occurs in $A$ before any $R^{'} \in d o m (ρ^{'})$ , then $ρ (A) = ρ^{'} ([R \mapsto r] (A))$ . Every application $[R \mapsto r] (A)$ corresponds to a substitution $σ = [X \mapsto A^{'} (r)]$ (as defined above), and we denote with $σ_{ρ}^{A}$ the idempotent substitution aggregating all these substitutions $σ$ from applying $ρ$ to $A$ .

Note that if $ρ$ is a choice of recipes for a simple FLIC $A$ , then $ρ (A)$ is simple, because the fresh recipe variables added in $ρ (A)$ map to fresh intruder variables.

We denote with $m g u (s_{1} ≐ t_{1} \land \dots \land s_{n} ≐ t_{n})$ the result, called most general unifier (mgu), of unifying the $s_{i}$ and $t_{i}$ , which is either some substitution or $⊥$ whenever no unifier exists. Slightly abusing notation, we consider a substitution $[x_{1} \mapsto t_{1}, \dots, x_{n} \mapsto t_{n}]$ as the formula $x_{1} ≐ t_{1} \land \dots \land x_{n} ≐ t_{n}$ and $⊥$ as $f a l s e$ . We modify the standard mgu algorithm so that when we have to unify an intruder variable $X$ with a privacy variable $x$ , it will always result in $[X \mapsto x]$ (i.e. privacy variables are never substituted with intruder variables).

Moreover, we add a postprocessing step to $m g u$ : if the resulting $σ$ contains $x \mapsto c$ where $x$ is a privacy variable chosen from a domain $D$ that does not contain $c$ , then the result is $⊥$ .

In order to solve the constraints, we define a reduction relation $⇝$ on FLICs: $⇝$ is Noetherian and a FLIC that cannot be further reduced is either simple or unsatisfiable. Moreover, $⇝$ is not confluent, but rather is meant to explore different ways for the intruder to satisfy constraints, and thus we will consider the set of all simple FLICs that are reachable from a given one: the simple FLICs together will be equivalent to the given FLIC. Since $⇝$ is not only Noetherian, but also finitely branching, the set of reachable simple FLICs is always finite by König’s lemma.

Definition 3.6 (Lazy intruder rules)

The relation

⇝

is a relation on triples

(ρ, A, σ)

of a choice of recipes

ρ

, a FLIC

A

and a substitution

σ

, where

ρ

and

σ

keep track of all variable substitutions performed in the reduction steps so far and are such that

d o m (ρ) \cap r v a r s (A) = \emptyset

and

d o m (σ) \cap v a r s (A) = \emptyset

. The rules are defined in Table 3.

Table 3.
Lazy intruder rules.

Unification	$(ρ, A_{1} . - l \mapsto s . A_{2} . + R \mapsto t . A_{3}, σ) ⇝ (ρ^{'}, σ^{'} (A_{1} . - l \mapsto s . A_{2} . A_{3}), σ^{'})$	if $A_{1} . - l \mapsto s . A_{2}$ is simple,
	where $ρ^{'} = [R \mapsto l] ρ$ and $σ^{'} = m g u (σ \land s ≐ t)$	$s, t \notin V$ and $σ^{'} \neq ⊥$
Composition	$(ρ, A_{1} . + R \mapsto f (t_{1}, \dots, t_{n}) . A_{2}, σ)$	if $A_{1}$ is simple, $f \in Σ_{p u b}$
	$⇝ (ρ^{'}, A_{1} . + R_{1} \mapsto t_{1} . \dots . + R_{n} \mapsto t_{n} . A_{2}, σ)$	and $σ \neq ⊥$
	where the $R_{i}$ are fresh recipe variables and $ρ^{'} = [R \mapsto f (R_{1}, \dots, R_{n})] ρ$
Guessing	$(ρ, A_{1} . + R \mapsto x . A_{2}, σ) ⇝ (ρ^{'}, σ^{'} (A_{1} . A_{2}), σ^{'})$	if $A_{1}$ is simple, $c \in d o m (x)$
	where $ρ^{'} = [R \mapsto c] ρ$ and $σ^{'} = m g u (σ \land x ≐ c)$	and $σ^{'} \neq ⊥$
Repetition	$(ρ, A_{1} . + R_{1} \mapsto X . A_{2} . + R_{2} \mapsto X . A_{3}, σ)$	if $A_{1} . + R_{1} \mapsto X . A_{2}$ is simple
	$⇝ (ρ^{'}, A_{1} . + R_{1} \mapsto X . A_{2} . A_{3}, σ)$	and $σ \neq ⊥$
	where $ρ^{'} = [R_{2} \mapsto R_{1}] ρ$

Unification. When the intruder has to send a message, they can use any message previously received and that unifies, choosing a label for the recipe variable. There is one less message to send, but the unifier might make other constraints non-simple. This rule is not applicable for variables: the intruder is lazy.

Composition. When the intruder has to send a composed message $f (t_{1}, \dots, t_{n})$ , they can generate it themselves if $f$ is public and they can generate the $t_{i}$ . The intruder thus chooses to compose the message themselves, so the recipe $R$ is the application of $f$ to other recipes.

Guessing. When the intruder has to send a privacy variable $x$ , they can guess the actual value of $x$ , say $c$ . In fact, this is a guessing attack as we let the privacy variables range over small domains of public constants. This rule represents the case that the intruder guesses correctly, and the variable $x$ is replaced by the guessed value $c$ . Note that using the Guessing rule does not yet mean that the intruder knows that $c$ is the correct guess: in the rest of the procedure, whenever there is such a guess we model both the right and wrong guesses, and the intruder may not be able to tell what is the case.

Repetition. If the intruder has to send an intruder variable that they have already sent earlier, they use the same recipe. Since there may be several ways to generate the same message, one may wonder if this is actually complete: could there be an attack where constructing the same message in two different ways would tell the intruder anything more? In fact, for what concerns the behavior of the honest agents, it cannot make a difference, and comparing different ways to construct the same message is covered in the intruder experiments in Section 5.

We now define the lazy intruder results as the set of choices of recipes $ρ$ that solve the constraints.

Definition 3.7 (Lazy intruder results)

Let $A$ be a FLIC and $σ$ be a substitution. Let $ε$ be the identity substitution. We define $L I (A, σ) = {ρ ∣ (ε, σ (A), σ) ⇝^{*} (ρ, A^{'},_) and A^{'} is simple}$ .

Example 3.3
Following Example 3.1, let us assume that the intruder has already observed a message encrypted for the server from another agent $x^{'}$ , and is now symbolically executing the transaction. With the constraint induced by the decryption from the server, the FLIC is now $- l \mapsto c r y p t (p k (s), x^{'}, r) . + R \mapsto c r y p t (p k (s), X, Y)$ . Since $p k$ is public, the lazy intruder returns two choices of recipes: $ρ_{1} = [R \mapsto l]$ , meaning the intruder replays the message from the knowledge (since it unifies), and $ρ_{2} = [R \mapsto c r y p t (p k (s), R_{1}, R_{2})]$ , meaning the intruder composes the message themselves where $R_{1}$ and $R_{2}$ stand for arbitrary recipes.
Definition 3.8 (Representation of choice of recipes)

Let $A$ be a FLIC, $I | \equiv A$ , $ρ_{0}$ be a ground choice of recipes and $ρ$ be a choice of recipes. We say that $ρ$ represents $ρ_{0}$ w.r.t. $A$ and $I$ iff there exists $ρ_{0}^{'}$ such that $ρ_{0}^{'}$ is an instance of $ρ$ and for every $R \in r v a r s (A)$ , $I (A) (ρ_{0}^{'} (R)) = I (A) (ρ_{0} (R))$ and:

If $ρ (R) \in d o m (A)$ , then $ρ_{0} (R) \in d o m (A)$ and either $ρ_{0}^{'} (R) = ρ_{0} (R)$ or $ρ_{0}^{'} (R) <_{A} ρ_{0} (R)$ .

If $ρ (R)$ is a composed recipe and $ρ_{0} (R) \in d o m (A)$ , then $ρ_{0}^{'} (R) <_{A} ρ_{0} (R)$ .

This notion of representation gives the lazy intruder some “liberty,” namely to be lazy in not instantiating recipe variables that do not matter, and to replace subrecipes with equivalent ones (that may be smaller according to our ordering between recipes and labels). In the completeness proof we show that, despite all these liberties, every solution of the constraint is represented by some choice of recipes that the lazy intruder finds. The lazy intruder rules are sound, complete and terminating.

Theorem 3.1 (Lazy intruder correctness)

Let $A$ be a FLIC, $σ$ be a substitution, $I | \equiv A$ such that $I ╞_{Σ} σ$ and let $ρ_{0}$ be a ground choice of recipes. Then $ρ_{0}$ constructs $I (A)$ iff there exists $ρ \in L I (A, σ)$ such that $ρ$ represents $ρ_{0}$ w.r.t. $A$ and $I$ . Moreover, $L I (A, σ)$ is finite.

4. The symbolic states

Our approach explores a transition system on symbolic states, where each symbolic state represents an infinite set of ground states. In the rest of the article, we denote symbolic states by $S$ , $S^{'}$ , and so on, and ground states by $S$ , $S^{'}$ , and so on.

Our notion of ground states in Section 2 is an adaptation of the states defined by Gondron et al.¹ A ground state may actually contain privacy variables, representing the possible uncertainty of the intruder in this state, but each variable has one concrete value that represents the truth in that state, which is expressed by a formula $γ$ that the intruder does not have access to (and the frame $c o n c r$ is an instance of one of the ${s t r u c t}_{i}$ under $γ$ ). This is the reason why we call it a ground state, even though it contains variables. A symbolic state includes actually two symbolic layers. For the first symbolic layer, we define a symbolic state to merge all those ground states that differ only in the concrete $γ$ and thus the concrete frame $c o n c r$ , that is, where the intruder has the same uncertainty. Therefore, a symbolic state does not contain $γ$ and $c o n c r$ , and has no underlined possibility. Thus, we need to keep track of the released formula $α_{i}$ for each possibility separately. A second symbolic layer is to use intruder variables and FLICs to avoid enumerating the infinite choices that the intruder has when sending messages, thus the frames ${s t r u c t}_{i}$ are generalized to FLICs $A_{i}$ in symbolic states. We will introduce in Section 5 the intruder experiments, and a symbolic state $S$ contains a record of all experiments the intruder has already performed.

Definition 4.1 (Symbolic state)

A symbolic state is a tuple $(α_{0}, β_{0}, P, C h e c k e d)$ such that:

$α_{0}$ is a $Σ_{0}$ -formula, the common payload;

$β_{0}$ is a $Σ_{0}$ -formula, the intruder reasoning about possibilities and privacy variables;

$P$ is a set of possibilities, which are each of the form $(P, ϕ, A, X, α, δ)$ , where $P$ is a process, $ϕ$ is a $Σ_{0}$ -formula, $A$ is a FLIC, $X$ is a disequalities formula (in the grammar below), $α$ is a $Σ_{0}$ -formula called partial payload, and $δ$ is a sequence of memory updates of the form $c e l l [s] := t$ for messages $s$ and $t$ ;

$C h e c k e d$ is a set of pairs $(l, r)$ , where $l$ is a label and $r$ is a recipe.

where disequalities formulas are of the following form:

X := X \land X ∣ \forall \vec{X} . \neg X_{0} Disequalities formula X_{0} := X_{0} \land X_{0} ∣ t ≐ t Equalities formula

A symbolic state is finished iff all the processes in

P

are

0

We may write $S [e \leftarrow e^{'}]$ to denote the symbolic state identical to $S$ except that $e$ is replaced with $e^{'}$ .

We have augmented the FLICs $A_{i}$ here with disequalities $X_{i}$ , that is, negated equality constraints, which allows us to restrict the choices of the intruder in a symbolic state. This is needed when we want to make a split between the case that the intruder makes a particular choice and the case that they choose anything else. This is formalized in the following definition of applying a recipe substitution which is only possible when all the respective $X_{i}$ are consistent with it:

Definition 4.2 (Choice of recipes for a symbolic state)

Let $S = (_,_, P, C h e c k e d)$ be a symbolic state and $ρ$ be a recipe substitution. We say that $ρ$ is a choice of recipes for $S$ iff $ρ$ is a choice of recipes for all FLICs in $P$ and for every FLIC $A$ and associated disequalities $X$ in $P$ , the formula $σ_{ρ}^{A} (X)$ is satisfiable, that is, the disequalities are satisfiable under the substitution induced by $ρ$ in $A$ (Definition 3.5). Moreover, we define

\begin{aligned} ρ (P) = & {(σ_{ρ}^{A} (P), ϕ, ρ (A), σ_{ρ}^{A} (X), α, σ_{ρ}^{A} (δ)) ∣ (P, ϕ, A, X, α, δ) \in P} \\ ρ (C h e c k e d) = & {(l, ρ (r)) ∣ (l, r) \in C h e c k e d} \\ ρ (S) = & S [P \leftarrow ρ (P), C h e c k e d \leftarrow ρ (C h e c k e d)] \end{aligned}

When writing $ρ (S)$ in the following, we implicitly assume that all disequalities in $S$ are satisfiable under $ρ$ , and that $ρ (S)$ is discarded otherwise. To decide whether disequality $X$ is satisfiable it suffices to replace the free variables with distinct fresh constants and check that the corresponding unification problems have no solution. Moreover, we will always use the lazy intruder in the context of a symbolic state, so we further assume that $L I (\cdot, \cdot)$ only returns choices of recipes for the current symbolic state, that is, excluding any $ρ$ that would contradict a disequality.

From a symbolic state we can define all the choices of recipes (instantiations of the recipe and intruder variables) for the messages sent by the intruder and all the concrete executions (instantiations of privacy variables) that the intruder considers possible. A symbolic state represents a set of ground states, where each ground state corresponds to one multi message-analysis problem. For every ground state, the common payload $α_{0}$ is augmented with the partial payload $α_{i}$ released in the corresponding possibility. Moreover, every model $γ$ of the privacy variables needs to be augmented with the fixed interpretation $γ_{0}$ of the relation symbols (recall that this $Σ_{0}$ -formula $γ_{0}$ is part of the protocol specification).

Meta-notation. In the specification of transactions, we allow in the release steps $⋆ ϕ$ the use of the meta-notation $γ (t)$ for a message $t$ . Recall that in every ground state, the real values of privacy variables is defined by a ground interpretation $γ$ . Thus, for instance, releasing $⋆ x ≐ γ (x)$ means allowing the intruder to learn the true value of $x$ . In the symbolic execution for ground states, the meta-notation can be resolved by using $γ$ as a substitution before adding the formula to $α$ .

Example 4.1
In Example 2.1, in case the agent $x$ is actually the intruder $i$ , that is, $x ≐ i$ , then the intruder can decrypt the message and observe what was the decision. Thus they would learn both that $x ≐ i$ as well as the value of $y$ (i.e. they know the server’s decision). This leads to a privacy violation, unless we declassify $x$ and $y$ by releasing, if $x$ is the intruder, the formula $⋆ x ≐ γ (x) \land y ≐ γ (y)$ . Releasing this information is still not enough because in case $x ≐̸ i$ the intruder can also deduce that; so we additionally need to release $⋆ x ≐̸ i$ in that case to remove the privacy violation.

In a symbolic state, however, there is no $γ$ since the symbolic state represents all possible $γ$ at once. Hence, in order to define the semantics, we need to resolve the meta-notation that we allow in the $α_{i}$ . Given $α_{i}$ and the truth $γ$ , let $[α_{i}]^{γ}$ be the instantiation of the meta-notation in $α_{i}$ , that is, replacing every occurrence of a term $γ (x)$ in $α_{i}$ (for a variable $x$ ) with the actual value of $x$ in the given $γ$ . For instance, if $γ (x) = i$ , then $[x ≐ γ (x)]^{γ} = x ≐ i$ .
Definition 4.3 (Semantics of symbolic states)

Let $S = (α_{0}, β_{0}, P,_)$ be a finished symbolic state. The ground states represented by $S$ are given by

\begin{aligned} [[S]] = { & (α_{0} \land [α_{i}]^{γ}, β_{0}, γ, ρ (P)) ∣ (0, ϕ_{i}, A_{i},_, α_{i},_) \in P, ρ is a ground choice of recipes for S, \\ γ is a Σ_{0} -interpretation of α_{0} \land β_{0} \land γ_{0} \land ϕ_{i}} \end{aligned}

where

ρ (P)

returns possibilities of the form

(0, ϕ_{j}, {s t r u c t}_{j}, δ_{j})

, that is, the additional components of symbolic possibilities are dropped because they are irrelevant for ground states (note that the

α_{i}

have already been used as part of the payload

α

); moreover, the possibility for which

γ ╞ ϕ_{i}

is underlined.

We say that a symbolic state $S$ satisfies privacy iff every ground state $S \in [[S]]$ satisfies privacy.

When computing the mgu between messages or solving constraints with the lazy intruder rules, we may deal with substitutions that contain both privacy and intruder variables. However, it is important to remember that the instantiation of privacy variables does not depend on the intruder, it is actually the goal of the intruder to learn about the privacy variables. On the other hand, intruder variables are instantiated according to the recipes chosen by the intruder. Thus, we distinguish substitutions that only substitute privacy variables (we will compute substitutions as mgus so we also have to consider $⊥$ when no mgu exists).

Definition 4.4 (Privacy substitution)

Given a substitution $σ$ , the predicate $i s P r i v$ is defined as: $i s P r i v (σ)$ iff $d o m (σ) \subseteq V_{p r i v a c y}$ . We also define $\underline{σ}$ as the privacy part of $σ$ , that is, $\underline{σ} (x) = σ (x)$ if $x \in V_{p r i v a c y}$ , and $\underline{σ} (x) = x$ otherwise. Moreover, define $i s P r i v (⊥) = f a l s e$ and $\underline{⊥} = ⊥$ .

Table 4 defines the transitions on symbolic states to evaluate processes (with the lazy intruder) as a relation $S \Rightarrow C$ between one symbolic state $S$ and a set $C$ of symbolic states. We extend the definition to relate sets of symbolic states: $C \Rightarrow C^{'}$ iff $S \in C$ , $S \Rightarrow C_{S}$ and $C^{'} = C ∖ {S} \cup C_{S}$ . We summarize here this semantics and we discuss in Supplemental Appendix A the correctness of the correspondence to Table 1.

Table 4.
Semantics of the execution for symbolic states.

Choice $(α_{0}, β_{0}, {(m o d e x \in D . P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)$

$\Rightarrow {(α_{0}^{'}, β_{0}^{'}, {(P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)}$

where $α_{0}^{'} \equiv α_{0} \land x \in D$ and $β_{0}^{'} \equiv β_{0}$ if $m o d e = ⋆$ , and $α_{0}^{'} \equiv α_{0}$ and $β_{0}^{'} \equiv β_{0} \land x \in D$ if $m o d e = ⋄$

Receive $(α_{0}, β_{0}, {(r c v (X) . P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)$

$\Rightarrow {(α_{0}, β_{0}, {(P_{i}, ϕ_{i}, A_{i} . + R \mapsto X, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)}$

where $R$ is a fresh recipe variable

Cell read $(α_{0}, β_{0}, {(X := c e l l [s] . P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$

$\Rightarrow {(α_{0}, β_{0}, {(P^{'}, ϕ, A, X, α, δ)} \cup P, C h e c k e d)}$

where $δ_{| c e l l} = c e l l [s_{1}] := t_{1} . \dots . c e l l [s_{k}] := t_{k}$ , the initial value of $c e l l$ is given by ground context $C [\cdot]$

and $P^{'} = i f s ≐ s_{1} t h e n P [X \mapsto t_{1}] e l s e \dots i f s ≐ s_{k} t h e n P [X \mapsto t_{k}] e l s e P [X \mapsto C [s]]$

Cell write $(α_{0}, β_{0}, {(c e l l [s] := t . P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$

$\Rightarrow {(α_{0}, β_{0}, {(P, ϕ, A, X, α, c e l l [s] := t . δ)} \cup C h e c k e d)}$

Let $P = t r y X := d (t_{1}, t_{2}) i n P_{1} c a t c h P_{2}$ , consider a fresh instance $d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}$

of the rewrite rule for $d$ , let $ψ = t_{1} ≐ k \land t_{2} ≐ c (k^{'}, X_{1}, \dots, X_{n})$ , and $σ = m g u (ψ)$ .

The rules for $t r y$ - $c a t c h$ are:

$(α_{0}, β_{0}, {(P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$

Destructor (1.1) $\Rightarrow {ρ ((α_{0}, β_{0}, {(P_{1} [X \mapsto s_{i}], ϕ \land \underline{σ^{'}}, A, X, α, δ), (P_{2}, ϕ \land \neg \underline{σ^{'}}, A, X, α, δ)} \cup P, C h e c k e d))$

$∣ ρ \in L I (A, σ), let c (s_{0}, \dots, s_{n}) = σ_{ρ}^{A} (t_{2}) and σ^{'} = m g u (σ_{ρ}^{A} (ψ))}$

Destructor (1.2) $\cup {\begin{cases} {(α_{0}, β_{0}, {(P_{2}, ϕ, A, X \land \forall \vec{Y} . \neg σ, α, δ)} \cup P, C h e c k e d)} & if σ (A) is not simple \\ \emptyset & otherwise \end{cases}$

if $σ \neq ⊥$ , where $\vec{Y} = i v a r s (σ) ∖ i v a r s (A)$

Destructor (2) $(α_{0}, β_{0}, {(P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d) \Rightarrow {(α_{0}, β_{0}, {(P_{2}, ϕ, A, X, α, δ)} \cup P, C h e c k e d)}$

if $σ = ⊥$

Conditional $(α_{0}, β_{0}, {(i f R (t_{1}, \dots, t_{n}) t h e n P_{1} e l s e P_{2}, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$

$\Rightarrow {(α_{0}, β_{0}, {(P_{1}, ϕ \land R (t_{1}, \dots, t_{n}), A, X, α, δ), (P_{2}, ϕ \land \neg R (t_{1}, \dots, t_{n}), A, X, α, δ)} \cup P, C h e c k e d)}$

For $i f s ≐ t t h e n P_{1} e l s e P_{2}$ , the transitions are like Destructor but with $ψ \equiv_{Σ} s ≐ t$

Release $(α_{0}, β_{0}, {(⋆ ψ . P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d) \Rightarrow {(α_{0}, β_{0}, {(P, ϕ, A, X, α \land ψ, δ)} \cup P, C h e c k e d)}$

Eliminate $(α_{0}, β_{0}, {(P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d) \Rightarrow {(α_{0}, β_{0}, P, C h e c k e d)}$

if $α_{0} \land β_{0} ⧸ ╞ ϕ$

Send $(α_{0}, β_{0}, {(s n d (t_{i}) . P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}} ⊎ P, C h e c k e d)$

$\Rightarrow {(α_{0}, β_{0} \land ⋁_{i = 1}^{n} ϕ_{i}, {(P_{i}, ϕ_{i}, A_{i} . - l \mapsto t_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)}$

$\cup {(α_{0}, β_{0} \land ⋀_{i = 1}^{n} \neg ϕ_{i}, P, C h e c k e d)}$

if every process in $P$ is $0$ , where $l$ is a fresh label

The non-deterministic choice is quite simple: instead of splitting into one successor state for each value in the domain, all these are handled in one symbolic state where we only add the domain constraint to $α_{0}$ or $β_{0}$ , respectively. For a receiving step $r c v (X)$ , recall that the ground model has here an infinite branching over all the recipes that the intruder could use. This is the very reason for introducing the FLICs in the symbolic model: we simply choose a fresh recipe variable $R$ and augment every FLIC with $+ R \mapsto X$ , saying that the intruder can choose any recipe $R$ (over the labels of the FLIC so far) to form the input message $X$ .

Due to the two symbolic representations of privacy choices and intruder choices, treating $t r y$ - $c a t c h$ is quite complicated. Consider a symbolic state $S$ where one possibility has process $t r y X := d (t_{1}, t_{2}) i n P_{1} c a t c h P_{2}$ . The class of algebraic theories we support (we give the precise definition in Definition 6.1) ensures that there is a unique rewrite rule for destructor $d$ . Let $d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}$ be a fresh instance of this rule (all variables renamed to fresh intruder variables). The destructor succeeds iff the formula $ψ = t_{1} ≐ k \land t_{2} ≐ c (k^{'}, X_{1}, \dots, X_{n})$ is satisfied. Let $σ = m g u (ψ)$ ; note that this mgu may not exist ( $σ = ⊥$ ). Note also that $σ$ may instantiate both privacy variables (that the intruder cannot control) and all the other variables (that the intruder can, at least indirectly, control by the choice of recipes for messages received). We now have several symbolic states for the different cases.

Destructor (1.1) is the case that there is a solution ( $σ \neq ⊥$ ) and the intruder makes a choice of recipes $ρ \in L I (A, σ)$ that may satisfy $σ$ . Note that $ρ$ can only determine intruder variables: it induces a substitution $σ_{ρ}^{A}$ in the given possibility (Definition 3.5). It is now guaranteed that $σ_{ρ}^{A} (t_{2})$ yields a term of the form $c (s_{0}, \dots, s_{n})$ , because we had required this in $ψ$ and $t_{2}$ cannot be a privacy variable. Thus we can now extract the exact term $s_{i}$ in case the destructor works. Whether it works depends however on the privacy variables. For instance if the destructor is asymmetric description with key $i n v (p k (a))$ and the intruder chooses a message encrypted with $p k (x)$ , this succeeds iff $x ≐ a$ . We thus need to compute a unifier $σ^{'}$ for $σ_{ρ}^{A} (ψ)$ , that is, the condition under the current choice of recipes, and $\underline{σ^{'}}$ is now the substitution of privacy variables under which the destructor succeeds. We thus split the possibility in two: one where we continue with $P_{1}$ , where $X$ is bound to the result $s_{i}$ of the destructor and condition $\underline{σ^{'}}$ , and one with $P_{2}$ and condition $\neg \underline{σ^{'}}$ .

Destructor (1.2) is the case that there is a solution ( $σ \neq ⊥$ ) and it depends on intruder choices ( $σ (A)$ is not simple), but the intruder chooses any recipe that does not satisfy $σ$ . For this we simply add the disequality $\forall \vec{Y} . \neg σ$ to $X$ , where $\vec{Y}$ are the intruder variables not bound by $A$ . (If $σ (A)$ is simple, then there is only one trivial choice of recipes, the identity substitution, so there is no symbolic state for excluding this choice.) Destructor (2) finally is the case that there is no unifier $σ$ , so we necessarily end up in $P_{2}$ .

The $i f$ - $t h e n$ - $e l s e$ conditional is handled in a very similar way when the condition is an equality $s ≐ t$ , obtaining a most general unifier $σ = m g u (s ≐ t)$ under which the condition is true. When the condition is a relation applied to some terms, we simply split on whether the relation holds. For a condition with negation, we swap the branches: $i f \neg ϕ t h e n P e l s e Q$ is rewritten into $i f ϕ t h e n Q e l s e P$ . For conjunction, we nest the branches: $i f ϕ \land ψ t h e n P e l s e Q$ is rewritten into $i f ϕ t h e n i f ψ t h e n P e l s e Q e l s e Q$ .

For releasing $α$ information, recall that we have an $α_{i}$ in each possibility that we can augment with the formula released. For sending or terminating, compared to Table 1 we merge the two rules so one symbolic state yields in general two symbolic states, one where we only keep the possibilities that send a message and one where we only keep those already terminated.

During the symbolic execution, if a symbolic state has an empty set of possibilities, then this state is discarded since it does not represent any ground state (e.g. in the Send rule, if $P = \emptyset$ then the second state yielded by the rule is discarded). Moreover, if several rules are applicable at the same time, then it does not matter which one is applied first so the procedure fixes an arbitrary order for applying the rules.

The symbolic executions transform a symbolic state into a set of finished symbolic states. When all symbolic executions have terminated, we shall check whether the reached symbolic states satisfy privacy.

5. The intruder experiments

So far, we have a symbolic transition relation that, for a given symbolic state and protocol transaction, gives a finite number of symbolic states that can be reached by executing the transaction. This notion includes the intruder’s reasoning about what is potentially happening, namely whether conditions and try-statements are satisfied, depending on the intruder choices and the privacy variables. The FLICs in these states are simple, that is, the constraints are solved and thus every remaining intruder variable represents an arbitrary message from the intruder’s knowledge—the truth value of any conditions executed previously did not depend on the concrete choice of message.

Now we come to the next step: the intruder can make experiments by choosing two recipes and checking for each FLIC, if the two recipes give the same message in that FLIC. If that outcome is not the same in every FLIC, the intruder can thus distinguish some FLICs. This may allow the intruder to rule out some possibilities or some models of the privacy variables, and this may lead to a violation of $(α, β)$ -privacy. Since terms can contain privacy and intruder variables, the outcome of the experiment may depend on the value of such variables.

The intruder variables are due to our symbolic approach: the intruder has chosen a concrete recipe earlier, and a symbolic state only represents several such concrete states (in general infinitely many). When we now evaluate the intruder experiments and the outcome depends on an intruder variable, then we will split the symbolic state into several states: states where the intruder made a particular choice of messages (that makes a comparison true in some FLIC), and one state where the intruder made any other choice. Together these symbolic states represent the same concrete states.

We show in Theorem 5.1 that there is a finite such split into symbolic states that are normal, that is, where no further experiment distinguishes the FLICs. The intruder’s conclusions during these experiments are formalized in $β_{0}$ , and we finally show in Theorem 5.2 that a normal symbolic state satisfies $(α, β)$ -privacy if its $β_{0}$ does not exclude any models of $α$ .

We first define the equivalence relation $≃$ between recipes. It formalizes that this pair of recipes does not distinguish any FLICs, that is, it will either give the same message ( $⊏ ⊐$ ) in all FLICs, or different messages ( $⋈$ ) in all FLICs:

Definition 5.1
Let $S = (α_{0}, β_{0}, P,_)$ be a symbolic state, where the possibilities $P$ have conditions $ϕ_{1}, \dots, ϕ_{n}$ and FLICs $A_{1}, \dots, A_{n}$ . Let $r_{1}$ and $r_{2}$ be two recipes and $σ_{i} = m g u (A_{i} (r_{1}) ≐ A_{i} (r_{2}))$ for $i \in {1, \dots, n}$ . We define $r_{1} ≃ r_{2}$ iff $r_{1} ⊏ ⊐ r_{2}$ or $r_{1} ⋈ r_{2}$ , where
$\begin{aligned} r_{1} ⊏ ⊐ r_{2} iff & for every i \in {1, \dots, n}, i s P r i v (σ_{i}) and α_{0} \land β_{0} \land ϕ_{i} ╞ σ_{i} \\ r_{1} ⋈ r_{2} iff & for every i \in {1, \dots, n}, L I (A_{i}, σ_{i}) = \emptyset or (i s P r i v (σ_{i}) and α_{0} \land β_{0} \land ϕ_{i} ╞ \neg σ_{i}) \end{aligned}$

This definition first considers the most general unifier $σ_{i}$ between the terms that the recipes produce in FLIC $A_{i}$ . For the experiment to produce the same message in every FLIC under every instantiation ( $⊏ ⊐$ ), the $σ_{i}$ can only have privacy variables and must be entailed by $α_{0}$ , $β_{0}$ , and the condition $ϕ_{i}$ from the respective possibility (if there were some intruder variables in $σ_{i}$ then the outcome of the experiment would depend on past intruder choices and thus allow for a distinction). For the experiment to produce different messages in every FLICs under any instantiation ( $⋈$ ), we have two cases: each $σ_{i}$ either depends on intruder variables but $σ_{i} (A_{i})$ is unsatisfiable (so the experiment will always be negative, no matter what the intruder does), or $σ_{i}$ substitutes no intruder variables and $α_{0} \land β_{0} \land ϕ_{i}$ implies $\neg σ_{i}$ .
Example 5.1
Based on Example 2.1, suppose that we reached a symbolic state containing two possibilities with $ϕ_{1} \equiv y ≐ y e s$ , $ϕ_{2} \equiv y ≐̸ y e s \land x ≐̸ a$ and
$A_{1} = + R \mapsto N . - l \mapsto c r y p t (p k (x), p a i r (y e s, N)), A_{2} = + R \mapsto N . - l \mapsto c r y p t (p k (x), n o)$
Here we again assume non-randomized encryption for the sake of the example. Then we have $l ⋈ c r y p t (p k (a), n o)$ , because in $A_{1}$ there is no unifier and in $A_{2}$ the unifier $[x \mapsto a]$ is excluded by $ϕ_{2}$ .

We now make use of the set $C h e c k e d$ to keep track of the experiments that the intruder has already performed. It is an (initially empty) set of pairs of recipes. As part of well-formedness of states we require that $l ≃ r$ holds for all $(l, r) \in C h e c k e d$ :
Definition 5.2 (Well-formed symbolic state)

Let $S = (α_{0}, β_{0}, P, C h e c k e d)$ be a symbolic state, with the possibilities $P = {(_, ϕ_{1}, A_{1}, X_{1}, α_{1},_), \dots, (_, ϕ_{n}, A_{n}, X_{n}, α_{n},_)}$ . We say that $S$ is well-formed iff

the $ϕ_{i}$ are such that $╞ \neg (ϕ_{i} \land ϕ_{j})$ for $i \neq j$ , $f v (ϕ_{i}) \subseteq f v (α_{0}) \cup f v (β_{0})$ and $α_{0} \land β_{0} ╞ ⋁_{i = 1}^{n} ϕ_{i}$ ;

the $A_{i}$ are simple FLICs with the same labels and same recipe variables, occurring in the same order;

the disequalities $X_{i}$ are satisfiable;

the $α_{i}$ are such that $f v (α_{i}) \subseteq f v (α_{0})$ and $α_{0} \land β_{0} \land γ_{0} \land ϕ_{i} ╞ α_{i}$ ; and

for every $(l, r) \in C h e c k e d$ , we have $l ≃ r$ .

Recipe variables can only occur in the FLICs

A_{i}

. Since

d o m (A_{1}) = \dots = d o m (A_{n})

, we may write

d o m (S)

for the domain of the symbolic state.

In the rest of the article, we only consider well-formed symbolic states (and well-formedness is preserved by the procedure).

Remember that so far, we considered an intruder who has no access to destructors (the next section will introduce destructors). Since we have no algebraic properties between constructors, everything behaves like in a free algebra, that is, $f (t_{1}, \dots, t_{n}) ≐ g (s_{1}, \dots, g_{m})$ implies $f = g$ and $t_{i} ≐ s_{i}$ . Thus we do not consider experiments where both recipes are composed, that is, it is sufficient to only consider experiments $(l, r)$ where $l$ is a label (and $r$ may be any recipe). In other words, we only need to check for every FLIC $A_{i}$ and for every label $l \in d o m (S)$ whether there is any recipe (other than $l$ ) to generate the same term $A_{i} (l)$ . We can compute the set of all such pairs using the lazy intruder and thus a finite worklist of all experiments to perform:

Definition 5.3 (Pairs and normal symbolic state)

Let $S = (_,_, P, C h e c k e d)$ be a symbolic state with FLICs $A_{1}, \dots, A_{n}$ in $P$ . The set of pairs of recipes to compare in $S$ is

P a i r s (S) = {(l, ρ (R)) ∣ l \in d o m (S), i \in {1, \dots, n}, ρ \in L I (A_{i} . + R \mapsto A_{i} (l), ε), ρ (R) \neq l} ∖ C h e c k e d .

We say that $S$ is normal iff $S$ is finished and $P a i r s (S) = \emptyset$ .

We define a reduction relation $↣$ that, given a symbolic state $S$ and a pair $(l, r) \in P a i r s (S)$ , yields a set of symbolic states after the experiment of comparing $l$ and $r$ . We call these experiments compose-checks. We will show that when $S ↣ {S_{1}, \dots, S_{k}}$ it follows that $[[S]] = \cup_{i = 1}^{k} [[S_{i}]]$ , thus this reduction does not change the represented ground states. Moreover, as long as there is an experiment $(l, r) \in P a i r s (S)$ , $S$ is a reducible expression for $↣$ . Thus, a normal state is eventually reached (and thanks to the semantic equivalence, it is not relevant in which order the steps were taken). In such a normal state, no experiment can distinguish the FLICs.

Definition 5.4 (Compose-checks)

Let $S$ be a symbolic state $(_, β_{0}, P, C h e c k e d)$ , with possibilities $P = {(0, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}$ , $(l, r) \in P a i r s (S)$ and $σ_{i} = m g u (A_{i} (l) ≐ A_{i} (r))$ for $i \in {1, \dots, n}$ . Then the set of symbolic states after the compose-check w.r.t. $(l, r)$ is as follows.

Privacy split If for every $i \in {1, \dots, n}$ , $i s P r i v (σ_{i})$ or $L I (A_{i}, σ_{i}) = \emptyset$ : $S ↣ {S_{1}, S_{2}}$ , where

\begin{aligned} S_{1} = S [[β_{0} & \leftarrow β_{0} \land ⋀_{i = 1}^{n} (ϕ_{i} \Rightarrow {\begin{cases} σ_{i} & if i s P r i v (σ_{i}) \\ f a l s e & otherwise \end{cases}) \\ P & \leftarrow {(0, ϕ_{i} \land σ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}, i s P r i v (σ_{i})} \\ C h e c k e d & \leftarrow C h e c k e d \cup {(l, r)}]] \\ S_{2} = S [[β_{0} & \leftarrow β_{0} \land ⋀_{i = 1}^{n} (ϕ_{i} \Rightarrow {\begin{cases} \neg σ_{i} & if i s P r i v (σ_{i}) \\ t r u e & otherwise \end{cases}) \\ P & \leftarrow {(0, ϕ_{i} \land \neg σ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}, i s P r i v (σ_{i})} \\ \cup {(0, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}, not i s P r i v (σ_{i})} \\ C h e c k e d & \leftarrow C h e c k e d \cup {(l, r)}]] \end{aligned}

Recipe split If there exists $i \in {1, \dots, n}$ such that not $i s P r i v (σ_{i})$ and $L I (A_{i}, σ_{i}) = {ρ_{1}, \dots, ρ_{k}}$ ( $k \geq 1$ ):

S ↣ {ρ_{1} (S), \dots, ρ_{k} (S), S [X_{i} \leftarrow X_{i} \land \neg σ_{i}]}

Similarly to the symbolic execution, we extend the definition to relate sets of finished symbolic states: $C ↣ C^{'}$ iff $S \in C$ , $S ↣ C_{S}$ and $C^{'} = C ∖ {S} \cup C_{S}$ .

Note that given a pair $(l, r)$ , either Privacy split is applicable, or some Recipe split is. In the case of Privacy split, the outcome of the experiment is independent of the intruder choices (the unifiers between messages produced by $l$ and $r$ are only using privacy variables or $σ_{i} (A_{i})$ is unsatisfiable). We split into two symbolic states. The first, $S_{1}$ , represents all those concrete states where $l$ and $r$ give the same result in the concrete intruder frame, and excluding all interpretations where they give different results. On the symbolic level this means that for possibility $i$ , if $σ_{i}$ substitutes only privacy variables, the intruder learns $ϕ_{i} ⟹ σ_{i}$ , because under all other instances, this FLIC would give unequal terms. Otherwise (since the rule is only applicable when $i s P r i v (σ_{i})$ or $σ_{i} (A_{i})$ is unsatisfiable), the possibility $i$ gives unequal terms no matter what the intruder sent earlier, and the intruder can thus rule this possibility out ( $ϕ_{i} ⟹ f a l s e$ ).

The second, $S_{2}$ , represents the rest, that is, where $l$ and $r$ give different results in the concrete frame. This means for the $i$ th possibility, either the unifier depends only on privacy variables and the intruder learns that $ϕ_{i}$ can only be true if $\neg σ_{i}$ (because under $σ_{i}$ the comparison should have been positive); or $σ_{i} (A_{i})$ is unsatisfiable and the intruder learns nothing.

In the case of Recipe split, for at least one FLIC, the unifier depends on intruder variables, making that FLIC not simple. For each lazy intruder result, there is one symbolic state in which the intruder takes a choice of recipes $ρ$ and the whole symbolic state is updated accordingly. Additionally, there is one symbolic state in which the intruder chooses something else for the recipes and one unifier is excluded.

Example 5.2
Let us consider again Example 2.1, where for now we assume that encryption is not randomized. Let $S = (α_{0}, β_{0}, P, \emptyset)$ be the symbolic state such that:
$\begin{aligned} α_{0} & \equiv x \in A g e n t \land y \in {y e s, n o}, β_{0} \equiv y ≐ y e s \lor y ≐̸ y e s \\ P & = {(0, y ≐ y e s, A_{1}, t r u e, t r u e, []), (0, y ≐̸ y e s, A_{2}, t r u e, t r u e, [])} \\ A_{1} & = + R \mapsto N . - l \mapsto c r y p t (p k (x), p a i r (y e s, N)), A_{2} = + R \mapsto N . - l \mapsto c r y p t (p k (x), n o) \end{aligned}$
$S$ is not normal since, for example, $(l, c r y p t (p k (a), n o)) \in P a i r s (S)$ . We can perform a compose-check, in this case by applying the Privacy split rule. In $A_{1}$ , we have to unify $c r y p t (p k (x), p a i r (y e s, N))$ and $c r y p t (p k (a), n o)$ , which is not possible. In $A_{2}$ we have to unify $c r y p t (p k (x), n o)$ and $c r y p t (p k (a), n o)$ , which gives the mgu $σ = [x \mapsto a]$ . Then we get two symbolic states $S_{1}$ and $S_{2}$ , which have the same $α_{0}$ as $S$ but we update $β_{0}$ and $P$ . Moreover, in both $S_{1}$ and $S_{2}$ we have $C h e c k e d = {(l, c r y p t (p k (a), n o))}$ .
$\begin{aligned} In S_{1} : & β_{0} & \equiv (y ≐ y e s \lor y ≐̸ y e s) \land (y ≐ y e s \Rightarrow f a l s e) \land (y ≐̸ y e s \Rightarrow x ≐ a) \\ P & = {(0, y ≐̸ y e s \land x ≐ a, A_{2}, t r u e, t r u e, [])} \\ In S_{2} : & β_{0} & \equiv (y ≐ y e s \lor y ≐̸ y e s) \land (y ≐ y e s \Rightarrow t r u e) \land (y ≐̸ y e s \Rightarrow x ≐̸ a) \\ P & = {(0, y ≐ y e s, A_{1}, t r u e, t r u e, []), (0, y ≐̸ y e s \land x ≐̸ a, A_{2}, t r u e, t r u e, [])} ◼ \end{aligned}$

Using the compose-checks, we can transform a symbolic state into a set of normal symbolic states, since by definition a symbolic state is normal when there are no more pairs to compare. Moreover, the compose-checks preserve the semantics of symbolic states by partitioning the ground states represented.
Theorem 5.1 (Compose-check correctness)

Let $S$ be a finished symbolic state, $(l, r) \in P a i r s (S)$ and $S_{1}, \dots, S_{n}$ be the symbolic states such that $S ↣ {S_{1}, \dots, S_{n}}$ w.r.t. $(l, r)$ . Then $[[S]] = ⨄_{i = 1}^{n} [[S_{i}]]$ . Moreover, there does not exist any infinite sequence $(S_{i})_{i \geq 1}$ where for every $i$ , there exists $C_{i}$ such that $S_{i} ↣ C_{i}$ and $S_{i + 1} \in C_{i}$ .

In a normal symbolic state, there are no more pairs of recipes that could distinguish the possibilities (they have all been checked). Thus, given a ground choice of recipes, all the concrete instantiations of frames are statically equivalent. This means that in a normal symbolic state, the FLICs do not contain any more insights for the intruder, and all remaining violations of $(α, β)$ -privacy can only result from any other information $β_{0}$ that the intruder has gathered. We thus define that a symbolic state is consistent iff $β_{0}$ cannot lead to violations either.

Definition 5.5 (Consistent symbolic state)

We say that a finished symbolic state $S$ is consistent iff $(α, β_{0})$ -privacy holds for every $(α, β_{0},_,_) \in [[S]]$ .

Even though $[[S]]$ is infinite, we need to consider only finitely many $(α, β_{0})$ pairs. This is because the corresponding $α$ and $β_{0}$ in $S$ do not contain intruder variables and we only need to resolve the meta-notation if present. For truth $γ$ , we also have only to consider finitely many instances of the privacy variables (as they range over finite domains). We ensure that $β_{0}$ only contains symbols in $Σ_{0}$ , and for each $α$ and $β_{0}$ , the $Σ_{0}$ -models are computable as we show in Supplemental Appendix C. While that algorithm is based on an enumeration of models as a simple means to prove we are in a decidable fragment, our prototype tool uses the SMT solver cvc5¹⁴ to check consistency more efficiently.

Example 5.3
In the symbolic state $S$ from Example 5.2, we have $α_{0} \equiv x \in A g e n t \land y \in {y e s, n o}$ and $β_{0} \equiv y ≐ y e s \lor y ≐̸ y e s$ . Since $(α_{0}, β_{0})$ -privacy holds, $S$ is consistent.

In the symbolic state $S_{1}$ that results from comparing recipes $l$ and $c r y p t (p k (a), n o)$ , we have the same $α_{0}$ but now $β_{0} \equiv y ≐̸ y e s \land x ≐ a$ . Here $(α_{0}, β_{0})$ -privacy does not hold anymore because $β_{0}$ rules out a model of $α_{0}$ , namely $[x \mapsto a, y \mapsto y e s]$ . Thus $S_{1}$ is not consistent.

To verify whether a symbolic state satisfies privacy, we perform all compose-checks to get a set of normal symbolic states, and then in each of these normal states it suffices to verify consistency.
Theorem 5.2
Let $S$ be a normal symbolic state. Then $S$ satisfies privacy iff $S$ is consistent.
6. Lifting to algebraic properties

So far, our procedure consists in (i) executing a transaction with the rules of Table 4, (ii) normalizing symbolic states with intruder experiments, and (iii) checking consistency in the reached normal symbolic states. The above gives us a decision procedure for $(α, β)$ -privacy (under a bound $k$ on the number of transitions) as long as the intruder has no access to destructors. Note that transactions can apply destructors already. This allows for a very convenient and economical way to extend the intruder model with destructors as well without painfully extending all the above machinery to destructors: we define a set of special transactions called destructor oracles, one for each destructor. They receive a term and decryption key candidate, and send back the result of applying the destructor unless it fails. Note that calling these oracles does not count towards the bound on the number of transitions, but rather we apply them to a reached symbolic state until destructors yield no further results.

6.1. The supported algebraic theories

We give in Figure 1 a concrete example theory, but our result can be quite easily used for similar theories. For instance, many modelers prefer for asymmetric cryptography that private keys are defined as atomic constants and the corresponding public key is obtained by a public function $p u b$ . We like, in contrast, to start with public keys and have a private function $i n v$ to obtain the respective public key. This allows us to define a public function from agent names to public keys, which can be convenient in reasoning about privacy when the public-key infrastructure is fixed. Similarly, one may want to define further functions, in particular transparent functions like $p a i r$ , that is, functions that describe message serialization and where the intruder can extract every subterm. Finally, in some cases it is convenient to model some private extractor functions when we are dealing with messages where the recipient has to perform a small guessing attack. For instance, in a protocol like Basic Hash³² (modeled in Supplemental Appendix D) the reader actually needs to try out every shared key with a tag to find out which tag it is. Rather than describing transitions that iterate over all tags and try to decrypt, it is convenient to model a private $e x t r a c t$ function that “magically” extracts the name of the tag, if the message is of the correct form, and returns false otherwise. This extraction must be a private function since the intruder should not be able to observe this unless they know the respective shared keys; if they do, then the experiments in our method automatically allow the intruder to perform the guessing attack. We thus distinguish three kinds of algebraic properties of destructors that can be used arbitrarily in our approach:

Definition 6.1 (Algebraic theory)

A destructor rule is a rewrite rule of one of the following forms:

Decryption: $d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}$ where $d$ is a destructor, $c$ is a constructor, $f v (k) = f v (k^{'})$ , the $X_{j}$ are variables and $i \in {1, \dots, n}$ .

Projection: $d_{i} (c (X_{1}, \dots, X_{n})) \to X_{i}$ where $i \in {1, \dots, n}$ , $d_{i}$ is a public destructor called a projector, $c$ is a constructor of arity $n$ , the $X_{j}$ are variables. There must be such a rule for every $i \in {1, \dots, n}$ and $c$ is then called transparent.

Private extraction: $d (c (t_{1}, \dots, t_{n})) \to t_{0}$ where $d$ is a private destructor called a private extractor, $c$ is a constructor and $t_{0}$ is a subterm of one of the $t_{i}$ .

Let

E

be a set of such rules, where we require that every destructor

d

occurs in exactly one rule of

E

and

E

forms a convergent term-rewriting system. Moreover, each constructor

c

cannot occur both in decryption and projection rules. Define

\approx

to be the least congruence relation on ground terms such that

d (k, t) \approx {\begin{cases} t_{i} & if t \approx c (k^{'}, t_{1}, \dots, t_{n}) and for some σ, (d (k, c (k^{'}, t_{1}, \dots, t_{n})) \to t_{i}) \in σ (E) \\ f f & otherwise \end{cases}

and for unary destructors the definition is the same but

k, k^{'}

are omitted. Moreover, we require for every decryption rule

d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}

that

k = k^{'}

k \approx f (k^{'})

k^{'} \approx f (k)

for some public function

f

The requirement $k = k^{'}$ or $k \approx f (k^{'})$ or $k^{'} \approx f (k)$ for some public $f$ means that, given the decryption key $k$ one can derive the encryption key $k^{'}$ , or the other way around. In particular, in most asymmetric encryption schemes, the public key can be derived from the private key; for signatures the private key takes the role of the “encryption key.” This requirement forces us to define in our example theory the rule $p u b k (i n v (k)) \to k$ . Suppose that we omitted this rule, denying the intruder the ability to derive the public key to a given private key. Suppose further that the intruder has received two messages $l_{1} \mapsto i n v (p k (x))$ and $l_{2} \mapsto p k (y)$ and is wondering whether maybe $x ≐ y$ . Then they could make the experiment whether $d c r y p t (l_{1}, c r y p t (l_{2}, r_{1}, r_{2})) \approx f f$ and this would be the case iff $x ≐̸ y$ . For our method, we want however to ensure that the intruder never needs to decrypt messages that they encrypted themselves. In the example, with the public-key extraction rule, the intruder can derive $p u b k (i n v (p k (x))) \approx p k (x)$ and now directly compare this with $l_{2}$ . The requirement allows us to show that the intruder cannot learn anything new from decrypting terms that they have encrypted themselves.

Observe that every ground term $t$ is equivalent to a unique destructor-free ground term $t_{0}$ and that can be computed by applying a rewrite rule, when possible, to an inner-most destructor^b in $t$ and replacing by $f f$ if no rewrite rule is applicable, and repeating this until all destructors are eliminated.

6.2. Destructor oracles

Since transactions can already apply destructors, we can model oracles that provide decryption services for the intruder, namely the intruder has to send a term to decrypt and the proposed decryption key and the oracle gives back the result of applying the destructor.

Definition 6.2 (Destructor oracle)

Given the decryption rule $(d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}) \in E$ , its destructor oracle is the transaction: $r c v (X) . r c v (Y) . t r y Z := d (Y, X) i n s n d (Z) . s n d (Y) . 0 c a t c h 0$ .

Given the projection rule $(d (c (X_{1}, \dots, X_{n})) \to X_{i}) \in E$ , we define a single oracle:

$r c v (X) . t r y Z_{1} := d_{1} (X) i n \dots t r y Z_{n} := d_{n} (X) i n s n d (Z_{1}) . \dots . s n d (Z_{n}) .0 c a t c h 0 \dots c a t c h 0$ .

For transparent functions, there is no need for a key and for each $i \in {1, \dots, n}$ , the $i$ th subterm can be retrieved with destructor $d_{i}$ , so we define one oracle returning all subterms. There are no oracles for private extractors since these functions are not available to the intruder.

Obviously, such transactions are redundant if the intruder has access to the destructors and also it is sound to add such transactions. Also redundant is the output $s n d (Y)$ , because $Y$ is already an input, but this ensures that different ways of composing the key will be considered by our compose-checks.

The reader may wonder why we do not do the same also for constructors, for example, using transactions of the form $r c v (X_{1}) . \dots . r c v (X_{n}) . s n d (c (X_{1}, \dots, X_{n})) .0$ , so we could use an intruder who neither encrypts nor decrypts and just uses oracles for both jobs. The reason is that constructors give rise to an infinite set of terms that can be generated and it is difficult to limit that—this is why we use the lazy intruder technique as a way to represent the infinitely many choices in a finite and yet complete way. For destructors on the other hand, we do not have the same problem since it is limited what we can achieve here. In particular, there is no need for the intruder to destruct terms that they have constructed themselves, thus allowing us to limit the use of destructors, respectively, the destructor oracles, in a simple way.

6.3. Analysis strategy

In general the destructor oracles are applicable without boundary. We use a strategy to apply them that does not lead into non-termination, but covers all applications that are necessary for any attack. Note also that the application of oracles does not count towards the bound on the number of transitions.

Definition 6.3 (Term marking)

All received terms and subterms in a FLIC shall be marked with one of three possible markings: $⋆$ for terms that might be decrypted but have not been so far; $+$ for terms that cannot be decrypted at the given intruder knowledge for any instance of the variables; and $✓$ for terms that either have already been decrypted or have been composed by the intruder themselves (so the intruder knows already the subterms that may result from a decryption).

The default initial marking is $⋆$ . The exceptions are privacy and intruder variables, as well as functions that do not have a public destructor; all such terms (and subterms if they have) are marked with $✓$ . Markings are only changed according to Definition 6.4. In particular, when a variable gets instantiated, the resulting term keeps its $✓$ marking.

Our strategy applies the destructor oracles to a given symbolic state $S$ to obtain a finite set of analyzed symbolic states $S_{1}, \dots, S_{n}$ that are together equivalent to $S$ except that the FLICs are augmented with the results of decryptions (or projections), which we call shorthands.

Definition 6.4 (Analysis strategy)

Let $S$ be a normal symbolic state (recall that in $S$ all FLICs are simple, and thus intruder variables represent messages the intruder composed; and $S$ is normal, that is, all compose-checks have been made).

The following strategy is applied as long as there exists a label $l$ that maps to a $⋆$ -marked term. Let $l$ be the first label (in the order of the domain) that maps to a term $c (s_{0}, \dots, s_{n})$ which is $⋆$ -marked in some FLIC; note that by construction, it can only be a constructor term. If $c (s_{0}, \dots, s_{n})$ is an encryption, that is, $c$ occurs in a decryption rule (the intruder can decrypt iff they can produce the appropriate key), then we apply the oracle for that rewrite rule under the specialization that the recipe for $X$ (the oracle input for the constructor term) must be the label $l$ . If $c$ is a transparent function, then we use the appropriate oracle that applies all its projectors and returns all subterms.

Executing the oracle transaction and performing experiments leads to a finite number of successor states $S_{1}, \dots, S_{m}$ (there is at least one, so $m \geq 1$ ) that are again normal and have simple FLICs. In each $S_{i}$ , the decryption has either worked in every FLIC, or failed in every FLIC. We now update the marks in the $S_{i}$ as follows.

If in $S_{i}$ decryption has failed, assuming that $c$ is the constructor for which we had executed the corresponding oracle, then in every FLIC where $l \mapsto c (t_{0}, \dots, t_{n})$ that is marked $⋆$ , we change to mark $+$ because it is (with the current knowledge) not decipherable. If it was already marked $✓$ , we do not change the label (note that in some FLIC, $l$ may map to a term with a different constructor $c^{'}$ ; if that term is marked $⋆$ , it maintains this marking, so that one of the next analysis steps will be to check if the respective destructor for $c^{'}$ can be applied).

If in $S_{i}$ decryption has worked, then we update and introduce markings in each FLIC as follows. In case of a decryption rule, and thus in a given FLIC, $l$ maps to some term $c (k^{'}, t_{1}, \dots, t_{n})$ , the result of the analysis is bound to a new label $l^{'} \mapsto t_{i}$ (for some $i \in {1, \dots, n}$ ); the decryption key is bound to new label $l^{″} \mapsto k$ . If $m_{i}$ is the mark of $t_{i}$ in $l$ , then the new occurrence of $t_{i}$ at $l^{'}$ shall also be marked with $m_{i}$ . In turn, $c (k^{'}, t_{1}, \dots, t_{n})$ are now all marked $✓$ , because they are fully analyzed. Similarly, the key term $l^{″} \mapsto k$ and all its subterms receive the $✓$ mark, because they have been produced by the intruder already (and are thus taken from another label that is already analyzed, or composed by the intruder and thus not interesting for decryption). All terms that were marked $+$ are changed with marking $⋆$ , because the newly analyzed term may allow for some decryption that was impossible before. In case of projection rules, the marking is similar for the new subterms.

We repeat this process of attempting to decrypt the first $⋆$ -marked term until there are no more $⋆$ -marks. A symbolic state is analyzed iff it does not contain any $⋆$ -marked terms.

We call a label $l$ in a symbolic state $S$ a shorthand iff there exists a recipe $r$ over labels before $l$ such that $A (l) \approx A (r)$ for every FLIC $A$ in $S$ .

The analysis strategy augments FLICs only by shorthands and thus does not change what is derivable for an intruder who can decompose.

Theorem 6.1 (Analysis correctness)

For a symbolic state $S$ , the analysis strategy produces in finitely many steps a set ${S_{1}, \dots, S_{n}}$ of symbolic states that are analyzed. Further, for every ground state $S \in [[S]]$ there exists $S^{'} \in [[S_{i}]]$ , for some $i \in {1, \dots, n}$ , such that $S$ and $S^{'}$ are equivalent except that the frames in $S^{'}$ may contain further shorthands; and vice versa, for every $S^{'} \in [[S_{i}]]$ there exists $S \in [[S]]$ such that $S^{'}$ is equivalent to $S$ except for shorthands.

Example 6.1
In the symbolic state reached after executing the transaction from Example 2.1, there is one FLIC that contains a received message $- l \mapsto c r y p t (p k (x), p a i r (y e s, N), r)$ (marked $⋆$ ) as well as $- l_{0} \mapsto i n v (p k (i))$ . Then the strategy will execute the asymmetric decryption oracle for label $l$ . This gives two states: $S_{1}$ where for this possibility we unify $x ≐ i$ and the intruder has a new label $- l_{1} \mapsto p a i r (y e s, N)$ , and $S_{2}$ where we have $x ≐̸ i$ and the intruder cannot decrypt $l$ (given the intruder knows no other private keys $i n v (p k (\cdot))$ ). The encrypted message at label $l$ is now marked $✓$ in $S_{1}$ and $+$ in $S_{2}$ .

Let $S_{0} = (t r u e, t r u e, {(0, t r u e, [], t r u e, t r u e, [])}, \emptyset)$ be the initial symbolic state. Given a transaction $P$ and a finished symbolic state $S$ , let $s t a r t (P, S)$ denote the symbolic state identical to $S$ but where the $0$ -process in every possibility of $S$ is replaced with process $P$ . Our decision procedure defines how to symbolically execute processes, perform intruder experiments and apply the analysis strategy such that, given a finished symbolic state $S$ and a bound $k$ on the number of transitions, we compute a finite set ${S_{1}, \dots, S_{n}}$ of normal, analyzed symbolic states that can be reached after executing at most $k$ transactions (not counting the destructor oracles). In normal analyzed states, the intruder does not need any destructors anymore, because we can show that for every recipe, there exists a destructor-free one (possibly using the shorthands added during analysis), and then there are also no relevant experiments that could be made with recipes using destructors. It then suffices to verify consistency in the reached normal analyzed symbolic states to decide whether $(α, β)$ -privacy holds.

We can now conclude the correctness of our decision procedure. All the proofs are shown in Supplemental Appendix B. Note that we need a bound on the number of transitions, and this bound is restricting the number of transactions that are executed. All “internal” transitions taken by our compose-checks and analysis steps do not count towards that bound.
Theorem 6.2 (Procedure correctness)

Given a protocol specification for $(α, β)$ -privacy, a bound on the number of transitions and an algebraic theory allowed by Definition 6.1, our decision procedure is sound, complete and terminating.

7. Tool support and case studies

We have developed a prototype tool called noname³³ implementing our decision procedure. The tool is a proof-of-concept showing that automation for $(α, β)$ -privacy is achievable and practical. The user must provide as input the protocol specification, consisting of the transactions that can be executed, and a bound on the number of transactions to execute. For the cryptographic operators, we make available by default primitives for asymmetric encryption/decryption, symmetric encryption/decryption, signatures and pairing (Figure 1). The user can define custom operators with the restriction to constructor/destructor theories given in Definition 6.1. We have also implemented an interactive running mode (the default is automatic, i.e., exploring all reachable states) in which the user is prompted whenever there are multiple successor states, so that one can manually explore the symbolic transition system.

In case there is a privacy violation, the tool provides an attack trace that includes the sequence of atomic transactions executed and steps taken by the intruder (i.e. the recipes they have chosen) to reach an attack state, as well as a countermodel proving that the privacy goals in that state do not hold, that is, a witness that the intruder has learned more in that state than what is allowed by the payload.

As case studies, we have focused on unlinkability goals in the following protocols: our running example, Basic Hash,³⁴ OSK³⁵ (which is particularly challenging as it is a stateful protocol), and several variants of BAC³⁶ and Private Authentication³⁷ (the $(α, β)$ -privacy specifications of these last two protocols are given by Fernet and Mödersheim³⁸). For each protocol, we describe briefly our results on whether it satisfies $(α, β)$ -privacy. The models, together with more details, are in Supplemental Appendix D.

Running example. As explained in Example 4.1, if the server is replying to a compromised agent, then there is a privacy violation because the intruder is able to learn the identity of that agent, and the tool finds this attack. When permitting that the intruder learns the compromised agent’s identity, the tool discovers another problem: if the agent is not compromised, then the intruder is also able to learn this fact. When releasing also that information, no more violations are found. This illustrates how the tool can help to discover all private information that is leaked, and thus either fix the protocol or permit that leak, and then finally verify that no additional information is leaked (given the bound on the number of transitions).

Basic Hash.³⁴ In this RFID protocol, a tag sends to a reader a pair of messages containing a nonce and a MAC, using a secret key shared between tag and reader. Then the reader tries to recompute the MAC with every secret key they know to identify the tag (this behavior of the reader is modeled with a private extractor that retrieves the tag name from the MAC). We have verified that the Basic Hash protocol satisfies unlinkability, but fails to provide forward privacy.³²

OSK.³⁵ This is also an RFID protocol with tags and readers. We have modeled two variants where, respectively, no desynchronization and one desynchronization step is tolerated. For both versions the tool finds the known linkability flaws.³⁹

BAC.³⁶ This standard RFID protocol is used to read data from passports. A tag and a reader perform a challenge-response, where the tag sends a nonce and an encrypted message containing that nonce, and the reader receives both and verifies that the nonces match. The tool finds the known problems in some implementations.^40–42

Private Authentication.³⁷ This protocol models agents that encrypt messages using a public-key infrastructure. The initiator sends a message containing their name and a nonce, and the responder either sends back a message with a fresh nonce or sends a decoy message. We consider several variants: AF0 denotes the situation where agents always want to talk to other agents, while AF denotes the situation where agents might not want to talk to some other agents. For AF0, there is one model with a privacy violation due to insufficient release in $α$ and another model fixing this issue; AF builds on top of the fixed AF0 and adds a binary relation to model whether agents want to talk.

Discussion of the results. Finding a privacy violation is usually fast, because the tool stops as soon as it finds one without exploring the rest of the transition system. Most protocols take a few seconds to analyze, but when incrementing the bound on the number of transitions we can notice a steep increase in the verification time. Table 5 in Supplemental Appendix D summarizes these results. Indeed, in our model, transactions can always be executed so there is in general a large number of possible interleavings. The tool seems thus to be limited by the substantial size of the search space, like earlier tools for deciding equivalence (APTE¹⁰). In our decision procedure, we are not deciding static equivalence between frames, but the experiments made by the intruder to try and distinguish the different possibilities seem to have a comparable complexity. For unlinkability goals, in particular, our tool and others (for bounded sessions) essentially provide similar privacy guarantees. We share the challenges and techniques such as symbolic representation of constraints for the unbounded intruder. Thus, we believe that optimizations implemented in tools such as DeepSec,⁴³ for example, forms of symmetries and partial order reductions, could be adapted to our procedure.

8. Typed model

We now define a simple type system for messages and the protocol specification includes the type of every constant and variable, for example, $a g e n t$ or $h (n o n c e)$ . This is first a mere annotation: we specify the intended type. The intruder is of course able to send messages of any type and an honest agent in general cannot check if a received message is of the intended type. We then develop a notion of type-flaw resistant protocols and show in the following section a typing result for them: if there is an attack, then there is a well-typed attack. Thus, given a type-flaw resistant protocol, it is sound to restrict the intruder model to well-typed messages.

To that end, we show that our procedure of the previous sections will never perform an ill-typed substitution, when it is applied to a type-flaw resistant protocol. This is in fact proved for an arbitrary reachable state, that is, our typing result holds without any bound on the number of transitions. We will make two adaptations to the procedure: we reduce the $t r y$ to pattern matching and conditions and we formulate analysis as built-in transitions instead of special transactions (destructor oracles); we also show that these transformations are correct.

8.1. Type system

Types are defined similarly to terms. Instead of a set of variables, we use a set of atomic types, for example, ${a g e n t, n o n c e}$ . The composed types are defined using the functions in $Σ$ , with the restriction to constructors of non-zero arity, that is, we forbid destructors and constants in composed types. The type system assigns an atomic or composed type to every message with the following requirements:

Definition 8.1 (Typing function)

A typing function $Γ$ is such that:

$Γ (c)$ is atomic for every function $c \in Σ$ of arity $0$ .

$Γ (f (t_{1}, \dots, t_{n})) = f (Γ (t_{1}), \dots, Γ (t_{n}))$ for every constructor $f \in Σ$ of arity $n > 0$ .

$Γ (x)$ is a type (atomic or composed) for every variable $x \in V$ .

Our type system does not include terms containing destructors, because they represent terms that need to be evaluated and we rather want to give a type to the result. In a protocol specification, destructors can only occur as part of a destructor application of the form $t r y Y := d (k, X) i n \dots$ where either the result is $f f$ and the transaction stops (for the typing result, we will require that all $c a t c h$ branches are empty), or $Y$ is bound to the respective subterm of $X$ , and thus shall have the respective (destructor-free) type.

The fact that instantiations of variables are well-typed is defined with the notion of a substitution being well-typed.

Definition 8.2 (Well-typed substitution)

A substitution $σ$ is well-typed iff for every $x \in d o m (σ)$ , we have $Γ (x) = Γ (σ (x))$ .

We need to ensure that the intruder is always able to make a well-typed choice, therefore, they must be able to compose arbitrarily many messages of each type, even before receiving any message from honest agents. Hence, we require that, for each atomic type, there is an infinite set of public constants of that type, that is, the intruder initially knows an unbounded number of constants of each atomic type. Suppose all function symbols were public, then the intruder would also immediately have access to an unbounded number of terms of every composed type. In fact, Hess and Mödersheim²⁶ observe that, even if all functions are public, one can still model a private function $f$ of arity $n$ by a public function $f^{'}$ of arity $n + 1$ , where the additional argument is filled with a distinct secret constant. Thus, private functions like $f$ are just syntactic sugar. We adopt this suggestion and, for the rest of the article, continue to use public and private functions, with the subset $Σ_{p u b} \subseteq Σ$ to identify the public functions.

We first define the precise class of algebraic theories that our typing result supports. We consider linear terms, that is, terms in which every variable occurs at most once. Compared to Definition 6.1, we include the requirement of linearity for the constructor terms in the rewrite rules and we exclude constants in encryption/decryption keys (they may still use private functions). This will be used when proving the typing result for state transitions (in particular in proofs relying on Definition 9.2).

Definition 8.3 (Algebraic theory for typing result)

Let $E$ be a set of rewrite rules satisfying Definition 6.1. For every decryption rule $(d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}) \in E$ , respectively, $(d (c (t_{1}, \dots, t_{n})) \to t_{0}) \in E$ for projection and private extraction, we require that the constructor term $c (k^{'}, X_{1}, \dots, X_{n})$ , respectively, $c (t_{1}, \dots, t_{n})$ , is linear, and that neither $k$ nor $k^{'}$ contains a constant.

In a protocol specification, we write type annotations with a colon, that is, $t : τ$ specifies that $Γ (t) = τ$ . We further define what it means for a protocol specification to type check. This does not yet include all the requirements for type-flaw resistance but simply ensures that the type annotations are consistent throughout the specification.

Definition 8.4 (Type checking)

For every constant $c$ , one has to specify $Γ (c)$ , that is, the type of that constant. For every memory cell $c e l l [\cdot]$ , one has to specify $Γ (c e l l)$ which is the type of the argument for cell reads. The type annotations of constants and memory cells are global to the specification, while type checking a transaction uses local type annotations for the variables bound in that transaction. Every transaction must satisfy the following:

For every choice $x \in D$ , we have that $D$ is a set of public constants of the same atomic type $τ$ , and we then set $Γ (x) = τ$ .

For every message received $r c v (X : τ)$ , we have that $τ$ is a type and we then set $Γ (X) = τ$ .

For every destructor application $t r y Y := d (t, X)$ , where the rule for $d$ is $d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}$ , there exist types for the free variables of the left-hand side such that $Γ (d (k, c (k^{'}, X_{1}, \dots, X_{n})) = Γ (d (t, X))$ . We then set $Γ (Y) = Γ (X_{i})$ .

For every cell read $X := c e l l [s]$ , we have $Γ (s) = Γ (c e l l)$ and we then set $Γ (X) = Γ (C [s])$ , where $C [\cdot]$ is the ground context for the initial value of $c e l l [\cdot]$ . For every cell write $c e l l [s] := t$ , we have $Γ (s) = Γ (c e l l)$ and $Γ (t) = Γ (C [s])$ .

For every equality $s ≐ t$ in a formula, we have $Γ (s) = Γ (t)$ .

For every step $ν n_{1} : τ_{1}, \dots, n_{k} : τ_{k}$ , the $τ_{i}$ are atomic types and we then set $Γ (n_{i}) = τ_{i}$ .

In the rest of this section and in Section 9, we will only consider protocol specifications such that the type checking requirements above are satisfied.

In Definition 2.2, there can be a process for handling failure, for example, sending an error message, while for the typing result we only support transactions that silently stop in case of destructor failure. For notation, we now omit writing $c a t c h 0$ , $e l s e 0$ and trailing $0$ ’s in processes. Moreover, $t r y$ in Definition 2.2 is part of the center process, while we now require it before branching, so that any destructor failure means that the entire transaction goes directly to $0$ . We also introduce additional requirements on protocols, which we use to ensure that the intruder knows the types of the messages in their knowledge and to control the shapes of messages that can occur during the protocol execution.

Definition 8.5 (Requirements)

For some control flow requirements on transactions, consider the tree that is induced by the conditionals of the transactions (i.e. every if-then-else is a node with the respective subprocesses as children). We say two execution paths are statically distinguishable for the intruder, iff a different number of messages are sent along the paths.^c Every transaction must satisfy the following:

Every destructor application occurs before any cell read or conditional statement, and every $c a t c h$ branch is empty, that is, it only contains the nil process.

For any two execution paths that are not statically distinguishable (and thus have the same number of sent messages), and under any instantiation of the intruder variables (including ill-typed instantiations), the $i$ th message sent in either path has the same type.

In every cell write $c e l l [s] := t$ , the term $t$ does not contain intruder variables.

When a decryption destructor is applied to a variable, this variable does not occur in other destructor applications.

If several projectors or private extractors are applied to the same variable, then the rewrite rules for these destructors are defined over the same constructor term.

For every message sent $s n d (t)$ and every subterm $t^{'}$ of $t$ , if $t^{'}$ is composed with a constructor $c$ occurring in a decryption rule $d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}$ , we have that $t^{'}$ is an instance of $c (k^{'}, X_{1}, \dots, X_{n})$ .

Requirement (1) is essential to ensure that the failure of a destructor does not reveal information about the type of the inputs.

An example for a protocol that does not satisfy Requirement (2) immediately, that is, that messages on two paths either are statically distinguishable or have the same type, is the model of Private Authentication given by Fernet and Mödersheim³⁸: here an agent $B$ receives a message and performs a check on it. If the check succeeds, then $B$ sends an encrypted reply as an answer. Otherwise, $B$ sends a random nonce as a decoy to hide whether the check succeeded. Thus there are two paths where the messages sent have different types, and indeed the point is to hide from the intruder which message was really sent. In the original model by Abadi and Fournet,³⁷ however, $B$ instead of a random nonce as decoy sends an encrypted message with a fresh key and random contents of the same type as the positive case. In that formulation, the protocol satisfies our requirement. The only example we can think of that would resist a similar transformation are onion-routing protocols where the intruder should not be able to tell the number of encryption layers of a given message. For protocols that do not rely on hiding the taken branch from the intruder, one can of course easily make the messages of the branches statically distinguishable and thus can also use messages of different types.

Requirement (3) is a significant restriction on cell writes, because it essentially means that we cannot update the memory with an arbitrary message sent by the intruder. Indeed, if the intruder was able to send some message to a transaction that writes this message in memory without doing any checks on it, then we could not maintain the invariant that the intruder always knows the types of the messages they observe.

Requirements (4) and (5) are not directly about the intruder knowing the types of the messages. We consider these requirements on the use of destructors as a reasonable restriction that ensures compatible destructor applications: whenever a variable is decomposed, we can instantiate the variable with a unique corresponding constructor term, because for this decryption there is a unique rewrite rule or for these projections/private extractions all rewrite rules are defined over the same term.

Requirement (6) on the use of constructor terms in messages sent will be useful when proving the well-typedness of analysis: if a subterm in a message sent is composed with a constructor that can be decomposed, it should be an instance of the constructor term in the corresponding rewrite rule. For instance, if we model signatures with the rewrite rule $o p e n (K, s i g n (i n v (K), M)) \to M$ , then signatures sent by honest agents must have a key starting with $i n v$ and cannot use a variable in this place, for example, we do not allow sending $s i g n (X, m)$ , because $s i g n (X, m)$ is not an instance of $s i g n (i n v (K), M)$ .

Using Definition 8.5, we can maintain the invariant than in a reachable state, a given label maps to the same type in every possibility, that is, the intruder always knows the types of the messages they have observed. Thus whatever recipe they use when sending a message, it corresponds to the same type in every possibility.

Lemma 8.1
Let $S$ be a reachable state in a protocol satisfying Definition 8.5, ${s t r u c t}_{1}, \dots, {s t r u c t}_{n}$ be the frames in $S$ and $r$ be a recipe over the domain of the ${s t r u c t}_{i}$ . Then $Γ ({s t r u c t}_{1} (r)) = \dots = Γ ({s t r u c t}_{n} (r))$ .
8.2. Message patterns

To show the typing result, it is convenient to replace the $t r y$ mechanism for handling destructors with pattern matching. In fact, the $(α, β)$ -privacy semantics does not have a notion of pattern matching, because in a general untyped model, it is unclear how to define such a construct in a suitable way. However, for a specification that satisfies Definition 8.5, the intruder knows the type of every message, and thus also knows whether a given message will agree with a given pattern. Hence, we make a conservative extension of the receive construct with pattern matching (under the restrictions of Definition 8.5).

Instead of $r c v (X)$ for an intruder variable $X$ , we now allow also $r c v (t)$ , where $t$ is a linear pattern term: it contains fresh intruder variables, where each intruder variable can only occur once, and no constants. The meaning is that the agent only accepts an incoming ground message $m$ , if $m$ is an instance of $t$ and then binds the variables of $t$ with the respective subterms of $m$ (this ignores how an agent would be able to check that $m$ is an instance of $t$ ). This is a conservative extension of the semantics on ground states (Table 1).

Definition 8.6
We extend the Receive rule of Table 1 with the following:
$(α, β_{0}, γ, {(r c v (t) . P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}}) \to (α, β_{0}, γ, {(P_{i}^{'}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$
for every recipe $r$ over the domain of the ${s t r u c t}_{i}$ , where for every $i \in {1, \dots, n}$ , $σ_{i} = m g u (t ≐ {s t r u c t}_{i} (r))$ , and $P_{i}^{'} = σ_{i} (P_{i})$ if $σ_{i} \neq ⊥$ , and $P_{i}^{'} = 0$ otherwise.

Note that for protocols satisfying Definition 8.5, either the unifier exists in every possibility or every possibility goes to $0$ . Now we can replace $t r y$ with pattern matching and a condition, because the intruder already knows the type of every message in their knowledge and thus knows whether the messages they send will have the correct structures for every destructor application to succeed (of course, a message with the correct structure can still fail, e.g., if it does not have the right key). Consider, for instance,
$r c v (X) . t r y Y := d s c r y p t (k, X) i n t r y Z := {p r o j}_{1} (Y) i n P$
If the intruder sends for $X$ any term that is not of the form $s c r y p t (K, p a i r (M, N), R)$ (for some $K$ , $M$ , $N$ , and $R$ ), then the destructors are going to fail. Thus we can split the $t r y$ ’s into a structural check that we can describe with a linear pattern like $s c r y p t (K, p a i r (M, N), R)$ and a condition on the pattern variables. This transformation allows us to get rid of destructors in processes entirely. The transformed example is
$r c v (s c r y p t (K, p a i r (M, N)), R) . i f k ≐ K t h e n P [Y \mapsto p a i r (M, N), Z \mapsto M]$

Definition 8.7 (Removing destructors)

Let $P$ be a transaction, from a protocol satisfying Definition 8.5, that contains a destructor application for decryption, that is, $P = C [t r y Y := d (t, X) i n P^{'}]$ for some process context $C [\cdot]$ that does not contain any destructor applications. Let $d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}$ be the corresponding rewrite rule with all variables freshly renamed. Let $σ = [X \mapsto c (k^{'}, X_{1}, \dots, X_{n}), Y \mapsto X_{i}]$ . Then we replace the transaction $P$ with $σ (C [i f t ≐ k t h e n P^{'}])$ .

In case of projectors or private extractors, $X$ may appear in $m$ destructor applications: we have $t r y Y^{j} := d^{j} (X) i n \dots$ , $j \in {1, \dots, m}$ , and rewrite rules of the form $d^{j} (c (t_{1}, \dots, t_{n})) \to t^{j}$ . Then we remove all destructor applications for $X$ since there are no keys, and we apply the substitution $[X \mapsto c (t_{1}, \dots, t_{n}), Y^{1} \mapsto t^{1}, \dots, Y^{m} \mapsto t^{m}]$ to the transaction.

This transformation is repeated until the transaction does not contain any destructor application anymore. The result is denoted $P_{p a t}$ .

Example 8.1
We adapt Example 2.1, where now the agent sends a message containing two nonces to the server and the server includes one of these nonces in their reply. We assume that we have three atomic types $a g e n t$ , $d e c i s i o n$ and $n o n c e$ . Every constant in the set $A g e n t$ and the constant $s$ are of type $a g e n t$ , and the constants $y e s, n o$ are of type $d e c i s i o n$ . We now apply the transformation to remove the destructors occurring in the following transaction $P$ :
$\begin{aligned} ⋆ x \in A g e n t . ⋆ y \in {y e s, n o} . \\ r c v (M : c r y p t (p k (a g e n t), p a i r (n o n c e, n o n c e), n o n c e)) . \\ t r y N := d c r y p t (i n v (p k (s)), M) i n \\ t r y N_{1} := {p r o j}_{1} (N) i n \\ t r y N_{2} := {p r o j}_{2} (N) i n \\ i f y ≐ y e s t h e n \\ ν r : n o n c e . s n d (c r y p t (p k (x), p a i r (y e s, N_{1}), r)) \\ e l s e ν r : n o n c e . s n d (c r y p t (p k (x), p a i r (n o, N_{2}), r)) \end{aligned}$

The first step is to remove $t r y N := d c r y p t (\dots)$ with the substitution $[M \mapsto c r y p t (X, Y, Z), N \mapsto Y]$ , and the second step is to remove both projections with the substitution $[Y \mapsto p a i r (Y_{1}, Y_{2}), N_{1} \mapsto Y_{1}, N_{2} \mapsto Y_{2}]$ . We now have $P_{p a t}$ :
$\begin{aligned} ⋆ x \in A g e n t . ⋆ y \in {y e s, n o} \\ r c v (c r y p t (X, p a i r (Y_{1}, Y_{2}), Z) : c r y p t (p k (a g e n t), p a i r (n o n c e, n o n c e), n o n c e)) \\ i f i n v (p k (s)) ≐ i n v (X) t h e n \\ i f y ≐ y e s t h e n \\ ν r : n o n c e . s n d (c r y p t (p k (x), p a i r (y e s, Y_{1}), r)) \\ e l s e ν r : n o n c e . s n d (c r y p t (p k (x), p a i r (n o, Y_{2}), r)) ◼ \end{aligned}$

Lemma 8.2
A protocol satisfying Definition 8.5 and its transformation to use pattern matching according to Definition 8.7 yield the same set of reachable ground states (up to logical equivalence of the contained formulas $α$ and $β$ ).

We now define how to compute the message patterns from a protocol specification using the $P_{p a t}$ version of transactions.
Definition 8.8 (Protocol message patterns)

For a protocol transaction $P$ , we define $p a t t e r n s (P)$ as the set of terms occurring in $P_{p a t}$ . For a memory cell $c e l l [\cdot]$ , we define the message pattern ${c e l l}_{p a t}$ as the message $C [X]$ , where $C [\cdot]$ is the ground context for the initial value of $c e l l [\cdot]$ and $X$ is a variable of type $Γ (c e l l)$ , that is, the argument type for the cell. For a protocol $S p e c$ , we define $p a t t e r n s (S p e c)$ as the union of the $p a t t e r n s (P)$ for every transaction $P$ and of the ${c e l l}_{p a t}$ for every $c e l l [\cdot]$ in the specification (up to $α$ -renaming of variables so they are distinct in each transaction/cell).

Example 8.2
Continuing Example 8.1, for the messages patterns of transaction $P$ , we consider the terms occurring in $P_{p a t}$ and this gives the following:
$\begin{aligned} p a t t e r n s (P) & = A g e n t \cup {x, y, r, y e s, n o, i n v (p k (s)), i n v (X), c r y p t (X, p a i r (Y_{1}, Y_{2}), Z)} \\ \cup {c r y p t (p k (x), p a i r (y e s, Y_{1}), r), c r y p t (p k (x), p a i r (n o, Y_{2}), r)} \end{aligned}$
where the type of $x$ is $a g e n t$ , $y$ is $d e c i s i o n$ , $X$ is $p k (a g e n t)$ and $r, Y_{1}, Y_{2}, Z$ are $n o n c e$ .
8.3. Type-flaw resistance

The core part in the proof of our typing result is that variables can always be instantiated with messages of the same type. We first define the set of sub-message patterns, which includes all subterms, well-typed instantiations and key terms. To prove our result we will use the fact that every message in the symbolic execution of the protocol is in this set of sub-message patterns.

Definition 8.9 (Sub-message patterns)

The set of sub-message patterns, $S M P (M)$ , of a set of terms $M$ is the least set closed under the following rules:

If $t \in M$ , then $t \in S M P (M)$ .

If $t \in S M P (M)$ and $t^{'}$ is a subterm of $t$ , then $t^{'} \in S M P (M)$ .

If $t \in S M P (M)$ and $σ$ is a well-typed substitution, then $σ (t) \in S M P (M)$ .

If $t \in S M P (M)$ , $k$ and $t^{'}$ are terms such that for some destructor $d$ we have $d (k, t) \to t^{'}$ as an instance of the rewrite rule for $d$ , then $k \in S M P (M)$ .

With rule (4), we ensure that relevant decryption keys are in $S M P (M)$ , because they may occur in the symbolic constraints when performing analysis steps.

We have now everything in place to formally define type-flaw resistance, which ensures that composed messages of different types cannot be unified.

Definition 8.10 (Type-flaw resistance)

A set of terms $M$ is type-flaw resistant iff for all $s, t \in S M P (M) ∖ V$ we have that $Γ (s) = Γ (t)$ if $s$ and $t$ are unifiable.

A protocol $S p e c$ is type-flaw resistant iff it satisfies Definition 8.5 and the set $p a t t e r n s (S p e c)$ is type-flaw resistant.

Example 8.3
The protocol from Example 8.2 is not type-flaw resistant, because in the message patterns we have the input pattern $c r y p t (X, p a i r (Y_{1}, Y_{2}), Z)$ and an output pattern $c r y p t (p k (x), p a i r (y e s, Y_{1}), r)$ , which can be unified even though they have different types: the mgu $[X \mapsto p k (x), Y_{1} \mapsto y e s, Y_{2} \mapsto y e s, Z \mapsto r]$ is not well-typed since $Γ (Y_{i}) \neq Γ (y e s)$ .

One can make the protocol type-flaw resistant by using formats, for instance, by replacing the function $p a i r$ with $f_{1}$ in the input and with $f_{2}$ in the outputs, where the $f_{i}$ are transparent functions (this requires also replacing the projectors in the process).
9. Typing result

9.1. Well-typedness of the constraint solving

We now turn back to the lazy intruder rules (Table 3) and show that, for a type-flaw resistant protocol, none of the rules perform ill-typed instantiations of intruder variables. In particular, recall that for the Unification rule, we have to unify two terms $s$ and $t$ which are not variables. If the protocol is type-flaw resistant and $s$ and $t$ are unifiable, then they must have the same type and their most-general unifier thus by well-typed.

Using type-flaw resistance, we can show that every lazy intruder rule preserves the well-typedness of the substitution $σ$ of variables performed in previous lazy intruder reduction steps. Let $t e r m s (A) = {t ∣ - l \mapsto t \in A or + R \mapsto t \in A}$ be the set of terms occurring in a FLIC $A$ . We extend the notion of well-typed substitutions to well-typed choices of recipes.

Definition 9.1 (Well-typed choice of recipes)

Let $A$ be a simple FLIC and $ρ$ be a choice of recipes for $A$ . We say that $ρ$ is well-typed w.r.t. $A$ iff for every $+ R \mapsto X \in A$ , we have $Γ (X) = Γ (ρ (A) (ρ (R)))$ .

We can now conclude that the lazy intruder results are doing only well-typed instantiations.

Theorem 9.1 (Lazy intruder well-typedness)

Let $S p e c$ be a type-flaw resistant protocol, $A$ be a simple FLIC such that $t e r m s (A) \subseteq S M P (p a t t e r n s (S p e c))$ and let $σ$ be a well-typed substitution. Then every $ρ \in L I (A, σ)$ is well-typed w.r.t. $A$ .

9.2. Well-typedness for state transitions

We have defined in Table 4 the relation $\Rightarrow$ that models the execution of processes for symbolic states. Since we have made an extension for pattern matching for ground states, we now define how to handle this construct for symbolic states, extending the relation $\Rightarrow$ and proving correctness for this case. To that end, we use the lazy intruder to consider all choices of recipes producing a linear pattern: the intruder can either use a label that produces a message of the same type, or compose the pattern themselves. We ensure that if a label is a solution in one FLIC, then it is a solution in every FLIC. This is why the linearity requirement in rewrite rules is crucial, since the type information cannot distinguish variables of the same type. For instance, if a message $r c v (f (X, X))$ was expected, it might be that in one FLIC a label $l$ maps to $f (t, t)$ for some message $t$ of type $τ$ , and in another FLIC the label $l$ maps to $f (t, s)$ , where $s ≐̸ t$ but $s$ is still of type $τ$ . We instead consider only linear patterns, so in the example we might have $r c v (f (X, Y))$ (the transaction could still check whether $X ≐ Y$ after the receive). Similarly, we forbid constants in patterns because otherwise we cannot, using only the type information, know which value matches a pattern.

Definition 9.2 (Receiving message patterns)

We extend the semantics of receive steps to support linear patterns, with the following transition if $t \notin V_{i n t r u d e r}$ :

\begin{aligned} (α_{0}, β_{0}, {(r c v (t) . P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d) \\ \Rightarrow {ρ ((α_{0}, β_{0}, {(P_{i}, ϕ_{i}, A_{i} . + R \mapsto X, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)) \\ ∣ ρ \in L I (A_{1} . + R \mapsto X, [X \mapsto t]), where R is a fresh recipe variable and \\ X is fresh intruder variable} \\ \cup {(α_{0}, β_{0}, {(0, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)} \end{aligned}

In case $t \in V_{i n t r u d e r}$ , the transition is the same as Receive in Table 4.

Example 9.1
Continuing Examples 8.1 and 8.3, the transaction $P_{p a t}$ starts by receiving the linear pattern $r c v (c r y p t (X, f_{1} (Y_{1}, Y_{2}), Z)$ . The intruder may compose that message themselves with the recipe $c r y p t (R_{X}, f_{1} (R_{Y_{1}}, R_{Y_{2}}), R_{Z})$ . Another solution, assuming they have observed earlier a message $- l \mapsto c r y p t (p k (s), f_{1} (n_{1}, n_{2}), r)$ sent by an honest agent, is to use the label $l$ to instantiate the pattern (if there are multiple possibilities, this label could map in other FLICs to other messages of the same type, e.g., where the nonces are different, and the substitutions are done accordingly in each process).

This conservative extension means that even when receiving patterns, we keep FLICs simple.
Lemma 9.1
Given a type-flaw resistant specification, then the set of reachable states in the symbolic semantics represents exactly the reachable states of the ground semantics.

The lazy intruder is used in two ways for the experiments: (i) to compute recipes that can be compared to labels, and (ii) to solve constraints whenever the outcome of an experiment depends on messages sent earlier. Since we have already shown that the lazy intruder results are well-typed, we have the guarantee that in a experiment with a pair $(l, r)$ , the label $l$ and the recipe $r$ produce messages of the same type and all transitions to determine the outcome of an experiment are only doing well-typed instantiations. Thus, there is nothing more to show for intruder experiments.

It remains to show that analysis also never introduces ill-typed instantiations. In a normal symbolic state, the intruder can perform analysis by decrypting messages in their knowledge, if they know the appropriate key. The analysis is always done in normal states, that is, after the experiments. In Definition 6.4, the analysis is performed through destructor oracles, which are defined as transactions available to the intruder. These destructor oracles do not work directly with the typing result: since they are defined as transactions, the computation of the sub-message patterns set $S M P$ would need to include the patterns from the destructor oracles. This prevents us from achieving type-flaw resistance even for reasonable protocols and when formats are used. For instance, consider a protocol that uses several times $c r y p t$ but with contents of different types, for example, $c r y p t (p k (a g e n t), f_{1} (a g e n t), n o n c e)$ and $c r y p t (p k (a g e n t), f_{2} (n o n c e), n o n c e)$ . To compute the message patterns, we have to consider the transformed destructor oracle that uses pattern matching instead of $t r y$ ; for $d c r y p t$ , this would yield the transaction $r c v (c r y p t (X, Y, Z)) . r c v (K) . i f K ≐ i n v (X) t h e n s n d (Y) . s n d (K)$ . We have the pattern $c r y p t (X, Y, Z)$ , because the decryption does not care about the actual content of the message but just about whether the key is correct. If we assume that there are multiple instances of this transaction where only the type annotations change (to cover all possible types), we would have $c r y p t (X_{1}, Y_{1}, Z_{1})$ and $c r y p t (X_{2}, Y_{2}, Z_{2})$ in $S M P$ , with, for instance, $Γ (X_{i}) = p k (a g e n t)$ , $Γ (Z_{i}) = n o n c e$ , $Γ (Y_{1}) = f_{1} (a g e n t)$ , and $Γ (Y_{2}) = f_{2} (n o n c e)$ . These two message patterns are unifiable but have different types, so type-flaw resistance is not achieved.

However, the procedure does not unconditionally apply destructor oracles but always restricts the step $r c v (X)$ to using a label $l$ as recipe for message $X$ , where $l$ maps to a message composed with the top-level constructor corresponding to the oracle. Therefore, we can be more precise and specialize the processes coming out of the destructor oracles: instead of a general pattern like $c r y p t (X, Y, Z)$ , we only consider instances of that pattern with messages that the intruder has observed, for example, $c r y p t (p k (a), f_{1} (A), R)$ .

We define analysis steps as part of the transition system instead of special transactions. We will show that, for a type-flaw resistant protocol, this alternative way of performing analysis is equivalent to using destructor oracles. The benefit of this formulation of analysis is that we ensure all messages are instances of the protocol message patterns, and thus we can obtain the typing result.
Definition 9.3 (Analysis transition)

Let $S$ be a reachable symbolic state in a type-flaw resistant protocol. The transition for analysis is:

\begin{aligned} (α_{0}, β_{0}, {(0, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d) \\ \Rightarrow^{∙} (α_{0}, β_{0}, {(P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d) \end{aligned}

S

is normal and there exist a label

l \in d o m (S)

and a public destructor

d \in Σ_{p u b}

such that

l

may be analyzed with

d

, that is, for every

i \in {1, \dots, n}

- l \mapsto c (k_{i}^{'}, t_{i}^{1}, \dots, t_{i}^{m}) \in A_{i}

where

d (k_{i}, c (k_{i}^{'}, t_{i}^{1}, \dots, t_{i}^{m})) \to t_{i}^{j}

(for some

j \in {1, \dots, m}

) is an instance of the rewrite rule for

d

and for every

i \in {1, \dots, n}

, let

P_{i} = r c v (Y) . i f Y ≐ k_{i} t h e n s n d (t_{i}^{j}) . s n d (k_{i})

. In case

c

is transparent, we define

P_{i} = s n d (t_{i}^{1}) . \dots . s n d (t_{i}^{m})

Note that the processes $P_{i}$ that we put in each possibility are exactly the instances of the corresponding destructor oracle, after transformation to pattern matching and substitution of the message to analyze with the respective message that the label maps to in each FLIC.

Example 9.2
Continuing Examples 8.1 and 8.3, suppose the intruder is an agent with their own private key, they have sent the message $c r y p t (p k (s), f_{1} (X_{1}, X_{2}), X_{3})$ to the server and received a reply. The intruder knowledge is represented with two possibilities, where one contains the following FLIC:
$- l_{1} \mapsto i n v (p k (i)) . + R_{1} \mapsto X_{1} . + R_{2} \mapsto X_{2} . + R_{3} \mapsto X_{3} . - l_{2} \mapsto c r y p t (p k (x), f_{2} (y e s, X_{1}), r_{1})$
The other possibility contains a similar FLIC with $f_{2} (n o, X_{2})$ in the reply. Applying the transition for analysis means that we execute $r c v (Y) . i f Y ≐ i n v (p k (x)) t h e n s n d (f_{2} (y e s, X_{1})) . s n d (i n v (p k (x))$ (respectively, $s n d (f_{2} (n o, X_{2}))$ ). Assuming the intruder does not know any other private key, the lazy intruder would return the label $l_{1}$ for instantiating the message $Y$ , which means $Y = i n v (p k (i))$ .

This yields two symbolic states, one in which decryption succeeded and one in which it failed. If it succeeded, the intruder would learn $x ≐ i$ and receive the decrypted pair; projecting the pair, the intruder would learn whether $y ≐ y e s$ . If it failed, they would learn $x ≐̸ i$ but nothing about $y$ .

We now consider two transition relations. $⟹$ is a relation on finished symbolic states induced by the transitions of Table 4 for executing a transaction with the evaluation of the process and by the normalization through experiments, where the transactions include the destructor oracles. More formally, $S ⟹ S^{'}$ iff there is a transaction $P$ (including destructor oracles) such that ${s t a r t (P, S)} \Rightarrow^{} ↣^{} C$ and $S^{'} \in C$ . In contrast, we define now a relation $⟹^{∙}$ that replaces the destructor oracles with the analysis transitions: $S ⟹^{∙} S^{'}$ iff either (there is a transaction $P$ (excluding destructor oracles) such that ${s t a r t (P, S)} \Rightarrow^{} ↣^{} C$ and $S^{'} \in C$ ) or ( $S \Rightarrow^{∙} S_{a}$ , ${S_{a}} \Rightarrow^{} ↣^{} C$ and $S^{'} \in C$ ).^d

We have made two changes to the procedure of Section 6: first, we have replaced explicit destructor applications with pattern matching (Definitions 8.7 and 9.2) and second, we have replaced destructor oracles with analysis transitions (Definition 9.3). In Lemmas 8.2 and 9.1, we have already shown that, for type-flaw resistant protocols, using pattern matching instead of explicit destructor applications is correct. Thus, for every transaction $P$ in the protocol specification, we now consider that the transaction $P_{p a t}$ is executed instead of $P$ . That way, we ensure that the messages in the symbolic constraints are always in the set of sub-message patterns $S M P$ of the protocol. For type-flaw resistant protocols, we can show that the analysis transitions are equivalent to destructor oracles, and thus the two transition relations are actually the same: $⟹ = ⟹^{∙}$ . Moreover, for type-flaw resistant protocols, all instantiations performed by the relation $⟹^{∙}$ are well-typed. Hence, we conclude and obtain our main typing result, which holds for an unbounded number of transitions.
Theorem 9.2 (Typing result)

Given a type-flaw resistant protocol, it is correct to restrict the intruder model to well-typed recipes/messages for verifying privacy.

9.3. Case studies for type-flaw resistance

We consider again the protocols already studied in Section 7, namely, our running example, Basic Hash, OSK, BAC, and Private Authentication.

Running example. We explained how to make the protocol type-flaw resistant using formats in Example 8.3.

Basic Hash.³⁴ Basic Hash is type-flaw resistant, where for the type annotations, we consider that we have the following atomic types: $t a g$ , used for the names of the tags and the privacy variable representing some tag name; $n o n c e$ , used for the fresh number created by the tag; and $o k$ , used for the reply from the reader when identification succeeds.

OSK.³⁵ This protocol is out of the scope of our typing result. In OSK, similarly to Basic Hash, a reader tries to identify a tag. However, in OSK, both the tag and the reader use memory cells as ratchets (initialized with a shared secret), instead of a MAC. The processes contain steps like $S := c e l l [x] . c e l l [x] := h (S)$ representing a turn of the ratchet with the application of a hash function, and thus the updates change the type of the content stored in memory, which is not allowed by Definition 8.4.

BAC.³⁶ In the model from Fernet and Mödersheim,³⁸ there is a non-empty $c a t c h$ branch and thus it violates our typing requirements. However, the interesting aspect of the $t r y$ in this case—namely that it can reveal whether it is the right agent—is independent of whether it is an encryption in the first place (which the intruder knows). Thus with the pattern matching notation introduced in Section 8, we can equivalently formulate this as a pattern match and an $i f$ condition with a non-empty $e l s e$ branch and achieve the requirements of type-flaw resistance.^e

Private Authentication.³⁷ The models of Fernet and Mödersheim³⁸ violate our typing requirements in three regards. First, the decoy message is a fresh nonce, while a normal reply is an encrypted message. It is intended that the intruder in general cannot tell which one is the case, violating our requirement that in this case the messages must have the same type. However, the original model from Abadi and Fournet³⁷ actually ensures that the decoy message is of the same type as the regular message: it is an encryption of a fresh nonce with a fresh key. Following this, the requirement is actually met, as the intruder now in each case knows the type of each message (just not whether its content and key are decoys or regular). Second, there are non-empty $c a t c h$ branches which however can now be solved using our pattern matching notation as in the case of BAC. Third, the message from the initiator and the reply from the responder are unifiable but do not have the same type. This is a type-flaw similar to Example 8.3, and we can use formats to solve this third issue and thus achieve type-flaw resistance.

For BAC and Private Authentication, we have been able to solve the issue of non-empty $c a t c h$ branches by using pattern matching. Thus, one may wonder if we could not do that in general and drop some restrictions on our typing result. In fact here is an example that we would not be able to transform to pattern matching: $r c v (X) . t r y Y := d s c r y p t (k, X) i n s n d (h (Y)) c a t c h s n d (s i g n (i n v (p k), X))$ , where the message in the $c a t c h$ is a signed (error) message on the input $X$ . Even if the intruder knows a priori that a particular message is not decipherable, obtaining the signature on it may be relevant in an attack that cannot be done in a well-typed way.

10. Related and future work

10.1. Decision procedure

It is a striking parallel between $(α, β)$ -privacy and equivalence-based privacy models that the vast amount of possibilities leads to very high complexity for procedures, as mentioned in, for example, Delaune and Hirschi.¹⁶ In equivalence-based approaches, the underlying problem is the static equivalence of (concrete) frames, representing two possible intruder knowledges. In $(α, β)$ -privacy, we have instead the multi message-analysis problem: there is just one concrete frame $c o n c r$ , the observed messages, and one or more ${s t r u c t}_{i}$ that result from a symbolic execution of the transactions by the intruder, where the privacy variables are not instantiated. Each possibility has a corresponding condition $ϕ_{i}$ , exactly one of which is actually true, and the intruder knows that $c o n c r$ is an instance of the corresponding ${s t r u c t}_{i}$ , that is, under the true instance of the privacy variables, $c o n c r \sim {s t r u c t}_{i}$ for the true $ϕ_{i}$ . Thus, evaluating the static equivalence can exclude several instantiations of privacy variables (even if there is just one $s t r u c t$ ) or rule out an entire possibility $ϕ_{i}$ . The methods for solving these two problems bear many similarities, in particular one essentially in both cases looks for a pair of recipes that distinguishes the frames, that is, the experiments that the intruder can do on their knowledge.

Like many other tools for a bounded number of sessions such as APTE¹⁰ and DeepSec,⁷ we also use the symbolic representation of the lazy intruder, using variables for messages sent by the intruder that are instantiated only in a demand-driven way when solving intruder constraints, turning frames into FLICs. This makes the frame distinction problems a magnitude harder (e.g. Baudet⁴⁴). In recipes we have to also take into account variables that represent what the intruder has sent earlier and the actual choice may allow for different experiments now. We tackle this problem by first considering a model where the intruder cannot use destructors. It suffices then to check only if any message in any ${s t r u c t}_{i}$ can be composed in a different way, which in turn can be solved with intruder constraint solving. This is the idea behind the notion of a normal state, that is, where all said experiments have been done, and we can thus check if the results of the experiments exclude any model of $α$ .

What makes the handling of destructors relatively easy is our requirement that all destructors yield a subterm or $f f$ , which the intruder and honest agents can observe. Thus we have no problem with “garbage terms” like decryption of a nonce. This allows us to show that it is sufficient that the intruder has applied destructors as far as possible to their knowledge using the oracles—the notion of an analyzed state: for any recipe that contains destructors, there is an equivalent recipe that uses the result of an oracle.

Concerning the complexity of decision procedures, Cheval et al.⁷ show that trace equivalence and labeled bisimilarity are both co-NEXP-complete for a bounded number of sessions of processes that can be specified in DeepSec. As it is shown in Theorem 2 of Gondron et al.¹, trace equivalence can be reduced to $(α, β)$ -privacy under a few restrictions. This indicates that also bounded-session $(α, β)$ -privacy may be co-NEXP-hard (since Cheval et al.⁷ like us limit algebraic reasoning to constructor/destructor theories) and also may be in co-NEXP (since the additional tasks in $(α, β)$ -privacy—reasoning about formulas and memory cells—are probably not exceeding co-NEXP). However, the details of such an argument are rather complicated so that we are at this point unable to prove a precise complexity class.

Recent work by Rajaona et al.,⁴⁵ in a spirit similar to our work, departs from equivalence-based approaches for privacy and instead uses epistemic model checking. It is implemented in the Phoebe tool⁴⁶ for a bounded number of sessions in a typed model. Rajaona et al.⁴⁵express the privacy properties as formulas in epistemic modal logic and a protocol specification generates a Kripke structure of “possible worlds.” While this has some similarities to our approach, the successor relation in this Kripke structure does not correspond to reachability but rather to (a kind of) indistinguishability from the intruder’s perspective. In contrast, $(α, β)$ -privacy does model a state space as a reachability relation and then every state itself contains a representation of all the possibilities that the intruder cannot exclude at this point. This allows us to keep a standard operational model of processes and the intruder (spanning the reachable states) and then put the reasoning about possibilities on top. As far as we can see, Rajaona et al.⁴⁵ do not support composed keys and cannot reason with ill-typed messages; an interesting question would thus be if our typing result can be adapted to their approach.

One may wonder if a procedure for an unbounded number of transitions is possible. If we look at the equivalence-based approaches, it seems the best option for this is the notion of diff-equivalence^8,16 as used in ProVerif⁵ and Tamarin.¹⁵ Roughly speaking, diff-equivalence sidesteps the problem of the intruder’s uncertainty in branching by requiring that the conditions are either true in both executions or both false. A similar restriction could be obtained in $(α, β)$ -privacy if we require that the intruder can always observe whether a condition was true or false, and we thus have just one ${s t r u c t}_{i}$ in each state. We are investigating whether this can allow for an unbounded-step procedure similar to ProVerif for $(α, β)$ -privacy. Again here is a striking similarity with equivalence-based approaches: it appears that one may either need a tight bound on the number of transitions or substantial restrictions on the processes one can model. There is, however, a static analysis approach^47,48 in form of a type checking procedure that guarantees trace equivalence for processes that do type in their system. This type system is not related in any way to the typed model and typing results in this article.

The major difference with other tools is in the way properties are specified and verified. Our tool looks at the reachable states from an $(α, β)$ -privacy specification of a protocol, and the privacy goals are constructed by the tool when exploring the transition system. Instead of verifying whether a number of properties hold, we thus verify whether the intruder is ever able to learn more than the information allowed (payload $α$ ). One advantage is that, in case of successful verification, we ensure that the intruder cannot learn anything more (about the privacy variables) than what the protocol is intentionally releasing. For some protocols such as Private Authentication, we believe that a characterization of the privacy goals with $(α, β)$ -privacy can give a better understanding of what guarantees the protocol actually provides, as we do not see an obvious way of expressing all the privacy goals with equivalences between processes.

10.2. Typing result

There are in our view two main benefits of typing results: robust engineering and decidability. First, robust engineering: we spend a few extra bits (if not already present) to explicitly say what messages mean and thereby “solve” type-flaw attacks. In fact, the intruder can still take an encrypted message and send it in a place where a nonce is expected (thus still sending an “ill-typed” message), but due to the clear annotation of the meaning, every honest agent will always treat this bitstring as a nonce and never try to decrypt it. Hence, if there is an attack, the same attack would work if the intruder had indeed sent a random nonce, and it is thus sound to consider an intruder model with only well-typed messages.

Model-checking approaches such as SATMC, OFMC, and CL-Atse of the AVISPA Tool and AVANTSSAR Platform^29,49–53 are concerned with bounded number of steps of the honest agents. However, for verifying protocol security without such bounds, one of the most popular tools is ProVerif,⁵ based on abstract interpretation, basically abstracting the fresh messages into a coarser set of abstract values, while maintaining unbounded steps of both honest agents and intruder. This is in general still undecidable, but with a typed model, it becomes decidable as shown by Blanchet and Podelski²⁰: essentially, we will have finitely many equivalence classes and thereby a finite set of well-typed messages that can occur in the saturation of Horn clauses that represent “what can happen.” A similar tool based on abstract interpretation is PSPSP,⁵⁴ which relies on a typed model and computes a finite fixedpoint for stateful protocols. While the abstraction is in general an over-approximation, PSPSP implements a decision procedure for the resulting abstraction under a typed model.

There are currently no tools and methods for $(α, β)$ -privacy that perform verification for an unbounded number of sessions; therefore we currently cannot demonstrate how a typed model can help here and possibly allow for a decision procedure here, as well, but this seems very likely.

Almost all existing typing results, for instance, Almousa et al.,²¹ Arapinis and Duflot,^22,23 Cortier and Delaune,²⁴ and Hess and Mödersheim^25,26 are concerned with standard trace properties such as secrecy and authentication. These results do not support privacy-type properties. A major challenge, and in fact the focus of our second contribution, is to give a typing result for privacy-type properties, where the most common approaches work with models based on trace-equivalence. Chrétien et al.^55,56 are, to our knowledge, the only major results for this question, and thus also the related work closest to ours. Since our approach is based on $(α, β)$ -privacy, it plays a quite different game but results in Section V of Gondron et al.¹ suggest that the two notions have similar expressive power.

Chrétien et al.⁵⁵ establish a typing result for trace equivalence in a process algebra, for an unbounded number of sessions. They introduce the notion of type-compliance, which requires that two unifiable encrypted subterms of the protocol are of the same type. The typing result is restricted to determinate processes and symmetric encryption. Significant extensions to this work are proposed by Chrétien et al.,⁵⁶ most notably providing a typing result for trace properties as an intermediate step, and enriching the supported class of cryptographic primitives. There are several decision procedures and decidability results^57–60 for privacy-type properties that rely on a typed model and use the existing typing results^55,56 to justify this. In contrast, our decision procedure does not require a typed model (the intruder can send messages of any type): it is actually the basis to show our typing result, namely for a type-flaw resistant protocol our lazy intruder approach will not run into any ill-typed substitution of privacy variables, and the remaining variables in a simple constraint can always be filled with well-typed values—thus establishing that there exists a well-typed attack whenever there exists an attack.

Our work is more general than Chrétien et al.⁵⁶ in the following three regards. First, they require that protocols are deterministic and they do not support if-then-else branching. In contrast, we allow non-deterministic choice of privacy variables by honest agents and if-then-else with conditions that can refer to all messages in scope (including privacy variables). This generalization is significant because it allows for protocols where the privacy also depends on the control flow, for example, where the intruder does not know whether a recipient accepted a message (and sent a legitimate answer) or not (and sent a decoy answer). Note also that a common restriction for verification tools is the notion of diff-equivalence which (at least in its original form) forbids dependence on conditions.

A second generalization is the handling of constructors and destructors. Chrétien et al.⁵⁶ do not model destructors in the processes (only in the intruder model) and rather obtains decryption by pattern matching. We instead support the explicit application of destructors by honest agents that $(α, β)$ -privacy uses in try-catch statements, where we only require the catch branch to be the nil process, that is, honest agents just abort when decryption fails. We in fact turn this into a pattern-matching problem, but it is part of the method (and its soundness proof) rather than being part of the model. Note that we assume that failure of a destructor is detectable; this is significant as an intruder may learn something from this failure. It seems reasonable to assume for the constructor-destructor theories supported here as most standard cryptographic implementations of primitives like AES and RSA indeed reveal if decryption failed. An interesting question is how to handle more algebraic properties like those of exponentiation with inverses that does not allow to detect failure to “decrypt” in general. However, such algebraic properties are not supported by any of the mentioned typing results.

A final generalization is that our approach supports protocol with long-term state (the memory cells). An interesting aspect of this is that there are several results concerning decidability based on typing and bounding the number of fresh nonces, for example, Chrétien et al.⁵⁵; one may wonder if this is also applicable in our case. However, there is an obstacle since our argument requires an infinite supply of constants of all types for the intruder to solve the disequalities that arise, among other things, from handling the long-term state. We thus leave this question to future work.

Another closely related problem is that of compositionality, which is also regarded as a relative soundness result: given that several protocols are secure in isolation, can we show that also their composition is secure? It works indeed also by similar methods, namely transforming an attack against the composed system to an attack against one component. Since here one of the key problems is when the attacker can use messages from one component in another component, and a solution can be similarly some form of tagging, one could call compositionality a form of “typing” for a family of protocols. In fact, typing can thus be a stepping stone for a compositionality result^24,26,61 and we plan to investigate if this is possible for $(α, β)$ -privacy.

Funding

The authors thank King′s College London and JISC for the financial support for the publication of this article.

Supplemental Material

sj-pdf-1-jcu-10.1177_0926227X251378716 - Supplemental material for A decision procedure and typing result for alpha-beta privacy

Supplemental material, sj-pdf-1-jcu-10.1177_0926227X251378716 for A decision procedure and typing result for alpha-beta privacy by Laouen Fernet, Sebastian Mödersheim and Luca Viganò in Journal of Computer Security

Footnotes

Declaration of conflicting interests

The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

Supplemental material

Supplemental material for this article is available online.

ORCID iDs

Laouen Fernet

Sebastian Mödersheim

Luca Viganò

Notes

References

Gondron

Mödersheim

Viganò

. Privacy as reachability. In: CSF 2022, 2022, pp.130–146. IEEE.

Mödersheim

Viganò

. Alpha-beta privacy. ACM Trans Priv Secur 2019; 22: 1–35.

Fernet

Mödersheim

. Deciding a fragment of (alpha, beta)-privacy. In: STM 2021, LNCS, Vol. 13075, 2021, pp.122–142. Springer.

Aparicio-Sánchez

Escobar

Gutiérrez

, et al. An optimizing protocol transformation for constructor finite variant theories in Maude-NPA. In: ESORICS 2020, LNCS, Vol. 12309, 2020, pp.230–250. Springer.

Blanchet

. An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW 2001, 2001, pp.82–96. IEEE.

Blanchet

Abadi

Fournet

. Automated verification of selected equivalences for security protocols. J Log Algebr Program 2008; 75: 3–51.

Cheval

Kremer

Rakotonirina

. DEEPSEC: deciding equivalence properties in security protocols theory and practice. In: SP 2018, 2018, pp.529–546. IEEE.

Cheval

Kremer

Rakotonirina

. The Hitchhiker’s guide to decidability and complexity of equivalence properties in security protocols. In: Logic, Language, and Security, LNCS, Vol. 12300, 2020, pp.127–145. Springer.

Rusinowitch

Turuani

. Protocol insecurity with a finite number of sessions and composed keys is NP-complete. Theor Comput Sci 2003; 299: 451–475.

10.

Cheval

. APTE: an algorithm for proving trace equivalence. In: TACAS 2014, LNCS, Vol. 8413, 2014, pp.587–592. Springer.

11.

Chadha

Cheval

Ciobâcă

, et al. Automated verification of equivalence properties of cryptographic protocols. ACM Trans Comput Logic 2016; 17: 1–32.

12.

Tiu

Dawson

. Automating open bisimulation checking for the spi calculus. In: CSF 2010, 2010, pp.307–321. IEEE.

13.

Tiu

Nguyen

Horne

. SPEC: an equivalence checker for security protocols. In: APLAS 2016, LNCS, Vol. 10017, 2016, pp.87–95. Springer.

14.

Barbosa

Barrett

Brain

, et al. cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022, LNCS, Vol. 13243, 2022, pp.415–442. Springer.

15.

Meier

Schmidt

Cremers

, et al. The TAMARIN prover for the symbolic analysis of security protocols. In: CAV 2013, LNCS, Vol. 8044, 2013, pp.696–701. Springer.

16.

Delaune

Hirschi

. A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J Log Algebraic Methods Program 2017; 87: 127–144.

17.

Cheval

Rakotonirina

. Indistinguishability beyond diff-equivalence in ProVerif. In: CSF 2023, 2023, pp.184–199. IEEE.

18.

Abadi

Needham

. Prudent engineering practice for cryptographic protocols. IEEE Trans Softw Eng 1996; 22: 6–15.

19.

Heather

Lowe

Schneider

. How to prevent type flaw attacks on security protocols. J Comput Secur 2003; 11: 217–244.

20.

Blanchet

Podelski

. Verification of cryptographic protocols: tagging enforces termination. Theor Comput Sci 2005; 333: 67–90.

21.

Almousa

Mödersheim

Modesti

, et al. Typing and compositionality for security protocols: a generalization to the geometric fragment. In: ESORICS 2015, LNCS, Vol. 9327, 2015, pp.209–229. Springer.

22.

Arapinis

Duflot

. Bounding messages for free in security protocols. In: FSTTCS 2007, LNCS, Vol. 4855, 2007, pp.376–387. Springer.

23.

Arapinis

Duflot

. Bounding messages for free in security protocols – extension to various security properties. Inf Comput 2014; 239: 182–215.

24.

Cortier

Delaune

. Safely composing security protocols. Form Methods Syst Des 2009; 34: 1–36.

25.

Hess

Mödersheim

. Formalizing and proving a typing result for security protocols in Isabelle/HOL. In: CSF 2017, 2017, pp.451–463. IEEE.

26.

Hess

Mödersheim

. A typing result for stateful protocols. In: CSF 2018, 2018, pp.374–388. IEEE.

27.

Fernet

Mödersheim

Viganò

. A decision procedure for alpha-beta privacy for a bounded number of transitions. In: CSF 2024, 2024, pp.159–174. IEEE.

28.

Hinrichs

Genesereth

. Herbrand logic. Technical Report LG-2006-02, Stanford University, USA. 2006. https://ginapp.stanford.edu/reports/LG-2006-02.pdf.

29.

Basin

Mödersheim

Viganò

. OFMC: A symbolic model checker for security protocols. Int J Inf Secur 2005; 4: 181–208.

30.

Millen

Shmatikov

. Constraint solving for bounded-process cryptographic protocol analysis. In: CCS 2001, 2001, pp.166–175. ACM.

31.

Cheval

Comon-Lundh

Delaune

. A procedure for deciding symbolic equivalence between sets of constraint systems. Inf Comput 2017; 255: 94–125.

32.

Brusó

Chatzikokolakis

den Hartog

. Formal verification of privacy for RFID systems. In: CSF 2010, 2010, pp.75–88. IEEE.

33.

Fernet

Mödersheim

. noname: formal verification of (alpha, beta)-privacy in security protocols, 2024. DOI: 10.5281/zenodo.14198336.

34.

Weis

Sarma

Rivest

, et al. Security and privacy aspects of low-cost radio frequency identification systems. In: Security in Pervasive Computing, LNCS, Vol. 2802, 2004, pp.201–212. Springer.

35.

Ohkubo

Suzuki

Kinoshita

. Cryptographic approach to “privacy-friendly” tags. In: RFID Privacy Workshop 2003, 2003.

36.

ICAO. Machine readable travel documents. Doc Series, Doc 9303. https://www.icao.int/publications/doc-series/doc-9303.

37.

Abadi

Fournet

. Private authentication. Theor Comput Sci 2004; 322: 427–476.

38.

Fernet

Mödersheim

. Private authentication with alpha-beta-privacy. In: OID 2023, 2023, LNI. GI.

39.

Baelde

Delaune

Moreau

. A method for proving unlinkability of stateful protocols. In: CSF 2020, 2020, pp.169–183. IEEE.

40.

Arapinis

Chothia

Ritter

, et al. Analysing unlinkability and anonymity using the applied pi calculus. In: CSF 2010, 2010, pp.107–121. IEEE.

41.

Chothia

Smirnov

. A traceability attack against e-passports. In: FC 2010, LNCS, Vol. 6052, 2010, pp.20–34. Springer.

42.

Filimonov

Horne

Mauw

, et al. Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity. In: ESORICS 2019, LNCS, Vol. 11735, 2019, pp.577–594. Springer.

43.

Cheval

Kremer

Rakotonirina

. Exploiting symmetries when proving equivalence properties for security protocols. In: CCS 2019, 2019, pp.905–922. ACM.

44.

Baudet

. Deciding security of protocols against off-line guessing attacks. In: CCS 2005, 2005, pp.16–25. ACM.

45.

Rajaona

Boureanu

Ramanujam

, et al. Epistemic model checking for privacy. In: CSF 2024, 2024, pp.1–16. IEEE.

46.

Rajaona

Boureanu

Ramanujam

, et al. Phoebe: epistemic model checker for privacy properties in security protocols. 2024. https://github.com/UoS-SCCS/phoebe/.

47.

Cortier

Grimm

Lallemand

, et al. A type system for privacy properties. In: CCS 2017, 2017, pp.409–423. ACM.

48.

Cortier

Grimm

Lallemand

, et al. Equivalence properties by typing in cryptographic branching protocols. In: POST 2018, LNCS, Vol. 10804, 2018, pp.160–187. Springer.

49.

Armando

Carbone

Compagna

. SATMC: a sat-based model checker for security-critical systems. In: TACAS 2014, LNCS, Vol. 8413, 2014, pp.31–45. Springer.

50.

Armando

Basin

Boichut

, et al. The AVISPA tool for the automated validation of internet security protocols and applications. In: CAV 2005, LNCS, Vol. 3576, 2005, pp.281–285. Springer.

51.

Armando

Arsac

Avanesov

, et al. The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: TACAS 2012, LNCS, Vol. 7214, 2012, pp.267–282. Springer.

52.

Mödersheim

Viganò

. The open-source fixed-point model checker for symbolic analysis of security protocols. In: FOSAD 2007/2008/2009 Tutorial Lectures, LNCS, Vol. 5705, 2009, pp.166–194. Springer.

53.

Turuani

. The CL-Atse protocol analyser. In: RTA 2006, LNCS, Vol. 4098, 2006, pp.277–286. Springer.

54.

Hess

Mödersheim

Brucker

, et al. Performing security proofs of stateful protocols. In: CSF 2021, 2021, pp.1–16. IEEE.

55.

Chrétien

Cortier

Delaune

. Typing messages for free in security protocols: the case of equivalence properties. In: CONCUR 2014, Vol. 8704, 2014, pp.372–386. Springer.

56.

Chrétien

Cortier

Dallon

, et al. Typing messages for free in security protocols. ACM Trans Comput Logic 2019; 21: 1–52.

57.

Chretien

Cortier

Delaune

. Decidability of trace equivalence for protocols with nonces. In: CSF 2015, 2015, pp.170–184. IEEE.

58.

Cortier

Dallon

Delaune

. SAT-Equiv: an efficient tool for equivalence properties. In: CSF 2017, 2017, pp.481–494. IEEE.

59.

Cortier

Dallon

Delaune

. Efficiently deciding equivalence for standard primitives and phases. In: ESORICS 2018, LNCS, Vol. 11098, 2018, pp.491–511. Springer.

60.

Cortier

Delaune

Sundararajan

. A decidable class of security protocols for both reachability and equivalence properties. J Autom Reason 2021; 65: 479–520.

61.

Hess

Mödersheim

Brucker

. Stateful protocol composition in Isabelle/HOL. ACM Trans Priv Secur 2023; 26: 1–36.

Choice	$(α, β_{0}, γ, {(m o d e x \in D . P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$
	$\to (α^{'}, β_{0}^{'}, γ \land x ≐ c, {(P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$
	for every $c \in D$
	where $α^{'} \equiv α \land x \in D$ and $β_{0}^{'} \equiv β_{0}$ if $m o d e = ⋆$ , and $α^{'} \equiv α$ and $β_{0}^{'} \equiv β_{0} \land x \in D$ if $m o d e = ⋄$
Receive	$(α, β_{0}, γ, {(r c v (X) . P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$
	$\to (α, β_{0}, γ, {(P_{i} [X \mapsto {s t r u c t}_{i} (r)], ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$
	for every recipe $r$ over the domain of the ${s t r u c t}_{i}$
Cell read	$(α, β_{0}, γ, {(X := c e l l [s] . P, ϕ, s t r u c t, δ)} ⊎ P) \to (α, β_{0}, γ, {(P^{'}, ϕ, s t r u c t, δ)} \cup P)$
	where $δ_{\| c e l l} = c e l l [s_{1}] := t_{1} . \dots . c e l l [s_{k}] := t_{k}$ , the initial value of $c e l l$ is given by ground context $C [\cdot]$
	and $P^{'} = i f s ≐ s_{1} t h e n P [X \mapsto t_{1}] e l s e \dots i f s ≐ s_{k} t h e n P [X \mapsto t_{k}] e l s e P [X \mapsto C [s]]$
Cell write	$(α, β_{0}, γ, {(c e l l [s] := t . P, ϕ, s t r u c t, δ)} ⊎ P) \to (α, β_{0}, γ, {(P, ϕ, s t r u c t, c e l l [s] := t . δ)} \cup P)$
Conditional	$(α, β_{0}, γ, {(i f ψ t h e n P_{1} e l s e P_{2}, ϕ, s t r u c t, δ)} ⊎ P)$
	$\to (α, β_{0}, γ, {(P_{1}, ϕ \land ψ, s t r u c t, δ), (P_{2}, ϕ \land \neg ψ, s t r u c t, δ)} \cup P)$
Release	$(α, β_{0}, γ, {(⋆ ψ . P, ϕ, s t r u c t, δ)} ⊎ P) \to (α^{'}, β_{0}, γ, {(P, ϕ, s t r u c t, δ)} \cup P)$
	where $α^{'} \equiv α \land ψ$ if $γ ╞ ϕ$ , and $α^{'} \equiv α$ otherwise
Eliminate	$S = (α, β_{0}, γ, {(P, ϕ, s t r u c t, δ)} ⊎ P) \to (α, β_{0}, γ, P)$
	if $β (S) ⧸ ╞ ϕ$
Send	$(α, β_{0}, γ, {(s n d (t_{i}) . P_{i}, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}} ⊎ P)$
	$\to (α, β_{0} \land ⋁_{i = 1}^{n} ϕ_{i}, γ, {(P_{i}, ϕ_{i}, {s t r u c t}_{i} . l \mapsto t_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$
	if $γ ╞ ⋁_{i = 1}^{n} ϕ_{i}$ and every process in $P$ is $0$ , where $l$ is a fresh label
Terminate	$(α, β_{0}, γ, {(0, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}} ⊎ P)$
	$\to (α, β_{0} \land ⋁_{i = 1}^{n} ϕ_{i}, γ, {(0, ϕ_{i}, {s t r u c t}_{i}, δ_{i}) ∣ i \in {1, \dots, n}})$
	if $γ ╞ ⋁_{i = 1}^{n} ϕ_{i}$ , $P$ is non-empty and every process in $P$ starts with $s n d (\cdot)$

Choice	$(α_{0}, β_{0}, {(m o d e x \in D . P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)$
	$\Rightarrow {(α_{0}^{'}, β_{0}^{'}, {(P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)}$
	where $α_{0}^{'} \equiv α_{0} \land x \in D$ and $β_{0}^{'} \equiv β_{0}$ if $m o d e = ⋆$ , and $α_{0}^{'} \equiv α_{0}$ and $β_{0}^{'} \equiv β_{0} \land x \in D$ if $m o d e = ⋄$
Receive	$(α_{0}, β_{0}, {(r c v (X) . P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)$
	$\Rightarrow {(α_{0}, β_{0}, {(P_{i}, ϕ_{i}, A_{i} . + R \mapsto X, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)}$
	where $R$ is a fresh recipe variable
Cell read	$(α_{0}, β_{0}, {(X := c e l l [s] . P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$
	$\Rightarrow {(α_{0}, β_{0}, {(P^{'}, ϕ, A, X, α, δ)} \cup P, C h e c k e d)}$
	where $δ_{\| c e l l} = c e l l [s_{1}] := t_{1} . \dots . c e l l [s_{k}] := t_{k}$ , the initial value of $c e l l$ is given by ground context $C [\cdot]$
	and $P^{'} = i f s ≐ s_{1} t h e n P [X \mapsto t_{1}] e l s e \dots i f s ≐ s_{k} t h e n P [X \mapsto t_{k}] e l s e P [X \mapsto C [s]]$
Cell write	$(α_{0}, β_{0}, {(c e l l [s] := t . P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$
	$\Rightarrow {(α_{0}, β_{0}, {(P, ϕ, A, X, α, c e l l [s] := t . δ)} \cup C h e c k e d)}$
	Let $P = t r y X := d (t_{1}, t_{2}) i n P_{1} c a t c h P_{2}$ , consider a fresh instance $d (k, c (k^{'}, X_{1}, \dots, X_{n})) \to X_{i}$
	of the rewrite rule for $d$ , let $ψ = t_{1} ≐ k \land t_{2} ≐ c (k^{'}, X_{1}, \dots, X_{n})$ , and $σ = m g u (ψ)$ .
	The rules for $t r y$ - $c a t c h$ are:

	$(α_{0}, β_{0}, {(P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$
Destructor (1.1)	$\Rightarrow {ρ ((α_{0}, β_{0}, {(P_{1} [X \mapsto s_{i}], ϕ \land \underline{σ^{'}}, A, X, α, δ), (P_{2}, ϕ \land \neg \underline{σ^{'}}, A, X, α, δ)} \cup P, C h e c k e d))$
	$∣ ρ \in L I (A, σ), let c (s_{0}, \dots, s_{n}) = σ_{ρ}^{A} (t_{2}) and σ^{'} = m g u (σ_{ρ}^{A} (ψ))}$
Destructor (1.2)	$\cup {\begin{cases} {(α_{0}, β_{0}, {(P_{2}, ϕ, A, X \land \forall \vec{Y} . \neg σ, α, δ)} \cup P, C h e c k e d)} & if σ (A) is not simple \\ \emptyset & otherwise \end{cases}$
	if $σ \neq ⊥$ , where $\vec{Y} = i v a r s (σ) ∖ i v a r s (A)$

Destructor (2)	$(α_{0}, β_{0}, {(P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d) \Rightarrow {(α_{0}, β_{0}, {(P_{2}, ϕ, A, X, α, δ)} \cup P, C h e c k e d)}$
	if $σ = ⊥$
Conditional	$(α_{0}, β_{0}, {(i f R (t_{1}, \dots, t_{n}) t h e n P_{1} e l s e P_{2}, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d)$
	$\Rightarrow {(α_{0}, β_{0}, {(P_{1}, ϕ \land R (t_{1}, \dots, t_{n}), A, X, α, δ), (P_{2}, ϕ \land \neg R (t_{1}, \dots, t_{n}), A, X, α, δ)} \cup P, C h e c k e d)}$

	For $i f s ≐ t t h e n P_{1} e l s e P_{2}$ , the transitions are like Destructor but with $ψ \equiv_{Σ} s ≐ t$
Release	$(α_{0}, β_{0}, {(⋆ ψ . P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d) \Rightarrow {(α_{0}, β_{0}, {(P, ϕ, A, X, α \land ψ, δ)} \cup P, C h e c k e d)}$
Eliminate	$(α_{0}, β_{0}, {(P, ϕ, A, X, α, δ)} ⊎ P, C h e c k e d) \Rightarrow {(α_{0}, β_{0}, P, C h e c k e d)}$
	if $α_{0} \land β_{0} ⧸ ╞ ϕ$
Send	$(α_{0}, β_{0}, {(s n d (t_{i}) . P_{i}, ϕ_{i}, A_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}} ⊎ P, C h e c k e d)$
	$\Rightarrow {(α_{0}, β_{0} \land ⋁_{i = 1}^{n} ϕ_{i}, {(P_{i}, ϕ_{i}, A_{i} . - l \mapsto t_{i}, X_{i}, α_{i}, δ_{i}) ∣ i \in {1, \dots, n}}, C h e c k e d)}$
	$\cup {(α_{0}, β_{0} \land ⋀_{i = 1}^{n} \neg ϕ_{i}, P, C h e c k e d)}$
	if every process in $P$ is $0$ , where $l$ is a fresh label

A decision procedure and typing result for alpha-beta privacy

Abstract

Keywords

1. Introduction

1.1. A decision procedure

1.2. A typing result

1.3. Outline

2. Preliminaries and problem definition

2.1. ( α , β )-privacy for a state

2.2. ( α , β )-privacy for a transition system

Definition 2.2 (Protocol specification)

Example 2.1. (Running example)

Definition 2.3 (Multi-message-analysis problem)

Definition 2.4 (The reachability problem)

3. FLICs: Framed lazy intruder constraints

3.1. Defining constraints

Definition 3.1 (FLIC)

Definition 3.3 (Simple FLIC)

Definition 3.6 (Lazy intruder rules)

Table 3. Lazy intruder rules.

Theorem 3.1 (Lazy intruder correctness)

4. The symbolic states

Definition 4.1 (Symbolic state)

Definition 4.2 (Choice of recipes for a symbolic state)

Definition 4.4 (Privacy substitution)

Definition 5.3 (Pairs and normal symbolic state)

Definition 5.4 (Compose-checks)

Definition 5.5 (Consistent symbolic state)

6.1. The supported algebraic theories

Definition 6.1 (Algebraic theory)

6.2. Destructor oracles

Definition 6.2 (Destructor oracle)

6.3. Analysis strategy

Definition 6.3 (Term marking)

Definition 6.4 (Analysis strategy)

Theorem 6.1 (Analysis correctness)

7. Tool support and case studies

8. Typed model

8.1. Type system

Definition 8.1 (Typing function)

Definition 8.2 (Well-typed substitution)

Definition 8.3 (Algebraic theory for typing result)

Definition 8.4 (Type checking)

Definition 8.5 (Requirements)

Lemma 8.1 Let S be a reachable state in a protocol satisfying Definition 8.5, s t r u c t 1 , … , s t r u c t n be the frames in S and r be a recipe over the domain of the s t r u c t i . Then Γ ( s t r u c t 1 ( r ) ) = ⋯ = Γ ( s t r u c t n ( r ) ) . 8.2. Message patterns

Definition 8.9 (Sub-message patterns)

Definition 8.10 (Type-flaw resistance)

9.1. Well-typedness of the constraint solving

Definition 9.1 (Well-typed choice of recipes)

Theorem 9.1 (Lazy intruder well-typedness)

9.2. Well-typedness for state transitions

Definition 9.2 (Receiving message patterns)

9.3. Case studies for type-flaw resistance

10. Related and future work

10.1. Decision procedure

10.2. Typing result

Funding

Supplemental Material

sj-pdf-1-jcu-10.1177_0926227X251378716 - Supplemental material for A decision procedure and typing result for alpha-beta privacy

Footnotes

Declaration of conflicting interests

Supplemental material

ORCID iDs

Notes

References

2.1. ( $α, β$ )-privacy for a state

2.2. ( $α, β$ )-privacy for a transition system

Table 3.
Lazy intruder rules.