PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL

Abstract

In protocol verification, we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants such as Isabelle/HOL. The latter provides overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely, and thus the risk of erroneously verifying a flawed protocol is nonnegligible. There are a few works that try to combine the advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step toward achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge, this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results, such as the soundness of a typed model.

1. Introduction

There are at least three reasons why it is desirable to perform proofs of security in a proof assistant such as Isabelle/HOL or Rocq. First, it gives us an overwhelming assurance that the proof of security is actually a proof and not just the result of a bug in a complex verification tool. This is because the basic idea of an LCF-style theorem prover is to have an abstract datatype theorem so that new theorems can only be constructed through functions that correspond to accepted proof rules; thus implementing just this data type correctly prevents us from ever accepting a wrong proof as a theorem, no matter what complex machinery we build for automatically finding proofs. Second, a human may have an insight into how to easily prove a particular statement where a “stupid” verification algorithm may run into a complex check or even be infeasible. Third, the language of a proof assistant can formalize all accepted mathematics, so there is no narrow limit on what aspects of a system we can formalize. For instance, we have proved in Isabelle/HOL a compositionality result ¹ for our protocol model: given a set of protocols for which we have proved security and that meet a number of requirements, then also their composition is correct. Since also the said requirements are proved in Isabelle, we arrive at a full security proof of the entire system checked by Isabelle. A result like this is beyond the scope of any standard verification tool. Note also that as part of the composition, some of the component protocols may be proved secure by different methods or even automatically.

Paulson ² and Bella ³ developed a protocol model in Isabelle and performed several security proofs in this model, for example, Paulson. ⁴ That the proof of a single protocol (for which even some automated security proofs exist) is worth a publication, underlines how demanding it is to conduct proofs in a proof assistant. This raised the question of how one can automatically generate machine-checkable proofs. Goubault-Larrecq ⁵ shows how one can verify Horn-clause based descriptions (e.g., in ProVerif ⁶ internally) by finding a (finite) model for it that can easily be machine-checked. Scyther-proof ⁷ produces Isabelle proofs for the backward search-based tool Scyther. ⁸

A drawback of these approaches so far is that they only apply to Alice-and-Bob style protocols where there is no relation between several sessions. When we consider, however, any system that maintains a mutable long-term state, for example, a security token or a server that maintains a simple database, we hit the limits of several tools for infinite sessions such as Scyther. For instance, ProVerif is based on an abstract interpretation that basically abstracts away from states (and time). To overcome these limitations, several amendments to the abstraction were suggested, such as set-based abstraction, ⁹ which our approach is based on, StatVerif ¹⁰ and GSVerif, ¹¹ and many of these ideas are now incorporated into ProVerif.

Moreover, there is also a tool that went a completely different way: Tamarin ¹² (which also is not limited to protocols without long-term state) is actually inspired by Scyther-proof and has the flavor of a proof assistant environment itself, namely combining partial automation with interactive proofs, that is, supplying the right lemmas to show. Interestingly, there is no connection to Isabelle or other LCF-style theorem provers, while one may intuitively expect that this should be easily possible. The reason seems to be that Tamarin combines several specialized automated methods, especially for term algebraic reasoning, that would be quite difficult to “translate” into Isabelle/HOL—at least the authors of this paper do not see an easy way to make such a connection. In fact, if it were possible for a large class of stateful protocols, the combination of overwhelming assurance of proofs and a high degree of automation would be extremely desirable.

The goal of this work is to achieve exactly this combination for a well-defined fragment of stateful protocols. We are here using as a foundation the Isabelle/HOL formalization and protocol model by Hess et al. ¹³ There are several reasons for this choice. First, the proof technique we present in this paper works only in a restricted typed model. Fortunately, that formalization ships with a typing result, ¹⁴ namely an Isabelle theorem that says: if a protocol is secure in this typed model, then it is also secure in the full model without the typing restriction—as long as the protocol in question satisfies a number of basic requirements. Thus, we get fully automated Isabelle proofs for most protocols even without a typing restriction.

Second, as described already in Hess et al., ¹ building on this protocol model has allowed us to seamlessly integrate the PSPSP tool with the compositional reasoning results: a user can specify multiple protocols in PSPSP and give annotations for their composition. The PSPSP tool can then automatically check the requirements for the composition, automatically verify each component individually, and obtain a proof of the composed system entirely verified by Isabelle/HOL from beginning to end.

Third, related to that, one may of course prove only some components of a composition automatically with PSPSP and prove other components manually when they do not fall into the scope of what PSPSP can support. Also, one may integrate manual reasoning with automated PSPSP analysis: when the runtime of automated analysis is high, a human prover may have an idea to prove some aspect more easily avoiding, for example, some lengthy enumerations.

The automated proof technique we employ in PSPSP is based on the set-based abstraction approach of Mödersheim and Bruni ¹⁵ and Bruni et al. ¹⁶ The basic idea is that we represent the long-term state of a protocol by a number of sets; the protocol rules specify how protocol participants shall insert elements into a set, remove them from a set, and check for membership or nonmembership. (The intruder may also be given access to some sets.) Based on this, we follow an abstract interpretation approach that identifies those elements that have the same membership status in all sets and compute a fixed point, more precisely a representation of all messages that the intruder can ever know after any trace of the protocol (including the set membership status of elements that occur in these messages). One may wonder if considering just intruder-known messages limits the approach to secrecy goals, but thanks to sets, a wide range of trace-based properties can be expressed by reduction to the secrecy of a special constant $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ . (We cannot, however, handle privacy-type properties in this way.)

We thus check if the fixed point contains the $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ constant, and if so, we can abort the attempt to prove the protocol correct. This may also happen for a secure protocol as the abstraction entails an overapproximation. However, vice versa, if $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ is not in the fixed point, then the protocol is secure—if the fixed point is indeed a sound representation of the messages the intruder can ever know. The proof we perform in Isabelle now is thus basically to show that the fixed point is closed under every protocol rule: given any trace where the intruder knows only messages covered by the fixed point, then every extension by one protocol step reveals only messages also covered by the fixed point.

Contributions

Our main contribution is the formalization in Isabelle of the abstract interpretation approach for stateful protocols, as the PSPSP tool. In a nutshell, we have implemented in Isabelle the computation of the abstract fixed point—the proof idea, so to speak—and how Isabelle can convince herself that this fixed point covers everything that can happen in the concrete protocol. The Isabelle security proof that one obtains consists of two main parts: first, we have a number of protocol-independent theorems that we have proved in Isabelle once and for all, and second, for every protocol and fixed point, we have a number of checks that Isabelle can directly execute to establish the correctness of the given protocol. The entire protocol-independent formalization consists of more than 25,000 lines of Isabelle code (definitions, theorems, and proofs).

A second contribution is the development and integration into Isabelle of a simple protocol specification language for stateful protocols that is based on a notion of atomic transactions: in a transaction, an entity may receive a message, consult its long-term database, make changes to the database, and finally send out a reply. This language is more high-level than, for instance, multiset rewriting while directly defining a state-transition system. The language additionally allows the specification of analysis rules, which are rules that express how the intruder can extract knowledge from received messages built using cryptographic functions.

New contributions in this journal paper

The aforementioned contributions were also part of the conference version of the present paper. ¹⁷ In the present journal version, we additionally have a number of new contributions and improvements. First, we have improved the verification method itself. We have devised a novel method for checking the fixed point coverage that significantly improves the runtime for two of our examples. We have also improved the check that the fixed point is analyzed, that is, covers also the knowledge that the intruder can gain by applying the analysis rules.

Second, we have improved the user experience of the tool, for example, by better error messages and support for understanding attacks. A trace of derivation steps for the $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ constant can be of great help: either this is a true attack and one can strengthen the protocol to prevent the attack, or it is a false positive induced by the over-approximation, and this may give a hint how to refine the model of the protocol. Our tool can now calculate such traces and present them to the user.

Third, we have two improvements on the semantic level of PSPSP. One improvement on the semantic level of PSPSP is that we have a soundness proof for the transformation that the tool is doing. The abstract interpretation approach requires that all values be sent out in the network as part of some message. However, our syntax for transactions does not enforce this, because it is reasonable to have a transaction that inserts a value in a set/database without sending it out as part of some message. Our tool solves this by a transformation that for every newly generated value $v$ in a transaction sends out a special message $\mathsf{o}\mathsf{c}\mathsf{c}\mathsf{u}\mathsf{r}\mathsf{s}(v)$ and modifies each transaction to receive $\mathsf{o}\mathsf{c}\mathsf{c}\mathsf{u}\mathsf{r}\mathsf{s}(v)$ for every nonfresh value $v$ . The tool includes this transformation, so the modelers do not have to make this encoding themselves. Now we have proved the soundness of this transformation. Another improvement concerns the definition of the semantics of transactions. While it is defined via symbolic traces of unbounded length (which is particularly practical for relative soundness results such as typing and compositionality), we have also proved the equivalence with a more standard ground semantics.

Fourth, we have a major new case study from working with the Danish company Logos. In this case study, we verify a protocol that the company is using for a travel card solution. The verification with PSPSP revealed a flaw in the protocol. After repairing the flaw, we were able to prove the security of the fixed protocol using PSPSP.

The complete formalization is available at the Archive of Formal Proofs (AFP) as the entry titled Automated Stateful Protocol Verification: ¹⁸ https://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html The latest development version and related works can be found at the following webpage: https://people.compute.dtu.dk/samo/pspsp.html

The rest of this paper is organized as follows: Section 2 introduces preliminaries, Section 3 defines the protocol model, Section 4 explains the set-based abstraction approach, Section 5 introduces the protocol checks with optimizations introduced in Section 6, Section 7 presents and reports on the results of a number of experiments applying our approach to a selection of protocols, Section 8 gives a short demonstration of PSPSP from the user’s perspective (and discusses the application of the compositionality result ¹ ), Section 9 presents and reports on a case study where we apply PSPSP to a protocol by the Danish company Logos and finally Section 10 is the conclusion where we also discuss related work.

2. Preliminaries

2.1. Terms and substitutions

We model terms over a countable set $\mathrm{\Sigma }$ of symbols (also called function symbols or operators) and a countable set $\mathcal{V}$ of variables disjoint from $\mathrm{\Sigma }$ . Each symbol in $\mathrm{\Sigma }$ has an associated arity, and we denote by ${\mathrm{\Sigma }}^n$ the symbols of $\mathrm{\Sigma }$ of arity $n$ . A term built from $S\subseteq \mathrm{\Sigma }$ and $X\subseteq \mathcal{V}$ is then either a variable $x\in X$ or a composed term of the form $f(t_1,\dots ,t_n),$ where each $t_i$ is a term built from $S$ and $X$ , and $f\in S^n$ . The set of terms built from $S$ and $X$ is denoted by $\mathcal{T}(S,X)$ . Arbitrary terms $t$ usually range over $\mathcal{T}(\mathrm{\Sigma },\mathcal{V})$ , unless stated otherwise. By $\mathit{s}\mathit{u}\mathit{b}\mathit{t}\mathit{e}\mathit{r}\mathit{m}\mathit{s}(t)$ we denote the set of subterms of $t$ .

The set of constants $\mathcal{C}$ is defined as the symbols with arity zero: $\mathcal{C}\equiv {\mathrm{\Sigma }}^0$ . It contains the following disjoint subsets:

The countable set $\mathbb{V}$ of concrete values (or just values).

The finite set $\mathbb{A}$ of abstract values.

The finite set $\mathbb{E}$ of enumeration constants.

The finite set $\mathbb{S}$ of database constants. [The databases that they refer to are simply sets of messages, and we therefore often refer to them simply as “sets” in this paper.]

And a special constant $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ .

Terms represent the messages sent during the run of a protocol, and the concrete values are atomic parts of these messages that are generated during the execution of the protocol, such as public keys, nonces, shared keys, and other data. The abstract values are then abstractions of the concrete values in the abstract interpretation approach that we are using. We elaborate on these in Section 4 and choose there a specific set for $\mathbb{A}$ that suits the concrete abstract interpretation approach we are using.

The analyst, that is, the author of a protocol specification, may freely choose $\mathbb{E}$ and $\mathbb{S}$ as well as any number of function symbols $\mathbb{F}$ with their arities (disjoint from the above subsets) which represent constructors and cryptographic functions used to build the messages.

Example 1

Consider a protocol with two users $\mathsf{a}$ and $\mathsf{b}$ , where each user $a$ has its own keyring $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(a)$ , and the server maintains databases of the currently valid keys $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(a)$ and revoked keys $\mathsf{r}\mathsf{e}\mathsf{v}\mathsf{o}\mathsf{k}\mathsf{e}\mathsf{d}(a)$ for $a$ . For such a protocol we define $\mathbb{E}=\{\mathsf{a},\mathsf{b}\}$ and $\mathbb{S}=\{\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(a),\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(a),\mathsf{r}\mathsf{e}\mathsf{v}\mathsf{o}\mathsf{k}\mathsf{e}\mathsf{d}(a)\mid a\in \mathbb{E}\}$ .

We regard all elements of $\mathbb{S}$ as constants, despite the function notation, which is just to ease specification. This work is currently limited to finite enumerations and finite sets, as handling infinite domains would require substantial complications of the approach (e.g., a symbolic representation or a small system result).

Arbitrary constants are usually denoted by $a$ , $b$ , $c$ , and $d$ , whereas arbitrary variables are denoted by $x$ , $y$ , and $z$ . By $\overline{x}$ , we denote a finite list $x_1,\dots ,x_n$ of variables.

We furthermore partition $\mathrm{\Sigma }$ into the public symbols (those symbols that are available to the intruder) and the private symbols (those that are not). We denote by ${\mathrm{\Sigma }}_{\mathit{p}\mathit{u}\mathit{b}}$ and ${\mathrm{\Sigma }}_{\mathit{p}\mathit{r}\mathit{i}\mathit{v}}$ the set of public and private symbols, respectively. By ${\mathcal{C}}_{\mathit{p}\mathit{u}\mathit{b}}$ and ${\mathcal{C}}_{\mathit{p}\mathit{r}\mathit{i}\mathit{v}}$ , we then denote the sets of public and private constants, respectively. The constant $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ , the values $\mathbb{V}$ , the abstract values $\mathbb{A}$ , and the database constants $\mathbb{S}$ are all private.

The set of variables of a term $t$ is denoted by $\mathit{f}\mathit{v}(t)$ , and we say that $t$ is ground iff $\mathit{f}\mathit{v}(t)=\mathrm{\varnothing }$ . Both definitions are extended to sets of terms as expected.

A substitution is a mapping from variables $\mathcal{V}$ to terms. The substitution domain (or just domain) $\mathit{d}\mathit{o}\mathit{m}(\theta )$ of a substitution $\theta$ is defined as the set of those variables that are not mapped to themselves by $\theta$ : $\mathit{d}\mathit{o}\mathit{m}(\theta )\equiv \{x\in \mathcal{V}\mid \theta (x)\ne x\}$ . The substitution range (or just range) $\mathit{r}\mathit{a}\mathit{n}(\theta )$ of $\theta$ is the image of the domain of $\theta$ under $\theta$ : $\mathit{r}\mathit{a}\mathit{n}(\theta )\equiv \theta (\mathit{d}\mathit{o}\mathit{m}(\theta ))$ . For finite substitutions, we use the notation $[x_1\mapsto t_1,\dots ,x_n\mapsto t_n]$ to denote the substitution with domain $\{x_1,\dots ,x_n\}$ and range $\{t_1,\dots ,t_n\}$ that sends each $x_i$ to $t_i$ . Substitutions are extended to composed terms homomorphically as expected. A substitution $\theta$ should be applied to a term $t$ only when $\mathit{f}\mathit{v}(t)\subseteq \mathit{d}\mathit{o}\mathit{m}(\theta )$ . A substitution $\delta$ is injective iff $\delta (x)=\delta (y)$ implies $x=y$ for all $x,y\in \mathit{d}\mathit{o}\mathit{m}(\delta )$ . An interpretation is a substitution $\mathcal{I}$ such that $\mathit{d}\mathit{o}\mathit{m}(\mathcal{I})=\mathcal{V}$ and $\mathit{r}\mathit{a}\mathit{n}(\mathcal{I})$ is ground. A variable renaming $\rho$ is an injective substitution such that $\mathit{r}\mathit{a}\mathit{n}(\rho )\subseteq \mathcal{V}$ . An abstraction substitution is a substitution $\delta$ such that $\mathit{r}\mathit{a}\mathit{n}(\delta )\subseteq \mathbb{A}$ .

2.2. The intruder model

We employ the intruder model from Hess et al., ¹³ which is in the style of Dolev and Yao: the intruder controls the communication medium and can encrypt and decrypt with known keys, but the intruder cannot break cryptography. More formally, we define that the intruder can derive a message $t$ from a set of known messages $M$ (the intruder knowledge, or just knowledge), written $M⊢t$ , as the least relation closed under the following rules:

where $\mathsf{A}\mathsf{n}\mathsf{a}(t)=(K,R)$ is a function that maps a term $t$ to a pair of sets of terms $K$ and $R$ . We also define a restricted variant ${⊢}_c$ of $⊢$ as the least relation closed under the $\mathit{(}\mathit{A}\mathit{x}\mathit{i}\mathit{o}\mathit{m}\mathit{)}$ and $\mathit{(}\mathit{C}\mathit{o}\mathit{m}\mathit{p}\mathit{o}\mathit{s}\mathit{e}\mathit{)}$ rules only.

The $\mathit{(}\mathit{A}\mathit{x}\mathit{i}\mathit{o}\mathit{m}\mathit{)}$ rule simply expresses that all messages directly known to the intruder are derivable, the $\mathit{(}\mathit{C}\mathit{o}\mathit{m}\mathit{p}\mathit{o}\mathit{s}\mathit{e}\mathit{)}$ rule closes the derivable terms under the application of public function symbols such as encryption or public constants (when $f\in {\mathrm{\Sigma }}_{\mathit{p}\mathit{u}\mathit{b}}^0={\mathcal{C}}_{\mathit{p}\mathit{u}\mathit{b}}$ ). The $\mathit{(}\mathit{D}\mathit{e}\mathit{c}\mathit{o}\mathit{m}\mathit{p}\mathit{o}\mathit{s}\mathit{e}\mathit{)}$ rule represents decomposition operations: $\mathsf{A}\mathsf{n}\mathsf{a}(t)=(K,R)$ means that $t$ is a term that can be analyzed, provided that the intruder knows all the “keys” in the set $K$ , and he will then obtain the “results” in $R$ . This gives us a general way to deal with typical constructor/destructor theories without needing to work with algebraic equations and rewriting. We may also write $\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)$ and $\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t)$ to denote the set of keys, respectively, results from analyzing $t$ , that is, $\mathsf{A}\mathsf{n}\mathsf{a}(t)=(\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t),\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t))$ .

Example 2

To model asymmetric encryption and signatures, we first fix two public $\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t},\mathsf{s}\mathsf{i}\mathsf{g}\mathsf{n}\in {\mathbb{F}}^2$ and one private $\mathsf{i}\mathsf{n}\mathsf{v}\in {\mathbb{F}}^1$ function symbols. The term $\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(k,m)$ then denotes the message $m$ encrypted with a public key $k$ , and $\mathsf{s}\mathsf{i}\mathsf{g}\mathsf{n}(\mathsf{i}\mathsf{n}\mathsf{v}(k),m)$ denotes $m$ signed with the private key $\mathsf{i}\mathsf{n}\mathsf{v}(k)$ of $k$ . To obtain a message $m$ encrypted with a public key $k$ , the intruder must produce $\mathsf{i}\mathsf{n}\mathsf{v}(k)$ . Formally, we define the analysis rule ${\mathsf{A}\mathsf{n}\mathsf{a}}_{\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}}(x_1,x_2)=(\{\mathsf{i}\mathsf{n}\mathsf{v}(x_1)\},\{x_2\})$ . For signatures, we define the rule ${\mathsf{A}\mathsf{n}\mathsf{a}}_{\mathsf{s}\mathsf{i}\mathsf{g}\mathsf{n}}(x_1,x_2)=(\mathrm{\varnothing },\{x_2\})$ modeling that the intruder can open any signature that he knows. We also model a transparent pairing function by fixing $\mathsf{p}\mathsf{a}\mathsf{i}\mathsf{r}\in {\mathrm{\Sigma }}^2$ and defining the rule ${\mathsf{A}\mathsf{n}\mathsf{a}}_{\mathsf{p}\mathsf{a}\mathsf{i}\mathsf{r}}(x_1,x_2)=(\mathrm{\varnothing },\{x_1,x_2\})$ .

Note that we have in this example used a simple notation for describing $\mathsf{A}\mathsf{n}\mathsf{a}(t)$ for an arbitrary term $t$ : each rule ${\mathsf{A}\mathsf{n}\mathsf{a}}_f(x_1,\dots ,x_n)=(K,R)$ defines $\mathsf{A}\mathsf{n}\mathsf{a}$ for a constructor $f\in {\mathbb{F}}^n$ . Here $x_i$ are distinct variable symbols, and $K$ and $R$ are sets of terms such that $R\subseteq \{x_1,\dots ,x_n\}$ and $K\subseteq \mathcal{T}(\mathbb{F},\{x_1,\dots ,x_n\})$ . Note that for each constructor $f$ , we have at most one analysis rule. For those constructors $f$ that have such a rule we define for each term $f(t_1,\dots ,t_n)$ the function $\mathsf{A}\mathsf{n}\mathsf{a}$ as $\mathsf{A}\mathsf{n}\mathsf{a}(f(t_1,\dots ,t_n))\equiv {\mathsf{A}\mathsf{n}\mathsf{a}}_f(t_1,\dots ,t_n)$ and for all constructors $g$ without an analysis rule we just have $\mathsf{A}\mathsf{n}\mathsf{a}(g(t_1,\dots ,t_n))\equiv (\mathrm{\varnothing },\mathrm{\varnothing })$ . (An example for the latter is a hash function: the intruder cannot obtain information from a hash value.)

The reason for this convention is that the formalization of Hess et al. ¹³ requires that the $\mathsf{A}\mathsf{n}\mathsf{a}$ function satisfies certain conditions, most notably that it is invariant under substitutions. [One may wonder why we do not allow for analysis rules of the form ${\mathsf{A}\mathsf{n}\mathsf{a}}_f(t_1,\dots ,t_n)=(K,R)$ , where the $t_i$ are arbitrary terms instead of just variables. Because of the substitution invariance requirement from Hess et al. ¹³ on $\mathsf{A}\mathsf{n}\mathsf{a}$ , such analysis rules would not lead to more expressive $\mathsf{A}\mathsf{n}\mathsf{a}$ functions.] Without going into detail, our notation of the $\mathsf{A}\mathsf{n}\mathsf{a}$ rules allows for an automated proof that all these requirements are satisfied. Thus, this allows the user to specify an arbitrary constructor/destructor theory with these $\mathsf{A}\mathsf{n}\mathsf{a}$ rules without having to prove anything manually.

2.3. Typed model

PSPSP works in a typed model. That means every variable has an intended type, and the intruder can send only well-typed messages. Many protocol verification methods^2–4,19,20 rely on such a typed model since it simplifies the protocol verification problem. There exist many typing results^14,21–25 that show that a restriction to a typed model is sound for large classes of protocols: for a protocol falling in such a class, it is without loss of attacks to restrict the intruder to well-typed messages. Hess and Mödersheim ¹⁴ is such a result that is part of the Isabelle formalization we employ. Since this result has itself been proved in Isabelle, to obtain the Isabelle proof that a protocol is secure in the unrestricted model, it is sufficient to have a proof that the protocol is secure in the typed model (e.g., automatically using PSPSP) and that the protocol satisfies type-flaw resistance, that is, the requirements of the typing result. We have automated the Isabelle proof of type-flaw resistance for the protocol specification language we present. Note that PSPSP only assumes a typed model, and the typing result here is just one way to discharge this assumption; there may be other ways to prove it, or one may leave it as an assumption. As PSPSP is not conceptually tied to the typing result, we give here only a brief summary of the result of Hess and Mödersheim. ¹⁴

The typed model is parameterized over a typing function $\mathrm{\Gamma }$ and a finite set of atomic types ${\mathfrak{T}}_a$ satisfying the following:

$\mathrm{\Gamma }(x)\in \mathcal{T}(\mathrm{\Sigma }\setminus \mathcal{C},{\mathfrak{T}}_a)$ for $x\in \mathcal{V}$ (where ${\mathfrak{T}}_a$ here acts like a set of “variables”).

$\mathrm{\Gamma }(c)\in {\mathfrak{T}}_a$ for $c\in \mathcal{C}$ .

$\mathrm{\Gamma }(f(t_1,\dots ,t_n))=f(\mathrm{\Gamma }(t_1),\dots ,\mathrm{\Gamma }(t_n))$ for $f\in \mathrm{\Sigma }\setminus \mathcal{C}$ .

A substitution $\theta$ is then said to be well-typed iff $\mathrm{\Gamma }(\theta (x))=\mathrm{\Gamma }(x)$ for all variables $x$ .

For instance, we may have a transaction with a step $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}(X)$ , where $\mathrm{\Gamma }(X)=h(\mathsf{N}\mathsf{o}\mathsf{n}\mathsf{c}\mathsf{e})$ . Note that in general the recipient would be unable to check if the received message is really of this form (e.g., the intruder could send them any value); the typing result shows that (if the protocol satisfies type-flaw resistance), if there is an attack, then there is a well-typed attack, and it is thus sound to replace the above step by $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}(h(N))$ for a new variable $N$ of type $\mathsf{N}\mathsf{o}\mathsf{n}\mathsf{c}\mathsf{e}$ (and replace all occurrences of $X$ with $h(N)$ in the rule). This does not mean that the recipient would learn $N$ , but only that the term can only be of the form $h(N)$ for some $N$ of type $\mathsf{N}\mathsf{o}\mathsf{n}\mathsf{c}\mathsf{e}$ .

For such a typing result, one considers a set of submessage patterns ( $\mathit{S}\mathit{M}\mathit{P}$ ) that contains the messages of the protocol description and is closed under well-typed instances, subterms, and key terms that can occur during analysis steps. For instance with the operators in Example 2, if $\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(k,m)\in \mathit{S}\mathit{M}\mathit{P}$ , then also $k,m,\mathsf{i}\mathsf{n}\mathsf{v}(k)\in \mathit{S}\mathit{M}\mathit{P}$ . The main requirement of type-flaw resistance is: if two terms $s,t\in \mathit{S}\mathit{M}\mathit{P}\setminus \mathcal{V}$ have a unifier, then $\mathrm{\Gamma }(s)=\mathrm{\Gamma }(t)$ .

For example, if $\mathit{S}\mathit{M}\mathit{P}$ contains messages $s=\mathsf{s}\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(X,\mathsf{p}\mathsf{a}\mathsf{i}\mathsf{r}(A,Y))$ and $t=\mathsf{s}\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(X^{\prime },Z)$ for $\mathrm{\Gamma }(X)=\mathrm{\Gamma }(X^{\prime })=\mathrm{\Gamma }(Y)=\mathrm{\Gamma }(Z)=\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ and $\mathrm{\Gamma }(A)=\mathsf{e}\mathsf{n}\mathsf{u}\mathsf{m}$ , then $s,t$ have a unifier, but $\mathrm{\Gamma }(s)\ne \mathrm{\Gamma }(t)$ , so this violates type-flaw resistance. There is a cheap way to make basically any protocol type-flaw resistant: instead of pairs, consider formats, that is, public functions that represent a particular way of structuring clear-text messages (e.g., XML), one format for each type of message. In the example, it can be a binary format $f_1$ and a unary format $f_2$ , and using them for the different types of encrypted messages: $s=\mathsf{s}\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(X,f_1(A,Y))$ and $t=\mathsf{s}\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(X^{\prime },f_2(Z))$ . Now $s$ and $t$ are no longer unifiable, since they use different formats, and it is just following prudent engineering principles that one should not encrypt raw data such as nonces, but add a few bits identifying what type of data it is.

As mentioned, we have now automated this check for type-flaw resistance; of course, $\mathit{S}\mathit{M}\mathit{P}$ is infinite, so we cannot directly compute it, but it is rather straightforward to compute the property symbolically. (One can avoid concrete constants and does not need to consider variants of terms that are equal modulo renaming of variables.)

The typing result for type-flaw resistant protocols is proved in Hess and Mödersheim ¹⁴ by considering a symbolic search technique called the lazy intruder. The key idea is that the only way that the lazy intruder instantiates variables is by a substitution $\sigma$ that is the most general unifier of two nonvariable terms. For a type-flaw resistant protocol, the considered terms are always within $\mathit{S}\mathit{M}\mathit{P}$ , and the unifier between two nonvariable terms of $\mathit{S}\mathit{M}\mathit{P}$ is thus necessarily well-typed (thus, applying the unifier to other terms in the search keeps them also in $\mathit{S}\mathit{M}\mathit{P}$ ). Because the technique is sound and complete, it will find an attack if there is one, and this attack is well-typed for a type-flaw-resistant protocol.

In fact, like Hess and Mödersheim, ¹⁴ we consider here stateful protocols where a message $m$ can be inserted, deleted, and checked for containment/noncontainment in a set $s$ . The requirement here is the following: if we have in the protocol a set operation with message $m$ and set $s$ and another set operation with message $m^{\prime }$ and set $s^{\prime }$ and if the pairs $(m,s)$ and $(m^{\prime },s^{\prime })$ have a unifier, then they must be of the same type. For instance, we cannot put messages of different types into the same set.

In this paper, we use as atomic types only ${\mathfrak{T}}_a=\{\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e},\mathsf{e}\mathsf{n}\mathsf{u}\mathsf{m},\mathsf{s}\mathsf{e}\mathsf{t}\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e},\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}\}$ , and the elements of $\mathbb{A}\cup \mathbb{V}$ have type $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ , the elements of $\mathbb{E}$ have type $\mathsf{e}\mathsf{n}\mathsf{u}\mathsf{m}$ , the elements of $\mathbb{S}$ have type $\mathsf{s}\mathsf{e}\mathsf{t}\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}$ and $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ has type $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}$ .

As a consequence of the typing result, when we have a variable $X$ of a composed type $\mathrm{\Gamma }(X)=f({\tau }_1,\dots ,{\tau }_n)$ , it is sound to replace it by the term $f(X_1,\dots ,X_n),$ where $X_i$ are fresh variables of type ${\tau }_i$ . Repeatedly applying this, it is thus not a restriction to have variables of only atomic types.

3. Transactions

The Isabelle protocol model of Hess et al. ¹³ consists of a number of transactions (also called rules) specifying the behavior of the participants. A transaction consists of any combination of the following: input messages to receive, checks on the sets, modifications of the sets, and output messages to send. A transaction can only be executed atomically, that is, it can only fire when input messages are present, such that the checks are satisfied, and then they produce all changes and the output messages in one state transition. Instead of defining a ground state transition system, ¹³ consider building symbolic traces as sequences of transactions with their variables renamed apart, and with any instantiation of the variables that satisfies the checks and the intruder model in the sense that the intruder can produce every input message from previous output messages. (Transactions can also describe additional abilities of the intruder, such as reading a set.) Security goals are formulated by transactions that check for a situation we consider as a successful attack, and then reveal the special constant $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ to the intruder. Thus, a protocol is safe if no symbolic constraint with the intruder finally sending $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ has a satisfying interpretation. Note that the length of symbolic traces is finite but unbounded (i.e., an unbounded session model), and that the number of enumeration constants and databases currently supported is arbitrary but fixed in the specification.

For the convenience of an automated verification tool, we have defined a small language called trac based on transactions with a bit of syntactic sugar, and this language is directly embedded into Isabelle. It is a simple text-based format directly accepted by our tool—see Section 8. To begin with, we introduce this language using a keyserver example adapted from Hess et al. ¹³ that we also use as a running example for the remainder of this paper.

3.1. A keyserver protocol

Before we proceed with the formal definitions, we illustrate our protocol model through the keyserver example. The protocol specifies $\mathbb{E}=\{\mathsf{a},\mathsf{b},\mathsf{i}\}$ and uses the specification of $\mathbb{S}$ from Example 1 and of $\mathbb{F}$ from Example 2. We consider users $\mathsf{a}$ and $\mathsf{b}$ as honest users and $\mathsf{i}$ as dishonest. In the specification, we will use sets $\mathsf{u}\mathsf{s}\mathsf{e}\mathsf{r}=\mathbb{E}$ , $\mathsf{h}\mathsf{o}\mathsf{n}\mathsf{e}\mathsf{s}\mathsf{t}=\{\mathsf{a},\mathsf{b}\}$ , and $\mathsf{d}\mathsf{i}\mathsf{s}\mathsf{h}\mathsf{o}\mathsf{n}\mathsf{e}\mathsf{s}\mathsf{t}=\{\mathsf{i}\}$ as types in the parameters of the transaction we specify. In the keyserver example, users can register public keys at a trusted keyserver, and these keys can later be revoked. Each user $U$ has an associated keyring $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(U)$ with which it keeps track of its keys. (The elements of $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(U)$ are actually public keys; we implicitly assume that the user $U$ knows the corresponding private key.)

First, we model a mechanism $\mathsf{o}\mathsf{u}\mathsf{t}\mathsf{O}\mathsf{f}\mathsf{B}\mathsf{a}\mathsf{n}\mathsf{d}$ by which a user $U$ can register a new key $\mathit{P}\mathit{K}$ at the keyserver out-of-band, for example, by physically visiting the keyserver. The user $U$ first constructs a fresh public key $\mathit{P}\mathit{K}$ and inserts $\mathit{P}\mathit{K}$ into its keyring $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(U)$ . We model that the keyserver—in the same transaction—learns the key and adds it to its database of valid keys for user $U$ , that is, into a set $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(U)$ . Finally, $\mathit{P}\mathit{K}$ is published: Note that there is no built-in notion of set ownership, or who exactly is performing an action: we just specify with such transactions what can happen. The intuition is that $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(U)$ is a set of public keys controlled by $U$ (and $U$ has the corresponding private key of each) while $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(U)$ is controlled by the server (who is not even given a name here). Putting it into a single transaction model that this is something happening in collaboration between a user and a server.

Next, we model a key update mechanism that allows for registering a new key while simultaneously revoking an old one. We model this as two transactions, one for the user and one for the server, since here we model a scenario where the user and server communicate via an asynchronous network controlled by the intruder. To initiate the key revocation process, the user $U$ first picks and removes a key $\mathit{P}\mathit{K}$ from its keyring to later revoke, then freshly generates a new key $\mathit{N}\mathit{P}\mathit{K}$ and stores it in its keyring. (Again, the corresponding private key $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{N}\mathit{P}\mathit{K})$ is known to $U$ , but this is not explicitly described.) As a final step, the user signs the new key with the private key $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{P}\mathit{K})$ of the old key and sends this signature to the server by transmitting it over the network: The check $\mathit{P}\mathit{K}\mathsf{i}\mathsf{n}\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(U)$ represents here a nondeterministic choice of an element of $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(U)$ . (Observe that a user can register any number of keys with the $\mathsf{o}\mathsf{u}\mathsf{t}\mathsf{O}\mathsf{f}\mathsf{B}\mathsf{a}\mathsf{n}\mathsf{d}$ transaction.) We declare $\mathit{P}\mathit{K}$ as a variable of type $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ , because $\mathit{P}\mathit{K}$ is not freshly generated here; all freshly generated elements, such as $\mathit{N}\mathit{P}\mathit{K}$ here, are automatically of type $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ .

When the server receives the signed message, it checks that $\mathit{P}\mathit{K}$ is indeed a valid key, that $\mathit{N}\mathit{P}\mathit{K}$ has not been registered earlier, and then revokes $\mathit{P}\mathit{K}$ and registers $\mathit{N}\mathit{P}\mathit{K}$ . To keep track of revoked keys, the server maintains another database $\mathsf{r}\mathsf{e}\mathsf{v}\mathsf{o}\mathsf{k}\mathsf{e}\mathsf{d}(U)$ containing the revoked keys of $U$ : As a last action, the old private key $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{P}\mathit{K})$ is revealed. This is, of course, not what one would do in a reasonable implementation, but it allows us to prove that the protocol is correct even if the intruder obtains all private keys to revoked public keys. (This could also be separated into a rule that just leaks private keys of revoked keys.)

Actions of the form $x\mathsf{n}\mathsf{o}\mathsf{t}\mathsf{i}\mathsf{n}s(\mathrm{\_})$ for $s\in {\mathrm{\Sigma }}^n$ are syntactic sugar for the sequence of actions $x\mathsf{n}\mathsf{o}\mathsf{t}\mathsf{i}\mathsf{n}s(a)$ for each $a\in \mathbb{E}$ .

Finally, we define that there is an attack if the intruder learns a valid key of an honest user. This, again, can be modeled as a sequence of actions in which we check if the conditions for an attack hold, and, if so, transmit the constant $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ that acts as a signal for goal violations. Recall that $\mathsf{h}\mathsf{o}\mathsf{n}\mathsf{e}\mathsf{s}\mathsf{t}$ is a subset of $\mathsf{u}\mathsf{s}\mathsf{e}\mathsf{r}$ that contains only the honest agents. Then we define: The last action $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ is just syntactic sugar for $\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ .

3.2. Protocol model

The keyserver protocol that we just defined consists of transactions (also called rules) that we now formally define. To keep the formal definitions simple, we omit the variable declarations and the syntactic sugar employed in our protocol specification language. Thus, only $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ -typed variables remain in transactions since the enumeration variables are resolved as syntactic sugar.

A transaction $T$ is then of the form $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}},$ where the $S_i$ are strands built from the following grammar:

$$\begin{array}{rl}{S}_{\mathit{r}}& ::=\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}{t}_1,\dots ,t_n\cdot S_{\mathit{r}}\mid 0,\\ S_{\mathit{c}}& ::=x\mathsf{i}\mathsf{n}s\cdot S_{\mathit{c}}\mid x\mathsf{n}\mathsf{o}\mathsf{t}\mathsf{i}\mathsf{n}s\cdot S_{\mathit{c}}\mid x\doteq ̸x^{\prime }\cdot S_{\mathit{c}}\mid 0,\\ \mathit{F}& ::=\mathsf{n}\mathsf{e}\mathsf{w}x\cdot \mathit{F}\mid 0,\\ S_{\mathit{u}}& ::=\mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}xs\cdot S_{\mathit{u}}\mid \mathsf{d}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{t}\mathsf{e}xs\cdot S_{\mathit{u}}\mid 0,\\ S_{\mathit{s}}& ::=\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}{u}_1,\dots ,u_n\cdot S_{\mathit{s}}\mid 0,\end{array}$$

where $x,x^{\prime }\in {\mathcal{V}}_{\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}}$ , $s\in \mathbb{S}$ , $t_i\in \mathcal{T}(\mathbb{E}\cup \mathbb{F},{\mathcal{V}}_{\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}})$ , $u_i\in \mathcal{T}(\mathbb{E}\cup \mathbb{F},{\mathcal{V}}_{\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}})\cup \{\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}\}$ , and where $0$ denotes the empty strand. We remark that only values can be inserted in the sets, which is why we require $x,x^{\prime }\in {\mathcal{V}}_{\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}}$ . This is needed for the abstract interpretation approach we present in Section 4.

The function $\mathit{f}\mathit{v}$ is extended to transactions by letting it collect all variables occurring in the strands of the transaction, and for a transaction $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}$ we define $\mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)\equiv \mathit{f}\mathit{v}(\mathit{F})$ (i.e., $x\in \mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ iff $\mathsf{n}\mathsf{e}\mathsf{w}x$ occurs in $T$ ).

Protocols are defined as finite sets of such transactions $\mathcal{P}=\{T_1,\dots ,T_n\}$ . Their semantics is defined in terms of a ground transition system in which each configuration is of the form $(M,D,C)$ , where $M$ is the intruder knowledge (the messages sent so far), $D$ is a set of pairs representing the current state of the databases (e.g., $(k,s)\in D$ iff $k$ is an element of the database $s$ ) and $C$ keeps track of the constants that have been used already and thus cannot be considered fresh. For a configuration and a transaction, we can check if the transaction is executable from that configuration, and if so, then there is a transition to the new configuration that results from executing the transaction. When executing a transaction, variables $x$ occurring in $\mathsf{n}\mathsf{e}\mathsf{w}x$ actions will be instantiated with fresh values. To ensure that these values are indeed fresh, they must not be in $C$ already. This instantiation takes care of the $\mathsf{n}\mathsf{e}\mathsf{w}x$ actions, which are then no longer needed. The instantiation also requires a slightly more flexible syntax compared to the transaction syntax, to allow for actions such as $\mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}ts$ , where $t\notin \mathcal{V}$ . We introduce a syntax that accounts for this, called constraints or traces:

$$\begin{array}{rl}\mathcal{A}::=& \mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}{t}_1,\dots ,t_n\cdot \mathcal{A}\mid \mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}{t}_1,\dots ,t_n\cdot \mathcal{A}\mid t\doteq ̸t^{\prime }\cdot \mathcal{A}\mid \mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}t{t}^{\prime }\cdot \mathcal{A}\mid \mathsf{d}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{t}\mathsf{e}t{t}^{\prime }\cdot \mathcal{A}\mid \\ & t\mathsf{i}\mathsf{n}{t}^{\prime }\cdot \mathcal{A}\mid t\mathsf{n}\mathsf{o}\mathsf{t}\mathsf{i}\mathsf{n}{t}^{\prime }\cdot \mathcal{A}\mid 0,\end{array}$$

where $t,t^{\prime }\in \mathcal{T}(\mathrm{\Sigma },\mathcal{V})$ and $0$ is the empty constraint. Note also that in contrast to transactions, constraints are seen from the intruder’s point of view, in the sense that the directions of transmitted messages are swapped (so $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ s become $\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}$ s and vice-versa).

For the semantics of constraints, we define a relation $\mathcal{I}{\models }_D^M\mathcal{A},$ where $\mathcal{A}$ is a constraint, $M$ is the intruder knowledge, $D$ is a set of pairs representing the current state of the databases, and $\mathcal{I}$ is an interpretation:

$$\begin{array}{lcl}\mathcal{I}{\models }_D^{M}0& \text{iff}& \mathit{t}\mathit{r}\mathit{u}\mathit{e},\\ \mathcal{I}{\models }_D^M\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}{t}_1,\dots ,t_n\cdot \mathcal{A}& \text{iff}& M⊢\mathcal{I}(t_i),\text{for all }i\in \{1,\dots ,n\},\text{and }\mathcal{I}{\models }_D^M\mathcal{A},\\ \mathcal{I}{\models }_D^M\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}{t}_1,\dots ,t_n\cdot \mathcal{A}& \text{iff}& \mathcal{I}{\models }_D^{M\cup \{\mathcal{I}(t_1),\dots ,\mathcal{I}(t_n)\}}\mathcal{A},\\ \mathcal{I}{\models }_D^M\mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}ts\cdot \mathcal{A}& \text{iff}& \mathcal{I}{\models }_{D\cup \{\mathcal{I}((t,s))\}}^M\mathcal{A},\\ \mathcal{I}{\models }_D^M\mathsf{d}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{t}\mathsf{e}ts\cdot \mathcal{A}& \text{iff}& \mathcal{I}{\models }_{D\setminus \{\mathcal{I}((t,s))\}}^M\mathcal{A},\\ \mathcal{I}{\models }_D^{M}t\doteq ̸t^{\prime }\cdot \mathcal{A}& \text{iff}& \mathcal{I}(t)\ne \mathcal{I}(t^{\prime })\text{ and }\mathcal{I}{\models }_D^M\mathcal{A},\\ \mathcal{I}{\models }_D^{M}t\mathsf{i}\mathsf{n}s\cdot \mathcal{A}& \text{iff}& \mathcal{I}((t,s))\in D\text{ and }\mathcal{I}{\models }_D^M\mathcal{A},\\ \mathcal{I}{\models }_D^{M}t\mathsf{n}\mathsf{o}\mathsf{t}\mathsf{i}\mathsf{n}s\cdot \mathcal{A}& \text{iff}& \mathcal{I}((t,s))\notin D\text{ and }\mathcal{I}{\models }_D^M\mathcal{A}.\end{array}$$

We say that $\mathcal{I}$ is a model of $\mathcal{A}$ , written $\mathcal{I}\models \mathcal{A}$ , iff $\mathcal{I}{\models }_{\mathrm{\varnothing }}^{\mathrm{\varnothing }}\mathcal{A}$ . We may also apply substitutions $\theta$ to constraints $\mathcal{A}$ , written $\theta (\mathcal{A})$ , by extending the definition of substitution application appropriately. The function $\mathit{f}\mathit{v}$ is also extended to constraints.

We define what an intruder learns when a constraint $\mathcal{A}$ is executed: $ik(\mathcal{A})=\{t_i|1\le i\le n,$ $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}{t}_1,\dots ,t_n\in \mathcal{A}\}$ . We also define the database $db(\mathcal{A},\mathcal{I},D)$ , which is the update of the database $D$ after the execution of the constraint $\mathcal{A}$ from database $D$ under interpretation $\mathcal{I}$ :

$$\begin{array}{rcl}\mathit{d}\mathit{b}(0,\mathcal{I},D)& =& D,\\ \mathit{d}\mathit{b}(\mathfrak{t}\cdot S,\mathcal{I},D)& =& \{\begin{array}{ll}\mathit{d}\mathit{b}(S,\mathcal{I},D\cup \{(\mathcal{I}(t),\mathcal{I}(s))\})& \text{if }\mathfrak{t}=\mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}ts,\\ \mathit{d}\mathit{b}(S,\mathcal{I},D\setminus \{(\mathcal{I}(t),\mathcal{I}(s))\})& \text{if }\mathfrak{t}=\mathsf{d}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{t}\mathsf{e}ts,\\ \mathit{d}\mathit{b}(S,\mathcal{I},D)& \text{otherwise},\end{array}\end{array}$$

With this in place, we define a transition relation ${\Rightarrow }_{\mathcal{P}}$ for protocols $\mathcal{P}$ in which states are configurations and the initial state is the empty configuration $(\mathrm{\varnothing },\mathrm{\varnothing },\mathrm{\varnothing })$ . First, we define the dual of a constraint $\mathcal{A}$ , written $\mathit{d}\mathit{u}\mathit{a}\mathit{l}(\mathcal{A})$ , as “swapping” the direction of the sent and received messages of $\mathcal{A}$ : $\mathit{d}\mathit{u}\mathit{a}\mathit{l}(0)=0$ , $\mathit{d}\mathit{u}\mathit{a}\mathit{l}(\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}t\cdot \mathcal{A})=\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}t\cdot \mathit{d}\mathit{u}\mathit{a}\mathit{l}(\mathcal{A})$ , $\mathit{d}\mathit{u}\mathit{a}\mathit{l}(\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}t\cdot \mathcal{A})=\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}t\cdot \mathit{d}\mathit{u}\mathit{a}\mathit{l}(\mathcal{A})$ , and $\mathit{d}\mathit{u}\mathit{a}\mathit{l}(\mathfrak{a}\cdot \mathcal{A})=\mathfrak{a}\cdot \mathit{d}\mathit{u}\mathit{a}\mathit{l}(\mathcal{A})$ otherwise. The transition

$$(M,D,C){\Rightarrow }_{\mathcal{P}}(M\cup \mathcal{I}(ik(\mathcal{A})),\mathit{d}\mathit{b}(\mathcal{A},\mathcal{I},D),C\cup (\mathit{s}\mathit{u}\mathit{b}\mathit{t}\mathit{e}\mathit{r}\mathit{m}\mathit{s}(\mathcal{A})\cap \mathbb{V}))$$

is then applicable for a transaction $T\in \mathcal{P}$ if the following conditions are met:

1. (1)

   $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}$ for some $\mathit{F}$ ,

   (2)

   $\sigma$ is an injective substitution mapping $\mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ to fresh values (i.e., $\mathit{d}\mathit{o}\mathit{m}(\sigma )=\mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ , $\mathit{r}\mathit{a}\mathit{n}(\sigma )\subseteq \mathbb{V}$ , and $\mathit{r}\mathit{a}\mathit{n}(\sigma )\cap C=\mathrm{\varnothing }$ ),

   (3)

   $\mathcal{A}=\mathit{d}\mathit{u}\mathit{a}\mathit{l}(\sigma (S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}))$ , and

   (4)

   $\mathcal{I}{\models }_D^M\mathcal{A}$ .

   A configuration $(M,D,C)$ is said to be ground reachable in $\mathcal{P}$ iff $(\mathrm{\varnothing },\mathrm{\varnothing },\mathrm{\varnothing }){\Rightarrow }_{\mathcal{P}}^{\star }(M,D,C)$ where ${\Rightarrow }_{\mathcal{P}}^{\star }$ denotes the transitive reflexive closure of ${\Rightarrow }_{\mathcal{P}}$ . For any configuration $(M,D,C)$ ground reachable in this transition system, $M$ and $D$ are ground because in each step the substitutions $\sigma$ and $\mathcal{I}$ replace variables with ground terms in the elements added to these sets.

   We now define a different semantics for protocols, namely one defined in terms of a symbolic transition system in which a single constraint is built up during transitions, essentially representing a trace of what has happened. We use this system as a basis for our formalization of both typing and compositionality because, for these two aspects, it is convenient to reason about the mentioned single constraint. For typing, it is convenient to reason about the many solutions it may have, and for compositionality, it is convenient to split the constraint into parts that then constitute constraints of the individual protocols. We call the system symbolic because we allow the built constraint to contain variables—this is in contrast to the ground transition system, which picks and applies a new interpretation $\mathcal{I}$ in each transition. The symbolic transition system is defined using a transition relation ${\Rightarrow }_{\mathcal{P}}^{\bullet }$ for protocols $\mathcal{P}$ in which states are constraints and the initial state is the empty constraint $0$ . The transition

   $$\mathcal{A}{\Rightarrow }_{\mathcal{P}}^{\bullet }\mathcal{A}\cdot \mathit{d}\mathit{u}\mathit{a}\mathit{l}(\rho (\sigma (S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}})))$$

   is applicable for a transaction $T\in \mathcal{P}$ if the following conditions are met:

   1. (1)

      $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}$ for some $\mathit{F}$ ,

   2. (2)

      $\sigma$ is an injective substitution mapping $\mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ to fresh values (i.e., $\mathit{d}\mathit{o}\mathit{m}(\sigma )=\mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ , $\mathit{r}\mathit{a}\mathit{n}(\sigma )\subseteq \mathbb{V}$ , and the elements of $\mathit{r}\mathit{a}\mathit{n}(\sigma )$ do not occur in $\mathcal{A}$ ), and

   3. (3)

      $\rho$ is a variable renaming sending the variables of $T$ not in $\mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ to new variables that do not occur in $\mathcal{A}$ or $\mathcal{P}$ (that is, $\mathit{d}\mathit{o}\mathit{m}(\rho )=\mathit{f}\mathit{v}(T)\setminus \mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ and $(\mathit{f}\mathit{v}(\mathcal{A})\cup \mathit{f}\mathit{v}(\mathcal{P}))\cap \mathit{r}\mathit{a}\mathit{n}(\rho )=\mathrm{\varnothing }$ ).

   A constraint $\mathcal{A}$ is said to be symbolically reachable in $\mathcal{P}$ iff $0{\Rightarrow }_{\mathcal{P}}^{\bullet \star }\mathcal{A}$ where ${\Rightarrow }_{\mathcal{P}}^{\bullet \star }$ denotes the transitive reflexive closure of ${\Rightarrow }_{\mathcal{P}}^{\bullet }$ . The protocol then has an attack iff there exists a symbolically reachable and satisfiable constraint where the intruder can produce the attack signal, that is, there exists a symbolically reachable $\mathcal{A}$ in $\mathcal{P}$ and an interpretation $\mathcal{I}$ such that $\mathcal{I}\models \mathcal{A}\cdot \mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ . If $\mathcal{P}$ does not have an attack, then $\mathcal{P}$ is secure.

   We show that the notions of reachability in the two systems correspond to each other:

   Theorem 1

   $$\begin{array}{rl}& \{(M,D)\mid \text{(M, D, C) is ground reachable in }\mathcal{P}\}\\ & =\{(ik(\mathcal{I}(\mathcal{A})),\mathit{d}\mathit{b}(\mathcal{A},\mathcal{I},\mathrm{\varnothing }))\mid \mathcal{A}\text{ is symbolically reachable in }\mathcal{P}\text{ and }\mathcal{I}\models \mathcal{A}\}\end{array}$$

   [This theorem is called protocol_model_equivalence in the Isabelle formalization and can be found in the Stateful_Protocol_Model.thy theory file.]

   For the remainder of the paper, we will focus our attention on the symbolic transition system as justified by the above theorem, and thus by reachable we will mean symbolically reachable.

   3.3. Well-formedness

   We are going to employ the abstraction-based verification technique from Mödersheim and Bruni ¹⁵ in the following to automatically generate security proofs. The technique has a few more requirements in order to work and which we bundle in a notion of well-formedness.

   First, if a transaction uses a variable for sending a message or performing a set update, then that variable must either be fresh or have occurred positively in a received message or check. Intuitively, transactions cannot produce a value “out of the blue,” but the value either has to exist before the transaction (in some message or set) or be created by the transaction. Formally, let $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}$ . Then, we require:

4. Set-based abstraction

We now come to the core of our approach: for a given protocol, how to automatically verify and generate a security proof that Isabelle can accept. As explained earlier, this is based on an abstract interpretation method called set-based abstraction.^9,15,16 Essentially, the method computes a fixed point which overapproximates the intruder’s accumulated knowledge in any sequence of transactions. While it is relatively easy to formalize the computation of this fixed point in Isabelle, the main work consists of convincing Isabelle that every transaction is covered by the fixed point in the following sense. Given any trace that is represented by the fixed point and in which a transaction is executable, then the resulting trace is covered by the fixed point. Thereby, all traces are covered by the fixed point, and when the attack predicate is not contained in the fixed point, it is not reachable in any trace of the protocol. The core of PSPSP is this coverage check that automatically performs a security proof in Isabelle. The fixed point can thus be regarded as a proof idea that no trace can contain an attack. If there was any mistake in the fixed point computation (or if the abstraction approach were actually unsound), then in the worst case, Isabelle would fail to be convinced by the coverage check.

Recall that in the previous section we formalized a protocol model by reachable constraints $\mathcal{A}$ (i.e., a sequence of transactions where variables have been named apart and the send/receive direction has been swapped in order to express it from the intruder’s point of view) with their satisfying interpretations $\mathcal{I}\models \mathcal{A}$ . Note that $\models$ is defined via a relation ${\models }_D^M$ , where here $M$ denotes the intruder knowledge (all the messages received so far) and $D$ denotes the state of the sets $\mathbb{S}$ (all values inserted into a set that were not deleted so far). Note also that the values that can no longer be considered fresh are the set $C=\mathit{s}\mathit{u}\mathit{b}\mathit{t}\mathit{e}\mathit{r}\mathit{m}\mathit{s}(\mathcal{A})\cap \mathbb{V}$ . We can thus characterize the state of the entire system after a number of instantiated transactions by these three items $M$ , $D$ , and $C$ .

Example 3

In our keyserver example, the following trace is possible (after taking a transition of $\mathsf{o}\mathsf{u}\mathsf{t}\mathsf{O}\mathsf{f}\mathsf{B}\mathsf{a}\mathsf{n}\mathsf{d}$ with variables instantiated by $[\mathit{P}\mathit{K}\mapsto {\mathsf{p}\mathsf{k}}_1,U\mapsto \mathsf{a}]$ followed by a transition of $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{U}\mathsf{s}\mathsf{e}\mathsf{r}$ with variables instantiated by $[\mathit{P}\mathit{K}\mapsto {\mathsf{p}\mathsf{k}}_1,U\mapsto \mathsf{a},\mathit{N}\mathit{P}\mathit{K}\mapsto {\mathsf{p}\mathsf{k}}_2]$ ):

$$\begin{array}{l}\mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}{\mathsf{p}\mathsf{k}}_1\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})\\ \mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}{\mathsf{p}\mathsf{k}}_1\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a})\\ \mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}{\mathsf{p}\mathsf{k}}_1\\ {\mathsf{p}\mathsf{k}}_1\mathsf{i}\mathsf{n}\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})\\ \mathsf{d}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{t}\mathsf{e}{\mathsf{p}\mathsf{k}}_1\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})\\ \mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}{\mathsf{p}\mathsf{k}}_2\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})\\ \mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}\mathsf{s}\mathsf{i}\mathsf{g}\mathsf{n}(\mathsf{i}\mathsf{n}\mathsf{v}({\mathsf{p}\mathsf{k}}_1),\mathsf{p}\mathsf{a}\mathsf{i}\mathsf{r}(\mathsf{a},{\mathsf{p}\mathsf{k}}_2))\end{array}$$

Suppose we start in state $M_0=\mathrm{\varnothing }$ , $D_0=\mathrm{\varnothing }$ , and $C_0=\mathrm{\varnothing }$ . After this trace, we have

$$\begin{array}{rl}M=& \{{\mathsf{p}\mathsf{k}}_1,\mathsf{s}\mathsf{i}\mathsf{g}\mathsf{n}(\mathsf{i}\mathsf{n}\mathsf{v}({\mathsf{p}\mathsf{k}}_1),\mathsf{p}\mathsf{a}\mathsf{i}\mathsf{r}(\mathsf{a},{\mathsf{p}\mathsf{k}}_2))\},\\ D=& \{({\mathsf{p}\mathsf{k}}_1,\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a})),({\mathsf{p}\mathsf{k}}_2,\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a}))\},\text{ and }\\ C=& \{{\mathsf{p}\mathsf{k}}_1,{\mathsf{p}\mathsf{k}}_2\}\end{array}$$

In general, $D$ consists of pairs $(v,s)$ where $v\in \mathbb{V}$ is a value and $s\in \mathbb{S}$ is a set. The idea of our abstract interpretation is that we stop distinguishing values that are members of the same sets. Let thus $\mathbb{A}$ be the powerset of $\mathbb{S}$ and define an abstraction function ${\alpha }_D$ from $\mathbb{V}$ to $\mathbb{A}$ that depends on the current state $D$ : and we extend it to terms and sets of terms as expected. We thus write for the abstract value that corresponds to the subset $A$ of $\mathbb{S}$ , for example, if $s_1,s_2\in \mathbb{S}$ then . Remember that $\mathbb{A}$ is included in ${\mathrm{\Sigma }}^0$ , so we can build abstract terms that include elements of $\mathbb{A}$ as abstract constants. [In fact, in the Isabelle type system, $\mathrm{\Sigma }$ cannot contain both $\mathbb{S}$ and subsets of $\mathbb{S}$ ; we thus technically define the elements of $\mathbb{A}$ as a constructor applied to any subset of $\mathbb{S}$ . This is reflected here by the shading to ease presentation.]

Example 4

In the previous example, we have and . Thus .

The key idea is to compute the fixed point of all the abstract messages that the intruder can obtain in any model of any reachable constraint. Note that this fixed point is, in general, infinite, even if $\mathbb{S}$ is finite (and thus so is $\mathbb{A}$ ), because the intruder can compose arbitrarily complex messages and send them. This is why tools such as those in the literature^9,15,16 do not directly compute the fixed point but represent it by a set of Horn clauses and check using resolution whether $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ is derivable.

However, remember that we can restrict ourselves to the typed model and use the typing result of Hess and Mödersheim ¹⁴ to infer the security proof without the typing restriction. All variables that occur in a constraint are of type $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ (the parameter variables of the transactions are desugared) and thus, in a typed model, it holds that $\mathcal{I}(x)\in \mathbb{V}$ for every variable $x$ and well-typed interpretation $\mathcal{I}$ . While $\mathbb{V}$ is still countably infinite, the abstraction (in any state $D$ ) maps to the finite $\mathbb{A}$ . Thus, the fixed point is always finite in a typed model.

There is a subtle point here: even though we limit the variables to well-typed terms, and thus also limit all messages that can ever be sent or received, the Dolev-Yao closure is still infinite, that is, for a (finite) set $M$ of messages there are still infinitely many $t$ such that $M⊢t$ . Only finitely many of these $t$ can be sent by the intruder in the typed model, but one may wonder if the entire derivation relation $⊢$ can be limited to “well-typed” terms without losing attacks. Indeed, we define well-typed terms as the set of terms that includes all well-typed instances of sent and received messages in transactions, and that is closed under subterms and $\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}$ . We have proved in Isabelle that for the intruder to derive any well-typed term, it is sound to also limit the intruder deduction to well-typed terms, so no ill-typed intermediate terms are needed during the derivation. (This is indeed very similar to some lemmas we have proved for parallel compositionality, namely for so-called homogeneous terms, the deduction does not need to consider any inhomogeneous terms. ¹³ ) Thus, it is sound to limit the fixed point and the intruder deduction to well-typed terms, which makes the fixed point finite.

4.1. Defining fixed points

Let us now see in more detail how to formally define the fixed point. An important aspect of the abstraction approach is that the global state is mutable, that is, the set membership of concrete values can change in transitions, and so their abstraction changes.

Example 5

The value ${\mathsf{p}\mathsf{k}}_1$ in Example 3 is created in the first transaction and has, after the first transaction, the abstraction . Since the second transaction deletes ${\mathsf{p}\mathsf{k}}_1$ from $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})$ , it changes its abstract class to .

As such, transitions of the abstraction of values play a crucial role in the approach; we define the following notion:

Definition 3 (Term implication)

A term implication $(a,b)$ is a pair of abstract values $a,b\in \mathbb{A}$ and a term implication graph $\mathit{T}\mathit{I}$ is a binary relation between abstract values, that is, $\mathit{T}\mathit{I}\subseteq \mathbb{A}\times \mathbb{A}$ . Instead of $(a,b)\in \mathit{T}\mathit{I}$ , we may also write $a\to \to b$ .

The reason we use the word “implication” is as follows. Suppose an abstract set of messages contains several occurrences of the same abstract value $a\in \mathbb{A}$ , say $M=\{f(a),g(a,a)\}$ . Due to the abstraction, we have lost the information of how many distinct constants are represented here, for example, two corresponding concrete set of messages could be $M_0=\{f(c_1),f(c_2),g(c_1,c_2),g(c_1,c_1)\}$ and $M_1=\{f(c_2),g(c_2,c_2),g(c_2,c_1)\},$ where both $c_1$ and $c_2$ have the same set memberships $a$ . If now value $c_1$ changes its set memberships to, say, $b\in \mathbb{A}$ , then the abstraction of $M_0$ becomes $\{f(b),f(a),g(b,b),g(b,a)\}$ and the abstraction of $M_1$ becomes $\{f(a),g(a,a),g(a,b)\}$ . Thus, in general, to include all possible terms that can be reached by a term implication $a\to \to b$ , each occurrence of $a$ can independently change to $b$ . This means that all of the original terms with now $a$ changed to $b$ are also reached, and hence we call it an implication. This is captured by the following definitions:

Definition 4 (Term transformation)

Let $(a,b)$ be a term implication. The term transformation under $(a,b)$ is the least relation ${}_a\to \to {}_b$ closed under the following rules:

$$\begin{array}{r}\begin{array}{c}{\displaystyle {\overline{x{}_a\to \to {}_{b}x}}^{x\in \mathcal{V}}\overline{a{}_a\to \to {}_{b}b}{\displaystyle \frac{t_1{}_a\to \to {}_b{s}_1\cdots t_n{}_a\to \to {}_b{s}_n}{f(t_1,\dots ,t_n){}_a\to \to {}_{b}f(s_1,\dots ,s_n)}f\in {\mathrm{\Sigma }}^n.}}\end{array}\end{array}$$

Note that this relation is also reflexive since $c{}_a\to \to {}_{b}c$ for $c\in \mathbb{A}\subseteq {\mathrm{\Sigma }}^0$ holds because of the third rule. If $t{}_a\to \to {}_b{t}^{\prime }$ then we say that $t^{\prime }$ is implied by $t$ under $(a,b)$ , or just $t^{\prime }$ is implied by $t$ for short.

Definition 5 (Term implication closure)

Let $\mathit{T}\mathit{I}$ be a term implication graph and let $t$ be a term. The term implication closure of $t$ under $\mathit{T}\mathit{I}$ is defined as the least set ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ closed under the following rules:

$$\begin{array}{r}\begin{array}{c}{\displaystyle \overline{t\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)}\frac{t^{\prime }\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)}{t^{″}\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)}\begin{array}{c}(a\to \to b)\in \mathit{T}\mathit{I},\\ t^{\prime }{}_a\to \to {}_b{t}^{″}\end{array}.}\end{array}\end{array}$$

This definition is extended to sets of terms $M$ as expected. If $t^{\prime }\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ then we say that $t^{\prime }$ is implied by $t$ (under $\mathit{T}\mathit{I}$ ).

Closing the fixed point under the term implication graph is actually quite large in many practical examples, and thus we just record the messages that are ever received by the intruder together with the term implication graph, but without performing this closure explicitly:

Definition 6 (Fixed point)

A protocol fixed point candidate, or fixed point for short, is a pair $(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ such that [here “candidate” is to emphasize that this is just a proof idea that has yet to be verified by Isabelle]

(1)

$\mathit{F}\mathit{P}$ is a finite and ground set of terms over $\mathcal{T}(\mathrm{\Sigma }\setminus \mathbb{V},\mathrm{\varnothing })$ .

(2)

$\mathit{T}\mathit{I}$ is a term implication graph: $\mathit{T}\mathit{I}\subseteq \mathbb{A}\times \mathbb{A}$ .

4.2. Limitations

There are some limitations of our approach that we now mention. First, PSPSP is limited to reachability properties. This is because privacy-type properties are quite hard to handle in infinite-state verification. To our knowledge, regarding automated tools for infinite sessions, only Tamarin ¹² and ProVerif ⁶ handle this by restriction to diff-equivalence. ²⁶

We inherit the free algebra term model from Hess et al. ¹³ (two terms are equal iff they are syntactically equal), and so we do not support algebraic properties such as needed for Diffie-Hellman. We inherit the limitations of AIF’s set-based abstraction approach:

We require each protocol to have a fixed and finite number of enumeration constants and sets. This typically means that also the number of agents is fixed—at least if the protocol has to specify a number of sets for each agent.

We require that the sets can only contain values. The reason is to allow these values to be abstracted by set membership. That would not work if we allowed composed terms in the sets.

We cannot refer directly to particular constants of type $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ . This would not be very useful, as every value with the same set-membership status is identified with the same abstract value under the set-based abstraction.

We cannot check the equality of values, again, because two values may have the same abstraction.

As the following protocol shows, the abstraction may lose “connections” between values, and this can lead to spurious attacks. The example illustrates this using the transactions $\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}\mathsf{\_}\mathsf{h}$ and $\mathsf{d}\mathsf{e}\mathsf{l}\mathsf{\_}\mathsf{s}\mathsf{e}\mathsf{t}$ which result in the intermediate fixed point and the term implication . Thus under term implication we get the terms , , , and . The latter term triggers $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}\mathsf{\_}\mathsf{d}\mathsf{e}\mathsf{f}$ , which emits an attack. However, on the concrete level. This attack is not possible because there any concrete chosen values for $\mathit{N}\mathit{1}$ and $\mathit{N}\mathit{2}$ in $\mathsf{h}(\mathit{N}\mathit{1},\mathit{N}\mathit{2})$ , are either both in $\mathsf{s}\mathsf{e}\mathsf{t}$ or both not in $\mathsf{s}\mathsf{e}\mathsf{t}$ . We remark that many protocols do not rely on such “connections” between values, as demonstrated by our benchmark suite.

Our approach allows for an unbounded number of sessions. The only difference here between our work and, for example, Tamarin ¹² and ProVerif⁶ is that we need, as mentioned, to fix the number of enumeration constants and sets, and thereby, in a typical specification, also fix the number of agents. However, there is no difference in the notion of unbounded sessions: We allow for an unbounded number of transitions, every set can contain an unbounded number of values, and the intruder can make an unbounded number of steps. There is potential for overcoming this limitation: Comon-Lundh and Cortier^27,28 show that a restriction to finitely many agents can often be without a loss of attacks. Mödersheim and Bruni ¹⁵ indirectly show that similar results are possible for set-based abstraction, since one can compute a symbolic fixed point leaving agents uninstantiated variables. This, however, requires several restrictions on the use of negation, suggesting close limits of such an approach for set-based abstraction. As this would have also required a substantially more complicated concept for the fixed point computation and checking, we opted for not using this approach in Isabelle/PSPSP.

A minor limitation is that the method of PSPSP requires a typed model. In order to also be safe against type-flaw attacks one needs to employ a typing result like ¹⁴ and thus also needs to satisfy the requirements of that result, but this is not a serious limitation for the class of protocols we consider and it is automatically checked (see Section 2.3).

Finally, PSPSP has a number of smaller limitations that we list here for completeness:

We require that all variables must have an atomic type. This restriction could actually be overcome because, for a type-flaw resistant protocol, it is sound to replace a variable of composed type with a corresponding composed term of atomic type variables. However, we consider it out of scope to implement and formally verify this transformation and its soundness, and thus require that all variables must have atomic type.

Our definition of the $\mathit{(}\mathit{D}\mathit{e}\mathit{c}\mathit{o}\mathit{m}\mathit{p}\mathit{o}\mathit{s}\mathit{e}\mathit{)}$ rule using ${\mathsf{A}\mathsf{n}\mathsf{a}}_f$ means that one cannot let secret keys be values $\mathit{S}\mathit{K}$ and then define the corresponding public key as $\mathsf{p}\mathsf{k}(\mathit{S}\mathit{K})$ . This is because ${\mathsf{A}\mathsf{n}\mathsf{a}}_f$ does not allow definitions on the form $\mathsf{A}\mathsf{n}\mathsf{a}(\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(\mathsf{p}\mathsf{k}(k),m))=(\{k\},\{m\})$ . We consider this a small restriction because, as the examples show, one can instead let the public keys be values, and then have a function $\mathsf{i}\mathsf{n}\mathsf{v}$ mapping them to private keys.

We are using pattern matching in the receipt of messaging. The user of our tool thus needs to understand that to implement a specified protocol, they need their implementation to reject messages received that are not in the expected format. This is in contrast to ProVerif’s $\pi$ -calculus, ⁶ where the steps checking the format are stated more explicitly in the specifications. We do not consider this a significant limitation because this kind of pattern matching is quite standard in the modeling of security protocols, for example, AVISPA, and Meier et al. ¹²

4.3. Example of a fixed point computation

Consider again the keyserver protocol defined in Section 3.1; for simplicity, we do this example for just one user $\mathsf{a}$ who is also honest: $\mathsf{u}\mathsf{s}\mathsf{e}\mathsf{r}=\mathsf{h}\mathsf{o}\mathsf{n}\mathsf{e}\mathsf{s}\mathsf{t}=\{\mathsf{a}\}$ . We show how the fixed point (or rather the candidate that we then check with Isabelle) is computed; to make it more readable, let us give the fixed point right away and then see how each element is derived: ${\mathsf{F}\mathsf{P}}_{\mathit{k}\mathit{s}}\equiv ({\mathit{F}\mathit{P}}_{\mathit{k}\mathit{s}},{\mathit{T}\mathit{I}}_{\mathit{k}\mathit{s}}),$ where

The term implication graph ${\mathit{T}\mathit{I}}_{\mathit{k}\mathit{s}}$ can be represented graphically as follows with each edge $a\to \to b$ corresponding to an element of ${\mathit{T}\mathit{I}}_{\mathit{k}\mathit{s}}$ :

Note that we can actually reduce the representation of the fixed point a little, as we do not need to include facts that can be obtained via term implication from others; with this optimization, we obtain:

To compute ${\mathsf{F}\mathsf{P}}_{\mathit{k}\mathit{s}}$ , we first consider the transaction $\mathsf{o}\mathsf{u}\mathsf{t}\mathsf{O}\mathsf{f}\mathsf{B}\mathsf{a}\mathsf{n}\mathsf{d}$ where a fresh key is inserted into both $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})$ and $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a})$ and sent out. The abstraction of this key is thus the value . This value is in the intruder’s knowledge in ${\mathit{F}\mathit{P}}_{\mathit{k}\mathit{s}}$ but redundant due to other messages we derive later. [In fact, the well-formedness conditions of the previous section require us to also include $\mathsf{o}\mathsf{c}\mathsf{c}\mathsf{u}\mathsf{r}\mathsf{s}$ facts, but for illustration, we have simply omitted them (as the intruder knows every public key that occurs).] Note that this rule cannot produce anything else, so we do not consider it for the remainder.

Next, let us look at the transaction $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{U}\mathsf{s}\mathsf{e}\mathsf{r}$ . For $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{U}\mathsf{s}\mathsf{e}\mathsf{r}$ , we need to choose an abstract value for $\mathit{P}\mathit{K}$ that satisfies the check $\mathit{P}\mathit{K}\mathsf{i}\mathsf{n}\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})$ . At this point in the fixed point computation, we have only . Since the transaction removes the key $\mathit{P}\mathit{K}$ from $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})$ , we get the term implication . A fresh value $\mathit{N}\mathit{P}\mathit{K}$ is also generated and inserted into $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})$ , and a signed message is sent out which gives us: . Also, this one is a message that later becomes redundant with further messages. By analysis, the intruder also obtains .

The new value allows for another application of the $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{U}\mathsf{s}\mathsf{e}\mathsf{r}$ rule, namely with this key in the role of $\mathit{P}\mathit{K}$ . This now gives the term implication and the message . After this, there are no further ways to apply this transaction rule, because we will not get to any other abstract value that contains $\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}(\mathsf{a})$ .

Applying the $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ transaction to the first signature we have obtained (i.e., with and ), we get the term implications and , and the intruder learns . Applying the $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ transaction with the second signature (i.e., with $\mathit{P}\mathit{K}=\mathrm{\varnothing }$ and $\mathit{N}\mathit{P}\mathit{K}$ as before) is not possible because $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a})\notin \mathrm{\varnothing }$ and thus the transaction’s check of $\mathit{P}\mathit{K}\in \mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a})$ will not be satisfied. However, because of the intruder’s knowledge of the first signature and the previously stated term implication , the intruder also knows the signature . If we apply the $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ transaction with this signature (i.e., with and ) then we get the new term implication , the term implication , which we already knew, and the intruder learns , but that was already in the intruder knowledge.

Any other signature that the intruder knows as a consequence of the two signatures sent by the agent and the term implications will not satisfy the checks of the $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ transaction. Note though, that we must also check if the intruder can generate a signature that works with $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ : however, the only private keys he knows are those represented by , and they are not accepted for this transaction. (In a model with dishonest agents, the intruder can, of course, produce signatures with keys registered to a dishonest agent’s name, but here we have just one honest user $\mathsf{a}$ .)

No other transaction can produce anything we do not have in ${\mathit{F}\mathit{P}}_{\mathit{k}\mathit{s}}$ already—in particular, we cannot apply the attack transaction, and this concludes the fixed point computation. Thus—according to our abstract interpretation analysis—the protocol is indeed secure. Next, we try to convince Isabelle.

5. Computing fixed points and checking fixed point coverage

In this work, we automatically calculate fixed points with the abstract interpretation approach as a “proof idea” for conducting the security proof on the concrete protocol. A major contribution of our work is the ability to turn this fixed point into a formal security proof in Isabelle. Essentially, we prove that the fixed point indeed “covers” everything that can happen. We break this down into an induction proof: given any trace that is covered by the fixed point, if we extend it by any applicable transition, then the resulting trace is also covered by the fixed point. This induction step we break down into a number of checks that are directly executable within Isabelle using the built-in term rewriting proof method code-simp. The induction is done in the proof of a protocol-independent Isabelle theorem (Theorem 3) that shows that any protocol that passes said checks is indeed secure. Note that these checks are not only fully automated, but they also terminate in all but a few degenerate cases. [It is technically possible to specify protocols for which the checks do not terminate. For instance, an analysis rule of the form ${\mathsf{A}\mathsf{n}\mathsf{a}}_f(x)=(\{f(f(x))\},R)$ , for some $f$ , $x$ and $R$ , would lead to termination issues when automatically proving the conditions for the typing result which we rely on, because we here need to compute a set that contains the terms occurring in the protocol specification and is closed under keys needed for analysis, and such a set would in this case be infinite. However, this is an artificial example that normally does not occur since it is usually the case that keys cannot themselves be analyzed.]

5.1. Automatically checking for fixed point coverage

Let us look at how we can automatically check if a fixed point covers a protocol. We first explain how this works in general and thereafter give an example, in Example 6, of how it works using the keyserver example.

A transaction of the protocol after resolving all the syntactic sugar has only variables of type $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{u}\mathsf{e}$ . Thus, in a typed model and under the abstraction, we can instantiate the variables only with abstract values, that is, elements from $\mathbb{A}$ . We first define what it means that a transaction is applicable under such a substitution of the variables with respect to the fixed point computed by the abstract interpretation:

Definition 7 (Fixed point coverage: preconditions)

Let $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}$ be a transaction and let $\mathsf{F}\mathsf{P}=(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ be a fixed point. Let further $\delta$ be an abstraction substitution mapping the variables of $T$ to abstract values of $\mathbb{A}$ . We say that $\delta$ satisfies the preconditions (for $T$ and $\mathsf{F}\mathsf{P}$ ), written $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{F}\mathsf{P},\delta ,T)$ , iff the following conditions are met:

F1.

${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})⊢\delta (t_i)$ for all $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}{t}_1,\dots ,t_n$ occurring in $S_{\mathit{r}}$ and for all $i\in \{1,\dots ,n\}$ .

F2.

$s\in \delta (x)$ for all $x\mathsf{i}\mathsf{n}s$ occurring in $S_{\mathit{c}}$ .

F3.

$s\notin \delta (x)$ for all $x\mathsf{n}\mathsf{o}\mathsf{t}\mathsf{i}\mathsf{n}s$ occurring in $S_{\mathit{c}}$ .

F4.

for all $x\in \mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ .

Here, F1 checks that the intruder can produce all input messages for the transaction under the given $\delta$ . Note that the intruder has control over the entire network, so he can use any message honest agents have sent and also construct other messages from that knowledge (hence the $⊢$ ). Moreover, we consider here the closure of the intruder knowledge $\mathit{F}\mathit{P}$ under the term implication rules, since that represents all variants of the messages that are available to the intruder; we will later show as an optimization that we can check whether ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})⊢\delta (t)$ holds without first explicitly computing ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})$ . The two next checks, F2 and F3, verify that are that all set membership conditions are satisfied, and F4 checks that all fresh variables represent values that are not members of any set.

Now, for every $\delta$ under which the transaction $T$ can be applied (according to $\mathsf{F}\mathsf{P}$ ), we compute what $T$ can “produce” and check that it is already covered by $\mathsf{F}\mathsf{P}$ . The transaction can produce outgoing messages and changes in set memberships. The latter is captured by an updated abstraction substitution ${\delta }_u$ that is identical with $\delta$ except for those values that changed their set memberships during the transaction:

Definition 8 (Abstraction substitution update)

Let $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}$ be a transaction and $\delta$ an abstraction substitution. We define the update of $\delta$ w.r.t. $T$ , written ${\delta }_u$ , as follows:

$$\begin{array}{rl}{\delta }_u(x)& \equiv \mathsf{u}\mathsf{p}\mathsf{d}(S_{\mathit{u}},x,\delta (x)),\text{ where}\end{array}$$

$$\begin{array}{rl}\mathsf{u}\mathsf{p}\mathsf{d}(0,x,a)& =a,\\ \mathsf{u}\mathsf{p}\mathsf{d}(\mathfrak{t}\cdot S,x,a)& =\{\begin{array}{ll}\mathsf{u}\mathsf{p}\mathsf{d}(S,x,a\cup \{s\})& \text{if }\mathfrak{t}=\mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}xs,\\ \mathsf{u}\mathsf{p}\mathsf{d}(S,x,a\setminus \{s\})& \text{if }\mathfrak{t}=\mathsf{d}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{t}\mathsf{e}xs,\\ \mathsf{u}\mathsf{p}\mathsf{d}(S,x,a)& \text{otherwise}.\end{array}\end{array}$$

Note that according to this definition, if a transaction contains insert and delete operations of the same value $x$ for the same set, then “the last one counts.” But there is a more subtle point: suppose the transaction includes the operations $\mathsf{i}\mathsf{n}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{t}xs$ and $\mathsf{d}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{t}\mathsf{e}ys$ . The above definition would not necessarily formalize the updates of the set memberships if the transaction were applicable (in the concrete) under an interpretation $\mathcal{I}$ with $\mathcal{I}(x)=\mathcal{I}(y)$ . Thanks to the preparations described in Section 3.3, we have in every transaction the constraint that all value variables have pairwise disjoint concrete values.

This leads to the following two postconditions:

Definition 9 (Fixed point coverage: post-conditions)

Let $T=S_{\mathit{r}}\cdot S_{\mathit{c}}\cdot \mathit{F}\cdot S_{\mathit{u}}\cdot S_{\mathit{s}}$ be a transaction and let $\mathsf{F}\mathsf{P}=(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ be a fixed point. Let $\delta$ be an abstraction substitution and ${\delta }_u$ the update of $\delta$ w.r.t. $T$ . We say that $\delta$ satisfies the postconditions (for $T$ and $\mathsf{F}\mathsf{P}$ ), written $\mathsf{p}\mathsf{o}\mathsf{s}\mathsf{t}(\mathsf{F}\mathsf{P},\delta ,T)$ , iff the following conditions are met:

G1.

$\delta (x)\to {\to }^{*}{\delta }_u(x)$ for all $x\in \mathit{f}\mathit{v}(T)\setminus \mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)$ .

G2.

${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})⊢{\delta }_u(t_i)$ for all $\mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}{t}_1,\dots ,t_n$ occurring in $S_{\mathit{s}}$ and for all $i\in \{1,\dots ,n\}$ .

Here G1 expresses that every update of a value must correspond to a path in the term implication graph (it does not need to be a single edge). G2 means that the intruder learns every outgoing message ${\delta }_u(t)$ and thus it must be covered by the fixed point when closed under term implication.

We can now put it all together: the preconditions restrict the coverage check to those abstraction substitutions that are actually possible in the fixed point. The postconditions check that the fixed point covers everything that the transaction produces under those same substitutions. Fixed point coverage is thus defined as follows:

Definition 10 (Fixed point coverage)

Let $T$ be a transaction and let $\mathsf{F}\mathsf{P}=(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ be a fixed point. We say that $\mathsf{F}\mathsf{P}$ covers $T$ iff for all abstraction substitutions $\delta$ with domain $\mathit{f}\mathit{v}(T)$ , if $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{F}\mathsf{P},T,\delta )$ then $\mathsf{p}\mathsf{o}\mathsf{s}\mathsf{t}(\mathsf{F}\mathsf{P},T,\delta )$ . For a protocol $\mathcal{P}$ we say that $\mathsf{F}\mathsf{P}$ covers $\mathcal{P}$ iff $\mathsf{F}\mathsf{P}$ covers all transactions of $\mathcal{P}$ .

With this defined, we can prove the following theorem:

Theorem 3

Let $\mathcal{P}$ be a protocol and let $\mathsf{F}\mathsf{P}=(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ be a fixed point. If $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}\notin \mathit{F}\mathit{P}$ , and if $\mathcal{P}$ is covered by $\mathsf{F}\mathsf{P}$ , then $\mathcal{P}$ is secure. [This theorem is called protocol_secure in the Isabelle code and can be found in the Stateful_Protocol_Verification.thy theory file.]

Proof Proof Sketch

We gave the intuition of this proof in the introductory text of this section. We supplement that here with some further intuition. First, we define a notion of abstract intruder knowledge, namely ${\alpha }_{ik}(\mathcal{A},\mathcal{I})={\alpha }_{db(\mathcal{A},\mathcal{I},\mathrm{\varnothing })}(\mathcal{I}(ik(\mathcal{A})))$ . The proof then relies on two insights about this abstract intruder knowledge.

The first insight is that if a term $t$ is in the intruder’s knowledge, then its abstraction is also in the abstract intruder knowledge. Formally if $t\in \mathcal{I}(ik(\mathcal{A}))$ then ${\alpha }_{db(\mathcal{A},\mathcal{I},\mathrm{\varnothing })}(t)\in {\alpha }_{ik}(\mathcal{A},\mathcal{I})$ .

The second insight is to prove that for any reachable constraint $\mathcal{A}$ , with satisfying interpretation $\mathcal{I}$ , it is the case that any message $t$ (e.g., the $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ constant) in the abstract intruder knowledge is also derivable from the fixed point. Formally if $t\in {\alpha }_{ik}(\mathcal{A},\mathcal{I})$ then ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})⊢t$ . The proof of this second insight is by an induction on how $\mathcal{A}$ was reached by ${\Rightarrow }^{\bullet }$ . The central part is the induction step where a reachable constraint ${\mathcal{A}}^{\prime }$ is extended with the dual of a transaction $T$ . Here we see that the abstract intruder knowledge achieved by running the dual of $T$ is a result of messages sent in $T$ . The definition of coverage ensures that these sent messages are also derivable from the fixed point’s term implication closure.

Example 6

Consider the key update transaction $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ from Section 3.1. We now show that the fixed point ${\mathsf{F}\mathsf{P}}_{\mathit{k}\mathit{s}}$ defined in Example 4.3 covers this transaction, that is, satisfies Definition 10.

The only variables occurring in $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ are $\mathit{P}\mathit{K}$ and $\mathit{N}\mathit{P}\mathit{K}$ , so we can begin by finding the abstraction substitutions with domain $\{\mathit{P}\mathit{K},\mathit{N}\mathit{P}\mathit{K}\}$ that satisfy the preconditions given in Definition 7. We denote by $\mathrm{\Delta }$ the set of these substitutions. Afterwards, we show that all $\delta \in \mathrm{\Delta }$ satisfy the postconditions given in Definition 9.

The variables $\mathit{P}\mathit{K}$ and $\mathit{N}\mathit{P}\mathit{K}$ are not declared as fresh in $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ so condition F4 is vacuously satisfied. From F2 and F3 we know that $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a})\in \delta (\mathit{P}\mathit{K})$ and $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a}),\mathsf{r}\mathsf{e}\mathsf{v}\mathsf{o}\mathsf{k}\mathsf{e}\mathsf{d}(\mathsf{a})\notin \delta (\mathit{N}\mathit{P}\mathit{K})$ , for all $\delta \in \mathrm{\Delta }$ . From F1 we know that ${\mathit{c}\mathit{l}}_{{\mathit{T}\mathit{I}}_{\mathit{k}\mathit{s}}}({\mathit{F}\mathit{P}}_{\mathit{k}\mathit{s}})⊢\delta (\mathsf{s}\mathsf{i}\mathsf{g}\mathsf{n}(\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{P}\mathit{K}),\mathsf{p}\mathsf{a}\mathsf{i}\mathsf{r}(\mathsf{a},\mathit{N}\mathit{P}\mathit{K})))$ . The intruder cannot compose the signature himself since he cannot derive a private key of the form $\mathsf{i}\mathsf{n}\mathsf{v}(b)$ where $b\in \mathbb{A}$ and $\mathsf{v}\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{d}(\mathsf{a})\in b$ . Hence, the only signatures available to him—that also satisfy the constraints for $\mathrm{\Delta }$ that we have deduced so far—are for each . The only surviving substitutions are

That is, $\mathrm{\Delta }=\{{\delta }^1,{\delta }^2\}$ .

Next, we compute the updated substitutions w.r.t. the transaction $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ :

Now we can verify that conditions G1 and G2 hold for ${\delta }^1$ and ${\delta }^2$ : We have that ${\delta }^i(x)\to \to {\delta }_u^i(x)$ is covered by ${\mathit{T}\mathit{I}}_{\mathit{k}\mathit{s}}$ , for all $i\in \{1,2\}$ and all $x\in \{\mathit{P}\mathit{K},\mathit{N}\mathit{P}\mathit{K}\}$ . We also have that the outgoing message $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{P}\mathit{K})$ is in ${\mathit{c}\mathit{l}}_{{\mathit{T}\mathit{I}}_{\mathit{k}\mathit{s}}}({\mathit{F}\mathit{P}}_{\mathit{k}\mathit{s}})$ under each ${\delta }_u^i$ . Thus $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{U}\mathsf{p}\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{e}\mathsf{S}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}$ is covered by ${\mathsf{F}\mathsf{P}}_{\mathit{k}\mathit{s}}$ .

We can, in a similar fashion, verify that the remaining transactions of the keyserver protocol are covered by the fixed point. Thus, the keyserver protocol is covered by ${\mathsf{F}\mathsf{P}}_{\mathit{k}\mathit{s}}$ .

5.2. Automatic fixed point computation

An interesting consequence of the coverage check is that we can also use it to compute a fixed point for protocols $\mathcal{P}$ . In a nutshell, we can update a given fixed point candidate ${\mathsf{F}\mathsf{P}}_0$ for $\mathcal{P}$ as follows: For each transaction of $\mathcal{P}$ , we first compute the abstraction substitutions $\mathrm{\Delta }$ that satisfy the preconditions F1 to F4. Secondly, we use the postconditions G1 and G2 to compute the result of taking $T$ under each $\delta \in \mathrm{\Delta }$ and add those terms and term implications to ${\mathsf{F}\mathsf{P}}_0$ . Starting from an empty initial iterand $(\mathrm{\varnothing },\mathrm{\varnothing })$ , we can then iteratively compute a fixed point for $\mathcal{P}$ . Definition 11 gives a simple method to compute protocol fixed points based on this idea.

Definition 11

Let $\mathcal{P}$ be a protocol and let $f$ be the function defined as follows:

$$\begin{array}{rl}f((\mathit{F}\mathit{P},\mathit{T}\mathit{I}))& \equiv (\mathit{F}\mathit{P}\cup \{t\in {\widehat{\mathit{F}\mathit{P}}}_{\delta }^T\mid T\in \mathcal{P},\delta \in {\mathrm{\Delta }}_{\mathit{F}\mathit{P},\mathit{T}\mathit{I}}^T\},\\ & \mathit{T}\mathit{I}\cup \{(a,b)\in {\widehat{\mathit{T}\mathit{I}}}_{\delta }^T\mid T\in \mathcal{P},\delta \in {\mathrm{\Delta }}_{\mathit{F}\mathit{P},\mathit{T}\mathit{I}}^T\}),\end{array}$$

where

$$\begin{array}{rl}{\mathrm{\Delta }}_{\mathit{F}\mathit{P},\mathit{T}\mathit{I}}^T& \equiv \{\delta \mid \mathit{d}\mathit{o}\mathit{m}(\delta )=\mathit{f}\mathit{v}(T),\mathsf{p}\mathsf{r}\mathsf{e}((\mathit{F}\mathit{P},\mathit{T}\mathit{I}),T,\delta )\},\\ {\widehat{\mathit{F}\mathit{P}}}_{\delta }^T& \equiv \{{\delta }_u(t_i)\mid \mathsf{s}\mathsf{e}\mathsf{n}\mathsf{d}{t}_1,\dots ,t_n\text{ occurs in }T,1\le i\le n\},\\ {\widehat{\mathit{T}\mathit{I}}}_{\delta }^T& \equiv \{(\delta (x),{\delta }_u(x))\mid x\in \mathit{f}\mathit{v}(T)\setminus \mathit{f}\mathit{r}\mathit{e}\mathit{s}\mathit{h}(T)\}.\end{array}$$

Then we can compute a fixed point for $\mathcal{P}$ by computing a fixed point of $f$ . This can be done, for example, by computing the least $n\in \mathbb{N}$ such that $f^n((\mathrm{\varnothing },\mathrm{\varnothing }))=f^{n+1}((\mathrm{\varnothing },\mathrm{\varnothing }))$ because then $f^n((\mathrm{\varnothing },\mathrm{\varnothing }))$ is indeed a fixed point.

We provide, as part of our Isabelle formalization, a function to compute such a fixed point (with some optimizations to avoid computing terms and term implications that are subsumed by the remaining fixed point), using the built-in code generation functionality of Isabelle.

6. Improving the coverage check

We describe a number of improvements that are essential to an efficient check. Since we have proven the checks correct in Isabelle, there is no risk of affecting the correctness of the entire approach.

There are two major issues that make the coverage check from the previous section quite inefficient when implemented directly. One concerns the fact that to see if a protocol is covered, we need to consider for every received term any message that is in the fixed point closed under term implications and intruder deduction. Even though the typed model allows us to keep even the intruder deduction closure finite, explicitly computing the closure is not feasible even on rather modest examples. The second issue is about the abstraction substitutions $\delta$ of the check: recall that in the check we defined above, for a given transaction we consider every substitution $\delta$ of the variables with abstract values, which is of course exponential both in the number of variables and the number of sets.

Let us first deal with this second issue. We can indeed compute exactly those substitutions that satisfy conditions F2 to F4: every positive set-membership check $x\mathsf{i}\mathsf{n}s$ of the transaction requires that $s\in \delta (x)$ , and similarly for the negative case. Moreover, $\delta (x)$ can be only an abstract value that actually occurs as a member of the fixed point or as a subterm in the fixed point. Starting from these constraints often substantially cuts down the number of substitutions $\delta$ that we need to consider in the check, especially when we have more agents than in the example. This is because typically (at least in a good protocol) most values will not be members of many sets that belong to different agents (but rather just a few that deal with that particular value).

The first issue, that is, avoiding computing the term implication closure ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})$ when performing intruder deductions, is more difficult. The majority of this section is therefore dedicated to improving on conditions F1 and G2 so that we can avoid computing the entire closure ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})$ —only in a few corner cases do we need to compute the closure for a few terms of $\mathit{F}\mathit{P}$ . A key to that is to saturate the intruder’s knowledge with terms that can be obtained by analysis and then work with composition only, that is, ${⊢}_c$ .

6.1. Intruder deduction modulo term implications

Recall that ${⊢}_c$ is the intruder deduction without analysis, that is, only the $\mathit{(}\mathit{A}\mathit{x}\mathit{i}\mathit{o}\mathit{m}\mathit{)}$ and $\mathit{(}\mathit{C}\mathit{o}\mathit{m}\mathit{p}\mathit{o}\mathit{s}\mathit{e}\mathit{)}$ rules. We first consider how we can handle in this restricted deduction relation the term implication graph $\mathit{T}\mathit{I}$ efficiently, that is, how to decide ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊢}_{c}t$ (for given $\mathit{T}\mathit{I}$ , $M$ , and $t$ ) without computing ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ . In a second step, we then show how to also handle analysis, that is, the full $⊢$ relation.

In fact, it boils down to checking the side condition of $\mathit{(}\mathit{A}\mathit{x}\mathit{i}\mathit{o}\mathit{m}\mathit{)}$ , that is, in our case, whether $t\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ , without having to compute ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ first. (The composition rule is then easier because it does not “directly look” at the knowledge.) For this, it is sufficient if we can check whether $t\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t^{\prime })$ for any $t^{\prime }\in M$ , without having to compute ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t^{\prime })$ .

Consider again Definition 5. We can use this to derive a recursive check function $t^{\prime }{⇝}_{\mathit{T}\mathit{I}}t$ for the question $t\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t^{\prime })$ : it can only hold if either

$t$ and $t^{\prime }$ are the same variable,

or $t$ , $t^{\prime }$ are abstract values with a path from $t^{\prime }$ to $t$ in $\mathit{T}\mathit{I}$ ,

or $t=f(t_1,\dots ,t_n)$ and $t^{\prime }=f(t_1^{\prime },\dots ,t_n^{\prime })$ , where recursively $t_i^{\prime }{⇝}_{\mathit{T}\mathit{I}}{t}_i$ holds for all $1\le i\le n$ .

With this we can define a recursive relation ${⊩}_c$ that checks for given $M$ , $\mathit{T}\mathit{I}$ , and $t$ whether ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊢}_{c}t$ without computing ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ :

$$\begin{array}{rcl}M{⊩}_c^{\mathit{T}\mathit{I}}t& \text{iff}& (\mathrm{\exists }{t}^{\prime }\in M.t^{\prime }{⇝}_{\mathit{T}\mathit{I}}t)\text{ or }\\ & & t\text{ is of the form }t=f(t_1,\dots ,t_n)\text{ where }f\in {\mathrm{\Sigma }}_{\mathit{p}\mathit{u}\mathit{b}}^n\text{ and }M{⊩}_c^{\mathit{T}\mathit{I}}{t}_i\text{ for all }i\in \{1,\dots ,n\}.\end{array}$$

This relation indeed fulfills its purpose:

Lemma 2

${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊢}_{c}t\text{ iff }M{⊩}_c^{\mathit{T}\mathit{I}}t$ .

Next, we show how to reduce the intruder deduction problem $⊢$ to the restricted variant ${⊢}_c$ .

6.2. Analyzed intruder knowledge

It has been observed that many intruder deduction problems can be regarded as local theories, that is, so that all intermediate terms in the deduction are subterms of the given intruder knowledge or the goal term to construct. This is because the intruder may, of course, compose a message and then decompose it again, but in most theories, that would only yield one of the terms that we started with. Observe that we only support theories where the result of an analysis step is $x$ direct subterms of the term being analyzed. This means that all deduction proofs that contain such a pair of encryption–decryption steps can be normalized to a simpler proof, eliminating the unnecessary detour. Thus, all decomposition steps are applied to messages composed by an honest agent, and thus all intermediate steps in an intruder deduction are subterms of what the intruder wants to construct or knows in advance. [We only mention here that this is indeed close to the concept of a local theory: it is sufficient to consider in a deduction $M⊢m$ only intermediate terms that are subterms of $M$ or $m$ . However, there are some exceptions to the locality property: in decomposition, the necessary key may not be a subterm of $M$ or $m$ . For instance, to decrypt $\mathsf{c}\mathsf{r}\mathsf{y}\mathsf{p}\mathsf{t}(K,M)$ , one needs $\mathsf{i}\mathsf{n}\mathsf{v}(K)$ , which may neither be part of $M$ nor $m$ . (In that case, since $\mathsf{i}\mathsf{n}\mathsf{v}$ is private, the deduction step is only possible if $\mathsf{i}\mathsf{n}\mathsf{v}(K)$ already occurs in $M$ .)]

The proof normalization argument we just sketched would be very difficult to integrate into Isabelle directly, since we would have to meta-reason in Isabelle about the definition of the intruder deduction rules. In fact, we have a similar way when reasoning about homogeneous message deduction in compositional proofs (i.e., that the intruder never needs to mix messages from the protocols being composed). Our Isabelle proofs work by induction over the size of terms (not over the structure of the deduction) that everything deducible is also deducible with a more restricted notion, in this case, that it is sufficient to only compose terms if the intruder’s knowledge is already analyzed. We note that such arguments do not hold in general when algebraic properties are considered (such as commutativity of exponents in Diffie-Hellman). For that case, our theory would need nontrivial adaptations.

The idea is thus that ${⊢}_c$ is actually already sufficient, if we have an analyzed intruder knowledge: we define that a knowledge $M$ is analyzed iff $M⊢t$ implies $M{⊢}_{c}t$ for all $t$ . More in detail, we can consider a knowledge $M$ that is saturated by adding all subterms of $M$ that can be obtained by analysis. Then $M$ is analyzed, that is, we do not need any further analysis steps in the intruder deduction. This is intuitively the case because the intruder cannot learn anything from analyzing messages he has composed himself.

We define formally what it means for a term $t$ to be analyzed using the keys ( $\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)$ ) and results ( $\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t)$ ) from the analysis as defined in Section 2.2:

Definition 12 (Analyzed term)

Let $M$ be a set of terms and let $t$ be a term. We then say that $t$ is analyzed in $M$ iff $M{⊢}_c\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)\text{ implies }M{⊢}_c\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t)$ (where $M{⊢}_{c}N$ for sets of terms $M$ and $N$ is a shorthand for $\mathrm{\forall }t\in N.M{⊢}_{c}t$ ).

The following lemma then provides us with a decision procedure for determining if a knowledge is analyzed:

Lemma 3

$M$ is analyzed iff all $t\in M$ are analyzed in $M$ .

We consider again an intruder’s knowledge given as the term implication closure of a set of messages, that is, ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ instead of $M$ . Efficiently checking whether an intruder’s knowledge term implication closure is analyzed, without actually computing it, is challenging. The following lemma shows that if we can derive the results of analyzing a term $t$ in the knowledge $M$ , then we can also derive the results of analyzing any implied term $t^{\prime }\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ :

Lemma 4

Let $t\in M$ . If ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊢}_c\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t)$ then for all $t^{\prime }\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ , ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊢}_c\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t^{\prime })$ .

Therefore, if all $k\in \mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)$ can be derived and $t$ is analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ then we can conclude that all implied terms $t^{\prime }\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ are analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ . If, however, some of the keys for $t$ are not derivable, then we are forced to check the implied terms as well as the following example shows:

Example 7

Let $f,g\in {\mathrm{\Sigma }}_{\mathit{p}\mathit{r}\mathit{i}\mathit{v}}^1$ , $\mathit{T}\mathit{I}=\{a\to \to b\}$ , and $M=\{f(a),g(b)\}$ . Define the analysis rules ${\mathsf{A}\mathsf{n}\mathsf{a}}_f(x)=(\{g(x)\},\{x\})$ and ${\mathsf{A}\mathsf{n}\mathsf{a}}_g(x)=(\mathrm{\varnothing },\mathrm{\varnothing })$ . Then ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)=\{f(b)\}\cup M$ . The term $f(a)$ is analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ because the key $g(a)$ cannot be derived: ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊬}_{c}g(a)$ . However, $f(a){}_a\to \to {}_{b}f(b)$ and $f(b)$ is not analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ : $\mathsf{A}\mathsf{n}\mathsf{a}(f(b))=(\{g(b)\},\{b\})$ but the key $g(b)$ is derivable from ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ in ${⊢}_c$ , whereas the result $b$ is not. Thus ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ is not an analyzed knowledge.

So in most cases we can efficiently check if ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ is analyzed, and in some cases we need to also compute the term implication closure ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ of problematic terms $t\in M$ (but not necessarily compute all of ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ ). The former corresponds to the three “if” cases of the following definition, and the latter corresponds to the final “else”-branch:

Lemma 5

${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ is analyzed iff for all $t\in M$ , the following holds:

$$\begin{array}{l}\mathbf{\text{if}}{\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊢}_c\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)\mathbf{\text{then}}t\text{ is analyzed in }{\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)\\ \mathbf{\text{else}}\mathbf{\text{if}}\mathbb{A}\cap \mathit{s}\mathit{u}\mathit{b}\mathit{t}\mathit{e}\mathit{r}\mathit{m}\mathit{s}(\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t))=\mathrm{\varnothing }\mathbf{\text{then}}\mathit{t}\mathit{r}\mathit{u}\mathit{e}\\ \mathbf{\text{else}}\mathbf{\text{if}}\mathrm{\forall }s\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)).{\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊬}_{c}s\mathbf{\text{then}}\mathit{t}\mathit{r}\mathit{u}\mathit{e}\\ \mathbf{\text{else}}\text{all }{t}^{\prime }\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)\text{ are analyzed in }{\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M).\end{array}$$

Lemma 5 provides us with the means to extend a knowledge $M$ to one whose term implication closure is analyzed: Suppose for a term $t\in M$ the three if conditions of the lemma fail, that is, when we have to check for every $t^{\prime }\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ that $t^{\prime }$ is analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ . If $t^{\prime }$ can be decrypted and the keys are available, but the result $\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t^{\prime })$ of the decryption cannot be composed in $M$ , then (and only then) we add this result to $M$ . For instance, in Example 7, we need to extend $M=\{f(a),g(b)\}$ with $b$ , resulting in the analyzed knowledge $M^{\prime }=\{f(a),g(b),b\}$ .

The two “else–if”-branches are an improvement we have made for this journal version of the paper. The idea is the following:

1. (1)

If $\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)$ are not derivable from the term-implication closed knowledge ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ , and if there is no abstract value occurring in $\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)$ , then $\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(s)=\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)$ for all implied terms $s$ of $t$ , and so $t$ is analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ .

(2)

If none of the implied keys of $t$ are derivable then $t$ is also analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ .

These two special cases are useful to speed up the analyzed-fixed point check when the fixed point contains terms that have lots of abstract values in them and that cannot be analyzed by the intruder (the last else branch would in such cases take a lot of time to compute since the size of ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ grows exponentially with the number of occurrences of abstract values in $t$ )—also, it is often the case that $\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t)$ has fewer abstract values in it than $\mathsf{R}\mathsf{e}\mathsf{s}\mathsf{u}\mathsf{l}\mathsf{t}(t)$ , and so the size of ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(t))$ is likely to be much smaller than ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(t)$ , hence the second “else–if” condition is usually much faster to check than the last else-branch.

As an example, when modeling private channels one may use terms of the form $\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}(\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}\mathsf{c}\mathsf{r}(a,b),t)$ , denoting that $t$ is sent on a private channel from agent $a$ to agent $b$ , where the term $t$ is derivable if the secret $\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}\mathsf{c}\mathsf{r}(a,b)$ is known, and where there would be an attack on the protocol if the intruder knew $\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}\mathsf{c}\mathsf{r}(a,b)$ for honest $a$ and $b$ . In a secure protocol, the term $\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}(\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}\mathsf{c}\mathsf{r}(a,b),t)$ , for honest $a$ and $b$ , would not be derivable by the intruder, and so it is sufficient to check that ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M){⊬}_c\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}\mathsf{c}\mathsf{r}(a,b)$ and $\mathbb{A}\cap \mathit{s}\mathit{u}\mathit{b}\mathit{t}\mathit{e}\mathit{r}\mathit{m}\mathit{s}(\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}\mathsf{c}\mathsf{r}(a,b))=\mathrm{\varnothing }$ instead of checking that all elements of ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}(\mathsf{s}\mathsf{e}\mathsf{c}\mathsf{c}\mathsf{h}\mathsf{c}\mathsf{r}(a,b),t))$ are analyzed in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(M)$ , which may take a significant amount of time since $t$ may contain a lot of abstract values.

The improvements described from Section 6 up to here are the Default version of our coverage check. We will now explain an alternative check that improves the run time for some protocols. Note that in our implementation, we can make use of Isabelle’s parallelization framework, executing the default version and the alternative version in parallel, returning the result of whichever check terminates first. By that, we can ensure that the user always benefits from the runtime of the fastest check.

6.3. Restricting the number of abstraction substitutions further

We return to the second issue described at the beginning of this section: restricting how many abstraction substitutions need to be considered in order to conclude that a transaction is covered. The solution presented so far restricted the set of abstraction substitutions considered to those that satisfy conditions F2 to F4 of Definition 7. We now show how to take into consideration also condition F1 to further restrict that set. This will not be exactly the set of substitutions that satisfy F1 to F4, but rather an overapproximation that can be computed in an efficient way.

F1 essentially says that for each received term $t$ of a considered transaction, its abstraction $\delta (t)$ must be derivable from the fixed point using the $⊢$ relation. However, we will, based on the previous two sections, restrict ourselves to the ${⊢}_c$ relation.

We, therefore, in this section, define functions that together calculate an overapproximation of the set of these $\delta$ . These functions can be seen as implementing the ${⊢}_c$ relation. We will now, in this first part of this section, consider two functions based on the Axiom rule of ${⊢}_c$ , and in the second part of this section, we will then consider a function combining the Axiom rule and the Compose rule. We therefore will now introduce two functions ${\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }$ and $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ that are based on the Axiom rule. They work by matching terms in $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -steps, possibly containing variables, with ground terms in the fixed point, possibly containing abstract values. The idea is that by inspecting a term $t$ from the $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -steps and comparing it to the terms available in the fixed point we will be able to see what the variables in $t$ could be instantiated to if $\delta (t)$ is to be a term from the fixed point. This is illustrated by the following example:

Example 8

Consider the term $t=\mathsf{f}(X,X)$ from a $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -step in a transaction of a protocol and the term from a given fixed point. Observe that $s$ and $t$ have a similar structure, but the first and second arguments of $s$ are different, so there is no match between $s$ and $t$ . However, modulo term implication, there could be a match if the two abstract values in $s$ can flow together.

Consider the following term implication graph: The closure of is the set and the term implication closure of is . We can see that both considered abstract values share that they actually represent and . Thus, $t$ can be made equal to $s$ modulo term implication by choosing either to replace all occurrences of $X$ with or by choosing to replace all occurrences of $X$ with . Therefore there are two abstraction substitutions $\delta$ such that $s\to \to \delta (t)$ , namely and .

What we have done in this example is to use three steps to find out if there is a $\delta$ such that $\delta (t)$ can be found in ${\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})$ . More generally, step 1 is to see if there is a term $s\in \mathit{F}\mathit{P}$ that matches $t$ , where different occurrences of the same variable may need to be matched with different abstract values (as for $X$ in the above example). Step 2 is to collect for each variable $X$ the set of every abstract value $a$ that works for every occurrence of $X$ simultaneously modulo term implication, that is, for every abstract value $b$ computed in step 1, $b\to \to a$ . Step 3 is to calculate every possible abstraction substitution $\delta$ from step 2.

Let us first consider ${\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }$ that captures the idea of step 1. It takes two terms $t$ and $s$ , where $t$ is a term from a rule (that may have variables) and $s$ is a term from the fixed point (that may not have variables). The function ${\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }$ checks if $t$ and $s$ can be made equal by replacing occurrences of variables in $t$ with abstract values. If this is possible, it returns a singleton set containing function $\theta$ mapping each variable $x$ to a set of abstract values, where each member of $\theta (x)$ is a possible replacement for $x$ . If it is not possible, it returns the empty set. When trying to match a variable $x$ with an abstract value $a$ , ${\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }$ returns a singleton set $\{\theta \}$ and $\theta$ maps $x$ to $\{a\}$ . For a composed term, we recursively compute the set of matches for each subterm and then pointwise merge the results, so that for each variable $x$ we get all abstract values it needs to have in some occurrence of $x$ in $t$ in order to allow for the match with $s$ . Note that in the following definition, $\delta$ and $\theta$ map from variables to sets of abstract values.

Definition 13

The function ${\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }$ is defined as follows:

$$\begin{array}{rl}{\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }(x,a)& =\{\theta \}\text{if }x\in \mathcal{V},a\in \mathbb{A},\mathrm{\forall }y.\theta (y)=\mathbf{i}\mathbf{f}x=y\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}\{a\}\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}\mathrm{\varnothing }\\ {\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }(t,s)& =\{\theta \}\text{if }t=f(t_1,\dots ,t_n),s=f(s_1,\dots ,s_n),\\ & \mathrm{\forall }i\in \{1,\dots ,n\}.{\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }(t_i,s_i)\ne \mathrm{\varnothing },\\ & \mathrm{\Delta }=\{\delta \in {\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }(t_i,s_i)\mid i\in \{1,\dots ,n\}\},\\ & \mathrm{\forall }x.\theta (x)=\bigcup _{\delta \in \mathrm{\Delta }}\delta (x),\\ {\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }(t,s)=& \mathrm{\varnothing }\text{otherwise}.\end{array}$$

Example 9

We return to Example 8 and see that ${\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }$ indeed will calculate what the occurrences of $X$ should be replaced by. Here we have that . We notice that the set to which $X$ is mapped to consists exactly of the two abstract values that we expected to get from Example 8.

Having defined a function that implements step 1, we now turn to implementing a function $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ that combines this with step 2. The function $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ checks if $t$ and $s$ can be made equal modulo term implication by replacing variables in $t$ with abstract values. If this is possible, it returns a singleton set containing a function $\theta$ mapping each variable $x$ to a set of abstract values, where each member of $\theta (x)$ is a possible replacement for $x$ . If it is not possible, it returns the empty set.

The function does this as follows: If ${\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }$ gave the solution $\sigma$ , $x$ is a variable, and $a\in \sigma (x)$ , that is, $a$ is one of the abstract values $x$ needs to match in some occurrence, then we compute all $b$ that can be reached from $a$ with term implication. Next, ${\sigma }^{\prime }(x)$ is the intersection of these sets (for any $a\in \sigma (x)$ ). Thus, $b\in {\sigma }^{\prime }(x)$ holds iff $a\to \to b$ for every $a\in \sigma (x)$ . This ensures that the term $s$ of the given fixed point can be rewritten by term implications so that it matches $t$ in every occurrence of $x$ . For instance, in Example 8, the variable $X$ could either be or , to allow a match between $s$ and $t$ modulo term implication. Match also checks that all free variables in $t$ can actually represent some abstract value, because if not, then it is not at all possible to make $t$ equal to $s$ modulo term implication. Finally, every variable that does not occur in $t$ we map to $\mathit{O}\mathit{C}\mathit{C}$ , the set of all abstract values that can occur.

Definition 14

Let $\mathsf{F}\mathsf{P}=(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ be a fixed point. Let $\mathit{O}\mathit{C}\mathit{C}$ be the abstract values that occur in $\mathsf{F}\mathsf{P}$ , that is, $\mathit{O}\mathit{C}\mathit{C}=\mathbb{A}\cap \mathit{s}\mathit{u}\mathit{b}\mathit{t}\mathit{e}\mathit{r}\mathit{m}\mathit{s}({\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P}))$ . The function $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ is defined as follows:

$$\begin{array}{rl}\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t,s)& =\{\theta \}\text{if }\sigma \in {\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}}^{\prime }(t,s),\\ & \mathrm{\forall }x.{\sigma }^{\prime }(x)=\bigcap _{a\in \sigma (x)}\{b\mid (a,b)\in {\mathit{T}\mathit{I}}^{*}\},\\ & \mathrm{\forall }x\in \mathit{f}\mathit{v}(t).{\sigma }^{\prime }(x)\ne \mathrm{\varnothing },\\ & \mathrm{\forall }x.\theta (x)=\mathbf{i}\mathbf{f}x\in \mathit{f}\mathit{v}(t)\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}{\sigma }^{\prime }(x)\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}\mathit{O}\mathit{C}\mathit{C},\\ \mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t,s)& =\mathrm{\varnothing }\text{otherwise}.\end{array}$$

We additionally lift $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ to sets of terms $M$ using the following definition:

$$\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t,M)=\{\theta \in \mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t,s)\mid s\in M\}.$$

We can finally conclude with step 3: $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t,s)$ either is empty (if there is no match) or a single map $\theta$ that tells for every variable the possible values under which we can match the terms. Now every abstraction substitution $\delta$ that maps each variable $x$ to an element of $\theta (x)$ is a solution:

Lemma 6

If $\delta (t)\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(s)$ and $\mathit{f}\mathit{v}(s)=\mathrm{\varnothing }$ , there are no abstract values occurring in $t$ , and $\delta$ is an abstraction substitution, then $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t,s)=\{\theta \}$ for some $\theta$ such that for all variables $x$ , if $x\in \mathit{f}\mathit{v}(t)$ then $\delta (x)\in \theta (x)$ , and if $x\notin \mathit{f}\mathit{v}(t)$ then $\theta (x)=\mathit{O}\mathit{C}\mathit{C}$ .

Example 10

Assume that the term implication graph is as in Example 8. Consider then the following calculation by the $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ function: Here the terms and are indeed equal to the term modulo term implication. As explained in Example 8, this will lead to two abstraction substitutions that map the term $\mathsf{f}(X,X)$ into the term modulo term implication, namely and .

This concludes our explanation of the two functions that are based on the Axiom rule of the ${⊢}_c$ relation: For a term $t$ from a $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -step and a fixed point $\mathsf{F}\mathsf{P}$ the function $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ allows us to calculate the abstraction substitutions $\delta$ such that $\delta (t)\in {\mathit{c}\mathit{l}}_{\mathit{T}\mathit{I}}(\mathit{F}\mathit{P})$ , or in other words, the abstraction substitutions $\delta$ such that $\delta (t)$ can be derived from $\mathit{F}\mathit{P}$ using the Axiom rule.

As promised, we will now introduce a function $\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}$ that combines the Axiom and Compose rules. This function works by matching terms in $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -steps, possibly containing variables, with ground terms derivable from the fixed point. The idea is that by inspecting the terms $t_1,\dots ,t_n$ from the $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -steps and comparing them to the terms derivable from the fixed point we will be able to see what the variables in $t_1,\dots ,t_n$ could be instantiated to if all terms $\delta (t_1),\dots ,\delta (t_n)$ are to be terms derivable from the fixed point. This is illustrated by the following example:

Example 11

Consider a transaction receiving the set of terms $\{{\mathsf{c}}_{\mathsf{p}\mathsf{u}\mathsf{b}},X,{\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{2}}(X,Y),{\mathsf{f}}_{\mathsf{p}\mathsf{u}\mathsf{b}\mathsf{2}}({\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{1}}(X),Y)\},$ where ${\mathsf{c}}_{\mathsf{p}\mathsf{u}\mathsf{b}}$ is a public constant, ${\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{1}}$ and ${\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{2}}$ are private functions, and ${\mathsf{f}}_{\mathsf{p}\mathsf{u}\mathsf{b}\mathsf{2}}$ is a public function.

Assume that we have the following fixed point:

Assume also, for the sake of simplicity, that there are no analysis rules. Then this fixed point is clearly analyzed because all messages that the intruder can derive from $\mathsf{F}\mathsf{P}$ using $⊢$ can also be derived using ${⊩}_c$ . We will now investigate whether each of the received terms matches a term derivable from the fixed point, and additionally determine for the variables $X$ and $Y$ the set of possible abstract values. The first step is to compute $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t,s)$ for every term $t$ in the received messages and every term $s$ in the fixed point. Additionally, if $t=f(t_1,\dots ,t_n)$ for a public $f$ such as ${\mathsf{f}}_{\mathsf{p}\mathsf{u}\mathsf{b}\mathsf{1}}$ , then we recursively check each $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(t_i,s)$ (for every $s$ in the fixed point) since the intruder can then apply $f$ to the respective instances of $t_i$ to generate an instance of $t$ that matches. We summarize this in Table 1.

Table 1.

Matching received terms with terms derivable from the fixed point.

Consider the row for ${\mathsf{c}}_{\mathsf{p}\mathsf{u}\mathsf{b}}$ . The term ${\mathsf{c}}_{\mathsf{p}\mathsf{u}\mathsf{b}}$ is immediately derivable using the Comp rule and this is the case with any replacement of $X$ or $Y$ in the term ${\mathsf{c}}_{\mathsf{p}\mathsf{u}\mathsf{b}}$ because these variables do not occur in ${\mathsf{c}}_{\mathsf{p}\mathsf{u}\mathsf{b}}$ . Consider the row for $X$ . For this to be a derivable abstract value, it needs to be some abstract value in $\mathit{F}\mathit{P}$ , that is, either or . Consider the row for ${\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{2}}(X,Y)$ . Since ${\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{2}}$ is private, we cannot derive it by composition, and so the only option is to use the two matching terms in the fixed point. Consider the row for ${\mathsf{f}}_{\mathsf{p}\mathsf{u}\mathsf{b}\mathsf{2}}({\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{1}}(X),Y)$ . No term in $\mathit{F}\mathit{P}$ matches it, but two matching terms can be constructed from the fixed point using the Comp rule.

Let us now construct the abstraction substitutions that map the variables in such a way that all the received terms are terms derivable from the fixed point. For $X$ , we thus need to pick the abstract values that appear in all cells in the “Replace $X$ with” column. In this case, there is only one such abstract value, namely . For $Y$ , we can pick or . This leads to two possible abstraction substitutions: and .

Example 12

Consider a transaction receiving the set of terms $\{{\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{2}}(X,Y)\}$ , where ${\mathsf{f}}_{\mathsf{p}\mathsf{r}\mathsf{i}\mathsf{v}\mathsf{2}}$ is a private function. Consider the fixed point and $\mathit{T}\mathit{I}=\mathrm{\varnothing }$ . Assume also, for the sake of simplicity, that there are no analysis rules. We apply the approach from Example 11. Thus, both $X$ and $Y$ can be or , and thus we get four possible abstraction substitutions, namely , , and . Notice that we see here that an overapproximation is happening because actually only the first two abstraction substitutions will generate terms represented by the fixed point. We will tolerate this overapproximation.

The function $\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}$ implements the idea from Examples 11 and 12. The function ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(M)$ computes the set of abstract values that the variable $x$ can take so that the intruder can produce all terms in the set $M$ . This set is empty in case the intruder cannot produce all the terms in $M$ (for any choice of $x$ ). We will use this for a transaction $T$ that has the terms $M$ as receive steps and $x$ is any free variable in $T$ .

Definition 15

Let $M\ne \mathrm{\varnothing }$ be a set of messages, $x$ be a variable, and $\mathsf{F}\mathsf{P}=(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ be an analyzed fixed point. We define ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(M)$ recursively as follows:

$$\begin{array}{r}\begin{array}{rll}{\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{y\})=& \{b\mid \mathrm{\exists }a\in \mathit{F}\mathit{P}\cap \mathbb{A}.(a,b)\in {\mathit{T}\mathit{I}}^{*}\}& \text{if }x=y,\\ {\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{y\})=& \mathit{O}\mathit{C}\mathit{C}& \text{if }x\ne y,\\ {\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{c\})=& \mathrm{\varnothing }& \text{if }c\in {\mathcal{C}}_{\mathit{p}\mathit{r}\mathit{i}\mathit{v}}\text{ and }c\notin \mathit{F}\mathit{P},\\ {\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{c\})=& \mathit{O}\mathit{C}\mathit{C}& \text{if }c\in {\mathcal{C}}_{\mathit{p}\mathit{u}\mathit{b}}\text{ or }c\in \mathit{F}\mathit{P},\\ {\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{f(t_1,\dots ,t_n)\})=& A& \text{if }f\in {\mathrm{\Sigma }}_{\mathit{p}\mathit{r}\mathit{i}\mathit{v}}^n,n>0,\\ & & \mathrm{\Delta }=\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(f(t_1,\dots ,t_n),\mathit{F}\mathit{P}),\\ & & A=\bigcup _{\delta \in \mathrm{\Delta }}\delta (x),\\ {\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{f(t_1,\dots ,t_n)\})=& A_1\cup A_2& \text{if }f\in {\mathrm{\Sigma }}_{\mathit{p}\mathit{u}\mathit{b}}^n,n>0,\\ & & \mathrm{\Delta }=\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}(f(t_1,\dots ,t_n),\mathit{F}\mathit{P}),\\ & & A_1=\bigcup _{\delta \in \mathrm{\Delta }}\delta (x),\\ & & A_2={\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{t_1,\dots ,t_n\}),\\ {\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{t_1,\dots ,t_n\})=& \bigcap _{i\in \{1,\dots ,n\}}{\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{t_i\})& \text{if }n>1.\end{array}\end{array}$$

The definition of ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(M)$ expresses how the requirement that the intruder has to produce the messages in $M$ constrains the choice of abstract values of $x$ . The first equation says that if $y=x$ is the message the intruder has to produce, we can choose for $x$ only abstract values that are in the fixed point or reachable via term implication. The second equation is the case where the intruder has to produce any other variable $x\ne y$ . In this case, this gives no constraint on $x$ , and we have thus $\mathit{O}\mathit{C}\mathit{C}$ . The third equation says that the intruder cannot produce a private constant that is not in the fixed point. The fourth equation says that the intruder can always produce all public constants and all constants in the fixed point, again not constraining the choice of $x$ . The fifth equation says that if the intruder has to produce a term $f(t_1,\dots ,t_n)$ that is composed of a private function then we use the $\mathsf{m}\mathsf{a}\mathsf{t}\mathsf{c}\mathsf{h}$ function to determine all the mappings $\mathrm{\Delta }$ that map variables to set of abstract values under which said term is in the fixed point modulo term implication. We then return the union $A$ of all abstract values that any of these mappings allow for $x$ . The sixth equation is similar, but here $f$ is public, so we additionally consider the case that the intruder can produce the subterms $t_1,\dots ,t_n$ (and apply $f$ to them), so we have the union of the values $A_1$ that give a direct match in the fixed point with the values $A_2$ under which the subterms can be produced. The final equation lifts ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x$ to sets of terms: to produce all the terms, the intruder must produce every single one of them.

In our implementation, we have one small optimization not presented above to avoid cluttering the presentation here. Consider again the sixth equation. If one of the $t_i$ is a private constant not in $\mathit{F}\mathit{P}$ , then we can “short circuit” the calculation of ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{t_1,\dots ,t_n\})$ because we then know that it will be equal to $\mathrm{\varnothing }$ .

In Example 11, we saw how calculating the possible replacements for each variable related to the abstraction substitutions that instantiate the received terms to derivable terms. We express this idea in the following lemma that captures the idea of $\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}$ :

Lemma 7

Let $T$ be a transaction with at least one $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -step, $\mathsf{F}\mathsf{P}=(\mathit{F}\mathit{P},\mathit{T}\mathit{I})$ be a fixed point where $\mathit{F}\mathit{P}$ is analyzed, $x\in \mathit{f}\mathit{v}(T)$ , $\delta$ be an abstraction substitution with domain $\mathit{f}\mathit{v}(T)$ , and let $t_1,\dots ,t_n$ be the terms occurring in the $\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{v}\mathsf{e}$ -steps of $T$ . If $\mathit{F}\mathit{P}{⊩}_c^{\mathit{T}\mathit{I}}\delta (\{t_1,\dots ,t_n\})$ then $\delta (x)\in {\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x(\{t_1,\dots ,t_n\})$ .

This lemma essentially says that if there is an abstraction substitution that will instantiate a set of received terms to terms that the intruder can actually derive, then the application of that abstraction substitution to any variable $x$ will indeed be one of the abstract values that ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_x$ calculates.

The following examples illustrate the idea:

Example 13

We here return to Example 11 and now apply the ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_X$ and ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_Y$ functions: We see that this corresponds to the choices for $X$ and $Y$ that we saw in Example 11. As in that example, this leads to two possible abstraction substitutions, namely and .

Example 14

We here return to Example 12 and now apply the ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_X$ and ${\mathsf{r}\mathsf{c}\mathsf{v}\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}\mathsf{r}\mathsf{s}}_Y$ functions: We see that this corresponds to the choices for $X$ and $Y$ that we saw in Example 12. As in that example, this leads to four possible abstraction substitutions, namely , , , and . We see again here that an overapproximation is happening because actually only the first two abstraction substitutions will generate terms represented by the fixed point.

We combine the techniques described from Section 6 up to here into an implementation of the coverage check that we denote the Receive coverage check.

This section demonstrates how the Isabelle formalization allows for describing different strategies in order to prove to Isabelle that the computed fixed point covers the transactions. Indeed, as part of such arguments, we show in Isabelle that the strategy is sound, such as in Lemma 7. Proving such theorems means that we do not need to be suspicious of implementation bugs even if a strategy gives significant improvements on some examples. The strategies can often negotiate an efficient solution between different extremes. For instance, not considering the messages the intruder needs to produce (F1) leads to an unnecessarily large set of abstractions to consider, while computing the precise set of abstractions that satisfy (F1) would often waste a lot of time on an optimization that is just not worth it (or it may even be undecidable). While we here used our intuition and experience with examples, in general, an extensive study of different variants on a larger benchmark suite could allow for further improvements.

7. Experimental results

In this section, we discuss empirical results. We start by introducing our main benchmark suite for individual protocols and discussing the performance of our tool, PSPSP, on this benchmark suite. Finally, we discuss an example of a composed protocol.

7.1. Our benchmark suite

We evaluated our tool, PSPSP, using the following protocols (see Table 2): The first group of protocols is based on a keyserver. The example KS_ $h$ _ $d$ is our keyserver running example for $h$ honest agents and $d$ dishonest agents. [We verify here a generalized version of the keyserver example (as compared to the running example): we include dishonest agents who can participate in the protocol. This also requires that agents maintain a set of deleted keys, because otherwise the abstraction $\mathrm{\varnothing }$ leads to false attacks.] The example KS_Comp_ $h$ _ $d$ with $h$ honest agents and $d$ dishonest agents is inspired by Hess et al. ¹³ where another keyserver protocol—named KS2_ $h$ _ $d$ here—runs in parallel on the same network and where databases are shared between the protocols.

Table 2.

Runtime measurements (time format: hh:mm:ss) experiments that took longer than 12 hours are marked with “-- : -- : --.”

						Verification
	Initialization		Fixed point			Safe check		NBE check		Eval check
Protocol	Transl.	Setup	Comp.	|FP|	|TI|	Default	Receive	Default	Receive	Default	Receive	Heuristic
KS_ $2$ _ $1$	00:00:03	00:00:27	00:00:03	13	28	00:00:28	00:01:07	00:00:19	00:00:15	00:00:14	00:00:12	00:00:46
KS_ $3$ _ $1$	00:00:04	00:00:26	00:00:03	17	41	00:00:40	00:03:02	00:00:21	00:00:18	00:00:16	00:00:12	00:01:01
KS_ $4$ _ $1$	00:00:04	00:00:26	00:00:03	21	54	00:01:29	00:07:58	00:00:20	00:00:26	00:00:14	00:00:13	00:01:52
KS2_ $2$ _ $1$	00:00:04	00:00:27	00:00:03	11	5	00:00:30	00:00:29	00:00:17	00:00:15	00:00:13	00:00:13	00:00:46
KS2_ $3$ _ $1$	00:00:04	00:00:28	00:00:04	14	7	00:00:43	00:00:40	00:00:19	00:00:16	00:00:16	00:00:13	00:01:00
KS2_ $4$ _ $1$	00:00:04	00:00:28	00:00:03	17	9	00:00:55	00:01:05	00:00:20	00:00:18	00:00:15	00:00:15	00:01:14
KS_Comp_ $2$ _ $1$	00:00:05	00:00:27	00:00:04	22	108	00:07:35	00:47:07	00:00:50	00:01:52	00:00:16	00:00:14	00:07:49
KS_Comp_ $3$ _ $1$	00:00:05	00:00:27	00:00:06	29	156	00:33:57	03:16:32	00:02:13	00:06:13	00:00:19	00:00:14	00:33:21
KS_Comp_ $4$ _ $1$	00:00:05	00:00:25	00:00:10	36	204	01:44:22	10:18:07	00:06:08	00:16:19	00:00:26	00:00:16	01:45:54
NSLclassic	00:00:03	00:00:26	00:00:03	35	6	00:03:15	00:03:06	00:00:20	00:00:18	00:00:32	00:00:14	00:03:28
NSPKclassic	00:00:04	00:00:28	00:00:03	16	6	attack	attack	attack	attack	attack	attack	attack
PKCS#11_3	00:00:06	00:00:36	00:00:08	8	4	attack	attack	attack	attack	attack	attack	attack
PKCS#11_7	00:00:06	00:00:37	00:00:26	13	30	attack	attack	attack	attack	attack	attack	attack
PKCS#11_9	00:00:05	00:00:37	00:00:12	40	20	attack	attack	attack	attack	attack	attack	attack
TLS12_auth_simp	00:00:08	00:00:34	00:00:07	40	20	-- : -- : --	04:23:08	01:31:14	00:03:05	00:00:38	00:00:30	04:30:37
Logos	00:00:07	00:00:37	00:00:14	48	31	-- : -- : --	11:01:55	01:38:56	00:36:29	00:01:23	00:01:07	11:13:23
TLS12_SSO	00:00:13	00:00:26	00:15:25	359	35	-- : -- : --	-- : -- : --	02:58:21	04:49:35	00:00:37	00:00:23	-- : -- : --

The next groups are NSLclassic and NSPKclassic, which are based on the NSL and Needham–Schroeder protocol specifications shipped with AIF- $\omega$ . ¹⁵

Then, we have several scenarios of the “PKCS#11” model that is distributed with AIF- $\omega$ . ¹⁵ Scenarios 3 and 7 (PKCS#11_3 and PKCS#11_7) are examples of another flavor of stateful protocols, namely security tokens that can store keys and perform encryption and decryption, and with which the intruder can interact through an application programming interface (API). Generally, modeling such tokens and their APIs works quite well with the set-based abstraction. There is a third scenario (PKCS#11_9) that is marked as correct in the AIF- $\omega$ distribution, but that is actually due to a mistake that our attempt to verify it in Isabelle has revealed. We discuss this example in more detail in the Appendix. This illustrates our main point that there can be surprises when one tries to verify in Isabelle the results of automated tools.

With TLS12_auth_simp, we have looked at one protocol that has been inspired by a practical protocol, that is, transport layer security (TLS) 1.2. For our experiments, we simplified the protocol by modeling only one variant of the flow and also simplifying the hashing.

Finally, we modeled a protocol developed by the Danish company Logos and a single sign-on protocol (TLS12_SSO) that composes the TLS key exchange with a custom SSO protocol. We will discuss TLS12_SSO in Section 7.3 and the industrial case study (Logos) in Section 9.

7.2. Evaluation of our benchmark suite

Table 2 shows the fixed point sizes of various example protocols together with measurements of the elapsed real time it takes to generate and verify the Isabelle specifications. All experiments have been conducted on a shared Linux server with an Intel Xeon E5-2640 CPU and 96 GB main memory using PSPSP based on Isabelle 2024. PSPSP provides an option to measure the elapsed time (wall-clock) required for executing individual “top-level” commands (e.g., protocol_security_proof, see Section 8). We only report the times that are specific to the individual protocols using a “pre-compiled” session that contains our generic protocol translator as well as the protocol-independent formalizations and proofs. First, we report the time for translating the protocol specifications into Isabelle/HOL (translation), the time for showing that the given protocol is an instance of the formal protocol model (setup), and the time for computing the fixed point and its size. [This includes the time for parsing the trac specification and, more importantly, the generation of the conservative HOL definitions.] In the next six columns, we report the run-time of four different strategies for the security proof that we will explain in the following. The last column reports the run-time of a heuristic that aims to select the fasted strategy automatically. We will explain the details of this heuristic later.

In the safe configuration, all proof steps are checked by Isabelle’s LCF-style kernel; internally, this makes use of the simplifier configuration called code-simp of Isabelle’s simplifier. NBE employs normalization by evaluation, a technique that uses a partially symbolic evaluation approach that, to a limited extent, relies on Isabelle’s code generator. Finally, eval is an approach that directly employs the code generator and internally uses the proof method eval. In general, the configurations NBE and eval require the user to trust the code generator. From a correctness perspective, the main difference is that the configuration of the code generator used by NBE is very small and cannot be changed by Isabelle users. Hence, this configuration can be easily audited manually and, moreover, is thoroughly tested. In contrast, eval uses a user-configurable configuration of the code generator and, hence, is hard to audit, and any theory our work depends on could, potentially, have modified this configuration. While Isabelle’s code generator is thoroughly tested, it is not formally verified. While, at the end, it is up to the user to decide which approach to use, we consider NBE to be a trustworthy configuration. [Interested users should consult ²⁹ to understand the software stack that needs to be trusted for each configuration.] Furthermore, a pragmatic approach is to use eval during the development (specification) of the protocol and only after no attacks are found, switching to NBE or safe for a higher level of trust.

For the first three strategies, we report the time of our default version of the coverage check (Default), which implements the improvements described in Section 6 up to and including Section 6.2. We also report the time of our alternative version of the coverage check (Receive), which also implements these improvements in addition to the further restriction of the number of abstraction substitutions described in Section 6.3. There is a fourth strategy, called Heuristic, that automatically selects the faster coverage check in the configuration Safe. We will explain its details at the end of this section.

For all our examples, verification times, using the eval check (i.e., making full use of Isabelle’s code generator), are at most 1 1/2 minutes. [We do not report runtimes for protocols with an attack. After the fixed point computation, checking for an attack takes less than a second, as we only need to check for the presence of the $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ constant. We will discuss the presentation of attack traces for such protocols in Section 8.] This makes this configuration ideal for interactive development, for example, while refining a protocol specification. In contrast, the verification using only Isabelle’s simplifier can take more than 12 hours (we record runtimes of more than 12 hours as $--:--:--$ ) for our example protocols. Thus, in most cases, this configuration will be used in “batch-mode” after the protocol has been checked using the configuration employing the code generator. For most protocols, NBE provides a good middle ground, bringing the verification times down to under a minute for most examples, and below 40 minutes for all examples using the fastest variant of the coverage check.

Furthermore, the Receive coverage check introduced in Section 6.3 significantly reduces the safe verification time for TLS12_auth_simp and Logos in safe mode from over 12 hours to around 4 1/2 (TLS12_auth_simp) and around 11 hours (Logos). For NBE, it reduces the runtime for both protocols from around 1 1/2 hours to 3 minutes (TLS12_auth_simp), respectively, and around 40 minutes (Logos). For the configuration fully relying on code generation (eval), the improvements are minor.

Comparing the runtime of the two coverage checks for all examples shows that the relative runtime behavior of the two coverage checks seems not to depend on the simplification strategy (i.e., eval, NBE, and safe). This motivated us to implement a heuristic that, first, runs the security proof for NBE for both coverage checks in parallel, measures their runtime, and then runs the Safe strategy using the coverage check that, for the given protocol, was faster for NBE. We have chosen NBE as the basis, as the runtimes for eval for both coverage checks are often very similar and, hence, cannot provide a solid base measurement. In theory, this heuristic should show a runtime behavior that roughly is the maximum of the runtime of the two coverage checks for NBE, plus the runtime for the faster coverage check in a safe configuration. Our measurements (last column in Table 2) do confirm this behavior for our example protocols. This makes our heuristic a reliable way for automatically selecting the faster coverage check.

Finally, as mentioned at the beginning of this section, we report the elapsed time in Table 2 and not the total CPU time. On average, the security proof using the default coverage check can run certain parts in parallel, resulting (in our benchmark suite) on an average speedup of 2.5. The Receive coverage check cannot be parallelized that well (having an average speedup of 1.3).

7.3. An example of protocol composition

Table 3 shows the runtimes for an example of a protocol composition, implementing a TLS-based single sign-on (TLS12_SSO). Note that the format of the table differs from Table 2: we report the runtimes for the three different verification checks (safe, NBE, and eval) on three separate lines. For each of these checks, we report the running time for the initialization and the fixed point computation (as well as its size) for each subprotocol (i.e., TLS and SSO). These aspects are the same for all three verification checks, as their implementation does not make use of the optimizations provided by the code generator. Next, we report the runtimes (as in Table 2 for both coverage checks) for the individual verification of the two subprotocols. The final column reports the runtime for the proof that the composition of the two sub-protocols is secure. Here, “-- : -- : --” denotes that the check takes more than 12 hours. Notably, the security verification of the individual protocols takes significantly longer than the proof that the composition of the two protocols is secure. For instance, the security proof for SSO takes several hours using the NBE check (the safe check takes more than 12 hours), while the proof that the composition of the two protocols (TLS and SSO) is secure only takes a few seconds.

Table 3.

Runtime measurements (time format: hh:mm:ss) for the composed protocol TLS12_SSO.

									Verification
	Initialization		Fixed point (TLS)			Fixed point (SSO)			TLS		SSO
Check	Trans.	Setup	Comp.	|FP|	|TI|	Comp.	|FP|	|TI|	Default	Receive	Default	Receive	Composition
Safe check	00:00:13	00:00:30	00:00:05	25	16	00:07:57	202	38	00:04:57	00:10:24	-- : -- : --	-- : -- : --	-- : -- : --
NBE check	00:00:13	00:00:30	00:00:05	25	16	00:07:57	202	38	00:00:41	00:00:46	02:18:27	01:59:03	00:00:12
Eval check	00:00:13	00:00:30	00:00:05	25	16	00:07:57	202	38	00:00:20	00:00:15	00:00:18	00:00:10	00:00:04

TLS: transport layer security; SSO: Single-Sign-On.

More importantly, the total runtime of the fastest NBE configuration is roughly two hours, compared to 3 h 15 min 25 s for directly verifying the monolithic TLS12_SSO protocol model using the default coverage check (cf. Table 2). The compositional verification takes only 2 h 8 min 41 s in total using the default coverage check for the TLS component and the receive coverage check for the SSO component (see Table 3). [Using the receive coverage check for both components increases the total runtime only by 5 s.]

Finally, note that the TLS protocol used in this composition case study focuses only on the core of TLS: the key exchange. In contrast, TLS12_auth_simp in Table 2 also includes the password authentication and the transmission of some dummy data. This explains the difference in runtimes (and fixed point sizes) between these two versions of TLS.

8. Isabelle/PSPSP

We implemented our approach on top of the Isabelle framework, ³⁰ resulting in a tool called Isabelle/PSPSP, ¹⁸ which is now part of the AFP [As part of the AFP, PSPSP will be maintained and, for instance, ported to the latest official release of Isabelle.] This includes a formalization of the protocol model in Isabelle/HOL, a data type package that provides a domain-specific language (called trac) for specifying security protocols, and fully automated proof support.

8.1. The architecture of Isabelle/PSPSP

For our implementation of Isabelle/PSPSP, we make use of the fact that Isabelle is not only an interactive theorem prover; it also provides an extensible framework for developing formal methods tools. ³¹

Figure 1 shows an overview of the Isabelle architecture, highlighting in green the additions provided by Isabelle/PSPSP. In particular:

Protocol formalization: PSPSP is built on, and re-uses, our stateful protocol formalization (and its typing results) formalized in Isabelle/HOL. This part is available as a stand-alone AFP entry, ³² consisting of $\sim 20,000$ lines of code. The formalization presented in this paper, formalizing the presented method for the automated verification of security protocols, adds another $25,000$ lines of code. ¹⁸ Note that these formalizations (proofs and definitions) are reusable, that is, independent of any concrete security protocol.

Automated proof support (PSPSP methods): We developed several proof methods using both Isabelle’s high-level proof development language Eisbach ³³ and the Isabelle/ML interface. Isabelle/ML is Isabelle’s programming API that allows one to extend Isabelle using the SML ³⁴ programming language. We use this, in particular, for computing fixed point that builds the backbone of our automation.

Support for trac: To improve the user-friendliness of PSPSP, we defined a trace-based specification language for security protocols, called trac. By supporting trac as input language, we allow users to use PSPSP without the need to understand all the details of our protocol formalization. Actually, users of PSPSP mostly need to understand trac, and our new Isabelle commands for verifying security protocols. Supporting trac requires a parser for trac (implemented in Isabelle/ML) and implementing an encoder (or datatype package) that translates trac into the corresponding HOL definitions. Furthermore, the trac datatype package also proves automatically a number of basic properties that are used within the actual security proof.

It is noteworthy that all our additions have been implemented in a logically safe way, that is, a bug in our implementation cannot result in an insecure protocol being successfully verified: any bug could only result in PSPSP not being able to verify a secure protocol.

Figure 1.

The system architecture of Isabelle and Isabelle/PSPSP.

8.2. Isabelle/PSPSP—A guided tour

Figure 2 shows the Isabelle IDE (called Isabelle/jEdit). The upper part of the window is the input area that works similarly to a programming IDE, that is, supporting auto completion, syntax highlighting, and automated proof generation and interactive proof development. The lower part shows the current output (response) with respect to the cursor position. In more detail, Figure 2 shows the specification and the fully automated verification of a toy keyserver protocol:

The protocol is specified using the domain-specific language trac that, for example, could also be used by a security protocol model checker (lines 8–58). Our implementation automatically translates this specification into a family of formal HOL definitions. Moreover, basic properties of these definitions are also already proven automatically (i.e., without any user interaction): for this simple example, already over 350 theorems are automatically generated.

Next (line 61), our implementation automatically shows that the protocol satisfies the requirement of our model (technically, this is done by instantiating several Isabelle locales, resulting in another 1750 theorems “for free”).

In line 62, we compute the fixed point. We can use Isabelle’s value command (line 74) to inspect its size.

After these steps, all definitions and auxiliary lemmas for the security proof are available. We can now perform a fully automated proof (line 64). The top-level command protocol_security_proof proves automatically a theorem showing the security of the defined protocol. This successful proof took $\sim 48$  s (see lower part of the Isabelle/jEdit window).

Figure 2.

Using Isabelle/PSPSP for verifying a keyserver protocol (KS2_ $2$ _ $1$ ).

Moreover, for the security proofs, we have also manual variants (e.g., manual_protocol_setup, manual_protocol_security_proof, or manual_protocol_composition_proof) of the automated proof commands that only create a proof obligation (i.e., establish the proof state) allowing the user to do an interactive proof utilizing the full power of Isabelle, instead of using the automated proof methods provided by us. [The commands still allow the user to copy the automated proof script, using “point-and-click” in the same way as the default sledgehammer tool, into the theory file.] This is potentially useful for introducing protocol-specific optimizations or for inspecting what the automated proof methods do.

In case of an insecure protocol, that is, the fixed point containing the $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ constant, Isabelle/PSPSP can support the protocol developer with an attack trace: optionally, while computing the fixed point, the computed traces are bound to a logical constant, which can then be printed in a user-friendly way. Figure 3 shows an example for the protocol PKCS#11_3: the proof that the $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ constant is contained in the fixed point (line 95) usually takes only a few seconds. The Isar top-level command print_attack_trace (line 98) then prints an attack trace (lower part of the window in Figure 3) showing the steps executed until an attack event is created.

Figure 3.

An example attack trace (for the protocol PKCS#11_3).

8.3. Compositionality

PSPSP is part of a larger Isabelle infrastructure for security protocols that also allows for compositionality, ¹ that is, for a result of the form: if two or more protocols are secure in isolation and satisfy certain requirements, then also their composition is secure, that is, when they run in parallel sharing the same network and even some sets. Especially the support for shared sets allows us to consider also complex interactions between two protocols, for instance, where one protocol negotiates keys and another protocol uses them.

The compositionality framework uses the same specification language (trac) as PSPSP. One can thus specify a set of component protocols, use PSPSP to prove the security of each of them in isolation, and use the compositionality framework to check that they fulfill the requirements for compositionality and then obtain an Isabelle proof that the composed system is secure.

As an example, we have modeled in Hess et al., ¹ a composition of TLS 1.2 and security assertion markup language (SAML) Single-Sign-On (SSO): TLS establishes a secure channel between a client and a server where the client is not yet authenticated. SSO then uses such a channel between a client and the identity provider to first authenticate the client to the identity provider (e.g., using a password); the identity provider then provides a credential for the client that the client can use to authenticate another TLS channel with a relying party. More in detail, the TLS protocol stores any exchanged keys that a client $A$ has negotiated with server $B$ in a set $\mathsf{c}\mathsf{l}\mathsf{i}\mathsf{e}\mathsf{n}\mathsf{t}\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(A,B)$ on the client side, and in the set $\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}\mathsf{K}\mathsf{e}\mathsf{y}\mathsf{s}(B)$ on the server side. The latter set of keys is only parameterized over the agent name $B$ , since $A$ is not authenticated. Each of these sets reflects the local point of view of each agent, and it is part of the verification that, for instance, the intruder does not find out a key between two honest agents $A$ and $B$ . Finally, the SSO protocol can just retrieve and use these keys, both to authenticate the connection between client and server, as well as between client and identity provider (where the password is transmitted). The composed protocol is specified in the trac specification language (see Figure 4, until line 299). We compute the $\mathit{S}\mathit{M}\mathit{P}$ common between both protocols (lines 305–309, see Hess et al. ¹ for more details) and fixed points (lines 312 and 313) for both protocols “in isolation.” These are used to prove the security of each of the two subprotocols (lines 315–318). Then we prove the security of the composition: we compute the shared secrets (line 321) and then use an automated proof method for the protocol composition proof (lines 323–237). Finally, we show the security of the composition (lines 329—340) with a simple proof “by auto.”

Figure 4.

Using Isabelle/PSPSP for verifying the composition of TLS 1.2 and SAML. TLS: transport layer security; SAML: security assertion markup language.

Note that the run time (recall Tables 2 and 3) for the TLS component of the composition is much smaller than the runtime of TLS12_auth_simp, because it is purely the key-exchange while all authentication and data-transmission is “outsourced” to the SSO protocol. Thus, in general, verification can be improved by using compositional reasoning, if one can split a complex system into smaller components.

The compositionality framework supports strictly more protocols than PSPSP; most importantly, it allows for composed messages in sets. In these cases, one cannot use PSPSP to verify the respective components, but of course, one can also consider compositions where a subset of the components is proved by PSPSP and the others are verified manually.

9. Case study: Logos

We had the opportunity to use PSPSP to formally verify a protocol by the Danish company Logos. This protocol stems from the area of reader terminals for a travel card solution, namely, to establish a secure connection between a terminal and the Logos server. The particular challenge here is that this should work after a terminal has been in storage for years and all public keys of the servers have been updated in the meantime; we do want to model the possibility that an intruder obtains old private keys—after all that is the reason for updating them regularly. Such a protocol, even though its messages are fairly simple, can be a challenge for verification tools as it requires mutable long-term states at its core. With some simplifications, we have built a model in PSPSP and found a security flaw. We then verified the protocol with PSPSP under a minor modification. Logos has applied this modification and has thus an Isabelle-verified product, one might say, although this should of course be taken with a grain of salt, given that we only verified a simplified model of the protocol (and in a black-box model of cryptography). The protocol is summarized in Figure 5, and we discuss it together with the PSPSP model of every step in the following.

Figure 5.

The Logos system in Alice-and-Bob notation.

9.1. Epochs

The abstract interpretation approach of PSPSP was originally inspired by ProVerif; both approaches essentially discard the notion of time to arrive at an overapproximation of everything that the intruder can ever know without the normal state explosion and restriction to bounded sessions. That, however, makes it challenging to model any aspect of time, such as injective agreement. However, the only aspect of time that we really need in the model of the Logos protocols is a distinction between past and present events, for example, distinguish nonces that were generated a long time ago from nonces that are fresh. More precisely, we divide the timeline into two epochs $\mathsf{e}\mathsf{p}\mathsf{o}\mathsf{c}\mathsf{h}=\{\mathsf{e}\mathsf{1},\mathsf{e}\mathsf{2}\}$ . We do not care about the order of events in each epoch: as a notion of time, the model only distinguishes between events that happened in $\mathsf{e}\mathsf{1}$ and those that happened in $\mathsf{e}\mathsf{2}$ . In this model, all events of $\mathsf{e}\mathsf{1}$ happen before all events of $\mathsf{e}\mathsf{2}$ .

9.2. Key generation and revocation

First, we define that the intruder can generate public–private key pairs. Note that when no epochs are mentioned, the rule can uniformly be applied in all epochs: The Logos server has a public–private key pair that is updated regularly. [In fact, there are several kinds of keys for different purposes; for simplicity, we consider only one kind of key.] We model this in PSPSP by the following two rules that can be applied in either epoch $E$ : Disregarding the epochs briefly, this simply means that the server can at every time point generate a new public–private key pair (publishing the public key) and at any time revoke one. (Like in the keyserver examples before, the knowledge of the corresponding private key $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{P}\mathit{K}\mathit{L})$ is implicit for honest agents like the Logos server.) In this model, the server may thus have any number of public keys at the same time; this is just an overapproximation. The fact that the set $\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}\mathsf{\_}\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{s}$ is parameterized over the epoch $E$ means that no key generated in the first epoch is available in the second and vice versa. Thus, the “cut” between the two epochs coincides with a key update, reflecting our intention that $\mathsf{e}\mathsf{1}$ represents events that happened longer in the past while $\mathsf{e}\mathsf{2}$ represents recent events.

When a batch of terminals is manufactured, each gets a unique hardware-id in $\mathsf{h}\mathsf{w}\mathsf{\_}\mathsf{i}\mathsf{d}$ . Since some sets will be parameterized over this hardware id, we need to give a finite enumeration, and we limit ourselves to two hardware-ids $\mathsf{h}\mathsf{w}\mathsf{\_}\mathsf{i}\mathsf{d}=\{\mathsf{t}\mathsf{1},\mathsf{t}\mathsf{2}\}$ . During manufacturing, all terminals of a batch have the same public–private key pair, called the batch key, which is registered also with the Logos server, so the terminals can authenticate themselves as legitimate terminals to the Logos server later. We assume here that batch generation happens only in epoch $\mathsf{e}\mathsf{1}$ , because with $\mathsf{e}\mathsf{2}$ we want to model only what happens long after manufacture. Before terminals can be manufactured, we first need to create a public/private key pair, and like for the Logos server, we allow for arbitrary such events and revocation at any point as an overapproximation of several manufacturing batches that can happen in $\mathsf{e}\mathsf{1}$ : Again, the corresponding private key $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{P}\mathit{K}\mathit{B}\mathit{a}\mathit{t}\mathit{c}\mathit{h})$ is implicit, since only the manufactured terminals would have it and are assumed to be honest. When manufactured, the terminals also have the current public key of the Logos server. This is the starting state for the Logos protocol of Figure 5.

9.3. The bootstrap protocol

Each terminal is required to run a bootstrap protocol with the server in order to establish an individual key $BKP$ . This must happen within 30 days after manufacture. We assume here that this is still within epoch $\mathsf{e}\mathsf{1}$ . (Failure to run it is modeled here by the fact that the batch and/or server key can be revoked, and thus the terminal cannot do any transactions.) In the bootstrap protocol, the terminal creates a fresh key pair, consisting of the bootstrap public key $\mathit{B}\mathit{K}\mathit{P}$ , and the corresponding private key $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{B}\mathit{K}\mathit{P})$ . For now, even the public key $\mathit{B}\mathit{K}\mathit{P}$ is kept secret between the terminal and server. This later allows the server to send messages to the terminal that can only come from the server. This is an unusual way to employ a public key; a more conventional solution would probably be a shared symmetric key instead. However, this is how the protocol works, and we have not found a principal security problem with it (other than the attack reported below that is independent of this). This rule corresponds to sending the first message in Figure 5. Here we have modeled that the terminal knows the batch key pair and the public key of the Logos server simply by looking them up in the respective sets. We have drastically simplified the bilaterally authenticated TLS session between terminal and server, by encryption of the message with the public key $\mathit{P}\mathit{K}\mathit{L}$ of the server and signing by the private key of the entire batch of terminals $\mathsf{i}\mathsf{n}\mathsf{v}(\mathit{P}\mathit{K}\mathit{B}\mathit{a}\mathit{t}\mathit{c}\mathit{h})$ . The terminal remembers its bootstrap key $\mathit{B}\mathit{K}\mathit{P}$ (and implicitly the private key) in the set $\mathsf{b}\mathsf{k}\mathsf{p}(T)$ . The server receives the public key $\mathit{B}\mathit{K}\mathit{P}$ in the following transaction and stores it in $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{s}(T)$ : This corresponds to the reception of the first message in Figure 5. The server expects a message that is encrypted with its current public key $\mathit{P}\mathit{K}\mathit{L}$ (and thus discards the message if decryption with the current private key failed), and then checks that the content is a signature that verifies with (one of) the current batch public keys $\mathit{P}\mathit{K}\mathit{B}\mathit{a}\mathit{t}\mathit{c}\mathit{h}$ (and discard the message if signature verification fails). The signed message is expected to be a pair where the first is interpreted as a hardware-id $T$ and the second as the bootstrap public key $\mathit{B}\mathit{K}\mathit{P}$ which the server stores in the $\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{s}(T)$ , so that later a secure connection with $T$ can be established using $\mathit{B}\mathit{K}\mathit{P}$ . Note again that this bootstrap protocol can only be executed in epoch $\mathsf{e}\mathsf{1}$ as demanded by the parameters of the server and batch key sets, but it can happen for arbitrarily many batches and updates of the server keys in $\mathsf{e}\mathsf{1}$ .

9.4. The truststore protocol

The second part of the Logos protocol, in Figure 5 separated by the dotted lines, is the truststore protocol. This protocol may be executed by a terminal after it was many years in storage. This is possible in both epochs. To initiate, the terminal sends its unique hardware ID and a fresh nonce $N$ : For simplicity, we omit that this is also done via TLS: since in general neither the terminal nor the Logos server can verify the certificate of the other, this is not much better than plaintext, and so we do not bother with modeling TLS here. Also, the nonce $N$ is inserted into an epoch-specific set, in order to express the property that the terminal would not accept an answer in epoch $\mathsf{e}\mathsf{2}$ with a nonce it has generated in epoch $\mathsf{e}\mathsf{1}$ .

The server now receives the request, looks up the $\mathit{B}\mathit{K}\mathit{P}$ of the claimed $T$ , and constructs a so-called truststore message, that is, a message with the current public key of the Logos server that the terminal can verify. To this end, the server generates a new shared key $\mathit{S}\mathit{K}$ , which is inserted into a set of current shared keys $\mathsf{s}\mathsf{k}\mathsf{\_}\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{s}$ , encrypts it with the $\mathit{B}\mathit{K}\mathit{P}$ of the terminal, and then authenticates the trust-store by MACing it (and the nonce $N$ ) with the $\mathit{S}\mathit{K}$ : Here, the unary function $\mathsf{s}\mathsf{k}$ is just a format to distinguish this message from other kinds of encrypted messages. This is the version for the case that the transaction is executed in $\mathsf{e}\mathsf{1}$ . Here we actually require that $N\mathsf{n}\mathsf{o}\mathsf{t}\mathsf{i}\mathsf{n}\mathsf{n}\mathsf{o}\mathsf{n}\mathsf{c}\mathsf{e}(\mathsf{e}\mathsf{2})$ . This does not correspond to a check that the server does, but our model that everything in epoch $\mathsf{e}\mathsf{1}$ happens before $\mathsf{e}\mathsf{2}$ , and this constraint reflects that $N$ cannot come from the future.

When this transaction is happening, however, in $\mathsf{e}\mathsf{2}$ , we cannot exclude that the nonce was generated in $\mathsf{e}\mathsf{1}$ (e.g., the intruder replaying an old request). Thus, we have a variant of the previous rule for $\mathsf{e}\mathsf{2}$ : We have also in both rules the insertion of $\mathit{P}\mathit{K}$ into the set $\mathsf{w}\mathsf{i}\mathsf{t}\mathsf{n}\mathsf{e}\mathsf{s}\mathsf{s}(T,\cdot )$ . This is just for formulating the authentication goal below.

To conclude the truststore protocol, the terminal receives the truststore message from the server: Actually, we do not model here further the store of the terminal, but we have authentication goals as discussed below.

9.5. Goals

We formulate several goals by specifying again what would be an attack. First, for secrecy goals: the $\mathit{B}\mathit{K}\mathit{P}$ (both public and private key) are secrets, and so is the $\mathit{S}\mathit{K}$ and the private key of the terminal batch: For the receiving of the truststore, we have that it is an attack (noninjective agreement) if the terminal accepts a truststore $\mathit{P}\mathit{K}$ that was not sent like this from the Logos server (in any epoch): The injective aspect now needs the formulation with epochs: it is an attack if the terminal accepts a message in epoch $\mathsf{e}\mathsf{2}$ that the server did not send in epoch $\mathsf{e}\mathsf{2}$ : Together with the $\mathsf{n}\mathsf{o}\mathsf{n}\mathsf{i}\mathsf{n}\mathsf{j}\mathsf{a}\mathsf{u}\mathsf{t}\mathsf{h}\mathsf{\_}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}\mathsf{\_}\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{s}$ , we have a goal close to injective agreement. Standard injective agreement ³⁵ in this case means that, on top of the noninjective agreement, it is an attack if the terminal accepts $\mathit{P}\mathit{K}$ more often than it was sent by the server. In PSPSP, we would express this by using another set $\mathsf{r}\mathsf{e}\mathsf{q}\mathsf{u}\mathsf{e}\mathsf{s}\mathsf{t}(T,E)$ and when the terminal accepts a $\mathit{P}\mathit{K}$ that is already in the set $\mathsf{r}\mathsf{e}\mathsf{q}\mathsf{u}\mathsf{e}\mathsf{s}\mathsf{t}(T,E)$ , then it is an attack; otherwise, it is added to the set $\mathsf{r}\mathsf{e}\mathsf{q}\mathsf{u}\mathsf{e}\mathsf{s}\mathsf{t}(T,E)$ . Thus, this means it is an attack if the same $\mathit{P}\mathit{K}$ is accepted more than once. This way of defining the goal is not suitable in this case, because during the validity of a single $\mathit{P}\mathit{K}$ it is allowed to run the truststore protocol several times, and then it is correct that the terminal in each run receives the same value $\mathit{P}\mathit{K}$ . It is in fact a limitation of our abstraction approach that we cannot really define the existence of an injective function between events.

The formulation with epochs solves this: it is an attack if the terminal accepts a value $\mathit{P}\mathit{K}$ in epoch $\mathsf{e}\mathsf{2}$ that was not sent by the server in epoch $\mathsf{e}\mathsf{2}$ .

9.6. The attack

Observe that in the protocol in Figure 5, we have highlighted the nonce $N$ in red. This is in fact the fixed version; the original version did not have this nonce. The goal $\mathsf{r}\mathsf{e}\mathsf{p}\mathsf{l}\mathsf{a}\mathsf{y}\mathsf{\_}\mathsf{s}\mathsf{e}\mathsf{r}\mathsf{v}\mathsf{e}\mathsf{r}\mathsf{\_}\mathsf{k}\mathsf{e}\mathsf{y}\mathsf{s}$ (without the constraint $N\in \mathsf{n}\mathsf{o}\mathsf{n}\mathsf{c}\mathsf{e}(\mathsf{e}\mathsf{2})$ ) is the one we found violated in the original protocol. The attack on the version without nonce $N$ is the following replay attack: a terminal gets manufactured, runs bootstrap, and sometime later it runs the truststore protocol with the intruder in the middle, who records the truststore message from the server. The terminal for some reason goes into storage and then later in epoch $\mathsf{e}\mathsf{2}$ it runs the truststore protocol again, where the intruder just acts as the Logos server and replies with the old truststore messages from $\mathsf{e}\mathsf{1}$ , so the terminal is made to accept the old Logos keys that are long revoked and possibly compromised by the intruder.

We note that this attack is not easy for the intruder to mount, but also not unrealistic, and invalidates exactly what the protocol should achieve, the reliable update of keys. The fix with the nonce is not very expensive, and in this version, all goals of the protocol are satisfied, including the subsequent server certification of new keys generated by the terminal, which we do not show here.

The PSPSP tool can verify this specification in about a minute with the eval strategy—see Table 2.

10. Conclusion and related work

The research into automated verification of security protocols resulted in a large number of tools (e.g., Blanchet, ⁶ Boichut et al., ³⁶ Chevalier and Vigneron, ³⁷ Basin et al., ³⁸ and Cremers ⁸ ). The implementation of these tools usually focuses on efficiency, often resulting in very involved verification algorithms. The question of the correctness of the implementation is not easy to answer and this is in fact one motivation for research in using LCF-style theorem provers for verifying protocols (e.g., Paulson, ² Bella, ³ Hess and Mödersheim ²³ Butin, ³⁹ Bella et al., ⁴⁰ and Bella et al. ¹⁹ ). While these works provide a high level of assurance into the correctness of the verification result, they are usually interactive,that is, the verification requires a lot of expertise and time.

This tradeoff between the trustworthiness of verification tools and the degree of automation inspired research of combining both approaches.^5,7,20 Goubault-Larrecq ⁵ considers a setting where the protocol and goal are given as a set $S$ of Horn clauses; the tool output is a set $S_{\mathrm{\infty }}$ of Horn clauses that are in some sense saturated and such that the protocol has an attack iff a contradiction is derivable. His tool is able to generate proof scripts that can be checked by Rocq ⁴¹ from $S_{\mathrm{\infty }}$ . Meier ⁷ developed Scyther-proof, ⁴² an extension to the backward-search used by Scyther, ⁸ which is able to generate proof scripts that can be checked by Isabelle/HOL. ⁴³ Brucker and Mödersheim ²⁰ integrate an external automated tool, OFMC, ³⁹ into Isabelle/HOL. OFMC generates a witness for the correctness of the protocol that is used within an automated proof tactic of Isabelle.

Our work generalizes on these existing approaches for automatically obtaining proofs in an LCF-style theorem prover, first and foremost by the support for stateful protocols and thus a significantly larger range of protocols—moving away from simple isolated sessions to distributed systems with databases, or devices that have a long-term storage.

We achieve this by employing the abstraction-based verification technique of AIF, ⁹ but with an important modification. The method of AIF produces a set of Horn clauses that is then analyzed with ProVerif ⁶ (or SPASS ⁴⁴ ), and the same holds true also for several similar methods for stateful protocol verification, namely StatVerif, ¹⁰ Set- $\pi$ , ¹⁶ AIF- $\omega$ , ¹⁵ and GSVerif. ¹¹ Note that a set of definite Horn clauses (i.e., Horn clauses with exactly one positive literal) in first-order predicate logic always has a trivial model, because one can simply interpret all predicates as true for all arguments. Thus, if we have modeled an attack by the truth of some predicate $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ , then there is trivially a model of the Horn clauses where $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ is true. Instead, one wants to check that $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ does not hold true in one particular model, namely the least model corresponding to the free algebra interpretation of terms and being true for the least number of ground predicates. This least model is uniquely defined in the case of Horn clauses. This is achieved in ProVerif (and SPASS) by checking whether the Horn clauses imply $\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{a}\mathsf{c}\mathsf{k}$ : If they do, then the attack predicate is true also in the free model. If they do not, that is, if the Horn clauses are consistent with the negation of the attack predicate, then the attack predicate is not true in all models, and in particular not in the least model. Thus, in a positive verification, the result from ProVerif is a consistent saturated set of Horn clauses. As first remarked by Goubault-Larrecq, ⁵ this is not a very promising basis for a proof, as one does not get a derivation of a formula (the way SPASS for instance is often used in combination with Isabelle) but rather a failure to conclude a proof goal. The only thing one can do to verify the result is to compute it again and compare the results. Therefore, Goubault-Larrecq ⁵ uses a different idea: showing that the Horn clauses and the negation of the attack predicate are consistent by trying to find some finite model and, if found, then using this finite model to generate a proof in Rocq that the Horn clauses are consistent with the negation of the attack predicate.

The limitation of Goubault-Larrecq ⁵ is that it checks the protocol proofs only on the Horn clause level, that is, after a nontrivial abstraction has been applied. In order to obtain Isabelle proofs for the original unabstracted stateful protocols, we use therefore another approach: rather than Horn clauses, we directly generate a fixed point of abstract facts that occur in any reachable state. This would in fact normally not terminate on most protocols due to the intruder deduction; however, we employ here the typing result we have formalized in Isabelle ¹⁴ to ensure that the fixed point is always finite, and our method is in fact guaranteed to terminate. This fixed point, if it does not contain the attack predicate, is the core of a correctness proof for the given protocol, namely as an invariant that the fixed point covers everything that can happen, and we essentially have to check that this invariant indeed is preserved by every transition rule of the protocol.

An interesting difference to previous approaches is that we do not rely on an external tool for the generation of the proof witness, but it is implemented within Isabelle itself. The reason is more of a practical than a principle matter: Computing the fixed point in Isabelle is actually not difficult and—thanks to Isabelle’s code generation—without much of a performance penalty; however, the fact that we do not rely on an external tool for the generation of the proof witness reduces the chances of synchronization and update problems (e.g., with new Isabelle versions). In fact, this work is part of the AFP (see https://www.isa-afp.org), a collection of Isabelle proofs that are kept up to date with each new version of Isabelle. This means that for each protocol that works in today’s version, it is highly likely that the proof works in future versions, because the proofs of all theorems of our (protocol-independent) Isabelle theory will be updated, and the fixed point and the checks about it do not have to change. Thus, we will also automatically benefit from all advances of Isabelle.

Another difference from previous approaches is that we do not directly generate proof scripts that Isabelle has to then check. Rather, we have a fixed set of (protocol-independent) theorems that imply that any protocol is secure if we have computed a fixed point representation that gives an upper bound of what (supposedly) can happen, and this representation passes a number of checks. These checks can either be done by generated code or entirely within Isabelle’s simplifier. Especially with the generated code, we have a substantial performance advantage, while using Isabelle’s simplifier gives the highest level of assurance since we only rely on the correctness of the Isabelle kernel. Many small practical advantages arise from the integration: We do not have an overhead of parsing proof scripts (which can be substantial for a larger fixed point). By using the internal API of Isabelle, we avoid the need for the Isabelle front-end parser to parse and type-check the fixed point (as we can directly generate a typed fixed point on the level of the abstract syntax tree). Parsing and type-checking (on the concrete syntax level) of large generated theories (as, e.g., those containing the generated fixed point) is, in fact, slow in Isabelle. ²⁰

Another point is that there exists a number of protocol verification methods and results that use slightly different models. Here we actually seamlessly integrate a verification method into a rich Isabelle theory of protocols without any semantic gaps: We provide here a method that is integrated into a large framework of Isabelle theories for protocols (approximately 25,000 lines of code), in particular a typing and compositionality result. This allows, for instance, to prove manually (in the typed model) the correctness of a protocol, use our automated method to prove the correctness of a different protocol, and then compose the proof to obtain the correctness of the composition in an untyped model. This seamless integration of results without semantic gaps between tools we considered as an important benefit of this approach. Even though many protocol models are not substantially different from each other, bridging over the small differences can be very hard to do, especially in a theorem prover that prevents one from glossing over details. Our deep integration into the existing formalization of security protocols in Isabelle ensures that the same protocol model (same semantics) is used—which would otherwise require additional work (e.g., to ensure that the semantics of the protocol specified in a tool such as Scyther-proof is faithfully represented in the generated Isabelle theory).

It is, in general, desirable to have proofs that are not only machine-checked but also human-readable. A reason is that, for instance, mistakes in the specification itself (e.g., a mistake in a sent message so that it cannot be received by anybody) may lead to trivial security proofs that a human may notice when trying to understand the proof. Here, Scyther-proof has the benefit that it produces very readable Isar-style proofs; in our case, there is, however, something that is also accessible: the fixed point that was computed is actually a high-level proof idea that is often quite readable as well (see, for instance, our running example). Moreover, the entire set of protocol-independent theorems is hand-written Isar-style proofs. [To avoid trivial security proofs, one may check if all transactions can be executed. While this is a useful technique, it is, unfortunately, in general not sufficient to avoid trivial security proofs. Consider, for example, a protocol with two variants of a transaction where a participant sends out an encrypted message. In one variant, it is sent by the attacker who also adds the plain text to his knowledge, and in another variant, it is sent by an honest agent only in the encrypted form. Now, say that only the attacker’s version is wrongly specified. In this case, all rules of the protocol may be executable except for the final attack rule, but the protocol is nonetheless trivially secure because the attacker is sending out a wrong message. Thus, checking for the executability of rules is not sufficient in general to discover trivial security proofs; however, inspecting the Scyther proofs or the fixed point may save the day.]

Furthermore, our work shares a lot of conceptual similarities with Tamarin, ¹² which can also be regarded as a kind of theorem prover. In fact, it was inspired by the mentioned work of Meier ⁴³ that generates Isabelle proofs from the Scyther tool, but Tamarin is not based on Isabelle and has instead a specialized proving environment based on a sound and complete constraint solver. This in principle shares two very nice features of Isabelle: that there are less limitations in what can be modeled, and that a user can supply proof ideas, but it also shares the disadvantage of Isabelle: that most of the interesting proofs are not automatic. There is work on improving this situation, that is, finding more proofs automatically for Tamarin. ⁴⁵ In contrast, PSPSP is, with respect to attacks on the abstract level, a complete decision procedure, assuming that users provide reasonable analysis rules that do not lead to nontermination. One concession in order to achieve this is indeed the abstraction. It ensures that protocols proved secure on the abstract level are also secure on the concrete level, but it may deem some protocols to be not secure on the abstract level due to a spurious attack. While we consider having this kind of decision procedure a selling point of PSPSP, it is worth remarking that, in practice, PSPSP may time out. Another main difference is that PSPSP is entirely formalized in Isabelle, and, as explained, does not rely on the correctness of any external tools. Also, the core of Isabelle is so well studied and used in so many projects that it can be considered more trustworthy than the specialized prover of Tamarin. On the other hand, Tamarin can support algebraic properties that we cannot at this point.

Finally, another approach that, such as Tamarin, is very much related to performing actual proofs of security protocols automatically and semiautomatically is CPSA.^46,47 Also here it might be possible to make a connection to a theorem prover, such as, Isabelle; however, the approach is even further away from our approach than Tamarin, because CPSA does not necessarily assume a closed world of transactions. Rather, it performs an enrich-by-need analysis, obtaining all ways to complete a particular scenario and thereby yielding the strongest security goals a given system would satisfy (even in the presence of other transactions). We believe it is even more challenging to integrate this kind of reasoning into a theorem prover such as Isabelle, but achievable. We like to investigate this as future work, as it could give interesting ways for an analyst to interact with the proving process and inject proof ideas.