A Reduced Semantics for Deciding Trace Equivalence
David Baelde, St\'ephanie Delaune, Lucca Hirschi
TL;DR
This paper introduces a reduced symbolic semantics and partial order reduction technique for trace equivalence checking in security protocols, significantly improving efficiency and integrated into the APTE tool.
Contribution
It generalizes and adapts partial order reduction for equivalence checking, providing a practical optimization for symbolic execution tools.
Findings
Dramatic improvements in benchmark performance
Effective elimination of redundant interleavings
Enhanced scalability of trace equivalence analysis
Abstract
Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. M\"odersheim et al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimisation in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. The obtained partial order reduction technique has been…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
\lmcsheading
1–LABEL:LastPageJul. 28, 2016Jun. 08, 2017
A reduced semantics for deciding trace equivalence
David Baelde\rsupera
,
Stéphanie Delaune\rsuperb
and
Lucca Hirschi\rsuperc
\lsupera,cLSV, ENS Cachan & CNRS, Université Paris-Saclay, France
{baelde,hirschi}@lsv.ens-cachan.fr
\lsuperbCNRS & IRISA, France
Abstract.
Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e. without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. Mödersheim et al. [40] have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimisation in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. The obtained partial order reduction technique has been integrated in a tool called . We conducted complete benchmarks showing dramatic improvements.
This work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No 714955-POPSTAR), as well as the ANR projects JCJC VIP ANR-11-JS02-006 and Sequoia ANR-14-CE28-0030-01.
1. Introduction
Security protocols are widely used today to secure transactions that rely on public channels like the Internet, where malicious agents may listen to communications and interfere with them. Security has a different meaning depending on the underlying application. It ranges from the confidentiality of data (medical files, secret keys, etc.) to, e.g. verifiability in electronic voting systems. Another example is the notion of privacy that appears in many contexts such as vote-privacy in electronic voting or untraceability in RFID technologies.
To achieve their security goals, security protocols rely on various cryptographic primitives such as symmetric and asymmetric encryptions, signatures, and hashes. Protocols also involve a high level of concurrency and are difficult to analyse by hand. Actually, many protocols have been shown to be flawed several years after their publication (and deployment). For example, a flaw has been discovered in the Single-Sign-On protocol used, e.g. by Google Apps. It has been shown that a malicious application could very easily get access to any other application (e.g. Gmail or Google Calendar) of their users [6]. This flaw has been found when analysing the protocol using formal methods, abstracting messages by a term algebra and using the Avantssar validation platform [8]. Another example is a flaw on vote-privacy discovered during the formal and manual analysis of an electronic voting protocol [27].
Formal symbolic methods have proved their usefulness for precisely analysing the security of protocols. Moreover, it allows one to benefit from machine support through the use of various existing techniques, ranging from model-checking to resolution and rewriting techniques. Nowdays, several verification tools are available, e.g. [13, 28, 7, 38, 43]. A synthesis of decidability and undecidability results for equivalence-based security properties, and an overview of existing verification tools that may be used to verify equivalence-based security properties can be found in [36].
In order to design decision procedures, a reasonable assumption is to bound the number of protocol sessions, thereby limiting the length of execution traces. Under such an hypothesis, a wide variety of model-checking approaches have been developed (e.g. [39, 47]), and several tools are now available to automatically verify cryptographic protocols, e.g. [46, 7]. A major challenge faced here is that one has to account for infinitely many behaviours of the attacker, who can generate arbitrary messages. In order to cope with this prolific attacker problem and obtain decision procedures, approaches based on symbolic semantics and constraint resolution have been proposed [39, 42]. This has lead to tools for verifying reachability-based security properties such as confidentiality [39] or, more recently, equivalence-based properties such as privacy [47, 20, 15]. Unfortunately, the resulting tools, especially those for checking equivalence (e.g. [19], [47], [16]) have a very limited practical impact because they scale badly. This is not surprising since they treat concurrency in a very naive way, exploring all possible symbolic interleavings of concurrent actions.
Related work.
In standard model-checking approaches for concurrent systems, the interleaving problem is handled using partial order reduction (POR) techniques [41]. In a nutshell, these techniques aim to effectively exploit the fact that the order of execution of two independent (parallel) actions is irrelevant when checking reachability. The theory of partial order reduction is well developed in the context of reactive systems verification (e.g. [41, 11, 34]). However, as pointed out by Clarke et al. in [26], POR techniques from traditional model-checking cannot be directly applied in the context of security protocol verification. Indeed, the application to security requires one to keep track of the knowledge of the attacker, and to refer to this knowledge in a meaningful way (in particular to know which messages can be forged at some point to feed some input). Furthermore, security protocol analysis does not rely on the internal reduction of a protocol, but has to consider arbitrary execution contexts (representing interactions with arbitrary, active attackers). Thus, any input may depend on any output, since the attacker has the liberty of constructing arbitrary messages from past outputs. This results in a dependency relation which is a priori very large, rendering traditional POR arguments suboptimal, and calling for domain-specific techniques.
In order to improve existing verification tools for security protocols, one has to design POR techniques that integrate nicely with symbolic execution. This is necessary to precisely deal with infinite, structured data. In this task, we get some inspiration from Mödersheim et al. [40], who design a partial order reduction technique that blends well with symbolic execution in the context of security protocols verification. However, we shall see that their key insight is not fully exploited, and yields only a quite limited partial order reduction. Moreover, they only consider reachability properties (like all previous work on POR for security protocol verification) while we seek an approach that is adequate for model-checking equivalence properties.
Contributions.
In this paper, we revisit the work of [40] to obtain a partial order reduction technique for the verification of equivalence properties. Among the several definitions of equivalence that have been proposed, we consider trace equivalence in this paper: two processes are trace equivalent when they have the same sets of observable traces and, for each such trace, sequences of messages outputted by the two processes are statically equivalent, i.e. indistinguishable for the attacker. This notion is well-studied and several algorithms and tools support it [14, 24, 47, 20, 15]. Contrary to what happens for reachability-based properties, trace equivalence cannot be decided relying only on the reachable states. The sequence of actions that leads to this state plays a role. Hence, extra precautions have to be taken before discarding a particular interleaving: we have to ensure that this is done in both sides of the equivalence in a similar fashion. Our main contribution is an optimised form of equivalence that discards a lot of interleavings, and a proof that this reduced equivalence coincides with trace equivalence. Furthermore, our study brings an improvement of the original technique [40] that would apply equally well for reachability checking. On the practical side, we explain how we integrated our partial order reduction into the state-of-the art tool [20], prove the correctness of this integration, and provide experimental results showing dramatic improvements. We believe that our presentation is generic enough to be easily adapted for other tools (provided that they are based on a forward symbolic exploration of traces combined with a constraint solving procedure). A big picture of the whole approach along with the new results is given in Figure 1. Vertically, it goes from the regular semantics, to symbolic semantics and ’s semantics. Those semantics have variants when our optimisations are applied or not: no optimisation, only compression or compression plus reduction.
This paper essentially subsumes the conference paper that has been published in 2014 [9]. However, we consider here a generalization of the semantics used in [9]. This generalization notably allows us to capture the semantics used in , which allows us to formally prove the integration of our optimisations in that tool. In addition, this paper incorporates proofs of all the results, additional examples, and an extensive related work section. Finally, it comes with a solid implementation in the tool [19].
Outline.
In Section 2, we introduce our model for security processes. We then consider the class of simple processes introduced in [22], with else branches and no replication. Then we present two successive optimisations in the form of refined semantics and associated trace equivalences. Section 3 presents a compressed semantics that limits interleavings by executing blocks of actions. Then, by adapting well-known argument, this is lifted to a symbolic semantics in Section 4. Section 5 presents the reduced semantics which makes use of dependency constraints to remove more interleavings. In Section 6, we explain how this reduced semantics has been integrated in the tool , prove its correcteness, and give some benchmarks obtained on several case studies. Finally, Section 7 is devoted to related work, and concluding remarks are given in Section 8. An overview of the different semantics we will define and the results relating them is depicted in Figure 1. A table of symbols can be found in Appendix A.
2. Model for security protocols
In this section, we introduce the cryptographic process calculus that we will use to describe security protocols. This calculus is close to the applied pi calculus [1]. We consider a semantics in the spirit of the one used in [9] but we also allow to block some actions depending on a validity predicate. This predicate can be chosen in such a way that no action is blocked, making the semantics as in [9]. It can also be chosen as in as we eventually do in order to prove the integration of our optimisations into this tool.
2.1. Syntax
A protocol consists of some agents communicating on a network. Messages sent by agents are modeled using a term algebra. We assume two infinite and disjoint sets of variables, and . Members of are denoted , , , whereas members of are denoted and used as handles for previously output terms. We also assume a set of names, which are used for representing keys or nonces111 Note that we do not have an explicit set of restricted (private) names. Actually, all names are restricted and public ones will be explicitly given to the attacker., and a signature consisting of a finite set of function symbols. Terms are generated inductively from names, variables, and function symbols applied to other terms. For , the set of terms built from by applying function symbols in is denoted by . We write for the set of syntactic subterms of a term . Terms in are denoted by , , etc. while terms in represent recipes (describing how the attacker built a term from the available outputs) and are written , , . We write for the set of variables (from or ) occurring in a term . A term is ground if it does not contain any variable, i.e. it belongs to . One may rely on a sort system for terms, but its details are unimportant for this paper.
To model algebraic properties of cryptographic primitives, we consider an equational theory . The theory will usually be generated from a finite set of axioms enjoying nice properties (e.g. convergence) but these aspects are irrelevant for the present work.
Example \thethm.
In order to model asymmetric encryption and pairing, we consider:
[TABLE]
To take into account the properties of these operators, we consider the equational theory generated by the three following equations:
[TABLE]
For instance, we have .
Our model is parameterized by a notion of message, intuitively meant to represent terms that can actually be communicated by processes. Formally, we assume a special subset of ground terms , only requiring that it contains at least one public constant. Then, we say that a ground term is valid, denoted , whenever for any , we have that there exists such that . This notion of validity will be imposed on communicated terms. As we shall see, can be chosen in such a way that the validity constraint allows us to discard some terms for which the computation of some parts fail. Note that can also be chosen to be the set of all ground terms, yielding a trivial validity predicate that holds for all ground terms. The following developments are parametrized by .
Example \thethm.
The signature used in is where:
[TABLE]
where may contain some additional user-defined function symbols. The equational theory of is an extension of the theory generated by adding the following equations:
[TABLE]
The validity predicate used in the semantics of is obtained by taking , i.e. the ground terms built using constructor symbols. This choice allows us to discard terms for which a failure will happen during the computation and which therefore do not correspond to a message: e.g. is not valid since is not equal modulo to a term in .
We do not need the full applied pi calculus [1] to represent security protocols. Here, we only consider public channels and we assume that each process communicates on a dedicated channel. Formally, we assume a set of channels and we consider the fragment of simple processes without replication built on basic processes as defined in [22]. A basic process represents a party in a protocol, which may sequentially perform actions such as waiting for a message, checking that a message has a certain form, or outputting a message. Then, a simple process is a parallel composition of such basic processes playing on distinct channels.
Definition \thethm (basic/simple process).
The set of basic processes on is defined using the following grammar (where and ):
[TABLE]
A simple process is a multiset of basic processes on pairwise distinct channels . We assume that null processes are removed.
Intuitively, a multiset of basic processes denotes a parallel composition. For conciseness, we often omit brackets, null processes, and even “else 0”. Basic processes are denoted by the letters and , whereas simple processes are denoted using and .
During an execution, the attacker learns the messages that have been sent on the different public channels. Those messages are organized into a frame.
Definition \thethm (frame).
A frame is a substitution whose domain is included in and image is included in . It is written . A frame is ground when its image only contains ground terms.
In the remainder of this paper, we will actually only consider ground frames that are made of valid terms.
An extended simple process (denoted or ) is a pair made of a simple process and a frame. Similarly, we define extended basic processes. When the context makes it clear, we may omit “extended” and simply call them simple processes and basic processes.
Example \thethm.
We consider the protocol given in [2] designed for authenticating an agent with another one without revealing their identities to other participants. In this protocol, is willing to engage in communication with and wants to be sure that she is indeed talking to and not to an attacker who is trying to impersonate . However, does not want to compromise her privacy by revealing her identity or the identity of more broadly. The participants and proceed as follows:
[TABLE]
First sends to a nonce and her public key encrypted with the public key of . If the message is of the expected form then sends to the nonce , a freshly generated nonce and his public key, all of this being encrypted with the public key of . Moreover, if the message received by is not of the expected form then sends out a “decoy” message: . This message should basically look like ’s other message from the point of view of an outsider.
Relying on the signature and equational theory introduced in Example 2.1, a session of role played by agent (with private key ) with (with public key ) can be modeled as follows:
[TABLE]
Here, we are only considering the authentication protocol. A more comprehensive model should include the access to an application in case of a success. Similarly, a session of role played by agent with can be modeled by the following basic process, where .
[TABLE]
To model a scenario with one session of each role (played by the agents and ), we may consider the extended process where:
- •
, and
- •
.
The purpose of will be clear later on. It allows us to consider the existence of another agent whose public key is known by the attacker.
2.2. Semantics
We first define a standard concrete semantics using a relation over ground extended simple processes, i.e. extended simple processes such that (as said above, we also assume that contains only valid ground terms). The semantics of a ground extended simple process is induced by the relation \mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}} over ground extended simple processes as defined in Figure 2.
A process may input any valid term that an attacker can build (rule In): is a substitution that replaces any occurrence of with . Once a recipe is fixed, we may note that there are still different instances of the rule, but only in the sense that is chosen modulo the equational theory . In practice, of course, not all such are enumerated. How this is achieved in practice is orthogonal to the theoretical development carried out here. In the Out rule, we enrich the attacker’s knowledge by adding the newly output term , with a fresh handle , to the frame. The two remaining rules are unobservable ( action) from the point of view of the attacker. When contains all the ground terms, is true for any term and this semantics coincides with the one defined in [9]. However, this parameter gives us enough flexibility to obtain a semantics similar to the one used in , and therefore formally prove in Section 6 how to integrate our techniques in .
The relation A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}B between extended simple processes, where and each is an observable or a action, is defined in the usual way. We also consider the relation defined as follows: if, and only if, there exists such that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}B, and is obtained from by erasing all occurrences of .
Example \thethm.
Consider the simple process introduced in Example 2.1 (with equal to as in ). We have:
[TABLE]
This trace corresponds to the normal execution of one instance of the protocol. The two silent actions have been triggered using the Then rule. The resulting frame is as follows:
[TABLE]
2.3. Trace equivalence
Many interesting security properties, such as privacy-type properties studied, e.g. in [5], are formalized using the notion of trace equivalence. Before defining trace equivalence, we first introduce the notion of static equivalence that compares sequences of messages.
Definition \thethm (static equivalence).
Two frames and are in static equivalence, , when we have that , and:
- •
* for any term ; and*
- •
* for any terms such that and .*
Intuitively, two frames are equivalent if an attacker cannot see the difference between the two situations they represent, i.e. they satisfy the same equalities and failures.
Example \thethm.
Consider the frame given in Example 2.2 and the frame below:
[TABLE]
We have that . This is a non-trivial equivalence. Intuitively, it holds since the attacker is not able to decrypt any of the ciphertexts, and each ciphertext contains a nonce that prevents him to build it from its components.
Now, if we decide to give access to to the attacker, i.e. considering and , then the two frames and are not in static equivalence anymore as witnessed by and . Indeed, we have that whereas , and all these witnesses are valid.
Definition \thethm (trace equivalence).
Let and be two extended simple processes. We have that if, for every sequence of actions such that , there exists such that and . The processes and are trace equivalent, denoted by , if and .
Example \thethm.
Intuitively, the private authentication protocol presented in Example 2.1 preserves anonymity if an attacker cannot distinguish whether is willing to talk to (represented by the process ) or willing to talk to (represented by the process ), provided , and are honest participants. This can be expressed relying on the following equivalence:
[TABLE]
For illustration purposes, we also consider a variant of the process , denoted , where its branch has been replaced by [math] (i.e. the null process). We will see that the “decoy” message plays a crucial role to ensure privacy. We have that:
[TABLE]
where . We may note that this trace does not correspond to a normal execution of the protocol. Still, the first input is fed with the message which is a message of the expected format from the point of view of the process . Therefore, once conditionals are positively evaluated, the output can be triggered.
This trace has no counterpart in . Indeed, we have that:
[TABLE]
Hence, we have that .
However, it is the case that . This equivalence can be checked using the tool [17] within few seconds for a simple scenario as the one considered here, and that takes few minutes/days as soon as we want to consider 2/3 sessions of each role.
3. Compression based on grouping actions
Our first refinement of the semantics, which we call compression, is closely related to focusing from proof theory [4]: we will assign a polarity to processes and constrain the shape of executed traces based on those polarities. This will provide a first significant reduction of the number of traces to consider when checking equivalence-based properties between simple processes. Moreover, compression can easily be used as a replacement for the usual semantics in verification algorithms.
The key idea is to force processes to perform all enabled output actions as soon as possible. In our setting, we can even safely force them to perform a complete block of input actions followed by ouput actions.
Example \thethm.
Consider the process with . In order to reach , we have to execute the action (using a recipe that allows one to deduce ) and the action (giving us a label of the form ). In case of reachability properties, the execution order of these actions only matters if uses . Thus we can safely perform the outputs in priority.
The situation is more complex when considering trace equivalence. In that case, we are concerned not only with reachable states, but also with how those states are reached. Quite simply, traces matter. Thus, if we want to discard the trace when studying process and consider only its permutation , we have to make sure that the same permutation is available on the other process. The key to ensure that identical permutations will be available on both sides of the equivalence is our restriction to the class of simple processes.
3.1. Compressed semantics
We now introduce the compressed semantics. Compression is an optimisation, since it removes some interleavings. But it also gives rise to convenient “macro-actions”, called blocks, that combine a sequence of inputs followed by some outputs, potentially hiding silent actions. Manipulating those blocks rather than indiviual actions makes it easier to define our second optimisation.
For sake of simplicity, we consider initial simple processes. A simple process is initial if for any , we have that , or for some term such that . In other words, each basic process composing starts with an input unless it is blocked due to an unfeasible output.
Example \thethm.
Continuing Example 2.1, is not initial. Instead, we may consider where
[TABLE]
assuming that is a (public) constant in our signature.
The main idea of the compressed semantics is to ensure that when a basic process starts executing some actions, it actually executes a maximal block of actions. In analogy with focusing in sequent calculus, we say that the basic process takes the focus, and can only release it under particular conditions. We define in Figure 3 how blocks can be executed by extended basic processes. In that semantics, the label denotes the stage of the execution, starting with , then after the first input and after the first output.
Example \thethm.
Going back to Example 2.3, we have that:
[TABLE]
where is as given in Example 2.3. As illustrated by the proof tree below, we also have with .
[TABLE]
where for some message .
Then we define the relation \mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{c} between extended simple processes as the least reflexive transitive relation satisfying the rules given in Figure 4.
A basic process is allowed to properly end a block execution when it has performed outputs and it cannot perform any more output or unobservable action (). Accordingly, we call proper block a non-empty sequence of inputs followed by a non-empty sequence of outputs, all on the same channel. For completeness, we also allow blocks to be terminated improperly, when the process that is executing has performed inputs but no output, and has reached the null process [math] or an output which is blocked. Accordingly, we call improper block a non-empty sequence of inputs on the same channel.
Example \thethm.
Continuing Example 3.1, using the rule block, we can derive
[TABLE]
where is defined in Example 3.1. We can also derive
[TABLE]
using the rule Failure. Note that the resulting simple process is reduced to even though has never been executed.
At first sight, killing the whole process when applying the rule Failure may seem too strong. However, even if this kind of scenario is observable by the attacker, it does not bring him any new knowledge, hence it plays only a limited role in trace equivalence: it is in fact sufficient to consider such improper blocks only at the end of traces.
Example \thethm.
Consider . Its compressed traces are of the form and . The concatenation of those two improper traces cannot be executed in the compressed semantics. Intuitively, we do not loose anything for trace equivalence, because if a process can exhibit those two improper blocks they must be in parallel and hence considering their combination is redundant.
We now define the notions of compressed trace equivalence (denoted ) and compressed trace inclusion (denoted ), similarly to and but relying on \mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{c} instead of .
Definition \thethm (compressed trace equivalence).
Let and be two extended simple processes. We have that if, for every sequence of actions such that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P};\Phi), there exists such that B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime};\Phi^{\prime}) and . The processes and are compressed trace equivalent, denoted by , if and .
Example \thethm.
We have that . The trace exhibited in Example 3.1 is executable from . However, this trace has no counterpart when starting with .
3.2. Soundness and completeness
We shall now establish soundness and completeness of the compressed semantics. More precisely, we show that the two relations and coincide on initial simple processes (Theorem 3.2). All the proofs of this section are given in Appendix B.
Intuitively, we can always permute output (resp. input) actions occurring on distinct channels, and we can also permute an output with an input if the outputted message is not used to build the inputted term. More formally, we define an independence relation over actions as the least symmetric relation satisfying:
- •
and as soon as ,
- •
when in addition .
Then, we consider to be the least congruence (w.r.t. concatenation) satisfying:
for all and with ,
and we show that processes are equally able to execute equivalent (w.r.t. ) traces.
Lemma \thethm.
Let , be two extended simple processes and , be such that . We have that if, and only if, .
Now, considering traces that are only made of proper blocks, a strong relationship can be established between the two semantics.
Proposition \thethm.
Let , be two simple extended processes, and be a trace made of proper blocks such that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime}. Then we have that .
Actually, the result stated in Proposition 3.2 immediately follows from the observation that \mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{c} is included in for traces made of proper blocks since for them Failure cannot arise.
Proposition \thethm.
Let , be two initial simple processes, and be a trace made of proper blocks such that . Then, we have that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime}.
This result is more involved and relies on the additional hypothesis that and have to be initial to ensure that no Failure will arise.
Theorem \thethm.
Let and be two initial simple processes. We have that
[TABLE]
Proof sketch, details in Appendix B.
The main difficulty is that Proposition 3.2 only considers traces composed of proper blocks whereas we have to consider all traces. To prove the implication, we have to pay attention to the last block of the compressed trace that can be an improper one (composed of several inputs on a channel ). The implication is more difficult since we have to consider a trace of a process that is an interleaving of some prefix of proper and improper blocks. We will first complete it with to obtain an interleaving of proper and improper blocks. We then reorder the actions to obtain a trace such that and where is made of proper blocks while is made of improper blocks. For each improper block of , we show by applying Lemma 3.2 and Proposition 3.2 that is able to perform in the compressed semantics and the resulting extended process can execute the improper block . We thus have that is able to perform in the compressed semantics and thus as well. Finally, we show that the executions of all those (concurrent) blocks can be put together, obtaining that can perform , and thus as well. ∎
Note that, as illustrated by the following example, the two underlying notions of trace inclusion do not coincide.
Example \thethm.
Let and accompanied with an arbitrary frame . We have but since in the compressed semantics is not allowed to stop its execution after its first input.
4. Deciding trace equivalence via constraint solving
In this section, we propose a symbolic semantics for our compressed semantics following, e.g. [39, 12]. Such a semantics avoids potentially infinite branching of our compressed semantics due to inputs from the environment. Correctness is maintained by associating with each process a set of constraints on terms.
4.1. Constraint systems
Following the notations of [12], we consider a new set of second-order variables, denoted by , , etc. We shall use those variables to abstract over recipes. We denote by the set of free second-order variables of an object , typically a constraint system. To prevent ambiguities, we shall use instead of for free first-order variables.
Definition \thethm (constraint system).
A constraint system consists of a frame , and a set of constraints . We consider three kinds of constraints:
[TABLE]
where , , and .
The first kind of constraint expresses that a second-order variable has to be instantiated by a recipe that uses only variables from a certain set , and that the obtained term should be . The handles in represent terms that have been previously outputted by the process.
We are not interested in general constraint systems, but only consider constraint systems that are well-formed. Given a constraint system , we define a dependency order on first-order variables in by declaring that depends on if, and only if, contains a deduction constraint with . A constraint system is well-formed if:
- •
the dependency relationship is acyclic, and
- •
for every (resp. ) there is a unique constraint in .
For , we write for the domain of the deduction constraint associated to in .
Example \thethm.
Continuing Example 2.1, let with , and be a set containing two constraints:
[TABLE]
We have that is a well-formed constraint system. There is only one first-order variable , and it does not occur in , which is empty. Moreover, there is indeed a unique constraint that introduces .
Our notion of well-formed constraint systems is in line with what is used, e.g. in [39, 12]. We use a simpler variant here that is sufficient for our purpose.
Definition \thethm (solution).
A solution of a constraint system is a substitution such that , and for any . Moreover, we require that there exists a ground substitution with such that:
- •
for every in , we have , , and ;
- •
for every in , we have , , and ; and
- •
for every in , we have , or , or .
Moreover, we require that all the terms occurring in are valid. The set of solutions of a constraint system is denoted ). Since we consider constraint systems that are well-formed, the substitution is unique modulo given . We denote it by when is clear from the context.
Note that the validity constraints in the notion of solution of symbolic processes reflect the validity constraints of the concrete semantics (i.e. outputted and inputted terms must be valid and the equality between terms requires the two terms to be valid). Since we consider well-formed constraint systems, we may note that the substitution above is not obtained through unification. This substitution is entirely determined (modulo ) from by considering the deducibility constraints only.
Example \thethm.
*Consider again the constraint system given in Example 4.1. We have that is a solution of . Its associated first-order solution is . *
4.2. Symbolic processes: syntax and semantics
Given an extended simple process , we compute the constraint systems capturing its possible executions, starting from the symbolic process . Note that we are now manipulating processes that are not ground anymore, but may contain free variables.
Definition \thethm (symbolic process).
A symbolic process is a tuple where is a constraint system and .
We give in Figure 5 a standard symbolic semantics for symbolic basic processes. From this semantics given on symbolic basic processes only, we derive a semantics on simple symbolic processes in a natural way:
[TABLE]
We can also derive our compressed symbolic semantics \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c} following the same pattern as for the concrete semantics (see Figure 6). We consider interleavings that execute maximal blocks of actions, and we allow improper termination of a block only at the end of a trace. Note that the conditions of the third Proper rule and the second Improper rule are replaced by constraints in their symbolic counterparts.
Example \thethm.
Continuing Example 2.1, we have that (\{Q_{0}(\mathit{skb},\mathsf{pk}(\mathit{ska}))\};\Phi_{0};\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\emptyset;\Phi;\mathcal{S}) where:
- •
, and
- •
* is the constraint system defined in Example 4.1.*
We are now able to define the notion of equivalence associated to these two semantics, namely symbolic trace equivalence (denoted ) and symbolic compressed trace equivalence (denoted ). For a trace , we note the trace obtained from by removing all actions.
Definition \thethm.
Let and be two simple processes. We have that when, for every trace such that (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}(\mathcal{P}^{\prime};\Phi^{\prime};\mathcal{S}_{A}), for every , we have that:
- •
(\mathcal{Q};\Psi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}(\mathcal{Q}^{\prime};\Psi^{\prime};\mathcal{S}_{B})* where with , and*
- •
* where (resp. ) is the substitution associated to w.r.t. (resp. ).*
We have that and are in trace equivalence w.r.t. \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}, denoted , if and .
We derive similarly the notion of trace equivalence induced by \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{c}. We do not have to take care of the actions since they are performed implicitly in the compressed semantics.
Definition \thethm.
Let and be two extended simple processes. We have that when, for every trace such that (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime};\Phi^{\prime};\mathcal{S}_{A}), for every , we have that:
- •
(\mathcal{Q};\Psi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{Q}^{\prime};\Psi^{\prime};\mathcal{S}_{B})* with , and*
- •
* where (resp. ) is the substitution associated to w.r.t. (resp. ).*
We have that and are in trace equivalence w.r.t. \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{c}, denoted , if and .
Example \thethm.
We have that . Continuing Example 4.2, we have seen that:
- •
(\{Q_{0}(\mathit{skb},\mathsf{pk}(\mathit{ska}))\};\Phi_{0};\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\emptyset;\Phi;\mathcal{S})* (see Example 4.2), and*
- •
* is a solution of (see Example 4.1).*
The only symbolic process that is reachable from using is with:
- •
, and
- •
\mathcal{S}^{\prime}=\big{\{}\{w_{0},w_{1},w_{2}\}\mathop{\vdash^{?}_{Y}}y;\;\;\pi_{2}(N)\mathop{{=}^{?}}\mathsf{pk}(ska^{\prime})\big{\}}.
One can check that is not a solution of .
For processes without replication, the symbolic transition system induced by \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}$ (resp $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}) is essentially finite. Indeed, the choice of fresh names for handles and second-order variables does not matter, and therefore the relations \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}$ and $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c} are essentially finitely branching. Moreover, the length of traces of a simple process is obviously bounded. Thus, deciding (symbolic) trace equivalence between processes boils down to the problem of deciding a notion of equivalence between sets of constraint systems. This problem is well-studied and several procedures already exist [12, 24], e.g. [20] (see Section 6).
4.3. Soundness and completeness
It is well-known that the symbolic semantics \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}$ is sound and complete w.r.t. $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}, and therefore that the two underlying notions of equivalence, namely and , coincide. This has been proved for instance in [12, 22]. Using the same approach, we can show soundness and completeness of our symbolic compressed semantics w.r.t. our concrete compressed semantics. We have:
- •
Soundness: each transition in the compressed symbolic semantics represents a set of transitions that can be done in the concrete compressed semantics.
- •
Completeness: each transition in the compressed semantics can be matched by a transition in the compressed symbolic semantics.
These results are formally expressed in Proposition 4.3 and Proposition 4.3 below. These propositions are simple consequences of similar propositions that link the (small-step) symbolic semantics and the (small-step) standard semantics. Lifting these results to the compressed semantics is straightforward since both semantics are built using exactly the same scheme (see Figures 3 and 6).
Proposition \thethm.
Let be an extended simple process such that (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime};\Phi^{\prime};\mathcal{S}^{\prime}), and . We have that (\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime}\lambda;\Phi^{\prime}\lambda) where is the first-order solution of associated to .
Proposition \thethm.
Let be an extended simple process such that (\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime};\Phi^{\prime}). There exists a symbolic process , a solution , and a sequence such that:
- •
(\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}_{s};\Phi_{s};\mathcal{S});
- •
; and
- •
**
where is the first-order solution of associated to .
Finally, relying on these two results, we can establish that symbolic trace equivalence () exactly captures compressed trace equivalence (). Actually, both inclusions can be established separately.
Theorem \thethm.
For any extended simple processes and , we have that:
[TABLE]
As an immediate consequence of Theorem 3.2 and Theorem 4.3, we obtain that the relations and coincide.
Corollary \thethm.
For any initial simple processes and , we have that:
[TABLE]
5. Reduction using dependency constraints
Unlike compression, which is essentially based on the input/output nature of actions, our second optimisation takes into account the exchanged messages. Let us first illustrate one simple instance of our optimisation and how dependency constraints [40] may be used to incorporate it into symbolic semantics.
Example \thethm.
Let with , and be a ground frame. We consider the simple process , and the two symbolic interleavings depicted in Figure 7. The two resulting symbolic processes are of the form where ,
[TABLE]
The sets of concrete processes that these two symbolic processes represent are different, which means that we cannot discard any of those interleavings. However, these sets have a significant overlap corresponding to concrete instances of the interleaved blocks that are actually independent, i.e. where the output of one block is not necessary to obtain the input of the next block. In order to avoid considering such concrete processes twice, we may add a dependency constraint in , whose purpose is to discard all solutions such that the message can be derived without using . For instance, the concrete trace would be discarded thanks to this new constraint.
The idea of [40] is to accumulate dependency constraints generated whenever such a pattern is detected in an execution, and use an adapted constraint resolution procedure to narrow and eventually discard the constrained symbolic states. We seek to exploit similar ideas for optimising the verification of trace equivalence rather than reachability. This requires extra care, since pruning traces as described above may break completeness when considering trace equivalence. As before, the key to obtain a valid optimisation will be to discard traces in a similar way on the two processes being compared. In addition to handling this necessary subtlety, we also propose a new proof technique for justifying dependency constraints. The generality of that technique allows us to add more dependency constraints, taking into account more patterns than the simple one from the previous example.
5.1. Reduced semantics
We start by introducing dependency constraints.
Definition \thethm.
A dependency constraint is a constraint of the form where is a vector of second-order variables in , and is a vector of handles, i.e. variables in .
Given a constraint system , a set of dependency constraints, and . We write when also satisfies the dependency constraints in , i.e. when for each there is some such that for all recipes satisfying and , we have that where is the substitution associated to w.r.t. .
Intuitively, a dependency constraint is satisfied as soon as at least one message among those in can only be deduced by using a message stored in .
Example \thethm.
Continuing Example 5, assume that and let . We have that and the substitution associated to w.r.t. is . However, does not satisfy the dependency constraint . Indeed, we have that whereas . Intuitively, this means that there is no good reason to postpone the execution of the block on channel if the output on is not useful to build the message used in input on .
We shall now define formally how dependency constraints will be added to our constraint systems. For this, we fix an arbitrary total order on channels. Intuitively, this order expresses which executions should be favored, and which should be allowed only under dependency constraints. To simplify the presentation, we use the notation as a shortcut for assuming that and . Note that and/or may be empty.
Definition \thethm (generation of dependency constraints).
Let be a channel, and be a trace. If there exists a rank such that and for all , then \mathrm{dep}\left(\mathsf{tr},c\right)=\{\;w~{}|~{}w\in\overrightarrow{w_{i}}\mbox{ with k\leq i\leq n}\}. Otherwise, we have that .
Then, given a trace , we define by and
[TABLE]
Intuitively, corresponds to the accumulation of the dependency constraints generated for all prefixes of .
Example \thethm.
Let , , and be channels in such that . The dependency constraints generated during the symbolic execution of a simple process of the form are depicted below.
\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\mathtt{io}_{a}\;\;\;\;\;$$\mathtt{io}_{b}\;$$\;\;\;\;\mathtt{io}_{c}$$\mathtt{io}_{b}\;\;$$\;\;\mathtt{io}_{c}$$\mathtt{io}_{a}\;\;$$\;\;\mathtt{io}_{c}$$\mathtt{io}_{a}\;\;\;\;\;\;$$\mathtt{io}_{b}\;\;\,$$\mathtt{io}_{c}\;$$\mathtt{io}_{b}\;$$\mathtt{io}_{c}\;$$\mathtt{io}_{a}\;$$\mathtt{io}_{b}\;$$\mathtt{io}_{a}\;
We use as a shortcut for and we represent dependency constraints using arrows. For instance, on the trace , a dependency constraint of the form (represented by the left-most arrow) is generated. Now, on the trace we add after the second transition, and (represented by the dashed -arrow) after the third transition. Intuitively, the latter constraint expresses that is only allowed to come after if it depends on it, possibly indirectly through .
Dependency constraints give rise to a new notion of trace equivalence, which further refines the previous ones.
Definition \thethm (reduced trace equivalence).
Let and be two extended simple processes. We have that when, for every sequence such that (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime};\Phi^{\prime};\mathcal{S}_{A}), for every such that , we have that:
- •
(\mathcal{Q};\Psi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{Q}^{\prime};\Psi^{\prime};\mathcal{S}_{B})* with , and ;*
- •
* where (resp. ) is the substitution associated to w.r.t. (resp. ).*
We have that and are in reduced trace equivalence, denoted , if and .
5.2. Soundness and completeness
In order to establish that and coincide, we shall study more carefully concrete traces, consisting of proper blocks possibly followed by a single improper block. We will then define a precise characterization of executions whose associated solution satisfies dependency constraints. We denote by the set of blocks such that , for each , and for each . In this section, a concrete trace is seen as a sequence of blocks, i.e. it belongs to .
Definition \thethm (independence between blocks).
Two blocks and are independent, written , when and none of the variables of occurs in , and none of the variables of occurs in . Otherwise the blocks are dependent.
It is easy to see that independent blocks that are proper can be permuted in a compressed trace without affecting the executability and the result of executing that trace. It is not the case for improper blocks, which can only be performed at the very end of a compressed execution.
However, this notion of independence based on recipes is too restrictive: it may introduce spurious dependencies. Indeed, it is often possible to make two blocks dependent by slightly modifying recipes without altering the inputted messages. For instance, does not occur in recipe but does in while induces the same message as . We thus define a more permissive notion of equivalence over traces, which allows permutations of independent blocks but also changes of recipes that preserve messages. During these permutations, we require that (concrete) traces remain plausible.
Definition \thethm (plausible).
A trace is plausible if for any input such that , we have where is the set of handles occurring in .
Given two blocks and , we note when , , , and . Intuitively, the two blocks only differ by a change of recipes such that the underlying messages are kept unchanged. We lift this notion to sequences of blocks, i.e. , in the natural way.
Definition \thethm.
Given a frame , the relation is the smallest equivalence over plausible traces (made of blocks) such that:
- (1)
* when ; and* 2. (2)
* when .*
Lemma \thethm.
Let A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P};\Phi) with be a trace made of proper blocks. We have that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P};\Phi) for any .
This result is easily proved, following from the fact that proper compressed executions are preserved by the two generators of . The first case is given by Lemma 3.2. The second one follows from a simple observation of the transition rules: only the derived messages matter, while the recipes that are used to derive them are irrelevant (as long as validity is ensured).
We established that compressed executions are preserved by changes of traces within -equivalence classes. We shall now prove that, by keeping only executions satisfying dependency constraints, we actually select exactly one representative in this class.
We lift the ordering on channels to blocks: if and only if . Finally, we define on concrete traces as the lexicographic extension of the order on blocks. Given a frame , we say that a plausible trace is -minimal if it is minimal in its equivalence class modulo .
Lemma \thethm.
Let A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P};\Phi;\mathcal{S}) and . We have that is -minimal if, and only if, .
Proof.
Let and be such that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P};\Phi;\mathcal{S}) and . Let be the substitution associated to w.r.t. .
We first show that if is -minimal then , by induction on the length of the trace . The base case, i.e. , is straightforward since . Now, assume that for some block and A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}_{0};\Phi_{0};\mathcal{S}_{0})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P};\Phi;\mathcal{S}). Let be the substitution restricted to variables occurring in , and be the associated first-order substitution. We have that , coincides with on variables occurring in , and coincides with on the domain of . As a prefix of , we have that is -minimal. We can thus apply our induction hypothesis on A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}_{0};\Phi_{0};\mathcal{S}_{0}) and . Assume that . If , we immediately conclude. Otherwise, it only remains to show that . By definition of the generation of dependency constraints, we know that is of the form where:
- •
,
- •
and for all ; and
- •
.
Assume that the dependency constraint is not satisfied, this means that for some such that and , we have that . Therefore, we have that
[TABLE]
Since , this would contradict the -minimality of . Hence the result.
Now, assuming that is not -minimal, we shall establish that there is a dependency constraint that is not satisfied by . Let be a -minimal trace of the equivalence class of . We have in particular and .
Let (resp. ) be the longest prefix of (resp. ) such that . We have that and with where (resp. ) is the channel used in block (resp. ). By definition of , block must have a counterpart in and, more precisely, in . We thus have a more precise decomposition of : such that .
Let . We now show that the constraint is in and is not satisfied by , implying . We have seen that and . Since , by definition of we deduce that . But, since we also know that and is a plausible trace, we have that for some recipes such that , , and . This allows us to conclude that . ∎
We are now able to show that the notion of trace equivalence based on this reduced semantics coincides with the compressed one (as well as its symbolic counterpart as given in Definition 4.2). Even though the reduced semantics is based on the symbolic compressed semantics, it is more natural to establish the theorem by going back to the concrete compressed semantics, because we have to consider a concrete execution to check whether dependency constraints are satisfied or not in our reduced semantics anyway.
Theorem \thethm.
For any extended simple processes and , we have that:
* if and only if .*
Proof.
Let and be two extended simple processes.
() Consider an execution of the form (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}_{s};\Phi_{s};\mathcal{S}_{A}) and a substitution such that . Thanks to Proposition 4.3, we have that (\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}_{s}\lambda^{A}_{\theta};\Phi_{s}\lambda^{A}_{\theta}) where is the substitution associated to w.r.t. .
Since , we deduce that there exists such that:
[TABLE]
Relying on Proposition 4.3, we deduce that there exists such that:
[TABLE]
where is the substitution associated to w.r.t. . The fact that we get the same symbolic trace and same solution comes from the third point of Proposition 4.3 and the flexibility of the symbolic semantics \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c} that allows us to choose second order variables of our choice (as long as they are fresh).
Lemma 5.2 tells us that is -minimal. Since , we easily deduce that is also -minimal, and thus Lemma 5.2 tells us that . This allows us to conclude.
() Consider an execution of the form (\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime};\Phi^{\prime}). We prove the result by induction on the number of blocks involved in , and we distinguish two cases depending on whether ends with an improper block or not.
Case where is made of proper blocks. Let be a -minimal trace in the equivalence class of . Lemma 5.2 tells us that (\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{P}^{\prime};\Phi^{\prime}). Thanks to Proposition 4.3, we know that there exist , , and such that:
[TABLE]
Using Lemma 5.2, we deduce that . By hypothesis, , hence:
- •
(\mathcal{Q};\Psi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\mathcal{Q}_{s};\Psi_{s};\mathcal{S}_{B}) with , and ;
- •
where is the substitution associated to w.r.t.
Thanks to Proposition 4.3, we deduce that
[TABLE]
Moreover, since , we get from the fact that . Applying Lemma 5.2, we conclude that
[TABLE]
Case where is of the form where is an improper block. We have that:
[TABLE]
Let be a -minimal trace in the equivalence class of . By definition of the relation , block must have a counterpart in . We thus have that is of the form where is the improper block corresponding to . We do not necessarily have that but we know that . If is an empty trace, i.e. is at the end of , the reasoning from the previous case applies.
Otherwise, we have that , is -minimal, and is non empty. Thus, thanks to Lemma 5.2, we have that:
[TABLE]
Since is made of proper blocks, we can apply our previous reasoning, and conclude that there exist and such that:
[TABLE]
Since we know that (\mathcal{P}^{\prime};\Phi^{\prime})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\emptyset;\Phi^{\prime}), and , we deduce that (\mathcal{P}_{1};\Phi_{1})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\emptyset;\Phi_{1}). We have that (\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}(\emptyset;\Phi_{1}), and is a -minimal trace (note that the improper block is at the end). Thus, applying our induction hypothesis, we have that:
[TABLE]
Since the channel used in does not occur in , we deduce that
[TABLE]
Relying on Lemma 5.2 and the fact that , we deduce that
[TABLE]
∎
Putting together Theorem 3.2 and Theorem 5.2, we are now able to state our main result: our notion of reduced trace equivalence actually coincides with the usual notion of trace equivalence. This result is generic and holds for an arbitrary equational theory, as well as for an arbitrary notion of validity (as defined in Section 2.1).
Corollary \thethm.
For any initial simple processes and , we have that:
* if and only if .*
6. Integration in
We validate our approach by integrating our refined semantics in the tool. As we shall see, the compressed semantics can easily be used as a replacement for the usual semantics in verification algorithms. However, exploiting the reduced semantics is not trivial, and requires to adapt the constraint resolution procedure.
It is beyond the scope of this paper to provide a detailed summary of how the verification tool actually works. A 50 pages paper describing solely the constraint resolution procedure of is available [21]. This procedure manipulates matrices of constraint systems, with additional kinds of constraints necessary for its inner workings. Proofs of the soundness, completeness and termination of the algorithm are available in a long and technical appendix (more than 100 pages).
In order to show how our reduced semantics have been integrated in the constraint solving procedure of , we choose to provide a high-level axiomatic presentation of ’s algorithm. This allows us to prove that our integration is correct without having to enter into complex, unnecessary details of ’s algorithm. Our axioms are consequences of results stated and proved in [18] and have been written in concertation with Vincent Cheval. However, due to some changes in the presentation, proving them will require to adapt most of the proofs. It is therefore beyond the scope of this paper to formally prove that our axioms are satisfied by the concrete procedure.
We start this section with a high-level axiomatic presentation of ’s algorithm, following the original procedure [20] but assuming public channels only (sections 6.1, 6.2). The purpose of this presentation is to provide enough details about to explain how our optimisations have been integrated, leaving out unimportant details. Next, we show that this axiomatization is sufficient to prove soundness and completeness of w.r.t. trace equivalence (Section 6.3). Then we explain the simplifications induced by the restriction to simple processes, and how compressed semantics can be used to enhance the procedure and prove the correctness of this integration (Section 6.4). We finally describe how our reduction technique can be integrated, and prove the correctness of this integration (Section 6.5).
We present some benchmarks in Section 6.6, showing that our integration allows to effectively benefit from both of our partial order reduction techniques.
6.1. in a nutshell
has been designed for a fixed equational theory (formally defined in Example 2.1) containing standard cryptographic primitives. It relies on a notion of message which requires that only constructors are used, and a semantics in which actions are blocked unless they are performed on such messages. This fits in our framework, described in Section 2, by taking .
We now give a high-level description of the algorithm that is implemented in . The main idea is to perform all possible symbolic executions of the processes, keeping together the processes that can be reached using the same sequence of symbolic action. Then, at each step of this symbolic execution, the procedure checks that for every solution of every process on one side, there is a corresponding solution for some process on the other side so that the resulting frames are in static equivalence. This check for symbolic equivalence is not obviously decidable. To achieve it, ’s procedure relies on a set of rules for simplifying sets of constraint systems. These rules are used to put constraint systems in a solved form that enables the efficient verification of symbolic equivalence.
The symbolic execution used in is the same as described in Section 4. However, ’s constraint resolution procedure introduces new kinds of constraints. Fortunately, we do not need to enter into the details of those constraints and how they are manipulated. Instead, we treat them axiomatically.
Definition \thethm (extended constraint system/symbolic process).
An extended constraint system consists of a constraint system together with an additional set of extended constraints. We treat this latter set abstractly, only assuming an associated satisfaction relation, written , such that always holds, and implies when . We define the set of solutions of as .
*An extended symbolic process * is a symbolic process with an additional set of extended constraints .
We shall denote extended constraint systems by , , etc. Extended symbolic processes will be denoted by , , etc. Sets of extended symbolic processes will simply be denoted by , , etc. For convenience, we extend and to symbolic processes and extended symbolic processes in the natural way:
[TABLE]
We may also use the following notation to translate back and forth between symbolic processes and extended symbolic processes:
[TABLE]
We can now introduce the key notion of symbolic equivalence between sets of extended symbolic processes, or more precisely between their underlying extended constraint systems.
Definition \thethm (symbolic equivalence).
Given two sets of extended symbolic processes and , we have that if for every , for every , there exists such that and where (resp. ) is the substitution associated to w.r.t. (resp. ). We say that and are in symbolic equivalence, denoted by , if and .
The whole trace equivalence procedure can finally be abstractly described by means of a transition system \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}^{\mathsf{A}}$ on pairs of sets of extended symbolic processes, labelled by observable symbolic actions. Informally, the intent is that a pair of processes is in trace equivalence iff only symbolically equivalent pairs may be reached from the initial pair using $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}.
We now define \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}^{\mathsf{A}}$ formally. A transition $(\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}} can take place iff and are in symbolic equivalence222 This definition yields infinite executions for \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A}} if no inequivalent pair is met. Each such execution eventually reaches while, in practice, executions are obviously not explored past empty pairs. We chose to introduce this minor gap to make the theory more uniform. .
Each transition for some observable action consists of two steps, i.e. (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A}^{\prime\prime};\mathbf{B}^{\prime\prime}) iff (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) and (\mathbf{A}^{\prime};\mathbf{B}^{\prime})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}^{\prime\prime};\mathbf{B}^{\prime\prime}), where the latter transitions are described below:
- (1)
The first part of the transition consists in performing an observable symbolic action (either or ) followed by all available unobservable () actions. This is done for each extended symbolic process that occurs in the pair of sets, and each possible transition of one such process generates a new element in the target set. Formally, we have (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) if
[TABLE]
and correspondingly for . Note that elements of that cannot perform are simply discarded, and that the constraint systems of individual processes are enriched according to their own transitions whereas the extended part of constraint systems are left unchanged. For a fixed symbolic action , the \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}} transition is deterministic. The choice of names for handles and second-order variables does not matter, and therefore the relation \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A1}} is also finitely branching. 2. (2)
The second part consists in simplifying the constraint systems of until reaching solved forms. This part of the transition is non-deterministic, i.e. several different may be reached depending on various choices, e.g. whether a message is derived by using a function symbol or one of the available handles. Although branching, this part of the transition is finitely branching. Moreover, only extended constraints may change: for any there must be a such that , and similarly for .
An important invariant of this construction is that all the processes occurring in any of the two sets of processes have constraint systems that share a common structure. More precisely the transitions maintain that for any , and occurs in iff it occurs in .
Example \thethm.
Consider the simple basic processes for , a public constant. We illustrate the roles of \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}^{\mathsf{A1}}$ and $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A2}}{} on the pair where . We have that
[TABLE]
where and are the two symbolic processes one may obtain by executing the observable action , depending on the conditional after that input. Specifically, we have:
- •
**
- •
**
After this first step, \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}{} is going to non-deterministically solve the constraint systems. From the latter pair, it will produce only two alternatives. Indeed, if holds then infers that the only recipe that it needs to consider is the recipe . In that case, the only considered solution is . Otherwise, holds but, at this point, no more information is inferred on . Formally,
[TABLE]
where
- •
* and where ;*
- •
.
The content of and is not important. Note that after {\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}}, only one alternative remains (i.e. there is only one extended symbolic process on each side of the resulting pair) because only one of the two processes complies with the choices made in each branch.
Definition \thethm ().
Let and be two processes. We say that when for any pair such that {(\left(\mathcal{P}_{A};\Phi_{A};\emptyset;\emptyset\right);\left(\mathcal{P}_{B};\Phi_{B};\emptyset;\emptyset\right))\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A};\mathbf{B})}.
As announced above, we expect to coincide with trace equivalence. We shall actually prove it (see Section 6.3), after having introduced a few axioms (Section 6.2). We note, however, that this can only hold under some minor assumptions on processes. In practice, does not need those assumptions but they allow for a more concise presentation.
Definition \thethm.
A simple process (resp. symbolic process) is said to be quiescent when A\not\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}} (resp. A\not\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}). An extended symbolic process is quiescent when \lfloor{A^{+}}\rfloor\not\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}.
In \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}} transitions, processes must start by executing an observable action and possibly some actions after that. Hence, it does not make sense to consider \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A}} transitions on processes that can still perform actions. We shall thus establish that and coincide only on quiescent processes, which is not a significant restriction since it is always possible to pre-execute all available -actions before testing equivalences.
6.2. Specification of the procedure
We now list and comment the specification satisfied by the exploration performed by . These statements are consequences of results stated and proved in [18] but it is beyond the scope of this paper to prove them.
Soundness and completeness of constraint resolution
The {\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}^{\mathsf{A2}}}$ step, corresponding to $\mathsf{Apte}$’s constraint resolution procedure, only makes sense under some assumptions on the (common) structure of the processes that are part of the pairs of sets under consideration. Rather than precisely formulating these conditions (which would be at odds with the abstract treatment of extended constraint systems) we start by defining an under-approximation of the set of pairs on which we may apply ${\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A2}}} at some point. We choose this under-approximation sufficiently large to cover pairs produced by the compressed semantics, and we then formulate our specifications in that domain. More precisely, the under-approximation has to cover two things:
- (1)
we have to consider additional disequalities of the form in constraint systems since they are eventually added by our compressed symbolic semantics (see Figure 6); 2. (2)
we have to allow the removal of some extended symbolic process from the original sets since they are eventually discarded by our compressed (resp. reduced) symbolic semantics.
Given an extended symbolic process , we denote the set of extended symbolic processes obtained from by adding into a number of disequalities of the form with . This is then extended to sets of extended symbolic processes as follows: .
Definition \thethm (valid and intermediate valid pairs).
The set of valid pairs is the least set such that:
- •
For all quiescent, symbolic processes and , is valid.
- •
*If is valid and , (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}(\mathbf{A}_{1};\mathbf{B}_{1}), , , , , and (\mathbf{A}_{3};\mathbf{B}_{3})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) then is valid. In that case, the pair is called an intermediate valid pair. *
It immediately follows that (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A};\mathbf{B}) implies that is valid and only made of quiescent, extended symbolic processes. But the notion of validity accomodates more pairs: it will cover pairs accessible under refinements of \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}^{\mathsf{A}}$ based on subset restrictions of $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}. We may note that these pairs are actually pairs that would have been explored by when starting with another pair of processes (e.g. a process that makes explicit the use of trivial conditionals of the form ). Therefore, those pairs do not cause any trouble when they have to be handled by .
Axiom 1** (soundness of constraint resolution).**
Let be an intermediate valid pair such that (\mathbf{A}^{\prime};\mathbf{B}^{\prime})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}^{\prime\prime};\mathbf{B}^{\prime\prime}). Then, for all (resp. ) there exists some (resp. such that (resp. ) and (resp. ).
treats almost symmetrically the two components of the pair of sets on which transitions take place. This is reflected by the fact that axioms concern both sides and are completely symmetric, like Axiom 1. In order to make the following specifications more concise and readable, we state properties only for one of the two sets and consider the other “symmetrically” as well.
The completeness specification is in two parts: it first states that no first-order solution is lost in the constraint resolution process, and then that the branching of \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}} corresponds to different second-order solutions.
Axiom 2** (first-order completeness of constraint resolution).**
Let be an intermediate valid pair. For all and there exists (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}_{2};\mathbf{B}_{2}), and such that and , where (resp. ) is the substitution associated to (resp. to ) w.r.t. . Symmetrically for .
Axiom 3** (second-order consistency of constraint resolution).**
Let be an intermediate valid pair such that (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}_{2};\mathbf{B}_{2}), for some and for some . Then there exists some such that and . Symmetrically for .
Partial solution
In order to avoid performing some explorations when dependency constraints of our reduced semantics are not satisfied, we shall be interested in knowing when all solutions of a given constraint system assign a given recipe to some variable. Such information is generally available in the solved forms computed by , but not always in a complete fashion. We reflect this by introducing an abstract function that represents the information that can effectively be inferred by the procedure.
Definition \thethm (partial solution).
We assume a partial solution333We use the notation to emphasize the fact that the two substitutions do not interact together. They have disjoint domain, i.e. , and no variable of occurs in with . function which maps sets of extended constraints to a substitution, such that for any , there exists such that . We extend to extended symbolic processes: .
Intuitively, given an extended constraint system, the function returns the value of some of its second-order variables (those for which their instantiation is already completely determined). Our specification of the partial solution shall postulate that the partial solution returned by is the same for each extended symbolic process occurring in a pair reached during the exploration. Moreover, there is a monotonicity property that ensures that this partial solution becomes more precise along the exploration.
Axiom 4**.**
We assume the following about the partial solution:
- (1)
For any valid pair , we have that for any . This allows us to simply write when . 2. (2)
For any intermediate valid pair such that (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) and , we have for some .
Example \thethm.
Continuing Example 6.1, we first note that is a valid pair. Second, the exploration (\{Q_{0}\};\{Q_{0}\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\{Q_{1}^{t}\};\{Q_{1}^{t}\}) covers all executions of the form \lfloor{Q_{0}}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{Q_{1}^{t}}\rfloor going to the branch even though the only solution of is . Indeed, if then the message computed by should be equal to and thus no first-order solution is lost as stated by Axiom 2. Moreover, because the value of is already known in , we may have .
6.3. Proof of the original procedure
The procedure, axiomatized as above, can be proved correct w.r.t the regular symbolic semantics \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}} and its induced trace equivalence as defined in Section 4.2. Of course, Axiom 4 is unused in this first result. It will be used later on when implementing our reduced semantics. We first start by establishing that all the explorations performed by correspond to symbolic executions.
This result is not new and has been established from scratch (i.e. without relying on the axioms stated in the previous section) in [18]. Nevertheless, we found it useful to establish that our axioms are sufficient to prove correctness of the original procedure. The proofs provided in the following sections to establish correctness of our optimised procedure follow the same lines as the ones presented below.
Lemma \thethm.
Let be a valid pair such that (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}). Then, for all there is some such that \lfloor{A}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{A^{\prime}}\rfloor for some with . Symmetrically for .
Proof.
We proceed by induction on . When is empty, we have that , and the result trivially holds. Otherwise we have that:
(\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}(\mathbf{A}_{1};\mathbf{B}_{1})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}_{2};\mathbf{B}_{2})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) with .
Let be a process of . By induction hypothesis we have some such that \lfloor{A_{2}}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{A^{\prime}}\rfloor with . By Axiom 1 there is some such that , and by definition of \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A1}} we finally find some such that \lfloor{A}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{A_{1}}\rfloor. To sum up, we have such that \lfloor{A}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{A^{\prime}}\rfloor with . ∎
We now turn to completeness results. Assuming that processes under study are in equivalence (so that will not stop its exploration prematurely), we are able to show that any valid symbolic execution (i.e. a symbolic execution with a solution in its resulting constraint system) is captured by an exploration performed by . Actually, since discards some second-order solution during its exploration, we can only assume that another second-order solution with the same associated first-order solution will be found.
Lemma \thethm.
Let , and be three quiescent, symbolic processes such that , A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A^{\prime}, and . Then there exists an exploration (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) and some , such that , and , where (resp. ) is the substitution associated to (resp. to ) with respect to . Symmetrically for B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}B^{\prime}.
Proof.
By hypothesis, we have that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A^{\prime}. We will first reorganize this derivation to ensure that actions are always performed as soon as possible. Then, we proceed by induction on . When is empty, we have that since is quiescent. Let , , . We have that and therefore , i.e. . We easily conclude.
Otherwise, consider A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A^{\prime} with . Let and . We have that . Since , we also have where . Therefore, we apply our induction hypothesis and we obtain that there exists an exploration (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A}_{1};\mathbf{B}_{1}) and some , such that , , and the first-order substitutions associated to and with respect to are identical. By hypothesis we have , thus . Hence a \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}^{\mathsf{A1}}$ transition can take place on that pair. By definition of $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}} and since \lfloor{A_{1}^{+}}\rfloor=A_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A^{\prime} with quiescent, there must be some (\mathbf{A}_{1};\mathbf{B}_{1})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}(\mathbf{A}_{2};\mathbf{B}_{2}) with , . Thus and we can apply Axiom 2. There exists (\mathbf{A}_{2};\mathbf{B}_{2})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}), , and such that , and the substitutions associated to (resp. ) w.r.t. coincide. To sum up, the exploration
(\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A}_{1};\mathbf{B}_{1})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}(\mathbf{A}_{2};\mathbf{B}_{2})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime})
together with , and satisfy all the hypotheses. ∎
Lemma \thethm.
Let be quiescent symbolic processes such that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A^{\prime}=(\mathcal{P}^{\prime};\Phi^{\prime};\mathcal{S}^{\prime}), and (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) with and for some . Then there exists some such that and . Symmetrically for B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}B^{\prime}.
Proof.
We proceed by induction on . When is empty, we have that (because is quiescent), , and . Let be . We deduce that from the fact that and .
We consider now the case of a non-empty execution:
[TABLE]
Note that, by reordering actions, we can assume to be quiescent. By assumption we have , and for some . By Axiom 1, there exists some such that . By definition of \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A1}} we obtain such that \lfloor{C_{1}}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{C_{2}}\rfloor and (i.e. the sets of extended constraints of and coincide). The first fact implies by monotonicity (where , i.e. second-order variables that occur in the set of non-extended constraints of ), and the second allows us to conclude more strongly that . Since we also have by monotonicity, the induction hypothesis applies and we obtain some with and .
By definition of \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A1}}, and since \lfloor{A^{+}_{1}}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A_{3}\not\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}} ( is quiescent by hypothesis), we have such that and . Therefore, we have that , and the fact that allows us to say that We can finally apply Axiom 3 to obtain some such that and . ∎
Theorem \thethm.
For any quiescent extended simple processes, we have that:
[TABLE]
Proof.
Let , , and . We prove the two directions separately.
() Assume and consider some exploration (\mathbf{A}_{0};\mathbf{B}_{0})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A};\mathbf{B}). We shall establish that . Let be in and . By Lemma 6.3, we have (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{A}\rfloor such that . By hypothesis, there exists such that (\mathcal{P}^{\prime};\Phi^{\prime};\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}B, , and . We can finally apply Lemma 6.3, which tells us that there must be some such that and .
() We now establish assuming . Consider (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A and . If is not quiescent, it is easy to complete the latter execution into (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}A^{\prime}=(\mathcal{P}_{A};\Phi_{A};\mathcal{S}_{A}) and such that is quiescent. By Lemma 6.3 we know that (\mathbf{A}_{0};\mathbf{B}_{0})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}}(\mathbf{A};\mathbf{B}) with , , with and where (resp. ) is the substitution associated to (resp. ) w.r.t. . By assumption we have and thus there exists some with , and where is the substitution associated to w.r.t. . By Lemma 6.3 we have (\mathcal{P}^{\prime};\Phi^{\prime};\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}\lfloor{B}\rfloor with . To conclude the proof, it remains to show that and that where is the substitution associated to w.r.t. .
For any , we have , , and
[TABLE]
where is the first-order variable associated to in . Since , we deduce that , and therefore , and its associated substitution w.r.t. coincides with , and therefore is a direct consequence of and . ∎
6.4. Integrating compression
We now discuss the integration of the compressed semantics of Section 4 as a replacement for the regular symbolic semantics in .
Although our compressed semantics \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{c} has been defined as executing blocks rather than elementary actions, we allow ourselves to view it in a slightly different way in this section: we shall assume that the symbolic compressed semantics deals with elementary actions and enforces that those actions, when put together, form a prefix of a sequence of blocks that can actually be executed (for the process under consideration) in the compressed semantics of Section 4. This can easily be obtained by means of extra annotations at the level of processes, and we will not detail that modification. This slight change makes it simpler to integrate compression into , both in the theory presented here and in the implementation.
Definition \thethm.
Given two sets of extended symbolic processes , and an observable action , we write (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A1}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) when
[TABLE]
and similarly for . We say that (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\mathbf{A}^{\prime\prime};\mathbf{B}^{\prime\prime}) when (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A1}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) and (\mathbf{A}^{\prime};\mathbf{B}^{\prime})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}^{\prime\prime};\mathbf{B}^{\prime\prime}).
Finally, given two simple extended processes and , we say that when for any (\{\lceil{(\mathcal{P}_{A};\Phi_{A};\emptyset)}\rceil\};\{\lceil{(\mathcal{P}_{B};\Phi_{B};\emptyset)}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\mathbf{A};\mathbf{B}).
As expected, \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}_{c}^{\mathsf{A1}}$ allows to consider much fewer explorations than with the original $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A1}}. It inherits the features of compression, prioritizing outputs, not considering interleavings of outputs, executing inputs only under focus, and preventing executions beyond improper blocks. These constraints apply to individual processes in , but we remark that they also have a global effect in \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{c}^{\mathsf{A1}}, e.g. all processes of must start a new block simultaneously: recall that the beginning of a block corresponds to an input after some outputs, and such inputs can only be executed if no more outputs are available.
Example \thethm.
Continuing Example 6.2, there is only one non-trivial444 We dismiss here the (infinitely many) transitions obtained for infeasible actions, which yield . compressed exploration of one action from the valid pair . It corresponds to the output on channel : (\{Q_{1}^{t}\};\{Q_{1}^{t}\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\{Q_{2}\},\{Q_{2}\}) for . In particular, for any , we have (\{Q_{1}^{t}\};\{Q_{1}^{t}\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\emptyset;\emptyset).
Observe that, because \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}_{c}^{\mathsf{A}}$ is obtained from $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}^{\mathsf{A}} by a subset restriction in \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}^{\mathsf{A1}}$ up to some disequalities, we have that $(\mathbf{A}^{\prime};\mathbf{B}^{\prime})$ is a valid pair when $(\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime})$ for some quiescent, symbolic processes $A,B$ having empty sets of constraints. Following the same reasoning as the one performed in Section [6.3](#S6.SS3), we can establish that $\approx^{s}_{c}{}$ coincides with $\approx^{\mathsf{A}}_{c}$. The main difference is that $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c} already ignores -actions, and therefore we do not need to apply the operator.
Lemma \thethm.
Let be a valid pair such that (\mathbf{A};\mathbf{B})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}). Then, for all there is some such that \lfloor{A}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}\lfloor{A^{\prime}}\rfloor. Symmetrically for .
Lemma \thethm.
Let , , and be three quiescent, symbolic processes such that , A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime} and . Then there exists an exploration (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) and some , such that and , where (resp. ) is the substitution associated to (resp. to ) with respect to . Symmetrically for B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}B^{\prime}.
Lemma \thethm.
Let and be quiescent, simple symbolic processes such that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime}=(\mathcal{P}^{\prime};\Phi^{\prime};\mathcal{S}^{\prime}), , and (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) with for some . Then there exists some such that and . Symmetrically for B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}B^{\prime}.
Theorem \thethm.
For any quiescent extended simple processes, we have that:
[TABLE]
6.5. Integrating dependency constraints in
We now define a final variant of explorations, which integrates the ideas of Section 5 to further reduce redundant explorations. We can obviously generate dependency constraints in , just like we did in Section 5, but the real difficulty is to exploit them in constraint resolution to prune some branches of the exploration performed by . Roughly, we shall simply stop the exploration when reaching a state for which we know that all of its solutions violate dependency constraints. To do that, we rely on the notion of partial solution introduced in Section 6.1. In other words, we do not modify ’s constraint resolution, but simply rely on information that it already provides to know when dependency constraints become unsatisfiable. As we shall see, this simple strategy is very satisfying in practice.
Definition \thethm.
We define \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}_{r}^{\mathsf{A}}$ as the greatest relation contained in $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}} and such that, for any symbolic processes and with empty constraint sets, (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{r}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) implies that there is no such that for all we have , and .
Finally, given two simple extended process and , we say that when for any pair such that ((\mathcal{P}_{A};\Phi_{A};\emptyset;\emptyset);(\mathcal{P}_{B};\Phi_{B};\emptyset;\emptyset))\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{r}^{\mathsf{A}}(\mathbf{A};\mathbf{B}).
Example \thethm.
Continuing Example 6.4, consider the following compressed exploration, where contains the constraints , , and :
[TABLE]
Assuming that (which is the case in the actual procedure) this compressed exploration is not explored by \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{r}^{\mathsf{A}} because
[TABLE]
Lemma \thethm.
Let , and be quiescent, simple symbolic processes such that , A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime}, and . Then there exists an exploration (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{r}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) and some , such that and , where (resp. ) is the substitution associated to (resp. to ) with respect to . Symmetrically for B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}B^{\prime}.
Proof.
We proceed by induction on . The empty case is easy. Otherwise, consider A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A_{3}=(\mathcal{P}_{3};\Phi_{3};\mathcal{S}_{3}) with , quiescent, and . Let and . We also have and , so the induction hypothesis applies and we obtain (\{\lceil{A}\rceil\};\{\lceil{B}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{r}^{\mathsf{A}}(\mathbf{A}_{1};\mathbf{B}_{1}) with , and such that the first-order substitutions associated to and w.r.t. coincide.
By hypothesis we have , thus . Hence a \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}_{c}^{\mathsf{A1}}$ transition can take place on that pair. By definition of $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A1}} and since \lfloor{A_{1}^{+}}\rfloor=A_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A_{3}, there must be some (\mathbf{A}_{1};\mathbf{B}_{1})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A1}}(\mathbf{A}_{2};\mathbf{B}_{2}) with , . Thus and we can apply Axiom 2 to obtain (\mathbf{A}_{2};\mathbf{B}_{2})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}^{\mathsf{A2}}(\mathbf{A}_{3};\mathbf{B}_{3}) with , and such that the subsitutions associated to and w.r.t. coincide.
It only remains to show that this extra execution step in \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}_{c}^{\mathsf{A}}$ is also present in $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{r}^{\mathsf{A}}, i.e. that does not violate in the sense of Definition 6.5. This is because, by definition of the partial solution, we have that for some , so that if violated then we would have . Since and induce the same first-order substitutions with respect to , we would finally have , contradicting the hypothesis on . ∎
Theorem \thethm.
For any quiescent initial simple processes and , we have that:
[TABLE]
Proof.
Let and be two quiescent, initial simple processes. Thanks to our previous results, we have that implies . Then, we obviously have : for any (\{\lceil{(\mathcal{P};\Phi;\emptyset)}\rceil\};\{\lceil{(\mathcal{Q};\Psi;\emptyset)}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{r}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) we have (\{\lceil{(\mathcal{P};\Phi;\emptyset)}\rceil\};\{\lceil{(\mathcal{Q};\Psi;\emptyset)}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) by definition of \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{r}^{\mathsf{A}}, and thus by hypothesis.
For the other direction, it suffices to show that implies . Let (\mathcal{P};\Phi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime}=(\mathcal{P}^{\prime};\Phi^{\prime};\mathcal{S}^{\prime}) with and . By Lemma 6.5 we have (\{\lceil{(\mathcal{P};\Phi;\emptyset)}\rceil\};\{\lceil{(\mathcal{Q};\Psi;\emptyset)}\rceil\})\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{r}^{\mathsf{A}}(\mathbf{A}^{\prime};\mathbf{B}^{\prime}) with , such that and where (resp. ) is the substitution associated to (resp. ) w.r.t. .
Since , we have : there must be some such that and where is the substitution associated to w.r.t. . By Lemma 6.4 we have (\mathcal{Q};\Psi;\emptyset)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}\lfloor{B^{+}}\rfloor. Furthermore, we can show as before (see the end of the proof of Theorem 6.3) that and , where is the substitution associated to w.r.t. . Finally, by , (i.e. sets of handles that second-order variables may use coincide), and , we obtain that . ∎
6.6. Benchmarks
The optimisations developed in the present paper have been implemented, following the above approach, in the official version of [23].
In practice, many processes enjoy a nice property that allows one to ensure that non-blocking outputs will never occur: it is often the case that enough tests have been performed before outputting a term to ensure its validity.
Example \thethm.
Consider the following process, where is assumed to be valid (e.g. because it is a pure constructor term):
[TABLE]
The term outputted during an execution is necessarily valid thanks to the test that is performed just before this output.
We exploit this property in order to avoid adding additional disequalities when integrating compression in . Therefore, in this section, we will restrict ourselves to simple processes that are non-blocking as defined below.
Definition \thethm.
Let be a simple process. We say that is non-blocking if is valid for any , , , , , such that (\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}(\{\mathtt{out}(c,u).Q^{\prime}\}\cup\mathcal{Q};\Psi).
This condition may be hard to check in general, but it is actually quite easy to see that it is satisfied on all of our examples. Roughly, enough tests are performed before any output action, and this ensures the validity of the term when the output action becomes reachable, as in Example 6.6.
Our modified version of can verify our optimised equivalences in addition to the original trace equivalence. It has been integrated into the main development line of the tool. The modifications of the code ( 2kloc) are summarized at
https://github.com/lutcheti/APTE/compare/ref...APTE:POR
For reference, the version of that we are using in the benchmarks below is available at https://github.com/APTE/APTE/releases/tag/bench-POR-LMCS together with all benchmark files, in subdirectory bench/protocols. More details, including instructions for reproducing our benchmarks are available at http://www.lsv.fr/~hirschi/apte_por.
We ran the tool (compiled with OCaml 3.12.1) on a single 2.67GHz Xeon core (memory is not relevant) and compared three different versions:
- •
reference: the reference version without our optimisations (i.e. );
- •
compression: using only the compression optimisation (i.e. );
- •
reduction: using both compression and reduction (i.e. ).
We first show examples in which equivalence holds. They are the most significant, because the time spent on inequivalent processes is too sensitive to the order in which the (depth-first) exploration is performed.
Toy example.
We consider a parallel composition of roles as defined in Example 6.1: . When executed in the regular symbolic semantics \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}$}}$, the $2n$ actions of $P_{n}$ may be interleaved in $(2n)!/2^{n}$ ways in a trace containing all actions. In the compressed symbolic semantics $\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}, the actions of individual processes must be bundled in blocks, so there are only interleavings containing all actions. In the reduced symbolic semantics \mathrel{\raisebox{-0.5pt}[5.0pt]{\xmapsto{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}}}_{r}, only one interleaving of that length remains: the trace cannot deviate from the priority order, since the only way to satisfy a dependency constraint would be to feed an input with a message that cannot be derived without some previously output nonce , but in that case the message will not be and the trace won’t be explored further. Note that there is still an exponential number of symbolic traces in the reduced semantics when one takes into account traces with less than actions.
We show in Figure 8 the time needed to verify for to in the three versions of described above: reference, compression and reduction. The results, in logarithmic scale, show that each of our optimisations brings an exponential speedup, as predicted by our theoretical analysis. Similar improvements are observed if one compares the numbers of explored pairs rather than execution times.
Denning-Sacco protocol.
We ran a similar benchmark, checking that Denning-Sacco ensures strong secrecy in various scenarios. The protocol has three roles and we added processes playing those roles in turn, starting with three processes in parallel.
Srong secrecy is expressed by considering, after one of the roles B, the output of a message encrypted with the established key on one side of the equivalence, and with a fresh key on the other side.
The results are plotted in Figure 9. The fact that we add one role out of three at each step explains the irregular growth in verification time. We still observe an exponential speedup for each optimisation.
Practical impact.
Finally, we illustrate how our optimisations make much more useful in practice for investigating interesting scenarios. Verifying a single session of a protocol brings little assurance into its security. In order to detect replay attacks and to allow the attacker to compare messages that are exchanged, at least two sessions should be considered. This means having at least four parallel processes for two-party protocols, and six when a trusted third party is involved. This is actually beyond what the unoptimised can handle in a reasonable amount of time. We show in Figure 10 how many parallel processes could be handled in hours by on various use cases of protocols, for the same three variants of as before, i.e. reference, compression and reduction. We verify an anonymity property for the Passive Authentication protocol of e-passports. For other protocols, we analyse strong secrecy of established keys:
for one of the roles we add, on one side of the equivalence, an output encrypted by the established key and, on the other side, an output encrypted by a fresh key.
We finally present the benefits of our optimisations for discovering attacks. We performed some experiments on flawed variants of protocols,
shown in Figure 11, corresponding to example files in subdirectory bench/protocols/attacks/ of the above mentioned release. The scenario Denning-Sacco A expresses strong secrecy of the (3-party) Denning-Sacco protocol, but this time on two instances of roles at the same time (instead of one as in Figure 10). In Denning-Sacco B, we consider again a form of strong secrecy expressed by outputting encrypted messages but this time at the end of role B. The Needham-Schroeder pub scenario corresponds to strong secrecy of the public-key Needham-Schroder protocol. The E-Passport PA exposed experiments show that anonymity is (obviously) lost with the Passive Authentication protocol when the secret key is made public. Similarly, the Yahalom exposed experiment shows that strong secrecy of Yahalom is lost when secrets keys are revealed.
Since stops its exploration as soon as an attack is found, the time needed for to find the attack highly depends on the order in which the depth-first exploration is performed. However, as shown in Figure 11, we always observe in practice dramatic improvements brought by our optimisations compared to the reference version of . In some cases, our optimisations are even mandatory for to find the attack using reasonable resources.
7. Related Work
The techniques we have presented borrow from standard ideas from concurrency theory and trace theory. Blending all these ingredients, and adapting them to the demanding framework of security protocols, we have come up with partial order reduction techniques that can effectively be used in symbolic verification algorithms for equivalence properties of security protocols. We now discuss related work, and there is a lot of it given the huge success of POR techniques in various application areas. We shall focus on the novel aspects of our approach, and explain why such techniques have not been needed outside of security protocol analysis. These observations are not new: as pointed out by Baier and Katoen [11], “[POR] is mainly appropriate to control-intensive applications and less suited for data-intensive applications”; Clarke et al. [25] also remark that “In the domain of model checking of reactive systems, there are numerous techniques for reducing the state space of the system. One such technique is partial-order reduction. This technique does not directly apply to [security protocol analysis] because we explicitly keep track of knowledge of various agents, and our logic can refer to this knowledge in a meaningful way.” We first compare our work with classical POR techniques, and then comment on previous work in the domain of security protocol analysis.
7.1. Classical POR
Partial order reduction techniques have proved very useful in the domain of model checking concurrent programs. Given a Labelled Transition System (LTS) and some property to check (e.g. a Linear Temporal Logic formula), the basic idea of POR [41, 34, 11] is to only consider a reduced version of the given LTS whose transitions of some states might be not exhaustive but are such that this transformation does not affect the property. POR techniques can be categorized in two groups [34]. First, the persistent set techniques (e.g. stubborn sets, ample sets) where only a sufficiently representative subset of available transitions is explored. Second, sleep set techniques memoize past exploration and use this information along with available transitions to disable some provably redundant transitions. Note that these two kinds of techniques are compatible, and are indeed often combined to obtain better reductions. Theoretical POR techniques apply to transition systems which may not be explicitly available in practice, or whose explicit computation may be too costly. In such cases, POR is often applied to an approximation of the LTS that is obtained through static analysis. Another, more recent approach is to use dynamic POR [31, 45, 3] where the POR arguments are applied based on information that is obtained during the execution of the system.
Clearly, classical POR techniques would apply to our concrete LTS, but that would not be practically useful since this LTS is wildly infinite, taking into account all recipes that the attacker could build. Applying most classical POR techniques to the LTS from which data would have been abstracted away would be ineffective: any input would be dependent on any output (since the attacker’s knowledge, increased by the output, may enable new input messages). Our compression technique lies between these two extremes. It exploits a semi-commutation property: outputs can be permuted before inputs, but not the converse in general. Further, it exploits the fact that inputs do not increase the attacker’s knowledge, and can thus be executed in a chained fashion, under focus. The semi-commutation is reminiscent of the asymmetrical dependency analysis enabled by the conditional stubborn set technique [34], and the execution of inputs under focus may be explained by means of sleep sets. While it may be possible to formally derive our compressed semantics by instantiating abstract POR techniques to our setting, we have not explored this possibility in detail555 Although this would be an interesting question, we do not expect that any improvement of compression would come out of it. Indeed, compression can be argued to be maximal in terms of eliminating redundant traces without analysing data: for any compressed trace there is a way to choose messages and modify tests to obtain a concrete execution which does not belong to the equivalence class of any other compressed trace. . Concerning our reduced semantics, it may be seen as an application of the sleep set technique (or even as a reformulation of Anisimov’s and Knuth’s characterization of lexicographic normal forms) but the real contribution with this technique is to have formulated it in such a way (see Definition 5.1) that it can be implemented without requiring an a priori knowledge of data dependencies: it allows us to eliminate redundant traces on-the-fly as data (in)dependency is discovered by the constraint resolution procedure (as explained in Section 6.5)—in this sense, it may be viewed as a case of dynamic POR.
Narrowing the discussion a bit more, we now focus on the fact that our techniques are designed for the verification of equivalence properties. This requirement turns several seemingly trivial observations into subtle technical problems. For instance, ideas akin to compression are often applied without justification (e.g. in [44, 45, 40]) because they are obvious when one does reachability rather than equivalence checking. To understand this, it is important to distinguish between two very different ways of applying POR to equivalence checking (independently of the precise equivalence under consideration). The first approach is to reduce a system such that the reduced system and the original systems are equivalent. In the second approach, one only requires that two reduced systems are equivalent iff the original systems are equivalent. The first approach seems to be more common in the POR literature (where one finds, e.g. reductions that preserve LTL-satisfiability [11] or bisimilarity [37]) though there are instances of the second approach (e.g. for Petri nets [33]). In the present work, we follow the second approach: neither of our two reduction techniques preserves trace equivalence. This allows stronger reductions but requires extra care: one has to ensure that the independencies used in the reduction of one process are also meaningful for the other processes; in other words, reduction has to be symmetrical. We come back to these two different approaches later, when discussing specific POR techniques for security.
7.2. Security applications
The idea of applying POR to the verification of security protocols dates back, at least, to the work of Clarke et al. [25, 26]. In this work, the authors remark that traditional POR techniques cannot be directly applied to security mainly because “[they] must keep track of knowledge of various agents” and “[their] logic can refer to this knowledge in a meaningful way”. This led them to define a notion of semi-invisible actions (output actions, that cannot be swapped after inputs but only before them) and design a reduction that prioritizes outputs and performs them in a fixed order. Compared to our work, this reduction is much weaker (even weaker than compression only), only handles a finite set of messages, and only focuses on reachability properties checking.
In [30], the authors develop “state space reduction” techniques for the Maude-NRL Protocol Analyzer (Maude-NPA). This tool proceeds by backwards reachability analysis and treats at the same level the exploration of protocol executions and attacker’s deductions. Several reductions techniques are specific to this setting, and most are unrelated to partial order reduction in general, and to our work in particular. We note that the lazy intruder techniques from [30] should be compared to what is done in constraint resolution procedures (e.g. the one used in ) rather than to our work. A simple POR technique used in Maude-NPA is based on the observation that inputs can be executed in priority in the backwards exploration, which corresponds to the fact that we can execute outputs first in forward explorations. We note again that this is only one aspect of the focused strategy, and that it is not trivial to lift this observation from reachability to trace equivalence. Finally, a “transition subsumption” technique is described for Maude-NPA. While highly non-trivial due to the technicalities of the model, this is essentially a tabling technique rather than a partial order reduction. Though it does yield a significant state space reduction (as shown in the experiments [30]) it falls short of exploiting independencies fully, and has a potentially high computational cost (which is not evaluated in the benchmarks of [30]).
In [32], Fokkink et al. model security protocols as labeled transition systems whose states contain the control points of different agents as well as previously outputted messages. They devise some POR technique for these transition systems, where output actions are prioritized and performed in a fixed order. In their work, the original and reduced systems are trace equivalent modulo outputs (the same traces can be found after removing output actions). The justification for their reduction would fail in our setting, where we consider standard trace equivalence with observable outputs. More importantly, their requirement that a reduced system should be equivalent to the original one makes it impossible to swap input actions, and thus reductions such as the execution under focus of our compressed semantics cannot be used. The authors leave as future work the problem of combining their algorithm with symbolic executions, in order to be able to lift the restriction to a finite number of messages.
Cremers and Mauw proposed [29] a reduction technique for checking secrecy in security protocols. Their method allows to perform outputs eagerly, as in our compressed semantics. It also uses a form of sleep set technique to avoid redundant interleavings of input actions. In addition to being applicable only for reachability property, the algorithm of [29] works under the assumption that for each input only finitely many input messages need to be considered. The authors identify as important future work the need to lift their method to the symbolic setting.
Earlier work by Mödersheim et al. has shown how to combine POR techniques with symbolic semantics [40] in the context of reachability properties for security protocols. This has led to high efficiency gains in the OFMC tool of the AVISPA platform [7]. While their reduction is very limited, it brings some key insight on how POR may be combined with symbolic execution. For instance, their reduction imposes a dependency constraint (called differentiation constraint in their work) on the interleavings of
[TABLE]
Assuming that priority is given to the process working on channel , this constraint enforces that any symbolic interleaving of the form would only be explored for instances of that depend on . Our reduced semantics constrains patterns of arbitrary size (instead of just size 2 diamond patterns as above) by means of dependency constraints. Going back to Example 5.1, their technique will only be able (at most) to exploit the dependencies depicted in plain blue arrows, and they will not consider the one represented by the dashed 2-arrow.
Moreover, while we generate dependency constraints on the fly, they implement their technique by looking for such a pattern afterwards.
This causes a tradeoff between reduction and the cost of redundancy detection: their technique fails to detect all patterns of this kind. Besides these differences, we note that Mödersheim et al. use dependency constraints to guide a dedicated constraint resolution procedure, while we chose to treat constraint resolution (almost) as a black box, and leave it unchanged. Finally, we recall that our POR technique has been designed to be sound and complete for trace equivalence checking as well as reachability checking.
Finally, in [10], the authors of the present paper extend some of the results presented here. Instead of considering the syntactic fragment of simple processes, we work under the more general semantical assumption of action-determinism. We show that compression and reduction can be extended to that case, preserving the main result: the induced equivalences coincide. However, that work is completely carried out in concrete rather than symbolic semantics. Thus, this development should be viewed as being orthogonal to the one carried out in the present paper. The main ideas behind the integration in symbolic semantics and would apply to the action-deterministic case as well. The line of research followed in [10], that consists in extending the supported fragment for our POR techniques, is still open: it would be interesting to support processes that are not action-deterministic, which are commonplace when analysing anonymity or unlinkability scenarios.
8. Conclusion
We have developed two POR techniques that are adequate for verifying trace equivalence properties between simple processes. The first refinement groups actions in blocks, while the second one uses dependency constraints to restrict to minimal interleavings among a class of permutations. In both cases, the refined semantics has less traces, yet we show that the associated trace equivalence coincides with the standard one. We have effectively implemented these refinements in , and shown that they yield the expected, significant benefit.
We claim that our POR techniques – at least compression – and the significant optimisations they allow are generic enough to be applicable to other verification methods as long as they perform forward symbolic executions. In addition to the integration in Apte we have extensively discussed, we also have successfully done so in Spec [35]. Furthermore, parts of our POR techniques have been independently integrated and implemented in the distributed version of 666See https://github.com/akiss/akiss..
We are considering several directions for future work. Regarding the theoretical results presented here, it is actually possible to slightly relax the syntactic condition we imposed on processes by an action-determinism hypothesis and apply our reduction techniques on replicated processes [10]. The question of whether the action-determinism condition can be removed without degrading the reductions too much is left open. Another interesting direction would be to adapt our techniques for verification methods based on backward search instead of forward search as is the case in this paper. We also believe that stronger reductions can be achieved: for instance, exploiting symmetries should be very useful for dealing with multiple sessions. Regarding the practical application of our results, we can certainly go further. We could investigate the role of the particular choice of the order , to determine heuristics for maximising the practical impact of reduction.
Acknowledgements
We would like to thank Vincent Cheval for interesting discussions and comments, especially on Section 6.
Appendix A Notations
[TABLE]
Appendix B Proofs of Section 3
See 3.2
Proof.
It suffices to establish that implies for any .
- •
Assume that we have with . Because we are considering simple processes, the two actions must be concurrent. More specifically, our process must be of the form with (resp. ) being a basic process on channel (resp. ). We assume that in our sequence of reductions, actions pertaining to are all executed before reaching , and that actions pertaining to are executed last. This is without loss of generality, because a action on a given basic process can easily be permuted with actions taking place on another basic process, since it does not depend on the context and has no effect on the frame. Thus we have that , . Since the actions taking place on rely neither on the frame nor on the first two basic processes, we easily obtain the permuted execution:
[TABLE]
- •
The permutation of two input actions on distinct channels is very similar. In this case, the frame does not change at all, and the order in which messages are derived from the frame does not matter. Moreover, the instantiation of the input variable on one basic process has no impact on the other ones.
- •
Assume that we have with and . Again, the two actions are concurrent, and we can assume that actions are organized conveniently so that is of the form with (resp. ) a basic process on (resp. ); is of the form ; and is of the form . As before, the actions from to are easily moved around. Additionally, implies and thus we have:
[TABLE]
The next step is trivial:
[TABLE]
- •
We also have to perform the reverse permutation, but we shall not detail it; this time we are delaying the derivation of from the frame, and it only gets easier.∎
See 3.2
Proof.
We first observe that implies if is initial and is a (possibly empty) sequence of output actions on the same channel. We prove this by induction on the sequence of actions. If it is empty, we can conclude using one of the Proper rules because is initial. Otherwise, we have:
[TABLE]
We obtain by induction hypothesis, and conclude using rules Tau and Out.
The next step is to show that implies , if is initial and is the concatenation of a (possibly empty) sequence of inputs and a non-empty sequence of outputs, all on the same channel. This is easily shown by induction on the number of input actions. If there are none we use the previous result, otherwise we conclude by induction hypothesis and using rules Tau and In. Otherwise, the first output action allows us to conclude from the previous result and rules Tau and Out.
We can now show that implies if is initial and is a proper block. Indeed, we must have
[TABLE]
which allows us to conclude using the previous result and rules Tau and In.
We finally obtain that implies A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime} when and are initial simple processes and is a sequence of proper blocks. This is done by induction on the number of blocks. The base case is trivial. Because is initial, the execution of its basic processes can only start with observable actions, thus only one basic process is involved in the execution of the first block. Moreover, we can assume without loss of generality that the execution of this first block results in another initial process: indeed the basic process resulting from that execution is either in the final process , which is initial, or it will perform another block, i.e. it can perform actions followed by an input, in which case we can force those actions to take place as early as possible. Thus we have
[TABLE]
where is a proper block, and we conclude using the previous result and the induction hypothesis. ∎
Before proving Theorem 3.2, we establish the following result.
Proposition \thethm.
Let be a trace of observable actions such that, for any channel occurring in the trace, it appears first in an input action. There exists a sequence of proper blocks and a sequence of improper blocks such that .
Proof.
We proceed by induction on the length of , and distinguish two cases:
- •
If has no output action then, by swapping input actions on distinct channels, we reorder so as to obtain where the ’s are pairwise distinct and is an improper block on channel .
- •
Otherwise, there must be a decomposition such that does not contain any output. We can perform swaps involving input actions of on all channel , so that they are delayed after the first output on . We obtain with . Next, we swap output actions on channel from that are not preceded by another input on , so as to obtain
[TABLE]
such that either does not contain any action on channel or the first one is an input action. We have thus isolated a first proper block, and we can conclude by induction hypothesis on .∎
Note that the above result does not exploit all the richness of . In particular, it never relies on the possibility to swap an input action before an output when the input message does not use the output handled. Indeed, the idea behind compression does not rely on messages. This is no longer the case in Section 5 where we use more fully.
We finally prove the main result about the compressed semantics relying on Proposition B stated and proved above. Given two simple process and , we shall write (or even ) instead of .
See 3.2
Proof.
We prove the two directions separately.
Let be an initial simple process such that and {A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A^{\prime}}. One can easily see that the trace must be of the form where is made of proper blocks and is a (possibly empty) sequence of inputs on the same channel . We have:
[TABLE]
Using Proposition 3.2, we obtain that . We also claim that for some having the same frame as which is itself equal to the one of . This is obvious when is empty—in that case we can simply choose . Otherwise, the execution of the improper block results from the application of rule Improper. Except for the fact that this rule “kills” the resulting process, its subderivation simply packages a sequence of inputs, and so we have a suitable . We thus have:
[TABLE]
By hypothesis, it implies that and with and . Relying on the fact that is a simple process, we have:
[TABLE]
It remains to establish that B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}B^{\prime} such that . We can assume that does not have any basic process starting with a test, without loss of generality since forcing actions cannot break static equivalence. Further, we observe that is initial. Otherwise, it would mean that a basic process of is not initial (absurd) or that one of the blocks of , which are maximal for , is not maximal for (absurd again, because it contradicts ). This allows us to apply Proposition 3.2 to obtain
[TABLE]
This concludes when is empty, because . Otherwise, we note that cannot perform any action on channel , because the execution of in the compressed semantics must be maximal. Since , it must be that cannot perform any observable action on the channel either. Thus can complete an improper step:
[TABLE]
We can finally conclude that B\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}B^{\prime} with .
Let be an initial simple process such that and . We “complete” this execution as follows:
- •
We force actions whenever possible.
- •
If the last action on in is an input, we trigger available inputs on using a valid public constant as a recipe.
- •
We trigger all the outputs that are available and not blocked.
We obtain a trace of the form . Let be the process obtained from this trace:
[TABLE]
We observe that is initial. Indeed, for each basic process that performs actions in , we have that:
- •
either the last action on its channel is an output and the basic process is of the form or with ,
- •
or the last action is an input and the basic process is reduced to [math] and disappears, or it is an output which is blocked.
Next, we apply Proposition B to obtain traces (resp. ) made of proper (resp. improper) blocks, such that . By Lemma 3.2 we know that this permuted trace can also lead to :
[TABLE]
As before, we can assume that cannot perform any action. Under this condition, since is initial, must also be initial.
By Proposition 3.2 we have that A\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A_{io}, and implies that:
[TABLE]
A simple inspection of the Proper rules shows that a basic process resulting from the execution of a proper block must be initial. Thus, since the whole simple process is initial, is initial too.
Thanks to Proposition 3.2, we have that . Our goal is now to prove that we can complete this execution with . This trace is of the form where contains only inputs on channel and the are pairwise disjoint. Now, we easily see that for each ,
[TABLE]
and has no more atomic process on channel . Thus we have A_{io}\mathrel{\raisebox{-0.5pt}[5.0pt]{\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{}}}}}_{c}A_{i}^{0} with . Since , we must have some such that:
[TABLE]
We can translate this back to the regular semantics, obtaining . We can now execute all these inputs to obtain an execution of towards some process :
[TABLE]
Permuting those actions, we obtain thanks to Lemma 3.2:
[TABLE]
We observe that , and it follows that because those frames have the same domain, which is a subset of that of . ∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proc. 28th Symposium on Principles of Programming Languages (POPL’01) , pages 104–115. ACM Press, 2001.
- 2[2] M. Abadi and C. Fournet. Private authentication. Theoretical Computer Science , 322(3):427–476, 2004.
- 3[3] P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas. Optimal dynamic partial order reduction. ACM SIGPLAN Notices , 49(1):373–384, 2014.
- 4[4] J.-M. Andreoli. Logic programming with focusing proofs in linear logic. J. Log. Comput. , 2(3), 1992.
- 5[5] M. Arapinis, T. Chothia, E. Ritter, and M. Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In Proc. 23rd Computer Security Foundations Symposium (CSF’10) , pages 107–121. IEEE Comp. Soc. Press, 2010.
- 6[6] A. Armando, R. Carbone, L. Compagna, J. Cuellar, and L. T. Abad. Formal analysis of saml 2.0 web browser single sign-on: Breaking the saml-based single sign-on for google apps. In Proc. 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008) , pages 1–10, 2008.
- 7[7] A. Armando et al. The AVISPA Tool for the automated validation of internet security protocols and applications. In Proc. 17th Int. Conference on Computer Aided Verification (CAV’05) , LNCS. Springer, 2005.
- 8[8] A. Armando et al. The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings , pages 267–282, 2012.