1 Introduction↩︎

Diffie-Hellman groups and their algebraic properties are the basis of many key exchange protocols, signature schemes, and symmetric encryption schemes. Diffie-Hellman groups are cyclic groups, defined by a group operation \(\cdot:G\times G \rightarrow G\) and a generator \(g\). For a natural number \(n\), we define \(g^n\) to denote \(g\cdot ...\cdot g\) applied \(n\) times.¹ By the definition of the group operators, \((g^a)^b=g^{ab}\) and \(g^a\cdot g^b=g^{a+b}\). Diffie-Hellman groups must furthermore satisfy the following property: finding \(a\) from \(g^a\) must be computationally hard. Examples of such groups are some modular arithmetic groups and some elliptic curves.

Given the widespread use of Diffie-Hellman groups in security protocols, there has been considerable effort to support these group operations in automatic protocol verification tools. Most state-of-the-art tools (Tamarin, ProVerif, Maude-NPA, etc.) can model Diffie-Hellman groups in some way. However, their models are restricted: they support exponentiation and multiplication of exponents, but none can model the multiplication of group elements and hence the addition of exponents.

Several challenges make modelling Diffie-Hellman group multiplication with these tools difficult. These tools operate in the symbolic model of cryptography, using equational theories to represent cryptographic primitives. Moreover, they rely on unification in their proof search. When the multiplication of group elements is considered, the exponents in Diffie-Hellman groups form a field. First, it is not straightforward to describe a field by an equational theory and hence any approach taken will use an equational theory that approximates fields. Second, to be practically useful, such an approximation must include associativity and commutativity of both the addition and the multiplication operator, and distributivity of multiplication over addition. Unfortunately, this interaction between distributivity and associativity makes unification both undecidable and infinitary [1]. Namely, the unification problem may have as a solution an infinite set of most general unifiers. So even if we had an algorithm enumerating all unifiers, this would be impractical for automated tools that use unification.

In this paper, we provide a semi-decision procedure for determining whether a protocol model that uses the full Diffie-Hellman group structure satisfies a given property, for a class of user-defined properties. Our approach does not rely on direct unification. Our starting point takes as inspiration results from Dougherty and Guttman [2], [3], who proposed a rewrite system containing both distributivity and associativity that closely approximates fields in the following sense: any theorem that can be proven using this rewrite system (henceforth called \(\mathit{DH}\)) holds in all Diffie-Hellman group structures. Conversely, any equation that holds in infinitely many Diffie-Hellman structures is a theorem of the \(\mathit{DH}\) rewrite system. Dougherty and Guttman showed how this system can be used to prove the security of a restricted class of protocols. In our work, we target a wider class of protocols, and show how to integrate this approach into the Tamarin prover [4]. To the best of our knowledge, this is the first time an automated verification tool succeeds in analyzing protocols based on this mathematical structure.

We restrict our results to protocols and properties that satisfy the following two conditions.

C1

We assume that all terms that represent group elements belong to the same group. In other words, we assume there is a fixed group generator \(g\), and all group elements are of the form \(g^{e}\) for some exponent \(e\) (possibly containing the addition operator).

C2

Our approach is applicable to security properties that contain terms whose subterms do not cancel each other out. For example, this holds for any term that does not contain the \(+\) or \(\cdot\) operator.

Since most protocols require parties to use a common fixed group, C1 is a modest restriction. The assumption C2 concerns the properties covered. In particular, it excludes making security verdicts about a term that can cancel itself out, i.e., which can be reduced to \(1\) or \(0\). It does not exclude the other terms in the protocol canceling out. If a term can reduce to \(1\) or \(0\), then it is likely that it will not satisfy many basic security properties (e.g. secrecy). Hence we expect that in most cases, either we find an attack for the property, or the protocol’s design and the property specification provide sufficient conditions to guarantee the non-cancellation assumption where necessary. The main idea of our approach is to first work with sub-terms in a simplified equational theory that does not contain the group multiplication, which allows us to use Tamarin’s current unification algorithm. In particular, to determine whether a target term is constructible, we first determine (via unification) whether its subterms are deducible. Since we assume they do not cancel each other out, if there is one such subterm that cannot be deduced, then we can already conclude that the target term cannot be constructed. If all subterms can be deduced, we then determine whether they can be combined, possibly using the group multiplication, to construct the target term. To do so, following [3], we interpret the symbolic terms as algebraic objects and use algebraic methods, e.g., Gauss elimination. Effectively, we replace the unification problem for terms containing the group operation with a system of algebraic equations.

We implement this approach by modifying Tamarin’s constraint solving algorithm, and we show that the resulting constraint solving relation obtained is still sound and (under the non-cancellation property) also complete, in the sense that if Tamarin returns an attack with respect to a given property, then there is actually a protocol execution that violates the property and if Tamarin declares the protocol secure, then there is no execution violating the property. This holds within our symbolic model, i.e., our extension of Tamarin will find attacks that exploit particular properties of particular groups, rather only properties that can be described by the equational theory. To illustrate the effectiveness of our approach, we perform case studies on common protocols that use such Diffie-Hellman group operations, notably ElGamal and MQV. Contributions. We see our work as making three contributions. First and foremost, we present a symbolic approach for reasoning about security protocols satisfying condition C1 that use the full structure of Diffie-Hellman groups, and prove its soundness and completeness under the assumption C2. If the condition C2 is not satisfied, Tamarin will still try to prove the protocol’s security properties. If a property is disproven, then the attack is a valid attack, unconditionally. If a property is proven, Tamarin will mark which terms fail to be non-cancellable for the security proof to hold. Showing that they do not cancel out requires manual inspection. Alternatively, if the condition C2 does not hold, Tamarin has then shown that if an attack trace exists, it must leverage those particular terms canceling each other out.

Second, we implement this approach in the Tamarin prover, resulting in the first automated tool that can handle such an equational theory. This required adding new rules to its constraint solving algorithm and combining algebraic equation solving with Tamarin’s proof search.

Finally, we carry out case studies to show that this approach and its implementation in Tamarin is effective in practice. Namely, we prove ElGamal secure and we rediscover known attacks on MQV. Both proofs and attacks are found within minutes. These examples illustrate the feasibility, scalability, and efficiency of our approach when applied to complex protocols utilizing not only Diffie-Hellman, but also other primitives such as symmetric encryption.

An executable of our Tamarin extension, its source code, and the case studies are provided at [5].

2 Previous work↩︎

2.1 General reasoning for equational theories↩︎

Prior work [6] extended ProVerif with an interface to an external first-order automated theorem prover to support properties modulo equational theories for which a complete unification algorithm is unavailable, by soundly translating these theories into universal axioms in first-order logic. However, these automated provers rely on resolution and will diverge if the axioms generate an infinite chain of inferences. The paper provides no results or experiments for our class of problems. Furthermore, the translation in [6] from the property to the automated theorem prover only covers secrecy properties.

2.2 Dougherty and Guttman’s rewrite system↩︎

State-of-the-art symbolic protocol verifiers represent messages as terms in a term algebra and operations as function symbols applied to these terms. The term algebra is equipped with an equational theory, representing the algebraic properties of the cryptographic primitives modeled. The equational theories are specified by sets of equations that describe how terms can be transformed or rewritten (by orienting equations left to right) according to these properties. To reason with such theories, the equations are often required to be convergent, namely that every term has a unique normal form (that cannot be reduced further using the equations) according to that theory.

We first introduce the rewrite theory we will use to represents fields, which is a slight modification of the theory presented by Dougherty and Guttman in [2]. We verify this theory is convergent modulo the associativity and commutativity of the theory’s operators (abbreviated by AC) using the Aprove termination tool [7] and the Maude Church-Rosser Checker [8]. We follow standard notions and conventions from term-rewriting, see [9]. In particular \(t:S\) indicates a term \(t\) of sort \(S\).

The operator \(\mu\) models a non-invertible function that coerces group elements into exponents. We will refer to this function as a hash function as we symbolically model it as one. We will write \(g^x\) for \(\operatorname{exp}(g,x)\). Dougherty’s and Guttman’s initial theory introduced a sub-sort \(\mathit{NZE}\) of \(E\) representing non-zero exponents and defined the operator \(\operatorname{inv}\) only on this sort. We remove this sub-sort in our rewrite theory, and instead ensure that we don’t invert the \(0\) symbol when solving algebraic equations.

From the above equations, we can extract rewrite rules by orienting the non-AC equations left-to-right. Finally, we added further equations derivable from those above to join critical pairs, see [2].

We denote this rewrite system by \(\rightarrow_{DH}\). Terms that are irreducible with respect to \(\rightarrow_{DH}\) are said to be in normal form.

The same proof as in [2] shows that:

Finally, we introduce the notion of a root term.

2.3 Follow-up rewriting work↩︎

In [2], Dougherty and Guttman present the term rewrite system just discussed, and prove it provides a decision procedure for equality for a structure representing generic finite fields. Furthermore, they use this rewrite system to derive a symbolic analogue of the discrete log assumption, a computational assumption stating that deducing \(e\) from \(g^e\) is hard. We rephrase this result in our setting in Section 4. Dougherty and Guttman then sketch how to apply these results in a strand space formalism, which is an alternative operational semantics for the symbolic model. In particular, they show how this discrete log assumption can be used to prove adversarial reachability properties for certain key-exchange protocols. However, their proofs are not mechanized and are based on pen-and-paper arguments. Moreover, they consider only a very restricted class of protocols and only properties stating whether a passive adversary can deduce a term.

In follow-up work [3], Dougherty and Guttman replace their rewrite system with algebraic methods, by interpreting \(\mathit{DH}\) messages not as terms in a rewrite theory but as elements in the traditional algebraic structure of fields.

The authors again work in the strand space formalism. They define a class of protocols, a new adversary who can employ the full algebraic structure of fields, and a language for expressing security properties as protocol goals. They then prove that the resulting combination of protocols, adversary, and goals has the small witness property: if there exists a protocol run that violates a security property, then some run smaller than a computable bound also violates it. The authors provide an algorithm to decide security goals for this class of protocols by testing every protocol run within the bound and verifying whether it satisfies the security goal. This process combines symbolic and algebraic methods: for each run, they build a constraint system, which in turn reduces to a system of linear equations that can be solved by Gaussian elimination.

In practice however, this procedure requires enumerating all possible protocol executions (up to a given bound) and hence is not suitable for automated tools. Instead, we incorporate the idea of combining symbolic and algebraic methods in a backwards search, constraint solving algorithm.

Furthermore, we remove some restrictions on the class of protocols being modeled. In particular, Dougherty and Guttman require all sent or received Diffie-Hellman group elements to be simple elements in the form \(g^x\) for a variable \(x\). Although the protocols may compute composite group elements in their local state, e.g. keys, they cannot transmit these elements to the adversary. This is a strong limitation as many protocols that use the full field structure transmit composite elements (e.g., El Gamal). Furthermore, their Diffie-Hellman rewrite theory cannot be combined with arbitrary user-defined equational theories. Finally, they additionally require that whether or not a specific exponent is deemed to be compromised is encoded as an assumption rather than a security goal to be proven.

In [10], Jackson proposes to adapt work from [2] to the framework of an automatic tool, the Tamarin prover. While his approach removes the restrictions from [2] and [3] on the protocols that can be modeled, it only targets passive adversarial reachability properties. Neither correctness proofs nor an implementation were provided.

In this work, we overcome above shortcomings. Namely, we implement support for full Diffie-Hellman structures in the Tamarin prover, taking inspiration from [10], and using the idea from [3] to combine symbolic and algebraic methods. Our approach hence supports protocols using arbitrary user-defined equational theories with no restrictions on the format of messages that are sent or received, as long as all Diffie-Hellman messages belong to the same group. We also allow for an active Dolev-Yao adversary and arbitrary security properties expressible in the Tamarin prover, provided the terms appearing in those properties satisfy a certain condition stating that their subterms cannot be inverses of each other (Definition 8). Finally, we provide an implementation, resulting in the first automated tool that can support protocols using full Diffie-Hellman structures.

3 The Tamarin prover↩︎

In Sections 3.1 and 3.4 we provide background on the Tamarin prover: its syntax and its contraint solving algorithm respectively. In Sections 3.2 and 3.3 we describe how we integrate the new equational theory into Tamarin.

3.1 Models and properties↩︎

The Tamarin prover [4] models protocols as labelled transition systems: protocol rules and adversarial capabilities are specified as multiset rewrite rules that define state transitions. The system’s state is modeled as a multiset of facts (symbols taking terms as arguments) representing the protocol state, adversary knowledge, and network messages.

Terms are elements of an order-sorted term algebra \(\mathcal{T}\) that has a unique sort \(\mathit{Msg}\) and two sub-sorts \(\mathit{Fresh}\) (representing unique messages) and \(\mathit{Public}\) (representing publicly known terms), incomparable to each another. This assumes an infinite set of fresh and public names \(\mathit{FN}\) and \(\mathit{PN}\), and an infinite set of variables \(\mathcal{V}\) with an infinite subset of variables for each sub-sort: \(\mathcal{V}_f\) (fresh) and \(\mathcal{V}_p\) (public). In Tamarin, public variables are annotated with a \(\$\)symbol. A user-defined signature \(\Sigma_{Usr}\) (a set of function symbols) is used to model cryptographic operators, and the function symbols’ semantics is defined by an equational theory \(\mathcal{E}_{Usr}\). Formally we define the term algebra \(\mathcal{T}\) to be the algebra over \(\Sigma_{Usr}\), \(\mathit{PN}\), \(\mathit{FN}\), and \(\mathcal{V}\).

Not all equational theories are supported by Tamarin. Supported theories must satisfy the so-called finite variant property, which ensures that there is a general unification algorithm modulo \(\mathcal{E}_{Usr}\) that returns a finite set of most general unifiers [11], [12]. Note that neither the theory representing Diffie-Hellman operators (Definition 1) satisfies this property nor does any theory including distributivity over an \(AC\) operator [1], [12].

A multiset rewrite rule is written as follows:

[escapeinside={*}{*}]
rule rulename:
[Premises(...)]--[Actions(...)]->[Conclusions(...)]

We refer to the zero or more facts appearing in the premises, labels, or conclusions of a rule as premise facts, action facts, and conclusion facts respectively.

As is usual in the symbolic setting with a Dolev-Yao adversary, the adversary controls the entire network and sees every message sent. Tamarin has a special fact K(m), where m is any term, that encodes the adversary’s knowledge (i.e. the adversary knows term m) and the special facts In(m) and Out(m) that encode network messages (i.e. m is received from the network, and m is sent out to the network). Adversary capabilities are also modeled by rewrite rules. For example, Tamarin models the adversary reading and sending messages on the network as follows:

rule send: [K(m)]--[K(m)]->[In(m)]
rule recv: [Out(m)]-->[K(m)]

Similarly, Tamarin gives the adversary the same computational capabilities as the other parties running the protocol. In particular, the adversary has access to all the function symbols defined in the protocol. It can apply each function f/n of arity \(n\) via rules of the form:

rule f: [K(t1),...,K(tn)]-->[K(f(t1,...,tn)]

All other message deduction rules and network rules can be found in [4]. Given a protocol, we denote by \(\mathcal{P}\) the set of all protocol rules and adversary capability rules. The transition system these rules define operates on ground terms: a rule is applied by removing the appropriately instantiated premises from the state and adding the instantiated conclusions. A protocol execution is an alternating sequence of states and instantiated rules, where each state in the sequence is obtained from the previous one by applying the interposed rule. The instantiated action facts in this sequence are the labels of the labelled transitions and they define traces, corresponding to protocol executions. We define security properties over these traces.

More precisely, security properties, called lemmas, are expressed as first-order temporal logic formulas over trace atoms, where quantification is allowed both on message terms and on timepoints (which in Tamarin are preceded by a # symbol). Trace atoms are: equality of terms, equality and ordering of timepoints, a label ActionName at a timepoint #i, written ActionName(arguments)@#i, or the \(\perp\) symbol, together with the usual logical connectives and quantifiers. There are some restrictions on the use of quantifiers within formulas. Before giving an overview of how Tamarin operates, and proves security properties, we explain how we integrate the full Diffie-Hellman theory into the Tamarin prover. In doing so, we provide a running example of modelling theories in Tamarin.

3.2 Introducing new sorts↩︎

We extend Tamarin’s term algebra with the two incomparable sorts \(G\) and \(E\). These two sorts are subsorts of the existing \(\mathit{Msg}\) sort, but are incomparable to the existing \(\mathit{Public}\) and \(\mathit{Fresh}\) sorts. We also introduce a public subsort \(\mathit{PubG}\) for \(G\) and a fresh subsort \(\mathit{FrE}\) for \(\mathit{E}\). For technical reasons described in Section 5, we also introduce a subsort \(\mathit{varE}\) of the sort \(E\). We again assume we have infinite sets of names \(\mathit{PN}_G\) and \(\mathit{FN}_{\mathit{E}}\) and an infinite set of variables \(\mathcal{V}_G\) and \(\mathcal{V}_E\) with respective infinite subsets \(\mathcal{V}_{PubG}\), \(\mathcal{V}_{varE}\), and \(\mathcal{V}_{Fr_{\mathit{E}}}\). By a \(\mathit{DH}\) term, we mean a term of sort \(G\) or \(E\). We extend the signature \(\Sigma_{Usr}\) with the function symbols in \(\Sigma_{DH}\), whose semantics is described by the equational theory \(\mathcal{E}_{DH}\). We assume that \(\mathit{DH}\) terms are always reduced to their normal form after each rule application. \[\begin{align} \Sigma & :=\Sigma_{Usr}\cup \Sigma_{DH},\\ \mathcal{E} &:= \mathcal{E}_{Usr} \cup \mathcal{E}_{DH}. \end{align}\] We will henceforth work in the term algebra \(\mathcal{T}'\), the term algebra over \(\Sigma \cup \mathit{PN} \cup \mathit{FN} \cup FN_G\cup \mathit{PN}_G\cup \mathit{FN}_{\mathit{E}} \cup PN_{\mathit{E}}\cup \mathcal{V}\cup \mathcal{V}_G \cup \mathcal{V}_E.\) Similar to terms of sort \(\mathit{Fresh}\), distinct terms of sort \(\mathit{FrE}\) cannot be equal and, like the terms of sort \(\mathit{Public}\), terms of sort \(\mathit{PubG}\) are known by the adversary.

Furthermore, for each operator, we add a rule allowing the adversary to apply it, and we add the following rules allowing the adversary to learn the constant terms and to generate fresh values.

rule FrE: [Fr(f:FrE)]--[K(f:FrE)]->[Out(f:FrE)]
rule const: []--[K(1), K(0)]->[Out(1), Out(0)] 

As a running example, consider the following simple protocol where Bob sends Alice an encrypted message \(m\) using ElGamal.

Note that prior to our work, Tamarin could not model such a protocol, since it did not support group multiplication and the associated equations. Note too that all the previous works mentioned in Section 2.3 also cannot model such a protocol, nor any other work that we are aware of. With our proposed extension for Tamarin, we can model the above protocol as follows, where g:PubG is a constant.

[escapeinside={*}{*}]
rule KeyGen:
[Fr(ska:FrE)] -->
  [!PubKey($A, g^ska:FrE), !SKey($A, ska:FrE),  
   Out(g^ska:FrE)]

rule CompromiseKey:
[!SKey($A, ska:FrE)] 
--[Compromised($A)]->
  [Out(ska:FrE)]

rule BobEncrypts:
let pka = g^{ka:E} 
in
[!PubKey($A, pka), Fr(m:FrE), Fr(y:FrE)] 
--[BSent(g^{m:FrE}), SecretB($B, $A, g^m:FrE)]-> 
[Out(<g^y:FrE, g^m:FrE.(pka^y:FrE)>)]

rule AliceReceives:
let m = (g^{c1:E})^(-ska:FrE).g^{c2:E}
in 
[In(<g^{c1:E}, g^{c2:E}>), !SKey($A, ska:FrE) ]
--[AReceived(m), SecretA($A, m) ]->
[]

For our running example, we will consider two properties:

• Executability: Tamarin finds a trace where both Alice and Bob execute their rule, and Alice receives the intended message.

• Secrecy: If Bob encrypts a message intended to be a secret for Alice, only Alice and Bob should learn it.

We formulate these properties in Tamarin as follows:

lemma executable: 
exists-trace
"Ex msg #i #j. BSent(msg)@i 
               & AReceived(msg)@j
               & not (Ex #l X. Compromised(X)@l)"

lemma secrecy:
"All msg #i B A. SecretB(B, A, msg)@i 
              & not (Ex #l. Compromised(A)@l)==> 
       not (Ex #j. K(msg)@j )"

Note that this model indeed assumes that all elements are of the form \(g^e\) for the same group generator \(g\). For example, when Alice receives messages from Bob in AliceReceives, the model explicitly enforces them (by pattern matching) to be of the form \(g^{c_1}\) and \(g^{c_2}\) for some arbitrary \(E\)-variables \(c_1\) and \(c_2\). Observe that an \(E\)-variable can be instantiated with a term containing the \(+\) symbol, so this does not exclude \(g^{c_1}\) from being a product of different terms. The same holds for Alice’s public key \(g^{\mathit{ka}}\) in BobEncrypts. It is the user’s responsibility to ensure that Bob never uses the \(\mathit{ka}\) variable in isolation. A syntactical translation on the compiler’s side (translating a variable \(\mathit{v_G:G}\) to the term \(g^{v_E:E}\)) would easily remove this burden. This constraint only misses attacks that use elements from different groups. However this should be an acceptable restriction, since validating group elements in a Diffie–Hellman key exchange is a standard practice.

3.3 Dependency graphs modulo full Diffie-Hellman↩︎

Tamarin has its own specialized data structure for efficiently representing the application of multiset rewriting rules, called dependency graphs. Intuitively, these graphs represent sequences of rewrite rule instances that correspond to protocol executions and capture which facts originate from which rules. In particular, nodes are labelled with rule instances and two nodes share an edge if a conclusion of the first node matches, modulo the protocol’s specified equational theory, a premise of the other. We formally define these graphs in Appendix 9.

A protocol satisfies an exists-trace property \(\exists x. \phi\) if there exists an instance of a dependency graph (e.g. a trace or protocol execution) that is a model of the formula \(\phi\). It satisfies a forall-trace property \(\forall x. \phi\) if there does not exist a graph that is a model of the formula \(\neg\phi\).

We refer again to [4] for Tamarin’s formal semantics, but intuitively an instance of a graph is a model of a formula if the action facts appearing in the formula appear in the graph and satisfy all timepoint equalities and inequalities expressed by the formula.

We define \(\mathit{DH}\)-extended dependency graphs to consider rules instantiated over the term algebra \(\mathcal{T}'\). Figure 1 illustrates a DH-extended dependency graph corresponding to an execution of the ElGamal protocol described above.

This is well defined because we can check whether two ground terms in \(\Sigma\) are equal, since \(\Sigma_{Usr}\) and \(\Sigma_{DH}\) have disjoint signatures, and we can check the equality modulo AC of ground terms within each equational theory by considering their normal forms.

3.4 Constraints and constraint solving↩︎

As mentioned, by negating the forall-trace formulas, it suffices to determine the existence of protocol traces that are models for a given formula. This problem is undecidable, so Tamarin’s search might not terminate.

Tamarin searches backwards, extracting a set of constraints on graphs from the targeted formula. Similar to atoms, constraints are action facts that must appear in traces (e.g. \(Fact@i\)), term equalities and timepoint orderings, and also rules that must be applied at certain timepoints (\(i:rule\)). To construct a solution to a constraint system (a finite set of constraint sets), Tamarin uses a constraint solving relation \(\rightsquigarrow\), where \(C_1 \rightsquigarrow C_2\) reduces the constraint system \(C_1\) to the constraint system \(C_2\) by inferring new constraints and performing case splits. We write \(c_1,\ldots,c_n,\Gamma\) to denote \(\{c_1,\ldots,c_n\}\cup \Gamma\). The rule \[\frac{\ c, \Gamma \ }{\\{ \Delta_i, f_i(\Gamma) \}_{1\leq i\leq n} \ }\ RuleName \end{crule}\] denotes that \[\{c\}\cup \Gamma \rightsquigarrow \{ \Delta_i \cup f_i(\Gamma),\ldots, \Delta_n \cup f_n(\Gamma) \}.\]

For example, denoting with acts(ri) all the action facts (i.e. neither including the premises nor the conclusions) of rule ri, Tamarin’s constraint solving rule \[\frac{\ \mathit{Fact}@i, \Gamma\ }{\ \{\mathit{Fact}=g, i:\mathit{ri}, \Gamma\}_{\mathit{ri}\in \mathcal{P}, g \in \mathit{acts}(ri)}\ }\ S_@ \end{crule}\] solves a constraint \(\mathit{Fact}@i\) by performing a case split over all rules \(ri\) and their actions \(g\) that might be equal to \(Fact\). In each case, a constraint \(\mathit{i:ri}\) (indicating that an instance \(\mathit{ri}\) of a protocol rule must be applied at timepoint \(i\)) is added. Additionally, for each of the actions \(g\) of \(ri\), an equality constraint between \(g\) and \(Fact\) is added.

Another example is the constraint solving rule that introduces an equality constraint, this time between the premises and conclusions of rules. More precisely, denoting by \(prems(ri)\) and \(concs(ri)\) the premise facts and conclusion facts of rule \(ri\), the rule \[\frac{\ i:ri, \Gamma\ }{\ \{i:ri,\;j:ru,\;pi=cj, \Gamma\}_{\substack{ru\in \mathcal{P}, pi \in prems(ri),\\ cj\in concs(ru)}}\ }\ S_{Prem} \end{crule}\] solves a constraint \(i:ri\) by performing a case split over each rule \(ru\) checking whether its conclusions are equal to some premise of \(ri\). In each case, an equality constraint between rule conclusions and premises is added.

Equality constraints are then solved by another rule \(S_{=}\) that performs unification. \[\frac{\ f=f', \Gamma\ }{\ \{\sigma(\Gamma)\}_{\sigma\in \operatorname{Unify}_{\mathcal{E}_{Usr}}(f,f')}\ }\ S_{=}. \end{crule}\] Note that this unification rule can also be used to solve timepoint equalities.

The full list of Tamarin’s constraint solving rules can be found in [4] along with a proof of the following theorem.

Finally, to find a model of the constraint system, Tamarin searches for a constraint reduction \(\{\phi\} \rightsquigarrow ^* \emptyset\) or a constraint reduction \(\{\phi\}\rightsquigarrow ^* \Delta\) such that there is a constraint system \(\Gamma\in\Delta\) for which we can directly confirm that it has a model. In the first case, Tamarin proves that \(\phi\) is not satisfiable (if \(\phi\) represents the negation of a security property, this proves the property). In the second case, Tamarin extracts a model (hence a dependency graph) \(dg\) of \(\phi\) from \(\Gamma\) (if \(\phi\) represents the negation of a security property, this represents a counterexample to the property). In both cases, such a constraint system is defined to be solved.

In Section 5, we show how we extend Tamarin’s current constraint solving algorithm by defining new constraint solving rules for terms of sort \(\mathit{DH}\). We leave Tamarin’s constraint solving rules unchanged on terms of other sorts. In Section 6, we show how we can merge approaches for terms that contain both sorts. Observe that in our protocol model of ElGamal, we have already used the pair function over terms of sort \(\mathit{DH}\), so this integration is crucial for usability.

Examples. Returning to our example, when trying to prove the lemma executable, Tamarin (as it currently stands) produces the constraint set²:

Let us see why Tamarin currently cannot solve such a constraint. Since \(BSent\) only appears in the BobEncrypts rule, Tamarin (using \(S_{@}\) and \(S_{=}\)) will replace the variable \(\mathit{msg}\) by the term \(g^{\sim m}\) in the entire constraint system, and will then try to solve the \(AReceived(g^{\sim m})\) constraint. This fact only appears in the AliceReceives rule, and, again via the \(S_{@}\) and \(S_{=}\) rules, Tamarin would try to unify \(g^{\sim m}\) and \((g^{c_1})^{-ska}\cdot g^{c_2}\). However, as mentioned, we do not have a unification algorithm for this!

When trying to prove the lemma secrecy, Tamarin tries to find a trace for its negation. After replacing the variable \(\mathit{msg}\) by \(g^{\sim m}\) (since \(SecretB(B,A,g^{\sim m})\) only appears in one rule), it will try to solve the remaining constraint system:

Solving adversarial facts is more complicated. Essentially, Tamarin would try to see if \(g^{\sim m}\) can be unified with a term coming from an \(Out\) fact or with the output of a function symbol applied on other terms in the adversary’s knowledge, again learnt from \(Out\) facts or via other function symbol (see rules send or f). Again, this approach is not possible with the full DH theory, as we cannot check if two terms are unifiable.

4 Indicators and non-cancellation↩︎

As illustrated in the previous examples, the two views we need to cover are: (i) honest protocol execution, and (ii) adversarial behaviour.

For honest agents, behavior is strictly described by the protocol rules. To unify the premise of one rule with the conclusions of others, we exploit the non-cancellation assumption: every root term in the premise must also appear in the conclusion. Rather than unifying full terms, we first unify premise root terms with conclusion root terms in a simplified theory with a dedicated unification algorithm. We then use algebraic reasoning to check whether the instantiated conclusion terms can be combined, possibly canceling surplus terms, to reconstruct the premise.

Adversarial behaviour is more complex as the adversary may freely apply all \(DH\) operators. To decide whether a target term can be deduced, we classify the exponents in the target term as known or unknown, isolating the secret components that must be obtained from the network. We unify these secret components with network messages in the simplified theory, and again use algebraic reasoning with the known exponents to reconstruct the target term.

A key step of the approach is determining which exponents are known to the adversary. Given a constraint system, we can keep track of the exponents leaked, i.e. made available to the adversary, within it:

These sets correspond to the non-basis and basis sets in Dougherty and Guttman’s terminology. Note that if \(e \in L^{\Gamma}_i\), then \(e\in L^{\Gamma}_j\) for all \(j>i\). The set \(L^{\Gamma}_i\) is easily computable from the current constraint system \(\Gamma\). In practice we store exponents and the timepoint at which they are learned in our constraint system. Each time we add a rule with action \(K(e)\) at timepoint \(j\), we add \((e,j)\) to the basis set of our constraint system and \(L^{\Gamma}_i\) consists of all exponents \((e,j)\) in this set such that \(j\leq i\).

As we explain in Section 5.2, to classify the remaining exponents appearing in our target term, we will follow Tamarin’s general strategy of using backwards search. For each exponent variable \(e\) appearing in our term, if it is not already in the leaked set \(L^{\Gamma}_i\) of the current constraint system \(\Gamma\), we introduce the constraints \(K(e)@j_e\) and \(j_e < i\), and attempt to solve these constraints. This works well when the exponent terms appearing in the term are known to be fresh, since in that case the unification sub-queries are extremely simple: fresh terms can only be unified with other fresh terms. In the more general case though, Tamarin may fail to terminate when trying to classify the exponent as secret or leaked. In general, we delay solving the \(K(e)@j_e\) constraints when \(e\) is not of sort fresh. In most protocols that use Diffie-Hellman groups, the exponents used to exchange keys are randomly chosen, hence we believe this limitation does not widely impact the usability of our approach.

Given a leaked set \(L\) and a term, we now define its ‘secret’ parts, one for each of its root terms.

Observe that the indicator is defined only on root terms and hence it is unique (for the given set \(L\)). For example, if \(L=\{y,w\}\), and \(t=g^{x*y}\), then \(Ind_L(t)=g^x\). When a term is already deducible from \(L\), we define its indicator to be \(1\), e.g., for the same \(L\), \(Ind_L(g^w) = 1\).

In general, \(Ind_L(t)\) only contains variables that belong to \(S\). An exception is when \(t\) contains a hashed term that contains elements both from \(L\) and \(S\). Since \(\mu\) models a one-way function, as soon as it contains one secret exponent, we must consider the entire term secret, e.g. \(Ind_L(g^{\mu(x*w)}) = g^{\mu(x*w)}\). We give the precise recursive definition of the indicator function in Appendix 9.4.

The following theorem states that new indicators cannot be created by function applications. It is a reformulation of Dougherty and Guttman’s Indicator Theorem from [2], rephrased with Tamarin-specific notation.

This theorem is an analogue of the discrete logarithm assumption. From Theorem [thm:cdh], once we have established the leaked set, given a term \(t\), it suffices to find one indicator of \(t\) that cannot be reconstructed by the adversary, or an agent, to conclude that the whole term cannot be known. Indeed, by Theorem [thm:cdh], all indicators must be known to construct the term. If, however, we cannot exclude any indicator, we must determine whether these indicators can be combined correctly to obtain the target term. We will elaborate on how this can be done with algebraic methods in Section 5.1.

Observe that this strategy does not consider variable substitutions. Since \(\Sigma_{DH}\) contains reducible functions, substitutions could cancel out particular root terms, invalidating the above reasoning. To apply Theorem [thm:cdh] in Tamarin’s unification-based setting, we need the extra assumption that particular root terms do not cancel each other out. We define the condition \(\operatorname{NoCanc}(X,Y)\), which states that the root term \(X\) cannot be cancelled out by the root term \(Y\).

For example, \(\operatorname{NoCanc}(X,Y)\) is satisfied when both \(X\) and \(Y\) only contain variables of sort \(\mathit{FrE}\). Another condition for which \(\operatorname{NoCanc}(X,Y)\) holds concerns the \(\mu\) operator.

We provide the proof in Appendix 9.4. Essentially, this follows from the fact that fresh variables cannot be instantiated with function applications. Hence in \(1)\) only the \(t\) term can be instantiated with an \(\operatorname{inv}\) term, creating an infinite recursion since \(t\) appears in both \(X\) and \(Y\). In \(2)\) the \(\operatorname{inv}\) symbol can only appear in a \(\mu\) term, which however has no associated equations, and hence cannot be ‘pulled out’.

Note that the definition excludes \(X\) from cancelling itself out (by excluding \(\theta(X)=1\)) and hence is asymmetric. To consider both directions, we define \(\operatorname{NoCanc}\) on all the root terms of a term simultaneously.

As mentioned, often a much weaker requirement suffices. If we know that \(X_1\) cannot be cancelled out by the other root terms of a term \(t=X_1\cdot ... \cdot X_n\), then it suffices to prove that \(X_1\) cannot be deduced to conclude that the entire term \(t\) cannot be deduced. In this case, we do not need the non-cancellation property on the other root terms. Hence we also define the weaker condition for a root term \(X\in \mathrm{rt}(t)\) of a term \(t\):

Before applying a constraint solving rule concerning a given term \(t\), our algorithm checks if these sufficient conditions on its root terms are satisfied. If they do not hold, we store the (minimal) set of pairs of root terms that need to satisfy the \(\operatorname{NoCanc}\) condition to guarantee the correctness of our approach and output these assumptions. In general, our approach is guaranteed to work for every protocol and security property such that every \(\mathit{DH}\) term \(t\) appearing as an argument of an action fact in the property statement either already satisfies \(\operatorname{NoCanc}(t)\) or the arguments of the corresponding action facts in the protocol satisfy the \(\operatorname{NoCanc}\) property.

5 Alternative strategy for DH terms↩︎

We extend all of Tamarin’s current constraint solving rules to be applicable to all constraints, except for the rule \(S_{=}\), and the rules that introduce equality constraints. Recall that we cannot apply the rule \(S_{=}\) to constraints containing \(\mathit{DH}\) terms as it requires unification in the \(\mathit{DH}\) rewrite system. The rules introducing equality constraints are: (1) \(S_@\), which tries to match an action fact coming from a security property (lemma) with an action fact appearing in a rule label and (2) \(S_{Prem}\), which tries to match a rule’s premise fact with another rule’s conclusion fact. We therefore introduce new constraint solving rules that complement these three rules for constraints containing Diffie-Hellman terms. Our new rules incorporate algebraic methods and replace unification by interpreting our rewrite theory as a traditional algebraic structure (i.e. a real field extension) and leveraging mathematical methods such as Gaussian elimination or Buchberger’s algorithm.

To produce mathematical equations, define a function that generalizes substitutions by variables of sort \(E\).

Finally, we define a simplified equational theory for which a unification algorithm is known.

We now show our approach for action facts \(Fact(\cdot)\) that are not the adversarial \(K\) fact, covering honest protocol execution. We will introduce constraint solving rules for adversarial \(K\) facts in Section 5.2.

Assume that \(\operatorname{NoCanc}(t)\) holds for a certain term \(t\). As a starting point, we also search for conclusions/actions of the form \(Fact(h)\) in the protocol rules. Let \(L\) be the leaked set of the rule to which \(Fact(h)\) belongs. To see if \(t\) and \(h\) are unifiable, we check if each root term of \(t\) can be unified in \(\varepsilon_{simp}\) with a root term of \(h\). Note that Tamarin currently supports unification in \(\varepsilon_{simp}\), returning a complete set of most general unifiers per unification query. Since we generalize the returned substitution, in most cases (see Appendix 10), we do not need the complete set and instead consider one unifier per query. Note that for unification queries in \(\varepsilon_{simp}\), a complete set of unifiers can consist of more than 40 unifiers.

In particular, let \(t_1,\ldots,t_n\) be the root terms of \(t\), and \(h_1,\ldots,h_m\) the root terms of \(h\). Consider all possible \(n\) (possibly repeated, by introducing a \(+\) symbol) combinations of the subterms \(h_i\). We solve the equations \[\{t_i =_{\varepsilon_{simp}} h_{j_i}\}_{i=1}^{n}\] for \(i=1,\ldots,n\), \(j_i \in \{1,\ldots,m\}\). If there is an \(i\), for which the above equation has no unifier for some \(j_i\), we conclude that the terms are not unifiable. If however there is a unifier \(\sigma\) that unifies each root terms of \(t\) with some root term of \(h\) we then solve the algebraic equation \[gen(\sigma)(t) \circeq gen(\sigma)(h)\] for the unknowns \(Y_i\) introduced by the function \(gen\). Note that we will henceforth use the symbol \(\circeq\) to denote equality constraints between terms containing unknown variables. In Appendix 10, we define the constraint solving rules that perform these steps. We name our new rules with the letter \(C\) to distinguish them from existing constraint solving rules (named with the letter \(S\)):

1. \(C_{@}\) replaces \(S_{@}\) for \(\mathit{DH}\) terms and performs a case split, generating a \(gen(\sigma)(t) \circeq gen(\sigma)(h)\) constraint for each \(\sigma\) obtained in the procedure above;

2. \(C_{Prem}\) replaces \(S_{Prem}\) for \(\mathit{DH}\) terms and is defined in the same way as \(C_{@}\), but with premises and conclusions instead of action facts;

3. \(C_{=}\) replacing \(S_{=}\) for \(\mathit{DH}\) terms, which solves the \(gen(\sigma)(t) \circeq gen(\sigma)(h)\) constraints (see Section 5.1).

4. \(C_{var}\) replaces \(S_{@}\) and \(S_{Prem}\) if \(t\) (or \(h\)) is a variable. It directly instantiates the variable \(t\) with the term \(h\) (or respectively \(h\) with \(t\)), skipping the above rules.

Observe that these rules replace their \(S\) counterparts only for \(\mathit{DH}\)-sorted terms. For constraints that contain terms of sort \(\mathit{Msg}\), we apply the usual \(S\) rules.

In Appendix 10, we also show that this extended constraint solving relation is sound (according to the previous definition) with respect to \(\mathit{DH}\)-extended dependency graphs, and under some assumptions (i.e. non-cancellation of subterms of \(t\)) it is also complete. This guarantees the correctness of Tamarin’s verdicts and hence whether a property \(\exists x. \phi\) or \(\forall x. \phi\) is verified will be determined by whether the constraint systems \(\{\phi \}\) or \(\{\neg \phi \}\) can be solved.

Examples. Returning to Example 1 from in the previous section, we were trying to solve the constraint set:

The only rule that contains a BSent action fact is BobEncrypts. Since \(\mathit{msg}\) is a variable, we can apply \(C_{var}\) to replace \(\mathit{msg}\) with \(g^{\sim m}\) and obtain:

The term \(t = g^{\sim m}\) is not a variable, so we must apply \(C_{@}\) to solve the constraint \(\mathit{AReceived}(g^{\sim m})@j\). Observe that \(\operatorname{NoCanc}(g^{\sim m})\) trivially holds. The only rule with the action fact AReceived is AliceReceives, with argument \(h = (g^{c_1})^{-ska}\cdot g^{c_2}\). We try to unify the root term \(g^{\sim m}\), in the simplified equational theory \(\varepsilon_{simp}\), with a root term of \(h=(g^{c_1})^{-ska}\cdot g^{c_2}\): \[\begin{align} &g^{\sim m} =(g^{c_1})^{-ska} \text{ or }\\ &g^{\sim m} =g^{c_2}. \end{align}\]

Choosing the second equation and unifying in \(\mathcal{E}_{Simp}\) gives \(\sigma= \{ c_2\mapsto \sim m\}\). The substitution \(\sigma\) leaves the other variables of our system unchanged. We generalize (see Definition 11) to \(gen(\sigma)= \{ c_2 \mapsto (\sim m) +Y_1, c_1\mapsto Y_2 \}\), producing the constraint system:

5.1 Algebraic Methods↩︎

In this section, we describe the rule \(C_=\), which excludes or finds a substitution for all the \(Y\) variables that makes the terms \(t\) and \(h\) equal. For honest executions, all variables appearing in \(\sigma(t)\) and \(\sigma(h)\) can be manipulated. However, for adversarial behaviour, some exponents are generally unknown to the adversary (and hence cannot be inverted, etc.). To distinguish between the two, for the rest of the section, we will work with a fixed leaked set \(L\) and its complementary set, the secret set \(S\). We denote them by \(L= \{l_1,\ldots,l_r\}\) and \(S=\{s_1,\ldots,s_l\}\) respectively. For honest executions, however, we set \(S=\emptyset\).

Recall that we assume all terms to be of the form \(g^e\), for a fixed group generator \(g\). Hence we can focus just on the expressions of the exponents of terms \(t=g^{e_t}\) and \(h=g^{e_h}\). By abuse of notation, we let \(t=e_t\) and \(h=e_h\) denote the terms in the exponents.

Since exponents in \(S=\{s_1,\ldots,s_l\}\) are secret, we treat them as abstract variables: for example, we cannot compute their inverses, nor multiply them with other terms. We cannot instantiate our unknowns \(Y_i\) with secret values. In contrast, we can fully manipulate elements in \(L= \{l_1,\ldots,l_r\}\). We can hence interpret \(t\) and \(h\) as a polynomials with variables in \(S=\{s_1,\ldots,s_l\}\) and coefficients in the polynomial field \(\mathbb{Q}(l_1,\ldots,l_r)[Y_i]\). This is similar to what is done in [3].

The function that interprets symbolic DH terms as elements in the field of rational functions in \(r\) variables \(\mathbb{Q}(l_1,\ldots,l_r)\) is a straightforward translation, which we define recursively in Appendix 9.5. Clearly, we can define this translation only from the set \(\operatorname{Gen}_{DH}({l_1,\ldots,l_r})\), since different variable names do not have counterparts in \(\mathbb{Q}(l_1,\ldots,l_r)\).

For example, for \(L=\{x,y\}\) and \(S =\{u,\operatorname{inv}(v),w\}\) we have \[\operatorname{toPoly}(x**\operatorname{inv}(y)**w**Y_1 + u**x - u**y**Y_2 + \operatorname{inv}(v)**w)\] \[= \cfrac{x}{y}\cdot Y_1 \cdot S_3 + (x- y\cdot Y_2)\cdot S_1 + S_2\cdot S_3,\] which is an element of \(\mathbb{Q}(x,y)[Y_1,Y_2][S_1,S_2,S_3]\), where we have changed the variable names \(u,\operatorname{inv}(v),w\) to \(S_1,S_2,S_3\) for clarity. Note that since they are just variables, their names are irrelevant.

Returning to our generated constraints \(gen(\sigma)(t)\circeq gen(\sigma)(h)\), we would like to answer the following question: Does there exist a substitution \(\sigma\) instantiating the \(\{Y_i\}_{i=1,\ldots,n}\) variables such that \[\operatorname{toPoly}(gen(\sigma)(h)) = \operatorname{toPoly}(gen(\sigma)(t))?\]

Defining \(H:= \operatorname{toPoly}(gen(\sigma)(h_i))\), and \(T := \operatorname{toPoly}(t)\), this corresponds to solving the equation with coefficients in \(\mathbb{Q}(l_1,...l_r)\) for the given variables \(\{Y_i\}_i\):

\[\label{eq:DHActionFacts} H(s_1,\ldots,s_r) = T(s_1,\ldots,s_r).\tag{1}\]

Matching each coefficient of the polynomials, this gives a system of equations in the variables \(\{Y_i\}_i\). If we assume \(H\) and \(T\) are linear in the \(Y_i\), this system of equations can be solved via Gaussian elimination. For the case of non-linear equations, one could use more powerful mathematical tools. For example, Barthe et al., in [13], show that this can be solved using Buchberger’s algorithm for Gröbner basis computations. We have currently only implemented the Gauss elimination strategy in the Tamarin prover as our case studies all produced linear equations.

Assume there is a solution to Equation (1 ), and let \(\{(y^{(1)}_1,...y^{(1)}_n)\),…,(\(y^{(m)}_1,\ldots,y^{(m)}_n)\}\) be a basis of the solution space to the Equation (1 ). Let \(\sigma^j = \{Y_i\mapsto y^{(j)}_i\}\) be the substitution obtained by interpreting each \(y^{(j)}_i\) as an abstract term. The rule that solves the DH-equality constraints is then as follows:

::: {#rul:C= .rul} Rule 1 (\(C_{=}\)).

If Equation (1 ) obtained from the constraint \(t \circeq h\) admits a solution, let \(\{\sigma^j\}\) be the set of substitutions corresponding to a basis of the solution space. \[\frac{\ t\circeq h,\;\Gamma\ }{\\{ \sigma^j(\Gamma) \}_j \ }\ C_{=}.\] :::

We show in Appendix 10.2 that Tamarin’s contraint solving relation remains sound when adding this rule and it is also complete under the non-cancellation assumption on \(t\).

The constraint system from Example 1 \[g^{(c_1 + Y_2)* (-ska)}\cdot g^{(\sim m)+Y_1}\circeq g^{(\sim m)}\] produces the equation: \[Y_2* (-ska) + Y_1 + (\sim m)= (\sim m).\]

Since \(S=\emptyset\), this is the only equation we need to solve, with solution: \(Y_1 = ska*Y_2.\) Introducing a new fresh variable \(v_{Y_2}:E\), the basis of the solution space is \(\langle ska*v_{Y_2}, v_{Y_2}\rangle\) corresponds to the substitution

\(\sigma = \{Y_2\mapsto v_{Y_2}, Y_1\mapsto ska*v_{Y_2}\},\) and thus the constraint system

The next steps in solving this system would be to solve the premises of the rule \(\sigma(j: AliceReceives)\), given by \(In(\langle g^{v_{Y_2}},g^{ska*v_{Y_2}}\cdot g^{\sim m}\rangle)\). We illustrate in the following section the optimizations we make for \(In/Out\) terms and our approach for combined terms.

5.2 Adversarial premise facts↩︎

As mentioned in Section 3.1, Tamarin has a default Dolev-Yao adversary that can read everything on the network and send messages on the network. It can use the given equational theories, and hence its knowledge set is always determined by the set of all terms sent in the network, all the terms of public sorts and all terms deducible from these terms by applying the equational theories’ function symbols. Tamarin has a smart way to avoid infinite loops, e.g. re-encrypting and decrypting continuously, which we do not describe here, but see [4].

For any rule i:ru containing a premise fact \(K(\cdot)\), we perform an optimization in our implementation, bypassing some applications of the Rule 3. Recall that for each operator \(f\) of arity \(n\) in our \(\mathit{DH}\) theory, we introduced a message deduction rule f:[K(x_1),…,K(x_n)] --> K(f(x_1,…,x_n)). Each such rule produces a conclusion \(K(\cdot)\) and hence applying the Rule 3 repeatedly without a suitable heuristic leads to an infinite search space. To address this issue, our implementation does not include the message deduction rules corresponding to the DH operators among our protocol rules. Instead we represent the adversary’s ability to apply these operators directly when passing to the algebraic setting.

In particular, we introduce the new constraint solving rules 9 and 12 that replace the Rules 3 and 1 in the case where the premise we want to solve is \(K(t)@i\) for a term \(t\) for which \(\operatorname{NoCanc}(t)\) holds.

5.2.1 General terms↩︎

We first assume that the term \(t\) is not a variable.

As a first step, we must determine whether the adversary can deduce all the indicators respect to the adversarial leaked set of each root term of \(t\). Recall that the indicator of a root term represents the minimal information required by the adversary to construct that term from its current knowledge. If the adversary cannot deduce all such indicators, we can immediately conclude that it cannot deduce the term \(t\) itself.

Since the adversary can manipulate and combine different terms he knows, we do not unify the indicators of the root terms of \(t\) with the root terms of a single term in an \(Out\) facts. Rather, we unify the indicators of \(t\) with the indicator of root terms of possibly different \(Out\) fact, as long as they are of the correct sort. In particular, if \(t\) has \(n\) root terms, we consider all possible \(Out(h_1),\ldots,Out(h_n)\) that appear as the conclusions of protocol rules and try to unify each indicator of \(t\) with the indicator of a root term of each \(h_i\): \[\{Ind_L(t_i)=Ind_L(h_i)\}_{t_i\in rt(t), Ind_L(t_i)\neq e_G}.\]

For this, it is necessary to establish the adversary’s knowledge set \(L\) at timepoint \(i\). In particular, for each choice of \(h_1,\ldots,h_n\), we only need determine whether the adversary could have learnt the exponents appearing in \(t\), \(h_1\),…, \(h_n\) previously. To do so, we consider the current leaked set \(L^{\Gamma}_i\) corresponding to the current constraint system \(\Gamma\), and consider all possible ways of expanding it to a larger set \(L\): for each exponent variable \(e\) that appears in \(t\), \(h_1\),…, \(h_n\), if it is not already in the current leaked set, we case split on whether the adversary could learn \(e\) or not. In the first case, we add the constraint \(K(e)@j_e, j_e < i\) to \(\Gamma\) and add \(e\) to \(L\). We will explain how we solve these variable constraints in the following subsection. In the second case, we consider \(e\) to be secret and we raise a contradiction if \(e\) is ever learned by the adversary.

For each option of \(L\), let \(\sigma\) be the generalized (via the \(gen\) function) unifier of the indicators, with respect to \(L\), of \(t\) with root terms of terms \(h_1,\ldots,h_n\). Then we introduce additional variables \(X_1,\ldots,X_n, X_{n+1}\) of sort \(\mathit{varE}\), introduce the constraints \(K(X_i)@j_i, j_i < i\), and consider the linear equation \[\operatorname{toPoly}(X_1\sigma(h_1) + \ldots + X_n\sigma(h_n) +X_{n+1})= \operatorname{toPoly}(\sigma(t)).\] The variables \(X_k\) represent the adversary exponentiating \(h_k\) with some terms he can derive and extra variable \(X_{n+1}\) represents the adversary multiplying the \(h_i\)’s with another derivable term. We match the coefficients of the above polynomials in the variables \(S=\{s_1,\ldots,s_l\}\), and we obtain a system of linear equations to solve. Crucially, for every solution, \(X_i\in \mathbb{Q}(l_1,\ldots,l_n)\). So by the definition of \(L\), \(X_i\) is indeed deducible by the adversary, since the adversary can apply all \(\mathit{DH}\) operators. The solution hence represents a valid attack.

In general, we try to solve the variable constraints with fresh variables as soon as they are added to the system. As a result, in practice most of the possible \(L\)’s are directly excluded before proceeding to solve the corresponding linear equations.

5.2.2 Variable terms↩︎

We now turn to goals of the form \(K(v)@i\), where \(v\) is a variable of sort \(FrE\). For example, the goals we have introduced above are of this form. If \(v\) is already in the leaked set \(L^{\Gamma}_i\) of the constraint system, we mark this goal as solved. Otherwise, we consider it to be secret, and we try solve the goal with the strategy above. That is, we try to unify this variable in the simplified \(\mathit{DH}\) theory with root terms \(h_i\) of \(Out\) facts containing an argument of sort \(E\). If there are other variables appearing in the \(h_i\) terms that are not \(v\) and that are not in the leaked set \(L^{\Gamma}_i\), we case split on them being known or not. Thus the only difference from the previous case is that we do not make a case split on the variable \(v\) itself.

For variables of sort \(E\), we delay solving \(K^{\uparrow}(\mathit{v:E})\) goals until we have solved all other goals and hence collected all the necessary restrictions on the variable \(\mathit{v:E}\). Solving other goals often involves a substitution that maps \(\mathit{v:E}\) to a different composite term.

We provide the full details of the constraint solving rules corresponding to adversarial action facts in Appendix 11, see Rules 9 and 10.

6 Combination with other equational theories.↩︎

To profit from Tamarin’s full expressive power, our approach supports combining the full Diffie-Hellman group structure with other equational theories, both Tamarin’s built-in ones (e.g. pairs, symmetric/asymmetric encryption etc.) and user defined ones. In particular, since \(\mathit{DH}\) is a subsort of \(\mathit{Msg}\), Diffie-Hellman terms are valid arguments of other equational theories’ operators. However, as is also natural, we cannot apply \(\mathit{DH}\) operators to terms that are not of sort \(\mathit{DH}\).

To handle facts that contain combined terms (i.e. terms that contain both \(\mathit{DH}\) and non-\(\mathit{DH}\) variables), we follow Baader and Schulz’s approach [14] of combining unification procedures. In particular, we successively replace \(\mathit{DH}\) sub-terms by new \(\mathit{DH}\) variables, effectively ‘hiding’ the DH term. We call this process cleaning. Note that we can unify cleaned terms with the user-defined equational theory \(\mathcal{E}_{Usr}\), excluding any \(\mathit{DH}\) equation. The solution to this unification problem might return substitutions that unify two different \(\mathit{DH}\) variables. If we keep track of what each of these variables replaces, this corresponds to a unification constraint on two now purely-DH terms. We can then use the approach described in the previous section for these constraints.

More formally, in Appendix 9.4, we define a function \({cl}\) that cleans combined terms by replacing \(\mathit{DH}\)-terms by fresh variables and storing this information. For example, when trying to match the \(In(\langle g^{c_1}, g^{c_2} \rangle)\) fact with an \(Out(\langle g^y, g^m\cdot pka^y \rangle)\) fact in Example 1, Tamarin cleans the terms by replacing the \(\mathit{DH}\) terms with fresh variables: \(u_1\mapsto g^{c_1}, u_2\mapsto g^{c_2}, v_1\mapsto g^y,\) and \(v_2\mapsto g^m\cdot pka^y\). It then produces the unification query \(\operatorname{Unify}(\langle u_1,u_2\rangle, \langle v_1, v_2 \rangle)\). This can be solved with Tamarin’s current variant-based unification algorithm, returning a most general unifier, \(\sigma: \{u_1\mapsto v_1, u_2\mapsto v_2\}\). Tamarin will then use the stored \(\mathit{DH}\) terms to transform this unifier into new constraints \[g^{c_1}=_{DH} g^y\quad\text{ and }\quad g^{c_2}=_{DH} g^m\cdot pka^y.\] These can be solved using the rules from Section 5. Appendix 10.3 defines the corresponding constraint solving rule, and shows that the constraint solving algorithm remains sound and complete.

7 Implementation and case studies↩︎

We implemented the above strategy in the Tamarin prover, providing a new DH-multiplication built-in theory that enables the use of all operators from \(\Sigma_{DH}\). Our goal was to make the integration as complete as possible, keeping all of the tool’s features. This required not only modifying the constraint solving rules, but also all other features that rely on unification. For example, Tamarin allows for restrictions that exclude certain protocol executions, and such restrictions may contain equality constraints. We adapted all such equality checks to use our approach for \(\mathit{DH}\) terms. Other features that are less commonly used (e.g. Tamarin’s diff-mode for verifying observational equivalence properties [15]) are left for future work. We have only implemented the Gaussian elimination algorithm within Tamarin, so our implementation only covers protocols that produce linear equations. This excludes for example, the ElGamal signature scheme. Adding support for other algebraic decision procedures (e.g. Buchberger’s algorithm) that solve the nonlinear equations generated by such protocols is an implementation task that is left for future work.

We first evaluate our implementation on existing models from the Tamarin repository [16] that use the limited Diffie-Hellman built-in equational theory. Afterwards, to illustrate the effectiveness of our approach on protocols using the group multiplication, we modelled the El Gamal encryption scheme [17] and the MQV key exchange [18]. All the above case studies were performed on a laptop with an Intel i7 6-core processor and 16GB memory.

7.1 Evaluation↩︎

We evaluate our implementation’s correctness using the following models taken from the Tamarin repository:

1. toy protocols using basic adversary capabilities regarding exponentiation;

2. 12 real world protocols that use the basic Diffie-Hellman key exchange in different variants, from a benchmark of 20 case studies from [19]. These protocols use different built-in equational theories (symmetric-encryption schemes, hash functions, signature schemes) and different user-defined functions. Each protocol model verifies one or two properties.

3. The Tamarin model of the Wireguard protocol from [20], a large case study containing multiple nested hashes, different user-defined functions, and reuse lemmas. This model contains 8 lemmas in total: 2 executability lemmas, 2 agreement properties, 2 secrecy properties, and 2 reuse lemmas to help prove the agreement properties.

As mentioned, these models do not make explicit use of the group multiplication in the protocol rules.

While we do allow the combination of different built-in theories, we do not allow different built-in function symbols or user-defined function symbols to be used as arguments of our Diffie-Hellman operators. For example, a term of the form \(g^{h(e)}\), where \(h:\mathit{Msg} \rightarrow Msg\) is a user-defined function symbol, is not allowed, since our Diffie-Hellman operator take as argument terms of sort \(G\) or \(E\).

Out of the 20 case studies in the benchmark in 2), two studies used user-defined function symbols as exponents and were hence excluded. Furthermore, we also excluded some models that did not use the Diffie-Hellman built-in theory at all, one model where the proof-search was reported to not terminate, and another model whose source file was missing from the Tamarin repository.

Enabling users to define function symbols that produce outputs of sort \(\mathit{DH}\) is left for future work. In cases where such functions have no associated equations, their integration is expected to be relatively straightforward. However, when these function symbols are subject to user-defined equations, the situation becomes more complex. It would be necessary to ensure that augmenting the current rewrite system \(\rightarrow_{\mathit{DH}}\) with these additional equations preserves termination and confluence. Moreover, how to incorporate such equations within the algebraic framework is an open question.

We rewrote each of these models in our extension’s new syntax, replacing the Diffie-Hellman function symbols with the symbols of our new DH-multiplication built-in theory. We did not change anything else, including how the protocol rules are defined, or how the properties are formulated. While the protocol itself is unchanged, our extension models a more powerful adversary, capable of using additional operators, namely addition and subtraction. Nevertheless, we argue that this enhanced adversary cannot derive new attacks if the protocol rules themselves do not make use of these additional operators.

To give an intuitive argument, observe that any lemma in the protocol necessarily refers only to terms appearing in the protocol’s rules, and thus these terms do not contain the new operators. Consider an an attack trace in which the adversary uses the new operators. Since the attack trace’s final goal is to contradict the property, we consider the last adversary rule in the trace that applies one of these new operators. By construction, this rule must produce a term free of these operators in order to match the property. Now consider the structure of such a rule: it must eliminate new operators. For example, one such rule is when the adversary applies the minus operator: \[\verb![K(a+b), K(b)] --> [K(a)].!\] In this case, the adversary can only construct \(a+b\) if they already know both \(a\) and \(b\) since the protocol participants themselves cannot have produced \(a+b\). Thus, the application of the operator-based rule is not essential: if the adversary already knew \(a\) then the use of the new operator in this step can be bypassed entirely. One can apply such an argument to all such rules in the trace. Therefore, for every attack trace that uses the new operators, there exists a corresponding trace that does not use them.

Indeed, for every model and its properties, we find the same results as with the restricted Diffie-Hellman theory. Table 1 reports the time it took to prove or disprove all of the properties of each given model. All properties of all models are proved automatically with the restricted Diffie-Hellman theory. Using our extension, for the WireGuard model we manually guided the proof search tree to reduce runtimes. In particular, for WireGuard we manually proved 6 out of the 8 lemmas: we proved the 2 executability lemmas, the 2 reuse lemmas and the 2 secrecy lemmas manually. For this model, the time in Table 1 indicates the seconds or minutes it took to prove all the lemmas with the search strategy stored.

Our extension results in slower performance. This is to be expected since with new operators, there are also more potential attack traces that Tamarin must consider and exclude. In particular, verifying the WireGuard protocol takes around 5 times as long as when verified without the Diffie-Hellman extension, even when the proof is manually guided. We believe that the primary cause of this major slowdown is not precomputing sources for each premise fact, as is instead done in Tamarin without the extension. As a result, in the current implementation, these sources must be recomputed for every occurrence of a premise.

More generally, however, the use of the extension is not needed for protocols that do not explicitly rely on group multiplication. In the next sections, we therefore look at protocols that do use this operation.

7.2 ElGamal↩︎

In Section 4, we provided a Tamarin model of the ElGamal encryption scheme. We defined an executability lemma and a lemma about the secrecy of the encrypted message from Bob’s perspective. We also add a lemma about the secrecy of the received message from Alice’s perspective:

lemma secrecyA:
"All msg #i A. SecretA(A, msg)@i 
              & not (Ex #l. Compromised(A)@l) ==> 
       not (Ex #j. K(msg)@j )"

Tamarin automatically proves the executability lemma, providing a valid trace of the protocol, which takes three minutes. With manual guidance in its search tree, Tamarin proves the lemma in a few seconds. Tamarin also proves secrecy of the encrypted message from Bob’s perspective, automatically, also in a few seconds.

For the lemma secrecyA, since the non-cancellation property on \(c_1^{-ska}\cdot c_2\) does not hold, a priori there are no security guarantees if no counterexample is found. However, in this case, Tamarin automatically disproves the property, finding an attack in a few seconds. This is not surprising, since Bob is not authenticated and an adversary can send Alice any message of his choice. Thus the approach can be useful even if the non-cancellation property fails, as the counterexamples found are always valid attacks.

ElGamal’s security has been extensively studied and it is widely regarded as secure, based on the hardness assumptions of the discrete logarithm problem. While proving its security in the symbolic model may not seem to be groundbreaking, we believe it represents a significant advance: in spite of ElGamal’s widespread use, this is the first time it is automatically verified, in the symbolic model.

7.3 MQV Key Exchange↩︎

We now turn to a more complex example. MQV [18], [21] is an authenticated key exchange protocol where the key is computed by combining static and ephemeral key pairs. The shared key should not agree if the other party’s public key is not employed, thus giving implicit authentication of the correct parties. MQV’s main attractiveness is its computational efficiency; it claims to achieve authentication in two message exchanges and a few group operations. In [22], Kaliski presented an unknown key-share attack on this protocol, where Eve can trick Bob into thinking he is sharing Alice’s key with Eve instead of with Alice.

The original protocol is as follows. Alice (in the initiator role) and Bob (in the receiver role) both have a long-term private/public key pair \(\langle a,pk_A=g^a\rangle\) and \(\langle b,pk_B=g^b \rangle\) and they each compute ephemeral key pairs \(\langle x,X=g^x\rangle\) and \(\langle y,Y=g^y\rangle\). Alice and Bob send each other their ephemeral public keys \(X\) and \(Y\) and it is assumed they know each other’s public key. Alice and Bob compute

\[K_{AB} = (Y\cdot pk_B^{\mu(Y)}) ^{x+\mu(X)a}, \label{eq:KAB}\tag{2}\] \[K_{BA} = (X\cdot pk_A^{\mu(X)}) ^{y+\mu(Y)b}. \label{eq:KBA}\tag{3}\] By the algebraic properties of the operators, \(K_{AB}=K_{BA}\).

Kaliski’s unknown key-share attack [22] is as follows. Alice initiates a protocol run with Bob.

1. Eve first intercepts Alice’s ephemeral key \(g^x\). She selects a random value \(r_E\) and computes the ephemeral public key \[Z =g^x\cdot (g^{a})^{\mu(g^x)}\cdot g^{r_E}.\] Observe that Eve does not know the secret key corresponding to this public key.

2. Eve computes the following private, public key pair: \[\langle e = -\frac{r_E}{\mu(Z)}, pk_E = g^{e} \rangle.\]

3. Eve initiates a protocol run with Bob as herself, i.e. with public key \(pk_E\) from (ii) and using the ephemeral key \(Z\) computed in (i).

4. Eve receives Bob’s key and forwards it to Alice.

After these steps, Alice will compute the shared key \(K_{AB}\) as before, while Bob will also compute the same key \(K_{BE}\) but with Eve: \[\begin{align} K_{BE} &= (Z \cdot pk_E^{\mu(Z)}) ^{y+\mu(Y)b} \\ & = (g^x\cdot g^{a \mu(g^x)} \cdot g^{r_E}\cdot g^{-r_E}) ^{y+\mu(Y)b} \\ & = (X\cdot pk_A^{\mu(X)}) ^{y+\mu(Y)b} = K_{AB}. \end{align}\] This is the same key obtained in an honest key-share with party \(A\), see (3 ). Observe that Eve does, in fact, not know this key. However there is still a mismatch between the identities who share the key. Kaliski names such an attack an unknown key-share attack. Observe that this attack is only possible on the responder: Eve needs the initiator’s ephemeral key to generate her malicious ephemeral key, making it impossible to also trick the initiator.

Modelling the MQV protocol in Tamarin equipped with the new \(\mathit{DH}\) equational theory is straightforward. We provide the Tamarin model in Appendix 12. We consider an adversary that can obtain certificates for arbitrarily chosen private/public key pairs. Observe that, without a subsequent message exchange using the shared key, there can be no agreement on the parties’ identities: Alice and Bob just compute a shared key with the (possibly adversarial) ephemeral public key they receive. The authentication is implicitly obtained when decrypting/encrypting messages with a key that matches the one they have computed. Indeed, our extension of Tamarin quickly (in less than a second) and automatically falsifies the agreement properties. We thus expand the protocol model to include two messages where Bob and Alice exchange fresh nonces encrypted with the shared key (see Appendix 12). In particular we use Tamarin’s built-in symmetric encryption primitive.

Below, we state two basic security properties regarding the secrecy of the key and agreement on the key and parties sharing the key.

lemma secrecyI:
 "All I R key #i. AgreeKeyI(I, R, key)@i & (not (Ex #k. Compromised(I)@k))& 
 (not (Ex #k. Compromised(R)@k))
  ==> not (Ex #i. K(key)@i)"
  
lemma agreementI:
"All I R key #i. AgreeKeyI(I, R, key)@i & (not (Ex #k. Compromised(I)@k))& 
(not (Ex #k. Compromised(R)@k)) 
 ==> Ex #j. RunningR(R, I, key)@j"

The action fact \(AgreeKeyI\) is declared in the rule where Alice correctly decrypts a message from Bob using the shared key she computed. \(RunningI\) is declared in the first rule where Alice can compute the shared key. We also declare \(AgreeKeyR\) and \(RunningR\) action facts in Bob’s respective rules and we define similar secrecyR and agreementR properties from Bob’s perspective. Finally, we also add an exists-trace lemma executable that verifies if Bob and Alice can actually complete all their steps, exchanging a key. Note that the keys satisfy the non-cancellation property by Theorem 4 of Appendix 9.

Observe that Kaliski’s unknown key-share attack is a counterexample to agreementI, since in that scenario Alice agrees to share her key with Bob, while Bob does not think he is sharing his key with her. We manually guide Tamarin’s proof for the executability lemma to find the expected execution. We first consider the secrecyI lemma and illustrate how Tamarin handles the \(\operatorname{NoCanc}\) property. In particular, this lemma refers to the key that Alice computes: \[\begin{align} \mathit{key} & = (g^y \cdot g^{b\mu(g^y)})^{x + a\mu(g^x)} \\ & = g^{y x}\cdot g^{ya\mu(g^x)}g^{bx\mu(g^y)}g^{ba\mu(g^y)\mu(g^x)}. \end{align}\] Recall that this key corresponds to Alice’s view, so only the variables \(a\) and \(x\) are of sort \(\mathit{FrE}\): \(a\) is Alice’s secret key and hence stored as a fresh variable in her state facts, and \(x\) is freshly generated by herself. The variables \(y\) and \(b\), corresponding to Bob’s ephemeral and private key, are instead \(E\) variables, since they are possibly adversarial. Hence, at this point, \(\operatorname{NoCanc}(\mathit{key})\) does not hold. However, our lemma excludes the case where Bob is compromised since trivially the key is not secret if we share it with the adversary. Hence, Tamarin can conclude that \(b\) comes from an honest private/public key generation fact, meaning that \(b\) must be of sort FrNZE. At this point \(\operatorname{NoCanc}(\mathit{key})\) still does not hold, since \(y\) can be adversarially chosen. However, by Theorem 4, \[\operatorname{NoCanc}'(g^{ba\mu(g^y)\mu(g^x)}, \mathit{key})\] does hold. When trying to unify indicators, Tamarin will prove that the indicator of \(g^{ba\mu(g^y)\mu(g^x)} = g^{ba}\) cannot be found in any root term of any \(Out\) fact. Since \(g^{ba\mu(g^y)\mu(g^x)}\) does satisfy \(\operatorname{NoCanc}\) with the other terms, this is enough to soundly conclude that the entire term cannot be constructed. We explain the constraint solving process for this lemma in Appendix 12. The secrecy lemmas are proven automatically in a few seconds, since the infeasibility of reaching the necessary indicator terms is established quickly.

As for the property agreementI, Tamarin returns different attacks. The attacks are valid unconditionally of the \(\operatorname{NoCanc}\) property, which in fact does not generally hold on the root terms of the keys shared with compromised parties. One attack is the trace illustrated in Figure 2, where a third party (E) can perform an unknown key-share attack using a trivial public key.

This attack is essentially an instantiation of Kaliski’s unknown key-share attack, where Eve’s random value is replaced with \(r_E = 0\). While we again do not have agreement on the parties’ identities, Eve still does not actually learn the key since Alice’s and Bob’s secret keys (\(x\) and \(y\)) are not compromised. Even if this attack is unrealistic in practice (assuming participants check that public keys are not trivial), the chosen ephemeral public key Eve must use, \(Y\cdot A^{\mu(Y)}\), involves group multiplication and we believe this attack is not straightforward to find by hand. If we exclude ephemeral and public keys from being trivial group elements, Tamarin also finds the attack proposed by Kaliski. A crucial step in Tamarin’s constraint-solving algorithm for finding the attack is the unification of the session keys in Alice’s and Bob’s rules. Alice’s key is \[g^{y_Ex}\cdot g^{b\mu(g^{y_E})x}\cdot g^{y_E\mu(g^x)a} \cdot g^{b\mu(g^{y_E})\mu(g^x)a},\] while Bob’s key is \[g^{x_E y}\cdot g^{e_E \mu(g^{x_E})y} \cdot g^{x_E\mu(g^{y})b}\cdot g^{e_E\mu(g^{x_E})\mu(g^{y})b}\] Here, \(g^a\) and \(g^x\) are Alice’s long-term and ephemeral keys, and \(g^b\) and \(g^y\) are Bob’s corresponding keys. The terms \(g^{e_E}\), \(g^{x_E}\), and \(g^{y_E}\) contain unbound variables of sort \(E\).

Tamarin proceeds by unifying the root terms of Alice’s key with (possibly repeated) root terms of Bob’s key. Kaliski’s attack arises when the root terms \(g^{y_E x}\) and \(g^{y_E\mu(g^x)a}\) are both matched to \(g^{x_E y}\) by splitting \(x_E\) into a sum, and the root terms \(g^{b\mu(g^{y_E})x}\) and \(g^{b\mu(g^{y_E})\mu(g^x)a}\) are both matched to \(g^{x_E\mu(g^{y})b}\). The variables introduced by the generalized unifier are then instantiated with algebraic methods to make the other root terms of Bob’s key cancel out. Appendix 12 explains the rules used to find the attack in more detail.

Finding this attack required manual interaction. Re-running Tamarin with the solving strategy stored, it takes around half a minute for Tamarin to return the attack.

Tamarin instead excludes attacks from Bob’s (the responder) perspective, proving agreementR. As for proving the secrecy lemmas, proving this lemma also required manual interaction. When re-running the proof with the solving strategy stored, it takes Tamarin again around a half a minute to verify agreementR. Writing specific heuristics for DH extended theories (deciding which constraint solving rules to apply first) would probably be enough for Tamarin to find the proofs and attacks automatically in a reasonable amount of time.

We therefore believe our approach scales to fairly complex protocols (e.g. using different equational theories and Tamarin features) albeit with some user interaction. Other protocols, such as HMQV (the improved version of MQV) use different function symbols as exponents. In particular, HMQV uses a hash function of arity 2 as an exponent. We hence plan to integrate arbitrary user-defined function symbols with no associated equations that produce outputs of sort \(\mathit{DH}\) to perform further large case studies.

8 Conclusion↩︎

We have presented a method for the symbolic analysis of protocols utilizing all Diffie-Hellman group operators, including addition in the exponents. We have successfully integrated this method into the Tamarin prover, providing the first symbolic verifier that supports such protocols. Our integration maintains compatibility with Tamarin’s basic features, built-in equational theories and user-defined ones. We have verified the effectiveness of our approach by analyzing the ElGamal and MQV protocol. To further improve our approach, we plan to write heuristics to make Tamarin’s search more automatic, to enable user-defined \(\mathit{DH}\) function symbols and to perform case studies on other large protocols such as HMQV [23].

9 Definitions omitted in main text↩︎

In Sections 9.1 and 9.2, we recall the formal definition of dependency graphs used by the Tamarin prover, and how we modify them slightly to incorporate our equational theory. In particular, we show that we can use Tamarin’s constraint solving approach to find counterexamples to security properties.

9.1 Notational Preliminaries↩︎

We present here the notation used in [4] and [24].

For a sequence \(s\), we write \(|s|\) for the length of \(s\) and \(id_x(s)=\{1,\ldots,|s|\}\) for the set of indices of \(s\). \(S^{\#}\) denotes the set of finite multisets with elements from \(S\).

For an equational theory \(\mathcal{E}\), we define the \(\mathcal{E}\)-instances of a term \(t\) as \(inst_\varepsilon=\{t' | \exists \sigma. t\sigma =_\varepsilon t'\}\), and we call the ground \(\mathcal{E}\)-instances \(ginsts_\mathcal{E}(t)\).

Recall that we consider a user defined signature \(\Sigma_{Usr}\), that we assume disjoint from \(\Sigma_{DH}\), with an equational theory \(\mathcal{E}_{Usr}\). We assume this theory can be decomposed (by orienting equations) in a rewrite system \(R_{Usr}\). Finally, if \(\Sigma_{DH}\) contains \(AC\) operators, it is assumed that \((\Sigma_{Usr}, R_{Usr}, AC)\) has the finite variant property.

We have defined \(\mathcal{T}'\) to be the term algebra over \(\Sigma\), \(\mathit{PN}\), \(\mathit{FN}\), \(FN_G\), \(\mathit{PN}_G\), \(\mathit{FN}_{\mathit{E}}\), \(PN_{\mathit{E}}\), \(\mathcal{V}\), \(\mathcal{V}_G\), and \(\mathcal{V}_E\), where \[\begin{align} \Sigma & :=\Sigma_{Usr}\cup \Sigma_{DH},\\ \mathcal{E} &:= \mathcal{E}_{Usr} \cup \mathcal{E}_{DH}. \end{align}\]

Finally, we also assume an unsorted signature \(\Sigma_F\) partitioned into linear and persistent fact symbols. We say that a fact \(F(t_1, ,t_k)\) is linear if \(F\) is linear and persistent if \(F\) is persistent. Linear facts model resources that can only be consumed once, whereas persistent facts model resources that can be consumed arbitrarily often.

A protocol is modelled as labelled transition systems: protocol rules and adversarial capabilities are represented as multiset rewrite rules. Given a set \(R\) of multiset rewrite rules, \(ginsts(R)\) denotes the ground instances of \(R\).

Recall that for a rule ru = l-[a]->r, we define the premises as \(prems(ru) = l\), the actions as \(acts(ru) = a\), and the conclusions as \(concs(ru) = r\).

Finally, as mentioned in Section 3.2, we define following set of adversarial message deduction rules.

rule pubG: []--[K(g:PubG)]-> [K(g:PubG)]
rule FrE: [Fr(x:FrE)]--[K(x:FrE)]->[K(x:FrE)]
rule zero: []--[K(0)]->[K(0)]
rule one: []--[K(1)]->[K(1)]
rule eG: []--[K(eG)]->[K(eG)]
rule mu: [K(t)] --[K(mu(t))] -> [K(mu(t))]

rule f: [K(x1),...,K(xn)]
        --[K(f(x1,...,xn))]->[K(f(x1,\ldots,xn))] 

In particular, we distinguish these rules from Tamarin’s built-in adverarial rules \(MD\).

9.2 Dependency graphs↩︎

We modify slightly Definition 3.9 of [24], to consider equality modulo \(\mathcal{E}_{DH}\) instead of syntactic equality.

Let \(I= \{l_1- [a_1]\rightarrow r_1,\ldots, l_k - [a_k]\rightarrow r_k\}\), we define the trace of \(dg\) as \(trace(dg) = [a_1,\ldots,a_k]\)

For all protocols (i.e. set of multiset rewrite rules) \(P\) over \(\mathcal{T}'\) and message deduction rules \(D\), it follows that: \[trace(execs(P\cup D)) = trace(dgraphs_{DH}^{\mathcal{E}_{Usr}}(P\cup D))\] This is equivalent to Lemma 3.10 in [24], for \(\mathit{DH}\)-extended dependency graphs.

As done in [24], we extend the previous definition to \(\mathit{DH}\)-extended dependency graphs modulo associativity and commutativity (AC).

Since the two rewrite systems have disjoint signatures, we can consider the rewrite systems individually. They are both convergent and coherent, thus there is a unique normal form with respect to \(\mathcal{R},AC\) rewriting, denoted by \(t\downarrow_\mathcal{R}\).

Given a term \(t\), denote by \(\lceil t \rceil ^{var}\) the complete set of \(R_{Usr},AC\)-variants. Denote by \(\lceil t \rceil ^{R_{Usr}}_{insts}\) the set \[\{\tau(t)\downarrow_R| \tau\in \lceil t \rceil ^{var} \}.\] Finally, a term \(t\) is \(\downarrow_\mathcal{R}\)-normal, if \(t=_{AC}t\downarrow_{\mathcal{R}}\). We extend this to dependency graphs, \(dg=(I,D)\) is \(\downarrow_\mathcal{R}\)-normal is all rule instances in \(I\) are. Similarly to Lemma 3.11 of [24] it follows that:

Finally [24] extends the notion of dependency graphs to consider normalized instances of Tamarin’s messaged deduction rules \(MD\). In particular, the Schmidt define normal message deduction rules \(ND\), and defines normal-form conditions for dependency graphs where the rules \(MD\) are replaced by \(ND\). Considering our \(\mathit{DH}\)-message deduction rules \(MD_{DH}\) as normal protocol rules, we can use the same normal-form conditions. In particular, we consider the graphs in \[dgraphs_{DH}(\lceil P\cup MD_{DH}\rceil^{(R_{Usr})}_{insts} \cup ND )\]

and impose the same normal-form conditions as Definition 3.18 of [24]. We call the set of all these graphs for \(P\) as \(ndgraphs_{DH}(P)\). Finally, as in Lemma 3.19 of [24], we obtain that for all protocols \(P\), \[\begin{align} &trace(execs(P\cup MD_{DH} \cup MD)) =_{AC} \\ &trace(ndgraphs(P)) \end{align}\]

Hence when searching for counterexamples to security properties, we can still search for dependency graphs instead of protocol executions.

9.3 Constraint solving↩︎

We use the definition of trace properties from [24]. We add to their definition of constraints and constraint solving rules, some new constraint definitions and new constraint solving rules (see Appendices 10 and 11). As done in [24], we define a structure to be a tuple \((dg,\theta)\) where \(dg\) is a \(\mathit{DH}\)-extended dependency graph and \(\theta\) a valuation. We will use some of the constraints introduced in [24] in the following sections. These constraints and their satisfaction relation \(\vdash\) with structures are as follows:

• A node constraint \(i:ri\). \((dg,\theta)\vdash i:ri\) if \(\theta(i)\in idx(I)\) and \(\theta(ri) = I_{\theta(i)}\)

• An edge constraint \((i,u)\rightarrow(j,v)\). \((dg,\theta)\vdash (i,u)\rightarrow(j,v)\) if \((\theta(i), u)\rightarrow (\theta(j),v)\in D\)

• A formula constraint \(Fact(t)@i\). \((dg,\theta)\vdash Fact(t)@i\) if \(\theta(i)\in idx(I)\) and \(Fact(\theta(t))\in acts(I_{\theta(i)})\)

For a protocol \(P\) and message deduction rules \(MD_{DH}\cup ND\), Definition 3.35 of [24] describes a class of constraint systems that admit a \(P\) model. Essentially, the definition requires that for every edge constraint \((i,u)\rightarrow (j,v)\) there are corresponding node constraint \(i:ri\) and \(j:rj\) such that premise and conclusion fact matched. Essentially, this definition ensures that all premises are matched by a conclusion, so that a model extraction is straightforward. We extend the same definition to including our \(MD_{DH}\) rules.

Theorem 3.36 of [24] states that every well-formed constraint system \(\Gamma\) for \(P\) that is solvable with respect to \(\rightarrow_P\) has at least one \(P\)-model and we can extract such a model. Hence the goal of our constraint solving algorithm is still that of constructing a well-formed constraint system.

9.4 Definitions regarding \(\mathit{DH}\) terms↩︎

In the above \(cl_1\) and \(cl_2\) indicate respectively the first and second element of the tuple returned by the function \(cl\). We assume that the variables introduced in the previous definition are always newly chosen variables. For example, \[{cl}(\langle g^y, g^m\cdot pka^y \rangle)= \langle \langle v_1, v_2\rangle,\{v_1\mapsto g^y, v_2\mapsto g^m\cdot pka^y \} \rangle.\]

::: {#kzdmcwgu .theorem} Theorem 1 (4 (from Section 4)). The condition \(\operatorname{NoCanc}_G(X,Y)\) holds for terms \(X\) and \(Y\) if:*

1. \(X =g^{b*\mu(g^t)}\) and \(Y=g^{a*t}\), or

2. \(X = g^{a*\mu(g^{t_1})}\) and \(Y = g^{b*\mu(g^{t_2})}\),

where \(a\) and \(b\) are terms that only contain distinct variables of sort \(\mathit{FrE}\) and no \(\operatorname{inv}\) function application. :::

Essentially, this follows from the fact that fresh variables cannot be instantiated with function applications. Hence in \(1)\) only the \(t\) term can be instantiated with an term containing the \(-\) operator, creating an infinite recursion since \(t\) appears in both \(X\) and \(Y\). In \(2)\) the \(-\) symbol can only appear in a \(\mu\) term, which however has no associated equations, and hence cannot be ‘pulled out’.

9.5 Algebraic setting↩︎

10 The new constraint solving rules↩︎

10.1 Defining new constraints↩︎

We extend Schmidt’s original definition of a constraint system [24], by introducing new constraints. We also define their satisfaction relation with dependency graphs and valuations.

• For terms \(t\), \(h\) and \(L\), we define \(Eq(t, h)\) to be a particular equality constraint between two terms \(t\) and \(h\) of sort \(\mathit{DH}\). \((dg,\theta) \vDash Eq(t, h)\) if and only if \[\theta(t) =_{\varepsilon_{DH}} \theta(h).\] Observe that equality is defined modulo the full Diffie-Hellman theory.

• We have already introduced the \(t\circeq h\) constraints in Section 5. \((dg,\theta) \vDash t\circeq h\) if and only if \[\theta(h) =_{\varepsilon_{DH}} \theta(t).\]

• Given a term \(t\) such that \(\operatorname{rt}(t)=\{t_1,\ldots,t_n\}\), we introduce the constraint \(EqK(t, \langle h _1,\ldots,h_n\rangle,L)\), where \(L\) is a set of exponents. \((dg,\theta) \vDash EqK(t, \langle h _1,\ldots,h_n\rangle, L)\) if and only if for all \(i\), \(Ind_L(\theta(t_i))=Ind_L(h^{(j)}_i)\), where \(h^{(j)}_i\) is a root term of \(\theta(h_i)\).

We introduce two rules, corresponding to \(S_@\) and \(S_{Prem}\) respectively. Instead of unifying \(Fact(t)=Fact(h)\), (where \(Fact\) is not the adversarial \(K\) fact), the rules unify indicators of root terms of \(t\) and root terms of \(h\).

::: {#rul:C@ .rul} Rule 2 (\(C_{@}\)). Assuming \(\operatorname{NoCanc}(t)\), \[\frac{\ Fact(t)@i,\;\Gamma\ }{\ \Large\substack{\{Eq(t,h),\;Fact(t)@i,\\ \quad i:ri,\;\Gamma\} _{ri\in \mathcal{P}, Fact(h) \in acts(ri)} }\ }\ C_{@}.\] :::

Observe that instead of a standard equality constraint \(t=h\), we have introduced a new constraint \(Eq(t,h)\). We define a similar rule that matches premises and conclusions of rules.

Recall that we denote by \(\mathcal{E}_{simp}\) the simplified equational theory that excludes multiplication, addition, and its associated laws directly. Using this theory, we want to check the root terms of \(t\) can be unified with root terms of \(h\).

Let \(t_1,\ldots,t_n\) be the root terms of \(t\) and let \(\operatorname{rt}(h)=\{h_1,\ldots,h_m\}\) be the root terms of \(h\). We construct unification queries by considering combinations of root terms from \(\operatorname{rt}(h)\), allowing repetition. Concretely, we select a sequence of \(s\) (possibly repeated) elements \(\operatorname{rt}(h)\): \[h_{j_1},\ldots,h_{j_n}.\]

The intuition is that if distinct root terms of \(t\) (e.g., \(t_1\) and \(t_2\)) originate from the same root term of \(h\), then that root term must internally contain an addition. Since the simplified theory \(\mathcal{E}_{\mathit{simp}}\) does not introduce additions on its own, we explicitly account for this possibility by introducint substitutions with the \(+\) operator.

Formally, suppose that some \(h_{j_i}\) appears \(p\) times in the chosen sequence, with \(2 \leq p \leq n\). If \(h_{j_i}\) does not contain any exponent terms of sort \(E\), we leave the sequence unchanged. Otherwise, let \(e\) be an exponent variable of sort \(E\) occurring in \(h_{j_i}\). We introduce fresh variables \(f_1,\ldots,f_p\) of sort \(E\) and define the substitutions \[\sigma:\{e\mapsto f_1+..+f_P\}, \qquad \{\sigma_i:e\mapsto f_i\}_i.\]

We then construct modified root terms as follows: for each occurrence of \((h_{j_i})_k\), \(k=1,...,p\) in the sequence, we replace it by \(\sigma_k(h_{j_i})\), and for all other root terms \(h_{j_k}\) we apply \(\sigma\), obtaining \(\sigma(h_{j_k})\). This yields a new sequence \[h'_{j_1},\ldots,h'_{j_n}.\]

Let \(\mathcal{H}\) denote the set of all sequences of length \(n\) obtained by applying the above transformation to all possible choices of repeated root terms. Using these sequences, we define the set of unification problems

\[\begin{align} eqs(t,\operatorname{rt}(h)) = \bigl\{ \langle t_1 = h'_{j_1},\ldots, t_n = h'_{j_n} \rangle \;\big|\; h'_{j_k} \in \mathcal{H} \bigr\}. \end{align}\]

Intuitively, each element of \(eqs(t,\operatorname{rt}(h))\) attempts to unify every root term of \(t\) with a (possibly repeated) root term of \(h\). or each such equation system \(eqs\), Tamarin uses variant-based unification algorithm \(\operatorname{Unify}_{\mathcal{E}_{simp}}(eqs)\), which return a complete set of most general unifiers. In practice, it is often unnecessary to consider all most general unifiers.

• If Tamarin returns a substitution \(\sigma\in\operatorname{Unify}_{\mathcal{E}_{simp}}(eqs)\) such that \(\sigma(v_i)\neq\sigma(v_j)\) for any \(\mathit{FrE}\)-sorted variables \(v_i\) and \(v_j\), we set \(\operatorname{Unify}_{\mathcal{E}_{simp}}(eqs)=\{\sigma\}\).

• Otherwise, we let \(\operatorname{Unify}_{\mathcal{E}_{simp}}(eqs)\) be the complete set of most general unifiers.

The rule that performs the above steps is as follows:

where \(\Gamma' = gen(\sigma)\Gamma \cup \{gen({\sigma})t \circeq gen(\sigma)h\}\). Recall that the substitution \(gen(\sigma)\) generalizes the substitution \(\sigma\) by extending every variable \(v_i\) in the domain of the substitution from \(v_i \mapsto term_i\) to \(v_i\mapsto term_i + {Y_i}\), where \(Y_i\) will later be interpreted as an unknown in linear equations.

If \(\operatorname{NoCanc}(t)\) instead does not hold, and unifiers for each of the root terms are found, Tamarin will add this as an assumption of the constraint system.

In the cases where \(t\) or \(h\) are variables of compatible sorts, we can instead directly apply the following rule:

We also introduce a variant of this rule with the same name, with \(t\) and \(h\) interchanged. These rules state that when trying to unify a variable with a term, we can directly instantiate that variable with that term.

10.2 Proofs of soundness and completeness↩︎

10.2.1 Proof for rule 2↩︎

• Soundness. Soundness follows since the rule only adds constraints. Any model to the system with added constraints is also a model of the system without the additional constraints.

• Completeness. Suppose there is a model before application of the rule. Then there exists a structure \((dg,\theta)\) that satisfies the constraint \(Fact(t)@i\). By the satisfaction relations, this means that in the dependency graph \(dg\) there is a node instance given by the rule \(ru:i\) whose label is \(Fact(h)\) such that \(\theta(t) =_{\varepsilon_{DH}} \theta(h)\). Hence by definition the constraint \(Eq(t, h)\) is also satisfiable.

10.2.2 Proof for rule 3↩︎

• Soundness. Since we are only adding more constraints, this rule is sound.

• Completeness. Suppose there is a model before application of the rule. Then there exists a structure \((dg,\theta)\) that satisfies the constraint system with the constraint \(i:ri\). By the satisfaction relations, this means that in the dependency graph \(dg\) there is a node instance given by the rule \(i:ri\) whose premises are connected to other nodes. In particular there is an outgoing edge to a node \(j:rj\) with a conclusion \(Fact(h)\) such that \(\theta(t) =_{\varepsilon_{DH}} \theta(h)\). Hence as in the previous proof, by definition the constraint \(Eq(t,h)\) is also satisfiable.

10.2.3 Proof for rule 4.↩︎

• Soundness. Let \((dg, \theta)\) be a solution of the constraint system after the application of the rule. Then \(\theta \circ (gen(\sigma))\) is a solution of the system before the rule application. Indeed \(Eq(\cdot)\) and \(\circeq\) have the same semantics.

• Completeness. Suppose that \((dg,\theta)\) is a solution of the constraint system before the rule application. Thus, \[\theta(t) =_{DH} \theta(h) \quad\text{and}\quad \theta(\Gamma)\;\text{is satisfiable}.\] We show that there exists a unifier \(\sigma\) produced by the rule and a substitution \(\tau\) such that \[\tau \circ gen(\sigma) = \theta,\] which implies that \((dg,\tau)\) is a solution after the rule application.

  We distinguish two cases.

  Case 1.

  Assume there exists a unifier \(\sigma\) such that \[\sigma(v_i) \neq \sigma(v_j) \quad\text{for all distinct variables } v_i,v_j \text{ of sort } \mathit{FrE}.\]

  For each variable \(v\) of sort \(\mathit{FrE}\), let \(v_\sigma = \sigma(v)\). Since \(\theta\) must also map \(\mathit{FrE}\) variables to \(\mathit{FrE}\) variables, define \(\tau\) on \(\mathit{FrE}\)-variables by \[\tau(v_\sigma) := \theta(v).\] This is well defined by the assumption on \(\sigma\).

  For variables \(v\) of sort \(E\), let \(Y_v\) be the fresh variable introduced by \(gen\). Define \[\tau(Y_v) := \theta(v) - \sigma(v).\]

  Then by construction, \[\tau \circ gen(\sigma) = \theta,\] and therefore \((dg,\tau)\) satisfies \(\Gamma'\).

  Case 2.

  Assume that no unifier satisfies the condition of Case 1, and consider the full set of most general unifiers returned by \(\operatorname{Unify}_{\mathcal{E}_{\mathit{simp}}}\).

  Let \(t_1,\ldots,t_n\) be the root terms of \(t\). By the linearity assumption, no root term contains a product of \(E\)-variables.

  We first consider the case where \(t\) contains no \(E\)-variables. Then \(\theta(t_i)\) must be a root term for each \(t_i\), since \(\mathit{FrE}\) variables cannot be instantiated with sums.

  Since \(\theta(t) =_{DH} \theta(h)\), for each \(t_i\) we have \[\theta(t_i) = \theta(h_{j_1})_{(k_1)}+\cdots +\theta(h_{j_s})_{(k_s)},\] where \(\theta(h_{j_\ell})_{(k_\ell)}\) denotes the \(k_\ell\)-th root term of \(\theta(h_{j_\ell})\).

  By \(\operatorname{NoCanc}(t)\), and because \(t\) does not contain \(E\) variables, all but one of these factors must cancel, so there exists a unique \(\theta(h_{j})_{(k)}\) such that \[\theta(t_i) = \theta(h_j)_{(k)}.\]

  We now extract a unification query for each \(t_i\):

  • If \(\theta(h_j)\) has exactly one root term, consider the equation \(t_i = h_j\), which is unified by \(\theta\).

  • If \(\theta(h_j)\) has multiple root terms, then (by linearity) \(h_j\) contains exactly one \(E\)-variable \(e\), and \[\theta(e) = f_1 + \cdots + f_m\] for irreducible monomials \(f_\ell\). Then \(\theta(h_j)_{(k)}\) contains one of these monomials, say \(f_k\). Define \(\theta'\) to agree with \(\theta\) except that \(\theta'(e) := f_k\), i.e. we ignore the other summands. Then \(\theta'\) unifies \(t_i = h_j\).

  Applying this construction to obtain unification queries for all \(t_i\) yields a set of equations belonging to \(eqs(t,\operatorname{rt}(h))\), unified by some substitution \(\sigma\). Since \(\sigma\) is most general, there exists a substitution \(\tau\) such that \(\tau \circ \sigma (t_i) = \theta(t_i)\) for root terms in the first case, or \(\tau\circ\sigma(t_i) = \theta'(t_i)\) for root terms in the second case.

  Recall that \(gen(\sigma)\) maps each exponent variable \(e\) to \(\sigma(e) + Y_e\), where \(Y_e\) is a fresh variable. We therefore define a substitution \(\rho = \tau' \circ \tau\), where \(\tau'\) maps each such \(Y_e\) to \(f_1 + \cdots + f_m - f_k\) in the second case. This definition is well formed, since all variables introduced by \(gen\) are fresh.

  By construction, we obtain \(\rho \circ gen(\sigma) = \theta\), and hence \((dg,\rho)\) satisfies the constraint system \(\Gamma'\).

  We now consider the case where a root term \(t_i\) contains an \(E\)-variable \(v\), then by linearity \[t_i = v \cdot m,\] where \(m\) is an irreducible monomial containing only \(\mathit{FrE}\) variables. If \(\theta(t_i)\) is a root term, the above argument applies directly. Otherwise, \(\theta(v)\) must be a sum, and by selecting a single summand we again extract a unification query as above and define \(\rho\) exactly with the same procedure.

10.2.4 Proof for rules 5↩︎

• Soundness. If \((dg, \rho)\) is a model of the system after applying this rule, then \((dg, \rho \circ \sigma )\) is a model of the original system.

• Completeness. Suppose \((dg, \rho)\) is a model of the system before the rule application. Then since \(\rho(v)\) is equal to \(\rho(X)\) and \(v\) is a variable, we can split \(\rho=\theta \cup \{v\mapsto \rho(X)\}\). Then \((dg, \theta)\) is a solution to our system after rule application.

10.2.5 Proof for rule 1↩︎

Recall the Rule \(C_=\) defined in Section 5.1.

• Soundness: We need to show that if there is a model of the constraint system after application of the rule, then there is a model before application of the rule. Let \(\sigma=\sigma^{j}\) be the substitution (the rule 1 case splits over the different substitutions consisting of the basis of the solution space) for which the system after rule application admits a model \((dg , \theta)\).

  Observe that \(dom(\sigma) \subset \{Y_i\}\), where \(\{Y_i\}\) are the freshly introduced variables of sort \(E\). Define \(\theta' = \theta \circ \sigma\) and \((dg, \theta')\) is a model of the system before application of the rule. Indeed, \(\theta'(\Gamma) = \theta(\sigma(\Gamma))\), hence all the constraint in \(\Gamma\) are satisfied by \((dg, \theta')\). Similarly \(\theta'(h)\circeq\theta'(t)\) is also satisfied, since \(\sigma(t) = \sigma(h)\) (and hence also \(\theta'(t) = \theta'(h)\)), by definition of \(\sigma\).

• Completeness. We need to show that if there is a model \((dg,\theta)\) of the constraint system before application of the rule, then there is one also after. Recall that \((dg,\theta) \vDash t\circeq h\) if and only if \(\theta(t) =_{DH} \theta(h).\)

  We split \(\theta=\tau\theta'\), where \(\theta'=\theta\raisebox{-.5ex}{|}_{\{Y_i\}}\). Then, \(\theta'\) corresponds to a solution of the system \(\tau(h)=\tau(t)\). In particular there exists a instantiation \(\rho\) of the free \(E\) variables in a particular \(\sigma^j\) such that \(\theta'=\rho\sigma^j\).

  Hence \((dg,\tau\rho)\) is a model of the constraint system after rule application for the case split corresponding to \(\sigma^j\), since \(\theta=\tau\theta'=\tau\rho\sigma^{j}\).

10.3 Combining \(\mathit{DH}\) and \(\mathit{Msg}\) terms↩︎

In this section we give the constraint solving rule that allows us to solve equality constraints containing terms of both sort \(\mathit{DH}\) and of sort \(\mathit{Msg}\). These equality constraints are introduced by Tamarin when unifying \(Fact(A)\) with \(Fact(B)\) via the rules \(S_@\) or \(S_{Prem}\). In the first case \(Fact\) is an action fact, while in the second it is a premise fact.

where \(\beta=\alpha_1 ... \alpha_n\) for each \(\alpha_i \in {cl}_2(A)\cup {cl}_2(B)\) and we define the function \({eq}\) below.

Intuitively, the rule separates unification into a \(\mathit{Msg}\) part and a \(\mathit{DH}\) part. The \(\mathit{Msg}\) components are unified using \(\mathcal{E}_{Usr}\)-unification on cleaned terms, while the \(\mathit{DH}\) components are reintroduced as explicit equality constraints to be solved using the dedicated \(\mathit{DH}\) rules from the previous sections.

In the following let \(M\) denote all variables of sort \(\mathit{Msg}\) but not \(\mathit{DH}\).

• Soundnesss: the rule does not introduce false solutions. Let \(\sigma \in \operatorname{Unify}_{\mathcal{E}_{Usr}}({cl}_1(A),{cl}_1(B))\) be a unifier such that there exists a model \((dg, \theta)\) satisfying both \(\beta\circ\sigma\raisebox{-.5ex}{|}_{Msg}(\Gamma)\) and \(\beta({eq}(\sigma\raisebox{-.5ex}{|}_{DH}))\).

  Since \(\theta\) satisfies \({eq}(\sigma\raisebox{-.5ex}{|}_{DH})\), the substitution \(\theta\raisebox{-.5ex}{|}_{DH}\) equalizes the \(\mathit{DH}\) subterms abstracted during cleaning. Likewise, \(\beta\sigma\raisebox{-.5ex}{|}_{Msg}\) equalizes the \(\mathit{Msg}\) parts of \(A\) and \(B\), and thus \[\theta \circ \beta \sigma\raisebox{-.5ex}{|}_{Msg}(A)= \theta \circ\beta\sigma\raisebox{-.5ex}{|}_{Msg}(B).\] By assumption, \((dg, \theta \circ \sigma\raisebox{-.5ex}{|}_{Msg})\) also satisfies \(\Gamma\). Hence \((dg,\theta \circ \sigma\raisebox{-.5ex}{|}_{Msg})\) is a solution of the original constraint system before application of the rule.

• Completeness. We show that the rule does not remove any solutions. The idea is that any unifier of \(A\) and \(B\) is composed of unifiers of \(cl(A)\) and \(cl(B)\) since \(\Sigma_{DH}\) and \(\Sigma_{Usr}\) are disjoint and hence we can separate the substitutions of \(Msg\) and \(\mathit{DH}\) variables. More precisely, let \((dg,\theta)\) be a model of the constraint system \(\Gamma\) such that \(\theta(A)=\theta(B)\). We decompose \(\theta\) into \(\theta\raisebox{-.5ex}{|}_{DH}\) and \(\theta\raisebox{-.5ex}{|}_{M}\) according to the sort of variables. For any substitution in \(\theta\raisebox{-.5ex}{|}_{M}\) that maps a \(Msg\) variable to a \(DH\) term \(t\), we replace the term by a fresh variable \(v\). This gives a new substitution \(\theta'\) which is a unifier of \(cl_1(A)\) and \(cl_2(B)\) and the \(v\mapsto t\) mapping corresponds to a subset of the \(\beta\) function, i.e. \(\beta\theta'=\theta\raisebox{-.5ex}{|}_{M}\). By definition of \(MGU\), there exists a \(\phi\) such that: \[\phi\sigma=\theta'\] Also, \(\theta\raisebox{-.5ex}{|}_{DH}\) is a solution to \(\beta({eq}(\sigma\raisebox{-.5ex}{|}_{DH}))\) since \(\theta(A)=\theta(B)\).

  Finally, we obtain that \((dg,\phi\raisebox{-.5ex}{|}_{M}\circ \theta\raisebox{-.5ex}{|}_{DH})\) is a solution to the constraint system after rule application. Indeed \[\begin{align} & \phi\raisebox{-.5ex}{|}_{M} \circ \theta\raisebox{-.5ex}{|}_{DH} \circ \beta\circ\sigma\raisebox{-.5ex}{|}_{M}= \\ & \theta\raisebox{-.5ex}{|}_{DH} \circ \phi\raisebox{-.5ex}{|}_{M} \beta\circ\sigma\raisebox{-.5ex}{|}_{M} \\ & \theta\raisebox{-.5ex}{|}_{DH} \circ \beta (\phi\raisebox{-.5ex}{|}_{M} \sigma\raisebox{-.5ex}{|}_{M}) \\ & \theta\raisebox{-.5ex}{|}_{DH} \circ \beta (\theta'\raisebox{-.5ex}{|}_{M}) =\\ & \theta\raisebox{-.5ex}{|}_{DH}\circ \theta\raisebox{-.5ex}{|}_{M} = \theta \end{align}\]

Finally, we can solve the constraints of the form \(Eq(\alpha, \beta)\) by unifying indicators and producing \(\circeq\) constraints as described in Section 5.

11 Optimization for \(K(\cdot)\) premises.↩︎

We use a specialized rule to solve the premise \(K(\cdot)\), representing the adversary’s capabilities to perform \(\mathit{DH}\) operations when solving algebraic equations, effectively replacing also Rule 1.

First, observe that for terms of the form \(\mu(t)\), there are two options for the adversary to deduce this term. Either (i) the adversary deduces \(t\) and applies the \(\mu\) operator, or (ii) the adversary learns \(\mu(t)\) directly. We introduce a rule that performs this simple case split and hence preserves solutions.

We now consider the more general approach for general terms that are not \(\mu\) terms. Given such a term \(t\) and constraint system, we first define all possible ways to categorize the exponents of \(t\) that are compatible with the current leaked set.

Now let \(t\) be a term such that \(\operatorname{rt}(t) = \{t_1,\ldots,t_n\}\), and \(t\) is not an \(E\)-variable.

where \(\Gamma_{L}=\Gamma \cup \{K(e)@j_e, j_e<i\}_{e\in L\setminus{L^{\Gamma}_i}}\). The constraints \(EqK(t, \langle h_1,\ldots, h_n\rangle, L)\) are defined in Section 10.1, and they pair each root term \(t_k\) of \(t\) with a term \(h_k\) containing its indicator.

We now define the respective rule for variables.

Where again \(\Gamma_{L}=\Gamma \cup \{K(e)@j_e, j_e<i\}_{e\in L\setminus{L^{\Gamma}_i}}\) and this time we don’t consider \(v\in L\) and we only case split over the exponents \(e\neq v\) appearing in \(h\).

The proofs of soundness and completeness for Rule 10 are identical to those for Rule 9. We therefore present only a single proof.

• Soundness. The rule only adds constraints.

• Completeness. If there is a dependency graph satisfying the system before rule application, by Lemma 2 (see below), each root term \(t_i\) of \(t\) is connected by a \(K\)-chain to a rule containing an \(Out(h_i)\) term such that \(Ind(\theta(t_i))=Ind(\theta(h_j))\), and \(h_j\in \operatorname{rt}(\theta(h_i))\).

recv: [Out(t)] -> [K(t)] 
f: [K(t1),...,K(tn)] -> [K(f(t1,...,tn))]

In a second step, when unifying these root/indicator terms in the simplified Diffie-Hellman theory, additionally to introducing variables directly within our terms, we also allow the adversary to manipulate and combine terms arbitrarily, representing that he can apply arbitrary DH operators.

We mentioned that to do so, we will pass through algebraic systems. In particular, we will create equations over the leaked and the secret variables.

Again, suppose \(\operatorname{NoCanc}(t)\) holds for a given term \(t\), for which we want to solve \(EqK(t, \langle h_1,\ldots, h_n\rangle, L)\), where \(\mathcal{H}=\{h_1,...,h_n\}\) is a set of root terms coming from different \(Out\) facts, and \(L\) an exponent set. Let \(eqs_L(t, \mathcal{H})\) be the set of combinations of root elements of \(h_1,\ldots,h_n\) and the associated set of equations obtained following the algorithm described for Rule 4, but instead of unifying \(t_i\) with \(h_i'\), we unify \(Ind_L(t_i)\) with \(Ind_L(h_i')\).

Consider a \(\sigma\in\operatorname{Unify}_{\varepsilon_{simp}}(eqs_L(t, \mathcal{H}))\). Similarly to Rule 4, we again consider a generalization of the substitution \(\sigma\).

We will consider a function that differs slightly from the generalization process from Definition 11. There, we generalized substitutions arising from the unification of entire root terms, whereas here we unify only their secret subcomponents. Furthermore, for the \(h_i\) terms, which do not necessarily satisfy the \(\operatorname{NoCanc}\) property, we must explicitly allow for monomials containing secret variables that may cancel each other out.

To take into account the adversary capabilities, we must check if the \(gen_{\mathcal{H}}(h_i)\) can actually be combined, possibly with other adversarially known terms to construct \(gen_{\mathcal{H}}(t)\).

More precisely, we further introduce new variables \(X_k\) for each term \(h_k\) that represent the adversary exponentiating \(h_k\) with some terms. We also introduce an extra variable \(X_{n+1}\) representing the adversary multiplying the \(h_i\)’s with a term of his knowledge. We hence also introduce the corresponding constraints \(K(X_l)@j_l\) with \(j_l<i\) and \(K(X_{k+1})@j_{k+1}\) with \(j_{k+1}<i\), where \(i\) is the timepoint of the rule whose premise \(K(t)\) we are solving.

Again, as the \(X_i\) are only solved in \(\mathbb{Q}(L)\), we must further explicitly allow the adversary to multiply with the other secret monomials in \(S_{\mathcal{H}}\). We introduce \(p\) more variables \(W_p\), add the constraints \(K(g^{\sum_{e_i\in S_{\mathcal{H}} }W_ie_i})@j_w\) and \(j_w<i\), and solve the following system of equations:

\[\begin{align} & \operatorname{eq}_{t,h_1,..,h_n} := \\ & \quad gen_{\mathcal{H}}(\sigma)(t) \circeq\\ & \quad \sum_{i=1}^{n}X_igen_{\mathcal{H}}(\sigma)(h_i) +X_{n+1} + \sum_{e_i\in S_{\mathcal{H}} }W_igen_{\mathcal{H}}(e_i) . \end{align}\]

Observe that the equation above is not necessarily a linear equation, since it may involve products of variables of the form \(X*Y\). Since the current implementation supports only linear equation-solving algorithms, we can address this limitation by replacing each product \(X*Y\) with a fresh variable \(Z\). We then solve the system of equations using the Gauss elimination algorithm, obtaining a solution \(Z=t\). Provided that the resulting solution term does not contain the \(+\) function symbol, we subsequently apply variant-based unification to compute a complete set of solutions to the equation \(X*Y=t\). Supporting the more general case in which this assumption is not satisfied would require implementing more advanced algebraic techniques, such as those based on Gröbner bases (e.g.Buchberger’s algorithm). However, such cases have not arisen in our examples.

where \(\{ i:ri,\;K(t)\in prems(ri), j_1:ru_1,\ldots, j_n:ru_n, j<i,\}\subset \Gamma\) and \[\begin{align} \Gamma_{\sigma} =& \sigma(\Gamma) \cup \{K(g^{X_{n+1}})@j_{n+1}\} \cup \{K(X_i)@j_i, j_i<i\}_{i=1}^{n} \\ & \cup \{K(g^{\sum W_igen_{\mathcal{H}}(\sigma)(e_i)})@l_i, l_i<i \}_{i=1}^{p} \cup\\ & \operatorname{eq}_{t,h_1,..,h_n}. \end{align}\] Again, we distinguish two cases for \(\operatorname{Unify}_{\mathcal{E}_{simp}}\).

• If Tamarin returns a substitution \(\sigma\in\operatorname{Unify}_{\mathcal{E}_{simp}}(eqs_L(t,\mathcal{H}))\) such that \(\sigma(v_i)\neq\sigma(v_j)\) for any \(\mathit{FrE}\)-sorted variables \(v_i\) and \(v_j\), we set \(\operatorname{Unify}_{\mathcal{E}_{simp}}(eqs_L(t,\mathcal{H}))=\{\sigma\}\).

• Otherwise, we let \(\operatorname{Unify}_{\mathcal{E}_{simp}}(eqs_L(t,\mathcal{H}))\) be the complete set of most general unifiers.

The proof that this rule preserves solutions of the system and doesn’t introduce spurious one is similar to the proof concerning Rule 4.

• Soundness Let \((dg,\theta)\) be a model of the constraint system after rule application, \((dg,\theta\sigma)\) is a model of the constraint system before rule application.

• Completeness Let \((dg,\theta)\) be a model of the constraint system before rule application. Analogously to the proof concerning Rule 4, we can show there exists \(\tau\) such that \(\tau\sigma = \theta\) on the variables that are not the \(W_i\) or \(X_i\) variables. Since \((dg, \theta)\) satisfied the constraints \(K(t)\) and \(Out(h_i)\in concs(ru_j)\), in the dependency graph \(dg\), there is a construction of \(\theta(t)\) from the \(\theta(h_i)\).

  If in this construction the adversary uses the \(exp\) operator, computing \(h_i^{e_K}\) for some exponent \(e_K\) (that must be of his knowledge, since the rule in \(dg\) requires the fact \(K(e_K)\) as premise, we set \(\tau_X:X_i\mapsto e_K\), and \(K(\tau_K(X_i))\) is satisfiable, since \(e_K\) must previously by known by the adversary in \((dg,\theta)\).

  If the adversary uses the multiplication operator, there are two cases:

  • The adversary multiplying the terms \(h_i\) with some other terms \(g_i\) that only contain exponents that are known by the adversary. Then \(g_i=g^f_i\in Gen(L)\), we set \(\tau_X:X_{k+1} = \sum_i f_i\), and again \(K(\tau_X(X_{k+1}))\) is satisfiable, since \(K(\sum_f{f_i})\) is also solved in \((dg,\theta)\).

  • If the adversary uses the multiplication operator multiplying the terms \(\theta(h_i)\) with some terms \(g_i\) that also contain secret exponents, they must be terms used to cancel out other root terms of \(h_i\). Indeed, recall that we assume \(\operatorname{NoCanc}(t)\) holds and all the indicators of \(t\) are already found in the \(h_i\). So the secret exponents in the \(g_i\) terms that do not appear in \(t\) must appear in the \(h_i\) terms. Hence, \(g_i\) is of the form \(g^{l_is_i}\), where \(s_i = \theta(e_i)\) for some \(e_i\). In this case we can set \(\tau_W:W_i\mapsto l_i\), and \(K(\tau_W(g^{\sum W_i \sigma(e_i)}))@j\) will also be satisfiable by \((dg, \tau)\) since \((dg,\theta)\) also satisfies the constraint \(K(g^{\sum W_i e_i})@j\).

  Hence, we have shown that \((dg, \tau_W\tau_X\tau)\) is a model to the constraint system after rule application.

As in Section 5.1, by abuse of notation, we will assume terms \(t\) and the \(h_i\) to be of the form \(g^t\) and \(g^{h_i}\). We now proceed to find a solution to the following equation with coefficients in \(\mathbb{Q}(l_1,...l_r)\) for the given variables \(\{W_i\}\cup \{X_i\}\cup \{Y_i\}\) \[\begin{align} & \operatorname{eq}_{t,h_1,..,h_n} := \\ & \quad gen_{\mathcal{H}}(\sigma)(t) \circeq\\ & \quad \sum_{i=1}^{n}X_igen_{\mathcal{H}}(\sigma)(h_i) +X_{n+1} + \sum_{e_i\in S_{\mathcal{H}} }W_igen_{\mathcal{H}}(e_i). \end{align}\]

Matching each coefficient of the polynomials, this gives a system of equations in the variables \(\{W_i\}\cup \{X_i\}\cup \{Y_i\}\).

::: {#rul:C=K .rul} Rule 12 (\(C_{=K}\)).

If Equation \(\operatorname{eq}_{t,h_1,..,h_n}\) admits a solution, let \(\{\sigma^j\}_j\) be the corresponding solution substitutions. \[\frac{\ {\Large \substack{\operatorname{eq}_{t,h_1,..,h_n},\;K(g^{\sum(W_iE_i)})@j, \\ \;K(g^{X_{k+1}})@j_{k+1},\;K(X_i)@j_i},\;\Gamma} \ }{\\{ \sigma^j(\Gamma') \} \ }\ C_{=}.\] where \(\Gamma' = \Gamma \cup \{K(g^{\sum(W_iE_i)})@j,\;K(g^{X_{k+1}})@j_{k+1}\}\cup \{K(X_i)@j_i\}\) :::

• Soundness. We first show that this rule is sound. Let \((dg,\theta)\) be a solution to the constraint system \(\sigma(\Gamma)\). To prove soundness, we use an argument analogous to that in Section 10.2.5. If we define \(\theta' = \theta \circ \sigma\), then \((dg, \theta')\) is a model of the system before application of the rule. Indeed, \(\theta'(\Gamma) = \theta(\sigma(\Gamma))\), hence all the constraints in \(\Gamma\) are satisfied by \((dg, \theta')\).

• Completeness. As for completeness, suppose we have a solution \((dg,\theta)\) of the constraint system before rule application. Because the \(K(W_i)\) and \(K(X_i)\) premises are satisfied by \(dg\), \(\theta(X_i), \theta(W_i)\in Gen(\theta(L))\). Similarly, because \(\sigma\) is the most general unifier of the secret variables, the remaining \(\theta(Y_i)\in Gen(\theta(L))\). Then \(\theta\) must be a solution of the equation system \(\operatorname{eq}_{t,h_1,..,h_n}\), and there is an instantiation \(\rho\) of the \(W_i\), \(X_i\) and \(Y_i\) variables such that \(\rho \sigma^{j} = \theta\raisebox{-.5ex}{|}_{\{W_i, X_i, Y_i\}}\). Hence \((dg,\theta\raisebox{-.5ex}{|}_{\mathcal{V}\setminus \{W_i, X_i, Y_i\}}\circ \rho)\) is a solution to the constraint system corresponding to case \(\sigma^{(j)}\).

12 Tamarin model of MQV↩︎

We show our Tamarin model of MQV and explain the reasoning steps the extended Tamarin prover tool is now following. Note that our newly added builtin of extended Diffie-Hellman is called DH-multiplication.

theory MQV
begin
builtins: DH-multiplication, symmetric-encryption

rule GenKey: 
   [ Fr(sk:FrE) ] 
   --[  ]->
   [ !SKey($A, sk:FrE), !PubKey($A, g^sk:FrE),
     Out(g^sk:FrE) ]

rule GenKeyCompromised:
    [K(sk:E)]
   --[ Compromised($A) ]->
   [ !PubKey($A, dhExp(g, sk:E) ) ,
     Out(g^ sk:E) ]

rule InitiatorRole:
  [!SKey($I, a:FrE),!PubKey($R, g^b:E)), 
   Fr(x:FrE)]
  --[ Neq($I, $R) ]->
  [Out(g^x:FrE), 
   Initiated($I, $R, a:FrE, x:FrE, g^b:E)]

rule ReceiverRole:
let kAB = (g^x:E . g^(a:E* mu(g^x:E)))^
                  (y:FrE + b:FrE*mu(g^y:FrE))
in
  [!SKey($R, b:FrE), !PubKey($I, g^a:E), 
  In(g^x:E), Fr(y:FrE), Fr(m:FrE)]
  --[ Neq($I, $R), Neq(a:E, b:FrE), 
      Neq(x:E, y:FrE), RunningR(R,I, kAB)]->
  [ Out(g^y:FrE), Out(senc(g^m:FrE, kAB)), 
    ReceiverSend($R,$I,kAB,m:FrE) ]

rule InitiatorRole2:
let kAB = (g^y:E . g^(b:E*mu(g^y:E)))^ 
          (x:FrE + a:FrE*mu(g^x:FrE))
in
  [ In(g^y:E)), Fr(m:FrE), In(senc(g^mr:E, kAB))
  Initiated($I, $R, a:FrE, x:FrE, g^b:E), ]
  --[Neq(y:E, x:FrE), Neq(a:FrE, b:E), 
     AgreeKeyI($I, $R, kAB)]->
  [Out(senc(g^m:FrE, kAB)) ]

rule ReceiverRole2:
  [ In(senc(g^mi:E, kAB)), 
    ReceiverSend($R, $I, kAB, m:FrE)]
  --[Neq(m:FrE,mi:E), AgreeKeyR($R, $I, kAB)]->
  [ ]
  
  end

12.1 Agreement property↩︎

We first explain how Tamarin disproves the property

lemma agreementI:
"All I R K #i. AgreeKeyI(I, R, K)@i & (not (Ex #k. Compromised(I)@k))& 
(not (Ex #k. Compromised(R)@k)) 
 ==> Ex #j. Running(R, I, K)@j"

In particular, this will reconstruct the attack by Kaliski. Tamarin searches for a counterexample, in a backward manner, starting from the action fact \(AgreeKeyI(I,R,K)\) trying to build a trace that does not contain the action fact \(RunningR(R,I,K)\).

The action fact \(AgreeKeyI\) only appears in the rule InitiatorRole2, implying that we must have:

\[\begin{align} K & = (g^{y_E}\cdot g^{b\cdot \mu(g^{y_E})})^{x+\mu(g^x)a}\\ & = g^{y_Ex}\cdot g^{b\mu(g^{y_E})x}\cdot g^{y_E\mu(g^x)a} \cdot g^{b\mu(g^{y_E})\mu(g^x)a}, \end{align}\] where \(g^b\) is Bob’s (authentic) public key and \(g^{y_E}\) is the ephemeral key received.

Since Alice checks the validity of the encrypted message, the received message must be encrypted with that key. Hence the message either comes from the rule ReceiverRole using the same key, or the adversary knows the key and has encrypted the message himself (Tamarin proved the key secret in the lemma secrecyI from Section 7.3, so can easily exclude the latter case). The key in ReceiverRole is \[\begin{align} K_B & = (g^{x_E}\cdot g^{e_E \mu(g^{x_E})})^{y+\mu(g^{y})b} \\ & = g^{x_E y}\cdot g^{e_E \mu(g^{x_E})y} \cdot g^{x_E\mu(g^{y})b}\cdot g^{e_E\mu(g^{x_E})\mu(g^{y})b}, \end{align}\] where \(g^{x_E}\) is the ephemeral key received, and \(g^{e_E}\) is the (possibly malicious) public key of the agent \(E\) Bob is talking to. In particular, note that we cannot have that \(E=I\), otherwise this trace would not be a counterexample (recall that our trace cannot contain the action fact \(RunningR(R,I,K)\)).

As mentioned, since Alice checks these two keys match, Tamarin inserts the constraint

\[Eq(K, K_B).\]

The root terms of \(K\) are \[g^{x},\;g^{b\mu(g^{y_E})x},\;g^{y_E\mu(g^x)a} ,\;g^{b\mu(g^{y_E})\mu(g^x)a}\]

We then consider all permutations of root terms of \(K_B\) and unify root terms. We consider here only a permutation that leads to an attack. In particular, we try to unify the root terms with only the subterms \(g^{x_Ey}\) and \(g^{x_E\mu(g^y)b}\). The only variable of sort \(E\) in these two terms is \(x_E\), so we replace it by \(x_E = f_1+f_2\), obtaining the four root terms \[g^{f_1*y}, g^{f_2*y}, g^{f_1*\mu(g^y)*b}, g^{f_2*\mu(g^y)*b}.\] Consider the permutation corresponding to the unification queries

\[\begin{align} & g^{x*{y_E}} = _{\varepsilon_{simp}} g^{f_1 *y} ,\\ & g^{b*\mu(g^{y_E})*x} = _{\varepsilon_{simp}} g^{f_1*\mu(g^y)*b}\\ & g^{y*\mu(g^x)*a} = _{\varepsilon_{simp}} g^{f_2*y} \\ & g^{b*\mu(g^{y_E})*\mu(g^x)*a} = _{\varepsilon_{simp}} g^{f_2*\mu(g^y)*b} \end{align}\] Solving these equations gives a possible unifier: \(\sigma=\{f_1\mapsto x, f_2\mapsto a\mu(g^x), y_E \mapsto y\}\). Its generalization is given by: \[\{x_E\mapsto x + a\mu(g^x)+ Y_1, e_E \mapsto Y_2, y_E\mapsto y + Y_3\}.\]

Recall that we abstract \(\mu\)-terms away, so we introduce new variables \(\mu_y,\mu_{y_E},\mu_x\) and \(\mu_e\), keeping track of the substitutions: \[\begin{align} &\mu_y=\mu(g^y),\\ &\mu_{y_E}=\mu(g^{y+Y_3}),\\ &\mu_x = \mu(g^x), \\ &\mu_e = \mu(g^{x + a\mu(g^x) + Y_1}). \end{align}\]

We then consider all possible equalities of \(\mu\) variables. In particular, we consider the case where \(\mu_y = \mu_{y_E}\) and the others are different, which corresponds to the substitution \(Y_3=0\).

Finally, we get the equation: \[\label{eq:ex} gen(\sigma)(K_B) = gen(\sigma)(K).\tag{4}\] which, when instantiating \(Y_3=0\), corresponds to the long equation of exponents: \[\begin{align} &(y + b\mu_y)(x+\mu_x a)=\\ &(x+a\mu_x+Y_1+Y_2\mu_e)(y+\mu_yb). \end{align}\]

Observe that \(Y_1\) appears inside the term that the variable \(\mu_e\) replaces. Hence if we were to solve the equation for \(Y_1\), it would contain the variable itself. Hence we instead solve the equation for \(Y_2\), yielding \[Y_2 =-\frac{Y_1}{\mu_e}.\] We have one free variable \(Y_1\), so we set \(Y_1=v_{Y}\), for a new variable \(v_{Y}\) of sort \(\mathit{E}\).

We plug this back in our constraint system, and we need to solve for the premises of rule ReceiverRole. In particular, we need to solve \[In(g^{x+\mu_xa +v_{Y}}),\] \[!PubKey(\$E, -\frac{v_Y}{\mu_e}).\]

Consider first the constraint \(In(g^{x+\mu_xa +v_Y})\). Using the \(C_{var}\) on the rule K(x) -> In(x), we know this must come from the fact: \[K(g^{x+\mu_xa +v_Y}).\] The term is a non-variable term of sort \(G\), so we apply the Rule 9 to try to construct this term from possible \(Out\) terms of sort \(G\). In particular, there are three rules that have as conclusion an \(Out\) fact: \(Out(g^x)\) (Alice’s key generation rule), \(Out(g^a)\) (rule InitiatorRole), and \(Out(g^{f})\) for a fresh adversarial \(\mathit{FrE}\) variable \(f\).

So far, there are no rules in our constraint system \(\Gamma\) that contain an action \(K(e)\) for any exponent variable \(e\). This means for any timepoint \(i\) our current leaked set is \(L^{\Gamma}_i = \emptyset\). We hence need to consider all possible cases \(L\in \mathcal{P}(\{x, \mu_x, a, v_Y,f\})\). For each of the above \(E\) variables \(e\in \{x, \mu_x, a, v_Y,f\}\) we consider whether \(e\in L\) and in that case add the constraint \(K(e)@j_e\). For all of the fresh variables we first try to solve these goals.

Tamarin proves \(K(x)\) and \(K(a)\) are not solvable, since both \(x\) and \(a\) are fresh and hence they are not unifiable (in the simplified \(DH\) equational theory) with any root term of an \(E\)-argument appearing in \(Out\) facts. This excludes the cases where \(x\in L\) and \(a\in L\).

Tamarin finds a solution for \(K(\mu_x)@j_{\mu_x}\). Recall that \(\mu_x= \mu(g^x)\). Indeed, Tamarin first applies the rule that case splits whether the adversary learns the entire term, or first the argument and then applies the \(\mu\) operator. We consider the latter case. This introduces the constraint \(K(g^x)@k, k<j_{\mu_x}\). This is solvable by unifying the indicator of \(g^x\) (which is again \(g^x\), since Tamarin has already shown \(x\in S\)) with the \(Out(g^x)\) conclusion coming from Alice’s key generation rule. The equation generated is \(X_1x +X_2 = x\), which, since \(x\) is secret, has a unique solution \(X_1=1\) and \(X_2=0\). The constraints \(K(1)\) and \(K(0)\) are solved using the zero and one rules.

Tamarin also finds a solution for the \(K(f)\) constraint (since the rule FrNZE also has an \(Out(f)\) fact). Hence for now Tamarin has shown \(\mu_x\in L, f \in L, x\notin L, a\notin L\).

The variable \(v_Y\) is of sort \(E\) so we delay solving the constraint \(K(v_Y)\) later. We hence only have 2 cases to consider: \(L=\{\mu_x,f, v_Y\}\) or \(L=\{\mu_x,f\}\), where the first case also introduces the \(K(v_Y)@j_{v_Y}\) constraint in the system.

Recall that we have three rules whose conclusions contain \(Out\) facts with arguments: \(g^x\), \(g^a\) and \(g^f\). For both possible \(L\)’s, we must consider all possibilities of matching the indicators of the term \(g^{x+\mu_xa +v_Y}\) with the indicators of these \(Out\) terms. We consider the case where \(L=\{\mu_x,f, v_Y\}\). In this case \(Ind_L(g^{v_Y}) = e_g\), so we don’t need to further search for this indicator. Consider the case where we try to unify the remaining indicators \(Ind_L(g^x)\) and \(Ind_L(g^{\mu_xa})\) with the indicators of the terms \(g^x\) and \(g^a\).

\[\begin{align} & g^{x}= g^x, \\ & g^{a} = g^a \end{align}\] These terms are already equal, so we just generalize the \(E\) variables in our system that are not modified by the substitution, in this case \(v_Y\mapsto Y\).There are no secret variables appearing in the RHS terms \(g^x\) and \(g^a\) that are not already in the LHS terms \(g^x, g^a\), and \(g^{v_Y}\). We hence only introduce new variables \(X_1\), \(X_2\), and \(X_3\) and we get the equation: \[x+\mu_xa + Y = xX_1 + aX_2 + X_3.\]

We add the new constraints \(K(X_i)@j_i\) for \(i=1,\ldots,3\). Since \(x, a\in S\), this corresponds to the equations \[\begin{align} & X_1 = 1, \\ & X_2 = \mu_x, \\ & X_3 = Y. \end{align}\] The solution is \(X_3=Y\), where we replace \(Y\) again with a free \(E\)-variable \(v_Y\), and the introduced constraints we need to solve become: \[K(1)@j_1, K(\mu_x)@j_2, \text{ and } K(v_Y)@j_3.\] \(K(1)@j_1\) is solved using the one rule. We always solve goals of the form \(K(v)@j\), with \(v\) a variable of sort \(E\), such as \(K(v_Y)@j_3\), last.

The constraint \(K(\mu_x)@j_2\) is solved exactly like the \(K(\mu_x)@j_{\mu_x}\) constraint solved above.

Finally, let us solve the \(!PubKey\) action fact. This cannot come from the honest key generation rule, as \(-\frac{v_Y}{\mu_e}\) can never be matched by a fresh variable. It must hence come from the dishonest key generation. For that, we must solve that rule’s premise \[K(-\frac{v_Y}{\mu_e}).\] The indicator of \(-\frac{v_Y}{\mu_e}\) is \(\mu_e\), and again this can be constructed by first constructing its argument \(g^{x+\mu_xa +v_Y}\). Hence this goal is solved in the same manner as the previous one.

At this point, the only constraint we have left is the constraint \(K(v_Y)@j_3\) we have postponed before. By solving this goal, we solve the constraint system. Observe that the choice \(v_Y=f\), obtained by solving the goal \(K(v_Y)\) with the FrNZE rule, corresponds to the attack described by Kaliski. The choice \(v_Y=0\), obtained by solving the goal \(K(v_Y)\) with the zero rule, corresponds to the attack using a trivial public key described in the main body of the paper.

12.2 Secrecy property↩︎

We next illustrate how Tamarin proves the lemma

lemma secrecyI:
 "All I R key #i. AgreeKeyI(I, R, key)@i & (not (Ex #k. Compromised(I)@k))& 
 (not (Ex #k. Compromised(R)@k))
  ==> not (Ex #i. K(key)@i)"

Again, the action fact \(AgreeKeyI\) only appears in the rule InitiatorRole2, hence \(C_{\mathit{var}}\) instantiates key with \[\begin{align} key & = (g^{y}\cdot g^{b \mu(g^{y})})^{x+\mu(g^{x})a} \\ & = g^{yx}\cdot g^{b\mu(g^{y})x} \cdot g^{y\mu(g^{x})a}\cdot g^{ab\mu(g^{y})\mu(g^{x})}, \end{align}\]

where \(g^b\) is Bob’s public key and \(g^y\) is the ephemeral key supposedly sent by Bob (but adversarially controlled).

Once we have added the i:InitiatorRole2 to our contraint system, Tamarin will immediately try to solve the premises of that rule (Tamarin’s heuristics always prioritize protocol state premise goals). In particular we solve the Initiated premise which in turn appears only in the InitiatorRole rule. Again, Tamarin immediately solves the premises of InitiatorRole, namely we choose the PubKey premise.

This time, there are two rules that generate a PubKey fact: GenKey and GenKeyCompromised. Tamarin excludes the compromised case, as the lemma statement excludes Compromised(B) from appearing in the trace. Hence \(b\) is instantiated with a fresh variable \(sk_B\).

Our key variable thus becomes: \[\begin{align} key & = (g^{y}\cdot g^{sk_B \mu(g^{y})})^{x+\mu(g^{x})a} \\ & = g^{yx}\cdot g^{sk_B\mu(g^{y})x} \cdot g^{y\mu(g^{x})a}\cdot g^{a*skB\mu(g^{y})\mu(g^{x})}, \end{align}\]

The only rule that contains an action fact \(K(t)@i\), for \(t\) a \(DH\) term is the rule K(x) -[K(x)]--> In(x). Using the \(C_{var}\), we add this rule to the system and need to solve its premise: \[K(g^{yx}\cdot g^{sk_B\mu(g^{y})x} \cdot g^{y\mu(g^{x})a}\cdot g^{a*sk_B\mu(g^{y})\mu(g^{x})}).\] The term is a non-variable term of sort \(G\), so we apply the Rule 9. Observe that at this point \(\operatorname{NoCanc}(key)\) does not hold, as \(\mathit{y:E}\) is adversarial and a priori could be chosen to cancel out some of the root terms (consider for example \(y \mapsto \operatorname{inv}(x)\)).

Tamarin tries to apply \(\operatorname{NoCanc}\) anyway, keeping track that the only weaker properties that hold are \[\begin{align} & \operatorname{NoCanc}(g^{sk_B\mu(g^{y})x}, key) \text{ and,} \\ & \operatorname{NoCanc}(g^{sk_Ba\mu(g^{y})\mu(g^{x})}, key). \end{align}\] At this point Rule 9 determines all possible leaked sets. The exponents appearing in the term \(key\) are: \(\{x,y,a,sk_B, \mu(g^y), \mu(g^x)\}\). As in previous example, Tamarin shows that \(\mu(g^y)\in L\) and \(\mu(g^x)\in L\). It also shows that \(sk_B\notin L\) and \(a\notin L\).

Hence the two cases to consider are \(L=\{\mu(g^y), \mu(g^x)\}\) and \(L=\{\mu(g^y), \mu(g^x),y\}\), where in the second case we add the constraint \(K(y)@j\), with \(j<i\).

For both cases: \[\begin{align} & Ind_L(g^{sk_B\mu(g^{y})x})= g^{sk_B*x} \\ & Ind_L(g^{sk_Ba\mu(g^{y})\mu(g^{x})}) = g^{sk_B*a} \end{align}\]

Tamarin will try to unify these indicators with all possible root terms of \(Out\) facts from the protocol rules, in the simplified \(DH\)-equational theory. However, none of these unification queries will succeed, as neither \(g^{sk_B*x}\) nor \(g^{sk_B*a}\) is contained in any root term of any message, not even as argument of an encrypted message of which the adversary knows the key.

This implies the adversary cannot learn these indicators (even just one would have been enough). Since these terms are not cancellable, this shows that the adversary cannot learn the whole term, and Tamarin marks this lemma as solved.

References↩︎