figure a

1 Introduction

Cryptographic protocols ensure the security of communications. They are distributed programs that make use of cryptographic primitives, e.g. encryption, to ensure security properties, such as confidentiality or anonymity. Their correct design is quite a challenge as security is to be enforced in the presence of an arbitrary adversary that controls the communication network and may compromise participants. The use of symbolic verification techniques, in the line of the seminal work by Dolev and Yao [19], has proven its worth in discovering logical vulnerabilities or proving their absence.

Nowadays mature tools exist, e.g. [7, 10, 24] but mostly concentrate on trace properties, such as authentication and (weak forms of) confidentiality. Unfortunately many properties need to be expressed in terms of indistinguishability, modelled as behavioral equivalences in dedicated process calculi. Typically, a strong version of secrecy states that the adversary cannot distinguish the situation where a value \(v_1\), respectively \(v_2\), is used in place of a secret. Privacy properties, e.g., vote privacy, are also stated similarly [2, 4, 18].

In this paper we present the DeepSec prover (Deciding Equivalence Properties in Security protocols). The tool decides trace equivalence for cryptographic protocols that are specified in a dialect of the applied pi calculus [1]. DeepSec offers several advantages over existing tools, in terms of expressiveness, precision and efficiency: typically we do not restrict the use of private channels, allow else branches, and decide trace equivalence precisely, i.e., no approximations are applied. Cryptographic primitives are user specified by a set of subterm-convergent rewrite rules. The only restriction we make on protocol specifications is that we forbid unbounded replication, i.e. we restrict the analysis to a finite number of protocol sessions. This restriction is similar to that of several other tools and sufficient for decidability. Note that decidability is nevertheless non-trivial as the system under study is still infinite-state due to the active, arbitrary attacker participating to the protocol.

2 Description of the Tool

2.1 Example: The Helios Voting Protocol

An input of DeepSec defines the cryptographic primitives, the protocol and the security properties that are to be verified. Random numbers are abstracted by names (\(a,b,\ldots \)), cryptographic primitives by function symbols with arity (f / n) and messages by terms viewed as modus operandi to compute bitstring. For instance, the functions \(\mathtt {aenc}/3, \mathtt {pk}/1\) model randomized asymmetric encryption and public-key generation: term \(\mathtt {aenc(pk(k),r,m)}\) models the plain text \(\mathsf {m}\) encrypted with public key \(\mathtt {pk(k)}\) and randomness \(\mathtt {r}\). In DeepSec we write:

figure b

On the other hand, cryptographic destructors are specified by rewrite rules. For example asymmetric decryption (\(\mathtt {adec}\)) would be defined by

figure c

A plain text m can thus be retrieved from a cipher \(\mathtt {aenc(pk(k),r,m)}\) and the corresponding private key k. Such user-defined rewrite rules also allow us to describe more complex primitives such as a zero-knowledge proof (ZKP) asserting knowledge of the plaintext and randomness of a given ciphertext:

figure d

Although user-defined, the rewrite system is required by DeepSec to be subterm convergent, i.e., the right hand side is a subterm of the left hand side or a ground term in normal form. Support for tuples and projection is provided by default.

Protocol Specification. Honest participants in a protocol are modeled as processes. For instance, the process Voter(auth,id,v,pkE) describes a voter in the Helios voting protocol. The process has four arguments: an authenticated channel auth, the voter’s identifier id, its vote v and the public key of the tally pkE.

figure e

The voter first generates a random number r that will be used for encryption and ZKP. After that, she encrypts her vote and assigns it to the variable bal which is output on the channel auth. Finally, she outputs the ballot, id and the corresponding ZKP on the public channel c. All in all, the process VotingSystem(v1,v2) represents the complete voting scheme: two honest voters id1 and id2 respectively vote for v1 and v2; the process Tally collects the ballots, checks the ZKP and outputs the result of the election. The instances of the processes Voter and Tally are executed concurrently, modeled by the parallel operator |. Other operators supported by DeepSec include input on a channel (in(c,x); P), conditional (if u = v then P else Q) and non-deterministic choice (P + Q).

Security Properties. DeepSec focuses on properties modelled as trace equivalence, e.g. vote privacy [18] in the Helios protocol. We express it at indistinguishability of two instances of the protocol swapping the votes of two honest voters:

figure f

DeepSec checks whether an attacker, implicitly modelled by the notion of trace equivalence, cannot distinguish between these two instances. Note that all actions of dishonest voters can be seen as actions of this single attacker entity; thus only honest participants need to be specified in the input file.

2.2 The Underlying Theory

We give here a high-level overview of how DeepSec decides trace equivalence. Further intuition and details can be found in [14].

Symbolic Setting. Although finite-depth, even non-replicated protocols have infinite state space. Indeed, a simple input in(c,x) induces infinitely-many potential transitions in presence of an active attacker. We therefore define a symbolic calculus that abstracts concrete inputs by symbolic variables, and constraints that restrict their concrete instances. Constraints typically range over deducibility contraints (“the attacker is able to craft some term after spying on public channels”) and equations (“two terms are equal”). A symbolic semantics then performs symbolic inputs and collects constraints on them. Typically, executing input in(c,x) generates a deducibility constraint on x to model the attacker being able to craft the message to be input; equations are generated by conditionals, relying on most general unifiers modulo equational theory.

Decision Procedure. DeepSec constructs a so-called partition tree to guide decision of (in)equivalence of processes P and Q. Its nodes are labelled by sets of symbolic processes and constraints; typically the root contains P and Q with empty constraints. The tree is constructed similarly to the (finite) tree of all symbolic executions of P and Q, except that some nodes may be merged or split accordingly to a constraint-solving procedure. DeepSec thus enforces that concrete instances of processes of a same node are indistinguishable (statically).

The final decision criterion is that P and Q are equivalent iff all nodes of the partition tree contain both a process originated from P and a process originated from Q by symbolic execution. The DeepSec prover thus returns an attack iff it finds a node violating this property while constructing the partition tree.

2.3 Implementation

DeepSec is implemented in Ocaml (16k LOC) and the source code is licensed under GPL 3.0 and publicly available [17]. Running DeepSec yields a terminal output summarising results, while a more detailed output is displayed graphically in an HTML interface (using the MathJax API [20]). When the query is not satisfied, the interface interactively shows how to mount the attack.

Partial-Order Reductions. Tools verifying equivalences for bounded number of sessions suffer from a combinatorial explosion as the number of sessions increases. We therefore implemented state-of-the-art partial-order reductions (POR) [8] that eliminate redundant interleavings, providing a significant speedup. This is only possible for a restricted class of processes (determinate processes) but DeepSec automatically checks whether POR can be activated.

Parallelism. DeepSec generates a partition tree (cf Sect. 2.2) to decide trace equivalence. As sibling nodes are independent, the computation on subtrees can be parallelized. However, the partition tree is not balanced, making it hard to balance the load. One natural solution would be to systematically add children nodes into a queue of pending jobs, but this would yield an important communication overhead. Consequently, we apply this method only until the size of the queue is larger than a given threshold; next each idle process fetches a node and computes the complete corresponding subtree. Distributed computation over n cores is activated by the option -distributed n. By default, the threshold in the initial generation of the partition tree depends on n but may be overwritten to m with the option -nb_sets m.

3 Experimental Evaluation

Comparison to Other Work. When the number of sessions is unbounded, equivalence is undecidable. Verification tools in this setting therefore have to sacrifice termination, and generally only verify the finer diff-equivalence [9, 11, 23], too fine-grained on many examples. We therefore focus on tools comparable to DeepSec, i.e. those that bound the number of sessions. SPEC [25, 26] verifies a sound symbolic bisimulation, but is restricted to fixed cryptographic primitives (pairing, encryption, signatures, hashes) and does not allow for else branches. APTE [13] covers the same primitives but allows else branches and decides trace equivalence exactly. On the contrary, Akiss [12] allows for user-defined primitives and terminates when they form a subterm-convergent rewrite system. However Akiss only decides trace equivalence without approximation for a subclass of processes (determinate processes) and may perform under- and over-approximations otherwise. Sat-Eq [15] proceeds differently by reducing the equivalence problem to Graph Planning and SAT Solving: the tool is more efficient than the others by several orders of magnitude, but is quite restricted in scope (it currently supports pairing, symmetric encryption, and can only analyse a subclass of determinate processes). Besides, Sat-Eq may not terminate.

Authentication. Figure 1 displays a sample of our benchmarks (complete results can be found in [17]). DeepSec clearly outperforms Akiss, APTE, and SPEC, but Sat-Eq takes the lead as the number of sessions increase. However, the Otway-Rees protocol already illustrates the scope limit of Sat-Eq.

Besides, as previously mentioned, DeepSec includes partial-order reductions (POR). We performed experiments with and without this optimisation: for example, protocols requiring more than 12 h of computation time without POR can be verified in less than a second. Note that Akiss and APTE also implement the same POR techniques as DeepSec.

Fig. 1.
figure 1

Benchmark results on classical authentication protocols

Full size image

Privacy. We also verified privacy properties on the private authentication protocol [2], the passive-authentication and basic-access-control protocols from the e-passport [21], AKA of the 3G telephony networks [6] and the voting protocols Helios [3] and Prêt-à-Voter [22]. DeepSec is the only tool that can prove vote privacy on the two voting protocols, and private authentication is out of the scope of Sat-Eq and SPEC. Besides, we analysed variants of the Helios voting protocol, based on the work of Arapinis et al. [5] (see Fig. 2). The vanilla version is known vulnerable to a ballot-copy attack [16], which is patched by a ballot weeding (W) or a zero-knowledge proof (ZKP). DeepSec proved that, (i) when no revote is allowed, or (ii) when each honest voter only votes once and a dishonest voter is allowed to revote, then both patches are secure. However, only the ZKP variant remains secure when honest voters are allowed to revote.

Fig. 2.
figure 2

Benchmark results for verifying privacy type properties

Full size image

Parallelism. Experiments have been carried out on a server with 40 Intel Xeon E5-2687W v3 CPUs 3.10 GHz, with 50 GB RAM and 25 MB L3 Cache, using 35 cores (Server 1). However the performances of parallelisation had some unexpected behavior. For example, on the Yahalom-Lowe protocol, the use of too many cores on a same server negatively impacts performances: e.g. on Server 1, optimal results are achieved using only 20 to 25 cores. In comparison, optimal results required 40–45 cores on a server with 112 Intel Xeon vE7-4850 v3 CPUs 2.20 GHz, with 1.5 TB RAM and 35 MB L3 Cache (Server 2). This difference may be explained by cache capacity: overloading servers with processes (sharing cache) beyond a certain threshold should indeed make the hit-miss ratio drop. This is consistent with the Server 2 having a larger cache and exploiting efficiently more cores than Server 1. Using the perf profiling tool, we confirmed that the number of cache-references per second (CRPS) stayed relatively stable up to the optimal number of cores and quickly decreased beyond (Fig. 3).

Fig. 3.
figure 3

Performance analysis on Yahalom-Lowe protocol with 23 roles

Full size image

DeepSec can also distribute on multiple servers, using SSH connections. Despite a communication overhead, multi-server computation may be a way to partially avoid the server-overload issue discussed above. For example, the verification of the Helios protocol (Dishonest revote W) on 3 servers (using resp. 10, 20 and 40 cores) resulted in a running time of 18 m 14 s, while the same verification took 51 m 49 s on a 70-core server (also launched remotely via SSH).