Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method

Abstract

Nowadays, formal cryptographic protocol analysis relies on symbolic techniques such as narrowing and equational unification, e.g. Maude-NPA, Tamarin or AKISS crypto tools. In previous works, we developed a new narrowing strategy, called canonical narrowing, which manages to reduce the state explosion problem by introducing irreducibility constraints. In this paper, we extend canonical narrowing to handle conditional rules with SMT constraints. We demonstrate the viability of this method with the Brands and Chaum protocol using time and location information described as SMT constraints on the real numbers.

This work has been partially supported by the EC H2020-EU grant agreement No. 952215 (TAILOR), by the grant RTI2018-094403-B-C32 funded by MCIN/AEI/10.13039/501100011033 and ERDF “A way of making Europe”, by the grant PROMETEO/2019/098 funded by Generalitat Valenciana, and by the grant PCI2020-120708-2 funded by MICIN/AEI/10.13039/501100011033 and by the European Union NextGenerationEU/PRTR.

1 Introduction

Formal protocol analysis allows to determine whether an attacker can cause a protocol to fail any of its security objectives. One of the ways to perform this type of analysis is through the use of symbolic techniques, such as narrowing. There are tools for protocol analysis, like Maude-NPA [8], that use narrowing together with equational unification as a basis. These techniques are efficiently supported by the Maude language, and are also used in other protocol analysis tools such as Tamarin [15] or AKISS [4]. In our works [10, 14], we already developed a new narrowing algorithm, called canonical narrowing, which manages to reduce the state explosion problem by introducing irreducibility constraints.

In a large number of protocols, the use of laws of physics that use real numbers to represent distances, time, or coordinates is essential. The formal analysis of this type of protocols can be done using either an explicit model with physical information, or by using an abstract model without physical information, e.g., untimed, and showing it is sound and complete with respect to a model with physical information. The former is more intuitive for the user, but the latter is often chosen because not all cryptographic protocol analysis tools support reasoning about, e.g., time or space. SMT solvers allow precisely the use of explicit models with physical information, translating the physical laws into SMT constraints. In order to analyze these models using narrowing algorithms, there is a need to extend them so that they are capable of handling these restrictions. One way to do it is by having narrowing to handle conditional rules, as in [19], in which each of the constraints will be collected at runtime. In the following example, we show one of the protocols that use laws of physics. This protocol really goes beyond existing narrowing approaches such as [10, 14, 19], since two cryptographic primitives are combined, exclusive-or over a set of nonces and a commitment scheme, apart of time and location represented as real numbers, requiring both irreducibility and SMT constraints.

Example 1

The Brands-Chaum protocol [3] specifies communication between a verifier V and a prover P. P needs to authenticate itself to V, and also needs to prove that it is within a distance “d” of it. A typical interaction between the prover and the verifier is as follows, where $N_A$ denotes a nonce generated by A, $S_A$ denotes a secret generated by A, X; Y denotes concatenation of two messages X and Y, $\textit{commit}(N,S)$ denotes commitment of secret S with a nonce N, $\textit{open}(N,S,C)$ denotes opening a commitment C using the nonce N and checking whether it carries the secret S, $\oplus$ is the exclusive-or operator, and $\textit{sign}(A,M)$ denotes A signing message M.

$$\begin{aligned} P&\rightarrow V :\textit{commit}(N_P,S_P) \\&\text{//The } \text{ prover } \text{ sends } \text{ his } \text{ name } \text{ and } \text{ a } \text{ commitment }\\ V&\rightarrow P :N_V \\&\text{//The } \text{ verifier } \text{ sends } \text{ a } \text{ nonce } \text{ and } \text{ records } \text{ the } \text{ time } \text{ when } \text{ this } \text{ message } \text{ was } \text{ sent }\\ P&\rightarrow V : N_P \oplus N_V \\&\text{//The } \text{ verifier } \text{ checks } \text{ the } \text{ answer } \text{ message } \text{ arrives } \text{ within } \text{ two } \text{ times } \text{ a } \text{ fixed } \text{ distance }\\ P&\rightarrow V : S_P \\&\text{//The } \text{ prover } \text{ sends } \text{ the } \text{ committed } \text{ secret } \text{ and } \text{ the } \text{ verifier } \text{ opens } \text{ the } \text{ commitment } \\ P&\rightarrow V : sign _P(N_V ; N_P \oplus N_V) \\&\text{//The } \text{ prover } \text{ signs } \text{ the } \text{ two } \text{ rapid } \text{ exchange } \text{ messages } \end{aligned}$$

We assume the participants are located at an arbitrary given topology (participants do not move from their assigned locations) with distance constraints, where travelled time and coordinates are represented by a real number. We assumed coordinates $P_x$, $P_y$, $P_z$ for each participant P.

The previous informal Alice &Bob notation was naturally extended to include time in [1] and to include both time and location in [2]. First, we add the time when a message was sent or received as a subindex $P_{t_1} \rightarrow V_{t_2}$. Second, the sending and receiving times of a message differ by the distance between them just by adding some location constraints

$$\lfloor d(A,B) \rfloor :=\ (d(A,B)\ge 0 \wedge d(A,B)^2=(A_x-B_x)^2+(A_y-B_y)^2+(A_z-B_z)^2)$$

Third, the distance bounding constraint of the verifier is represented as an arbitrary distance d. Time and space constraints are written using quantifier-free formulas in real arithmetic. For convenience, we allow both $2*x = x + x$ and the monus function $x \dot{-} y = \textit{if}\ y < x\ \textit{then}\ x - y\ \textit{else}\ 0$ as definitional extensions.

Example 2

(Cont’d Example 1). In the following time and space sequence of actions, a vertical bar differentiates between the process and corresponding constraints associated to the metric space. The following action sequence differs from [1] only on the terms $\lfloor d(P,V)\rfloor$.

$$ \begin{array}{@{}r@{}l@{\;}l@{}} P_{t_1} \rightarrow V_{t'_1} &{}\,:\, \textit{commit}(N_P,S_P) &{} \mid t'_1 = t_1 + d(P,V) \wedge \lfloor d(P,V)\rfloor \\ V_{t_2} \rightarrow P_{t'_2} &{}\,:\, N_V &{} \mid t'_2 = t_2 + d(P,V) \wedge t_2 \ge t'_1 \wedge \lfloor d(P,V)\rfloor \\ \ P_{t_3} \rightarrow V_{t'_3} &{}\,:\, N_P \oplus N_V &{} \mid t'_3 = t_3 + d(P,V) \wedge t_3 \ge t'_2 \wedge \lfloor d(P,V)\rfloor \\ \ V &{} \,:\, t'_3\, \dot{-}\, t_2 \le 2*d\\ P_{t_4} \rightarrow V_{t'_4} &{}\,:\, S_P &{} \mid t'_4 = t_4 + d(P,V)\wedge t_4 \ge t_3 \wedge \lfloor d(P,V)\rfloor \\ \ V &{} \,:\, \textit{open}(N_P,S_P,\textit{commit}(N_P,S_P))\\ P_{t_5} \rightarrow V_{t'_5} &{}\,:\, sign _P(N_V ; N_P \oplus N_V) &{} \mid t'_5 = t_5 + d(P,V) \wedge t_5 \ge t_4 \wedge \lfloor d(P,V)\rfloor \ \end{array}$$

Fig. 1.

Mafia Attack

Fig. 2.

Hijacking Attack

The Brands-Chaum protocol is designed to defend against mafia frauds, where an honest prover is outside the neighborhood of the verifier (i.e., $d(P,V) > d$) but an intruder is inside (i.e., $d(I,V) \le d$), pretending to be the honest prover as depicted in Fig. 1. The following is an example of an attempted mafia fraud, in which the intruder simply forwards messages back and forth between the prover and the verifier. We write I(P) to denote an intruder pretending to be an honest prover P.

$$ \begin{array}{@{}r@{}r@{}l@{}l@{}l@{}} P_{ t_1} &{}\rightarrow &{}I_{t_2} &{}: \textit{commit}(N_P,S_P) &{} \mid t_2 = t_1 + d(P,I) \wedge \lfloor d(P,I)\rfloor \\ I(P)_{t_2} &{}\rightarrow &{}V_{t_3}&{}: \textit{commit}(N_P,S_P) &{} \mid t_3 = t_2 + d(V,I) \wedge \lfloor d(V,I)\rfloor \\ V_{t_3} &{}\rightarrow &{}I(P)_{t_4} &{}: N_V &{} \mid t_4 = t_3 + d(V,I) \wedge \lfloor d(V,I)\rfloor \\ I_{t_4} &{}\rightarrow &{}P_{t_5} &{}: N_V &{} \mid t_5 = t_4 + d(P,I) \wedge \lfloor d(P,I)\rfloor \\ P_{t_5} &{}\rightarrow &{}I_{t_{6}} &{}: N_P \oplus N_V &{} \mid t_{6} = t_5 + d(P,I) \wedge \lfloor d(P,I)\rfloor \\ I(P)_{t_{6}} &{}\rightarrow &{}V_{t_{7}} &{}: N_P \oplus N_V &{} \mid t_{7} = t_{6} + d(V,I) \wedge \lfloor d(V,I)\rfloor \\ &{} &{} V &{} : t_{7} \dot{-} t_3 \le 2*d\\ P_{t_{8}} &{}\rightarrow &{}I_{t_{9}} &{}: S_P &{} \mid t_{9} = t_{8} + d(P,I) \wedge t_8 \ge t_5 \wedge \lfloor d(P,I)\rfloor \\ I(P)_{t_{10}} &{}\rightarrow &{}V_{t_{11}} &{}: S_P &{} \mid t_{11} = t_{10} + d(V,I) \wedge t_{11} \ge t_7 \wedge \lfloor d(V,I)\rfloor \\ I(P)_{t_{12}} &{}\rightarrow &{}V_{t_{13}} &{}: sign_P(N_V ; N_P \oplus N_V) &{} \mid t_{13} = t_{12} + d(V,I) \wedge t_{13} \ge t_{11} \wedge \lfloor d(V,I)\rfloor \end{array} $$

This attack is physically unfeasible, since it would require that $2 * d(V,I) + 2* d(P,I) \le 2*d$, which is unsatisfiable by $d(V,P)> d > 0$ and the triangular inequality $d(V,P) \le d(V,I) + d(P,I)$, satisfied in three-dimensional space. This attack was already unfeasible in [1] using only the metric space assumptions and in [2] using a Euclidean space.

However, a distance hijacking attack is possible (i.e., the time and distance constraints are satisfiable), as depicted in Fig. 2, where an intruder located outside the neighborhood of the verifier (i.e., $d(V,I) > d$) succeeds in convincing the verifier that he is inside the neighborhood by exploiting the presence of an honest prover in the neighborhood (i.e., $d(V,P) \le d$) to achieve his goal. The following is an example of a successful distance hijacking, in which the intruder listens to the exchanged messages between the prover and the verifier but builds the last message.

$$ \begin{array}{@{}r@{}l@{\;}l@{}} P_{t_1} \rightarrow V_{t_2}~~~~~ &{}\,:\, \textit{commit}(N_P,S_P) &{} \mid t_2 = t_1 + d(P,V) \wedge \lfloor d(P,V)\rfloor \\ V_{t_2} \rightarrow P_{t_3},I_{t'_3} &{}\,:\, N_V &{} \mid t_3 = t_2 + d(P,V) \wedge \lfloor d(P,V)\rfloor \\ &{}&{} \mid t'_3 = t_2 + d(I,V) \wedge \lfloor d(V,I)\rfloor \\ P_{t_3} \rightarrow V_{t_4},I_{t'_4} &{}\,:\, N_P \oplus N_V &{} \mid t_4 = t_3 + d(P,V) \wedge \lfloor d(P,V)\rfloor \\ &{}&{} \mid t'_4 = t_3 + d(I,P) \wedge \lfloor d(I,P)\rfloor \\ V~~~~~~~ &{} \,:\, t_4\, \dot{-}\, t_2 \le 2*d\\ P_{t_5} \rightarrow V_{t_6}~~~~~ &{}\,:\, S_P &{} \mid t_6 = t_5 + d(P,V) \wedge \lfloor d(P,V)\rfloor \\ &{}&{} \mid t_5 \ge t_3 \wedge t_6 \ge t_4 \\ I(P)_{t_7} \rightarrow V_{t_8}~~~~~ &{}\,:\, sign _I(N_V ; N_P \oplus N_V) &{} \mid t_8 = t_7 + d(I,V) \wedge \lfloor d(I,V)\rfloor \\ &{}&{} \mid t_7 \ge t'_4 \wedge t_8 \ge t_6 \\ \end{array} $$

This attack was feasible in [1] using the metric space assumptions, and it was also possible in three-dimensional space in [2].

In Sect. 2, we provide some preliminaries. In Sect. 3, we introduce our new canonical narrowing with irreducibility and SMT constraints. In Sect. 4, we describe our implementation. In Sect. 5, we present some experiments using the Brands and Chaum protocol that prove its viability. In Sect. 6, we conclude and give some future work.

2 Preliminaries

We follow the classical notation and terminology from [21] for term rewriting, and from [16, 19] for rewriting logic and order-sorted notions.

We assume an order-sorted signature $\varSigma$ with a poset of sorts $(S, \le )$. The poset $(\mathsf {S},\le )$ of sorts for $\varSigma$ is partitioned into equivalence classes, called connected components, by the equivalence relation $(\le \cup \ge )^+$. We assume that each connected component $[\mathsf {s}]$ has a top element under $\le$, denoted $\top _{[\mathsf {s}]}$ and called the top sort of $[\mathsf {s}]$. This involves no real loss of generality, since if $[\mathsf {s}]$ lacks a top sort, it can be easily added.

We assume an $\mathsf {S}$-sorted family $\mathcal X=\{\mathcal X_\mathsf {s}\}_{\mathsf {s} \in \mathsf {S}}$ of disjoint variable sets with each $\mathcal X_\mathsf {s}$ countably infinite. ${\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$ is the set of terms of sort $\mathsf {s}$, and $\mathcal T^{}_{\varSigma ,\mathsf {s}}$ is the set of ground terms of sort $\mathsf {s}$. We write ${\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$ and $\mathcal T^{}_{\varSigma }$ for the corresponding order-sorted term algebras. Given a term t, $Var (t)$ denotes the set of variables in t.

A substitution $\sigma \in \mathcal{S}ubst(\varSigma ,\mathcal X){}{}{}$ is a sorted mapping from a finite subset of $\mathcal X$ to ${\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$. Substitutions are written as $\sigma =\{X_1 \mapsto t_1,\ldots ,X_n \mapsto t_n\}$ where the domain of $\sigma$ is $Dom (\sigma )=\{X_1,\ldots ,X_n\}$ and the set of variables introduced by terms $t_1,\ldots ,t_n$ is written $Ran (\sigma )$. The identity substitution is $\textit{id}$. Substitutions are homomorphically extended to ${\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$. The application of substitution $\sigma$ to a term t is denoted by $t\sigma$ or $\sigma (t)$.

A $\varSigma$-equation is an unoriented pair $t = t'$, where $t,t' \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$ for some sort $\mathsf {s}\in \mathsf {S}$. Given $\varSigma$ and a set E of $\varSigma$-equations, order-sorted equational logic induces a congruence relation $=_{E}$ on terms $t,t' \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$ (see [17]). Throughout this paper we assume that $\mathcal T^{}_{\varSigma ,\mathsf {s}}\ne \emptyset$ for every sort $\mathsf {s}$, because this affords a simpler deduction system. We write ${{\mathcal T^{}_{\varSigma /E}(\mathcal X)}_{}^{}}$ and ${\mathcal T^{}_{\varSigma /E}}$ for the corresponding order-sorted term algebras modulo the congruence closure $=_{E}$, denoting the equivalence class of a term $t\in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$ as $[t]_E \in {{\mathcal T^{}_{\varSigma /E}(\mathcal X)}_{}^{}}$.

The first-order language of equational $\varSigma$-formulas is defined as: $\varSigma$-equations $t = t'$ as basic atoms, conjunction $\wedge$ of formulas, disjunction $\vee$ of formulas, negation $\lnot$ of a formula, universal quantification $\forall$ of a variable $x{:}\mathsf {s}$ in a formula, and existential quantification $\exists$ of a variable $x{:}\mathsf {s}$ in a formula. A formula is quantifier-free (QF) if it does not contain any quantifier. Given a $\varSigma$-algebra A, a formula $\varphi$, and an assignment $\alpha \in X\mapsto A$ for the free variables X in $\varphi$, $A,\alpha \models \varphi$ denotes that $\varphi$ is satisfied and $A \models \varphi$ holds if $\forall \alpha : A,\alpha \models \varphi$.

An equational theory $(\varSigma ,E)$ is a pair with $\varSigma$ an order-sorted signature and E a set of $\varSigma$-equations. An equational theory $(\varSigma ,E)$ is regular if for each $t = t'$ in E, we have $Var (t) = Var (t')$. An equational theory $(\varSigma ,E)$ is linear if for each $t = t'$ in E, each variable occurs only once in t and in $t'$. An equational theory $(\varSigma ,E)$ is sort-preserving if for each $t = t'$ in E, each sort $\mathsf {s}$, and each substitution $\sigma$, we have $t \sigma \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$ iff $t' \sigma \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$. An equational theory $(\varSigma ,E)$ is defined using top sorts if for each equation $t = t'$ in E, all variables in $Var (t)$ and $Var (t')$ have a top sort. Given two equational theories $G=(\varSigma ,E)$ and $T=(\varDelta ,\varGamma )$, we say T is the background theory of E iff $\varSigma \subseteq \varDelta$ and for each ground $\varSigma$-formula $\varphi$, $\mathcal T^{}_{\varSigma /E} \models \varphi \iff T \models \varphi$.

An E-unifier for a $\varSigma$-equation $t = t'$ is a substitution $\sigma$ such that $t\sigma =_{E} t'\sigma$. For $Var (t)\cup Var (t') \subseteq W$, a set of substitutions $\textit{CSU}^{W}_{E}({t = t'})$ is said to be a complete set of unifiers for the equality $t = t'$ modulo E away from W iff: (i) each $\sigma \in \textit{CSU}^{W}_{E}({t = t'})$ is an E-unifier of $t = t'$; (ii) for any E-unifier $\rho$ of $t = t'$ there is a $\sigma \in \textit{CSU}^{W}_{E}({t=t'})$ such that $\sigma |_{W} \sqsupseteq _{E} \rho |_{W}$ (i.e., there is a substitution $\eta$ such that $(\sigma \eta )|_{W} =_{E} \rho |_{W}$); and (iii) for all $\sigma \in \textit{CSU}^{W}_{E}({t=t'})$, $Dom (\sigma ) \subseteq ( Var (t)\cup Var (t'))$ and $Ran (\sigma ) \cap W = \emptyset$.

A conditional rewrite rule is an oriented pair $l \rightarrow r \text{ if } \varphi$, where $l \not \in \mathcal X$, $\varphi$ is a QF $\varSigma$-formula, and $l,r \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$ for some sort $\mathsf {s}\in \mathsf {S}$. An unconditional rewrite rule is written $l \rightarrow r$. A conditional order-sorted rewrite theory is a triple $(\varSigma ,E,R,T)$ with $\varSigma$ an order-sorted signature, E a set of $\varSigma$-equations, T is a background theory, and R a set of conditional rewrite rules. The set R of rules is sort-decreasing if for each $t \rightarrow t'$ (or $t \rightarrow t' \text{ if } \varphi$) in R, each $\mathsf {s} \in \mathsf {S}$, and each substitution $\sigma$, $t'\sigma \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$ implies $t\sigma \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$.

The rewriting relation on ${\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$, written $t \rightarrow _{R} t'$ or $t \rightarrow _{p,R} t'$ holds between t and $t'$ iff there exist a $p \in Pos _{\varSigma }(t)$, $l \rightarrow r \text{ if } \varphi \in R$ and a substitution $\sigma$, such that $T \models \varphi \sigma$, $t|_{p} = l\sigma$, and $t' = t[r\sigma ]_{p}$. The relation $\rightarrow _{R/E}$ on ${\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$ is ${=_{E} ;\rightarrow _{R};=_{E}}$. The transitive (resp. transitive and reflexive) closure of $\rightarrow _{R/E}$ is denoted $\rightarrow _{R/E}^+$ (resp. $\rightarrow ^*_{R/E}$). A term t is called $\rightarrow _{R/E}$-irreducible (or just R/E-irreducible) if there is no term $t'$ such that $t \rightarrow _{R/E} t'$. For $\rightarrow _{R/E}$ confluent and terminating, the irreducible version of a term t is denoted by $t{\downarrow _ {R/E}}$.

A relation $\rightarrow _{R,E}$ on ${\mathcal T^{}_{\varSigma }(\mathcal X)}_{}^{}$ is defined as: $t \rightarrow _{p,R,E} t'$ (or just $t \rightarrow _{R,E} t'$) iff there are a position $p \in Pos _{\varSigma }(t)$, a rule $l \rightarrow r \text{ if } \varphi$ in R, and a substitution $\sigma$ such that $T \models \varphi \sigma$, $t|_{p} =_{E} l\sigma$ and $t' = t[r\sigma ]_{p}$. Reducibility of $\rightarrow _{R/E}$ is undecidable in general since E-congruence classes can be arbitrarily large. Therefore, R/E-rewriting is usually implemented [13] by R, E-rewriting under some conditions on R and E such as confluence, termination, and coherence.

We call $(\varSigma ,B,E)$ a decomposition of an order-sorted equational theory $(\varSigma ,E\cup B)$ if B is regular, linear, sort-preserving, defined using top sorts, and has a finitary and complete unification algorithm, which implies that B-matching is decidable, and the equations E oriented into rewrite rules $\overrightarrow{E}$ are convergent, i.e., confluent, terminating, and strictly coherent [18] modulo B, and sort-decreasing.

Given a decomposition $(\varSigma ,B,E)$ of an equational theory, $(t',\theta )$ is an E, B-variant [6, 11] (or just a variant) of term t if $t\theta {\downarrow _ {E,B}} =_{E} t'$ and $\theta {\downarrow _ {E,B}} =_{E} \theta$. A complete set of E, B-variants [11] (up to renaming) of a term t is a subset, denoted by ${[\![t]\!]}_{E,B}$, of the set of all E, B-variants of t such that, for each E, B-variant $(t',\sigma )$ of t, there is an E, B-variant $(t'', \theta ) \in {[\![t]\!]}_{E,B}$ such that $(t'',\theta ) \sqsupseteq _{E,B} (t',\sigma )$, i.e., there is a substitution $\rho$ such that $t' =_{B} t''\rho$ and $\sigma |_{ Var (t)} =_{B} (\theta \rho )|_{ Var (t)}$. A decomposition $(\varSigma ,B,E)$ has the finite variant property (FVP) [11] (also called a finite variant decomposition) iff for each $\varSigma$-term t, a complete set ${[\![t]\!]}_{E,B}$ of its most general variants is finite.

In what follows, the set G of equations will in practice be $G=E\uplus B$ and will have a decomposition $(\varSigma ,B,E)$.

Definition 1

(Reachability goal). Given an order-sorted rewrite theory $(\varSigma ,G,R,T)$, a reachability goal is defined as a pair $t \mathop {{\mathop {\rightarrow }\limits ^{?}}\!\!{}^*_{R/G}} t'$, where $t, t' \in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s}}^{}$. It is abbreviated as $t \mathop {{\mathop {\rightarrow }\limits ^{?}}\!\!{}^*_{}} t'$ when the theory is clear from the context; t is the source of the goal and $t'$ is the target. A substitution $\sigma$ is a R/G-solution of the reachability goal (or just a solution for short) iff there is a sequence $\sigma (t) \rightarrow _{R/G} \sigma (u_1) \rightarrow _{R/G} \cdots \rightarrow _{R/G} \sigma (u_{k-1}) \rightarrow _{R/G} \sigma (t')$.

A set $\varGamma$ of substitutions is said to be a complete set of solutions of $t \mathop {{\mathop {\rightarrow }\limits ^{?}}\!\!{}^*_{R/G}} t'$ iff (i) every substitution $\sigma \in \varGamma$ is a solution of $t \mathop {{\mathop {\rightarrow }\limits ^{?}}\!\!{}^*_{R/G}} t'$, and (ii) for any solution $\rho$ of $t \mathop {{\mathop {\rightarrow }\limits ^{?}}\!\!{}^*_{R/G}} t'$, there is a substitution $\sigma \in \varGamma$ more general than $\rho$ modulo G, i.e., $\sigma |_{ Var (t)\cup Var (t')} \sqsupseteq _{G} \rho |_{ Var (t)\cup Var (t')}$.

This provides a tool-independent semantic framework for symbolic reachability analysis of protocols under algebraic properties. Note that we have removed the condition $Var (\varphi )\cup Var (r) \subseteq Var (l)$ for rewrite rules $l\rightarrow r \text{ if } \varphi \in R$ and thus a solution of a reachability goal must be applied to all terms in the rewrite sequence. If the terms t and $t'$ in a goal $t \mathop {{\mathop {\rightarrow }\limits ^{?}}\!\!{}^*_{T/G}} t'$ are ground and rules have no extra variables in their right-hand sides, then goal solving becomes a standard rewriting reachability problem. However, since we allow terms $t,t'$ with variables, we need a mechanism more general than standard rewriting to find solutions of reachability goals. Narrowing with R modulo G generalizes rewriting by performing unification at non-variable positions instead of the usual matching modulo G. Soundness and completeness of narrowing for solving reachability goals are proved in [13, 20] for unconditional rules R modulo an equational theory G and in [19] for conditional rules R modulo an equational theory G, both with the restriction of considering only order-sorted topmost rewrite theories, i.e., rewrite theories were all the rewrite steps happen at the top of the term.

3 Canonical Narrowing with Irreducibility and SMT Constraints

This section extends the canonical narrowing strategy of [10] with SMT constraints.

When $(\varSigma ,E\cup B)$ has a decomposition as $(\varSigma ,B,E)$, then the initial algebra $\mathcal T_{\varSigma /E\cup B}$ is isomorphic to the canonical term algebra $\mathcal C_{\varSigma /E\cup B}=(C_{\varSigma /E\cup B},{\rightarrow _{R/E \cup B}})$, where $C_{\varSigma /E\cup B}=\{C_{\varSigma /E\cup B,\mathsf {s}}\}_{\mathsf {s}\in \mathsf {S}}$ and $C_{\varSigma /E\cup B,\mathsf {s}}=\{[t{\downarrow _ {\overrightarrow{E},B}}]_{B} \in T_{\varSigma /B}\mid t{\downarrow _ {\overrightarrow{E},B}} \in T_{\varSigma ,\mathsf {s}}\}$ and where for each $f\in \varSigma$, $f_{\mathcal C_{\varSigma /E\cup B}}([t_1]_B,\ldots ,[t_n]_B)=$ $[f(t_1,\ldots ,t_n){\downarrow _ {\overrightarrow{E},B}}]_B$.

We have an isomorphism of initial algebras $\mathcal T_{\varSigma /E\cup B} \cong \mathcal C_{\varSigma /E\cup B}$. Likewise, we have an isomorphism of free $(\varSigma ,E\cup B)$-algebras $\mathcal T_{\varSigma /E\cup B}(\mathcal X) \cong \mathcal C_{\varSigma /E\cup B}(\mathcal X)$, where $\mathcal C_{\varSigma /E\cup B}(\mathcal X)=(C_{\varSigma /E\cup B}(\mathcal X),\rightarrow _{R/E\cup B})$ and

$$C_{\varSigma /E\cup B,\mathsf {s}}(\mathcal X)=\{[t{\downarrow _ {\overrightarrow{E},B}}]_{B} \in T_{\varSigma /B}(\mathcal X)\mid t{\downarrow _ {\overrightarrow{E},B}} \in T_{\varSigma }(\mathcal X)_{\mathsf {s}}\}.$$

The key point of canonical rewriting is that we can simulate rewritings $[t]_{E\cup B} \rightarrow _{R/E\cup B} [t']_{E\cup B}$ by corresponding rewritings $[t{\downarrow _ {\overrightarrow{E},B}}]_{B} \rightarrow _{R/E\cup B} [t'{\downarrow _ {\overrightarrow{E},B}}]_{B}$ and make rewriting decidable when $(\varSigma ,B,\overrightarrow{E})$ is FVP.

Definition 2

(Canonical Rewriting). Let $\mathcal R=(\varSigma ,E\cup B,R,T)$ be a topmost order-sorted rewrite theory such that $(\varSigma ,E\cup B)$ has an FVP decomposition $(\varSigma ,B,E)$. Let $\mathcal C^{\circ }_{\varSigma /E\cup B}(\mathcal X)_{\mathsf {State}}=\bigcup \mathcal C_{\varSigma /E\cup B}(\mathcal X)_{\mathsf {State}}$, i.e., $\mathcal C^\circ _{\varSigma /E\cup B}(\mathcal X)_{\mathsf {State}}=\{t{\downarrow _ {\overrightarrow{E},B}}\mid t{\downarrow _ {\overrightarrow{E},B}}\in T_{\varSigma }(\mathcal X)_{\mathsf {State}}\}$, so that $\mathcal C^{\circ }_{\varSigma /E\cup B}(\mathcal X)_{\mathsf {State}} \subseteq T_{\varSigma }(\mathcal X)_{\mathsf {State}}$. We then define the $\rightarrow _{R/E,B}$ canonical rewrite relation with rules R modulo $E\cup B$ as the following binary relation $\rightarrow _{R/E,B} \subseteq \mathcal C^\circ _{\varSigma /E\cup B}(\mathcal X)_{\mathsf {State}} \times \mathcal C^\circ _{\varSigma /E\cup B}(\mathcal X)_{\mathsf {State}}$, where $t \rightarrow _{R/E,B} t'$ iff $\exists l\rightarrow r \text{ if } \varphi \in R$ and $\exists \theta$ with $Dom (\theta ) \subseteq Var (l)\cup Var (r)\cup Var (\varphi )$ and $\theta =\theta {\downarrow _ {\overrightarrow{E},B}}$ such that: (i) $T\models \varphi \theta$, (ii) $(l\theta ){\downarrow _ {\overrightarrow{E},B}} =_{E\cup B} t$, and (iii) $t'=_{B} (r\theta ){\downarrow _ {\overrightarrow{E},B}}$.

The claim that $\rightarrow _{R/E,B}$ exactly captures/bisimulates the $\rightarrow _{R/E \cup B}$ rewrite relation is justified by the following result.

Theorem 1

For each $t,t'\in T_\varSigma (\mathcal X)_\mathsf {State}$, $t \rightarrow _{R/E\cup B} t'$ iff $t{\downarrow _ {\overrightarrow{E},B}} \rightarrow _{R/E,B} t'{\downarrow _ {\overrightarrow{E},B}}$.

A term $t(x_1{:}s_1,\ldots ,x_n{:}s_n)$ can be viewed as a symbolic, effective method to describe a (typically infinite) set of terms, namely the set

$$\lceil t(x_1{:}s_1,\ldots ,x_n{:}s_n)\rceil = \{t(u_1,\ldots ,u_n)\mid u_i\in {\mathcal T^{}_{\varSigma }(\mathcal X)}_{\mathsf {s_i}}^{}\}=\{t\theta \mid \theta \in \mathcal{S}ubst(\varSigma ,\mathcal X){}{}{}\}.$$

We think as t as a pattern, which symbolically describes all its instances (including non-ground). However, since $(\varSigma ,B,E)$ is a decomposition of an equational theory $(\varSigma ,E\cup B)$, we can consider only normalized instances of t

$$\lceil t\rceil _{\overrightarrow{E},B} = \{(t\theta ){\downarrow _ {\overrightarrow{E},B}} \mid \theta \in \mathcal{S}ubst(\varSigma ,\mathcal X){}{}{}\}$$

However, since we are interested in terms that may satisfy some irreducibility and SMT conditions, we can obtain a more expressive symbolic pattern language where patterns are constrained by both irreducibility and SMT constraints. That is, we consider constrained patterns of the form $\langle {t,\varPi ,\varphi }\rangle$ where $\varPi$ is a finite set of normalized terms and $\varphi$ is a QF $\varSigma$-formula. Then we can define:

$$\begin{aligned} \lceil \langle {t,(u_1,\ldots ,u_k),\varphi }\rangle \rceil _{\overrightarrow{E},B} = \{(t\theta ){\downarrow _ {\overrightarrow{E},B}}\ \mid&\ \theta \in \mathcal{S}ubst(\varSigma ,\mathcal X){}{}{}, T \models \varphi \theta ,\\&\ u_1\theta ,\ldots ,u_k\theta \text{ are } \overrightarrow{E},B\text{-normalized } \}. \end{aligned}$$

The canonical narrowing relation $\leadsto _{R/E,B}$ includes irreducibility constraints only for the left-hand sides of the rules and SMT constraints only from the conditional part of the rules.

Definition 3

(Canonical Narrowing). Given a topmost order-sorted rewrite theory $(\varSigma ,E\cup B,R,T)$ such that $(\varSigma ,B,E)$ is a decomposition of $(\varSigma ,E\cup B)$, the canonical narrowing relation with irreducibility constraints holds between $\langle {t,\varPi ,\varphi }\rangle$ and $\langle {t',\varPi ',\varphi '}\rangle$, denoted

$$\langle {t,\varPi ,\varphi }\rangle \leadsto _{\alpha ,R/E,B} \langle {t',\varPi ',\varphi '}\rangle $$

iff there exists $l\rightarrow r \text{ if } \varphi ''\in R$, which we always assume renamed, so that $Var (\langle {t,\varPi ,\varphi }\rangle )\cap ( Var (r)\cup Var (l)\cup Var (\varphi ''))=\emptyset$, and a unifier $\alpha \in \textit{CSU}^{W}_{E\cup B}({t = l})$, where $W= Var (\langle {t,\varPi ,\varphi }\rangle )\cup Var (r)\cup Var (l)\cup Var (\varphi '')$, and

• 1. $\langle {t',\varPi ',\varphi '}\rangle = \langle {r\alpha , \varPi \alpha \cup \{(l\alpha ){\downarrow _ {\overrightarrow{E},B}}\}, \varphi \alpha \wedge \varphi ''\alpha }\rangle$,

• 2. $\varPi \alpha \cup \{(l\alpha ){\downarrow _ {\overrightarrow{E},B}}\}$ are $\overrightarrow{E},B$-irreducible, and

• 3. $\varphi '$ is satisfiable, i.e., $\exists \alpha '$ s.t. $T \models \varphi '\alpha '$.

Note that we do not require a narrowing step to compute $\textit{CSU}_{E\cup B}({t \mathop {=}l})$ anymore, we perform regular equational unification but impose an irreducibility constraint on the normal form of the instantiated left-hand side, which can be handled in Maude by using asymmetric unification [7], i.e., equational unification is done with irreducibility constraints.

Irreducibility constraints are computed by using the normalized left-hand side of the rules that are used in the narrowing steps. SMT constraints are simply added to the third component and check for satisfiability. Note that we assume that satisfiability of QF $\varSigma$-formulas is decidable, indeed for a subsignature $\varSigma _0 \subseteq \varSigma$ associated to the background theory T. Maude is using the CVC4 SMT solver for satisfiability.

Each trace will carry a different set of irreducibility and SMT constraints, although some of the conditions are shared by having common predecessor nodes. In each new narrowing step, the list of irreducibility constraints computed previously in that sequence must be taken into account, so that if it is necessary to reduce one of the terms appearing in the list to compute a new step, it will be discarded. Similary, the SMT formula carried along the sequence must be taken into account, so that if it becomes unsatisfiable after one narrowing step, it will be discarded.

In this way, we eliminate redundancy as well as branches of the reachability tree, which will be less and less wide than the tree resulting from using standard narrowing. In some cases, we will even get infinite reachability trees to become finite, ensuring termination.

The key completeness property about this relation is the following.

Lemma 1

(Lifting Lemma). Given $\langle {t,\varPi ,\varphi }\rangle$, a $\overrightarrow{E},B$-normalized substitution $\theta$, and terms $u,v\in \mathcal C^\circ _{\varSigma /E,B}(\mathcal X)$ such that $u=(t\theta ){\downarrow _ {\overrightarrow{E},B}}$, $T \models \varphi \theta$, and $\varPi \theta$ are $\overrightarrow{E},B$-normalized and $u\rightarrow _{R/E,B} v$, there is a canonical narrowing step with irreducibility and SMT constraints

$$\langle {t,\varPi ,\varphi }\rangle \leadsto _{\alpha ,R/E,B} \langle {r\alpha ,\varPi \alpha \cup \{(l\alpha ){\downarrow _ {\overrightarrow{E},B}}\},\varphi '}\rangle $$

and a $\overrightarrow{E},B$-normalized substitution $\gamma$ such that

$$ \begin{array}{lcl} ~~\langle {t,\varPi ,\varphi }\rangle &{}\leadsto _{\alpha ,R/E,B} &{}\langle {r\alpha ,\varPi \alpha \cup \{(l\alpha ){\downarrow _ {\overrightarrow{E},B}}\},\varphi '}\rangle \\ ~~~\downarrow _{\theta } &{} &{} \downarrow _{\gamma }\\ \lceil \langle {t,\varPi ,\varphi }\rangle \rceil _{\overrightarrow{E},B} &{} \rightarrow _{R/E,B} &{}\lceil \langle {r\alpha ,\varPi \alpha \cup \{(l\alpha ){\downarrow _ {\overrightarrow{E},B}}\},\varphi '}\rangle \rceil _{\overrightarrow{E},B} \end{array} $$

• (i) $\theta =_B (\alpha \gamma )|_{ Var (\langle {t,\varPi ,\varphi }\rangle )}$,

• (ii) $(r\alpha \gamma ){\downarrow _ {\overrightarrow{E},B}} =_B v$,

• (iii) $\varPi \alpha \gamma \cup \{((l\alpha ){\downarrow _ {\overrightarrow{E},B}})\gamma \}$ are $\overrightarrow{E},B$-normalized,

• (iii) $T \models \varphi '\gamma$.

Note that this shows that $v\in \lceil \langle {r\alpha ,\varPi \alpha \cup \{(l\alpha ){\downarrow _ {\overrightarrow{E},B}}\},\varphi '}\rangle \rceil _{\overrightarrow{E},B}$.

4 Implementation

To implement SMT constraint handling in the narrowing algorithm, we have used our implementation of standard/canonical narrowing [14] as a starting point. To do this, we use the features of the Maude meta-level, thus creating an extension of the previous meta-level command.

4.1 Our Previous Narrowing Command

The meta-level command we use as a starting point already allows us to choose between several narrowing algorithms to use. First of all, it allows to invoke the standard narrowing algorithm, with a behavior similar to the standard narrowing built-in in Maude. It also allows the canonical narrowing algorithm [14] to be invoked, in which irreducibility constraints are used to reduce the width of the computed reachability tree. To control the algorithm used along with other parameters, such as the maximum depth of the tree or the maximum number of solutions to search for, the command uses ten arguments:

In the implementation of that command, we already prepared an adequate infrastructure to allow future extensions. Several data structures and substructures were defined to represent the reachability tree, its nodes, and the solutions found. Additionally, we divided the implementation into three main parts, which correspond to the main steps of the algorithm at a theoretical level: (i) the generation of nodes (terms) in the reachability tree, (ii) the attempt to unify each new term with the target term, and (iii) the computation of solutions in case the unification is successful. Those main parts are further broken down into highly distinguishable subparts, making it easy to make extensions or modifications to some parts without having to change the rest of the implementation.

4.2 Using Conditional Rules in Narrowing

To manage SMT constraints, our approach has been to use Maude’s conditional rules to add them as a condition in each of the narrowing steps. The problem that arises is that the Maude narrowing mechanisms are not capable of processing the conditional rules. The way to fix this is to transform those conditional rules into normal rules, in which the new left-hand side of the new rules will contain both the left-hand side of the conditional rules and the SMT constraints. An operator should separate both parts, so that later the original term can be distinguished from the SMT restrictions.

We have implemented a module that is responsible for carrying out the process of transformation of conditional rules. This module defines two operators:

The first receives a module, theory, module with strategy or theory with strategy. In either case, a new operator is added to the set of operators of the module or theory, which will be used to separate the terms from the SMT constraints in the transformed rules. It is also necessary to add the import of the Maude META-TERM module to the converted module, so that it is capable of processing the addition of this new operator. Finally, this operator calls the other defined operator, using as an argument the set of rules of the module to be transformed. For example, the equation used to transform a module without strategy would be the following:

The second operator, therefore, receives a set of rules, and is in charge of iterate through it looking for conditional rules. Each time a conditional rule is found, it is transformed into a new unconditional rule, in which the condition is added to the left-hand side using the >> operator defined above. The equations used to do this are as follows:

Thus, if we have a conditional rule of the form crl Lhs => Rhs if (SmtConst = BooleanValue) [Attrs], it will be automatically transformed into an unconditional rule of the form rl Lhs => (SmtConst>> Rhs) [Attrs narrowing], where Lhs and Rhs are variables of Universal type (that is, they can be instantiated as any sort), SmtConst is a variable that represents the SMT constraints, and BooleanValue is a Boolean variable expected to be true, used only to be able to encode SMT constraints in the conditions of the rules. The new form of the rule after transforming it will allow us later to make the >> operator disappear and separate the term from the SMT constraints. This is explained in detail in the following section.

4.3 Extension to Handle SMT Constraints

Once we have prepared the module transformation to convert all the conditional rules into unconditional ones, we can extend the previous command so that it processes the SMT terms that will be generated with the new rules. This extension has been done without making changes at the user level, except for the addition of possible values to one of the existing arguments, as well as a new argument that allows to indicate initial SMT constraints:

Until now, the fifth argument, of type AlgorithmOptionSet, only accepted the standard and canonical values, used to indicate the type of narrowing algorithm to use. Now, it also accepts combinations of those two values with the smt and noCheck values, although the second is a limitation of the first, so it cannot appear without it. By using the smt value, the transformation of the conditional rules will be performed in the module used as rewrite theory if necessary. Subsequently, the SMT constraints will be processed during the execution of the algorithm to check if they are satisfiable at each node of the reachability tree. If it is also accompanied by the value noCheck, only the transformation of the rules will be carried out, ignoring the satisfiability of the SMT constraints.

The most relevant changes to the algorithm occur before trying to unify the term of a new generated node with the target term, since the satisfiability of the SMT constraints for that node will have to be checked first. Until reaching that step, not many modifications are needed, since the narrowing steps will be given using the rules in a usual way, because the transformation of conditional rules will have been previously carried out just at the beginning of the algorithm, if the user indicates that SMT constraints are being used. Furthermore, we need to modify the previously used data structures. Now the main structure must save the initial SMT constraints indicated by the user. It will also be necessary for each of the nodes to contain a list of the SMT constraints carried so far. We have stored that list at each node in a {Term, Bool} pair, where the second value of the pair indicates the satisfiability of the constraints found in the first value. Two new operators are introduced in the algorithm that run after the generation of a new node and renaming of its variables, although they will only be used if the user indicates that SMT restrictions must be processed:

The evaluateSMT operator performs the separation of the SMT constraints from the new term generated with one of the transformed rules. In turn, it joins these restrictions with the list of restrictions carried so far, which will come from the predecessor nodes to the current one and from the initial restrictions indicated by the user. Additionally, it launches to evaluate all those restrictions, to know if they are satisfiable or not. To do this, we rely on Maude’s SMT interface, which is available in the meta-level. Specifically, we use the metaCheck [5, §16], which receives the module to use and the term to evaluate, returning a value of type Bool. If the result is true, the constraints are satisfiable. Otherwise, false is returned:

Note that in case the user has indicated, in addition to the smt value as an argument, the noCheck value, the evaluateSMT operator will only separate the SMT constraints from the term, ignoring the rest of the process, since we are not interested in checking the satisfiability, but in being able to process the constraints of the initial conditional rules.

The checkSat operator is responsible for processing the result obtained when executing the metaCheck function. If the restrictions are satisfiable, the next execution step should be the attempt to unify the term of the node with the objective term, to check if it corresponds to one or more solutions of the reachability problem. If the constraints are not satisfiable, then it will not make sense to perform the unification step, since we will not consider the term of the node as valid. We therefore return to the step of generating new nodes, marking the current node as invalid, so that it is not taken into account later, since we do not want to generate the possible child nodes of this node either.

4.4 Variable Consistency

As we explained in our previous work [14] on which we based this algorithm, the way Maude generates the fresh variables may lead to clashes. For this reason, the fresh variables that are generated in each narrowing step must be renamed using an internal counter, and using the $ symbol as an identifier. Since the variables in the SMT constraints are related to those used in the terms, as well as to the variables in the previously processed SMT constraints, there is a consistency problem with this renaming. That is why in each narrowing step, we now have to apply variable substitutions to the SMT constraints so that there is no such loss of consistency. Specifically, at each narrowing step, the computed substitution that must be applied to the term of the previous node to take that step must be applied to the new node’s SMT constraint. The substitution must also be applied to the SMT constraint list carried along the node branch. In turn, this list will already come with the variables renamed in the previous steps, so consistency builds up. Note that the initial SMT restrictions indicated by the user will also have to be renamed. This is not a problem, since these constraints are also automatically added to the list of constraints of each node, so it can be renamed at the same time as the rest.

5 Experiments

For the experiments, we have considered the Brands and Chaum protocol of Example 2 in two forms: its version with only time, published in [1], and its version with time and space, published in [2]. In both, the use of SMT restrictions is necessary, which in our case are codified with conditional rules. As explain in Sect. 4, these conditional rules will be processed to transform them into unconditional rules, in order to correctly obtain the SMT constraints at each narrowing step.

All the files used to define the new narrowing algorithm, as well as the experiments that we will see next and their results, can be found at the following link: https://github.com/ralorueda/smt-narrowing.

5.1 Handling SMT Constraints

We rely on the generic rewrite theory for protocol specification, inspired on the strand spaces [12] used by Maude-NPA [8], used in our previous work on canonical narrowing [14], but with some modifications that adapt it to include SMT constraints on the real numbers, inspired on the constraints used in [1, 2]. It is a module that allows us to specify a state, made up of sets of strands and the intruder knowledge, which represents the communication channel. With it we can represent the protocols in a generic way, adding the corresponding equational theories for each of them. Later, when coding the narrowing calls, we will specify the exact strands of each protocol.

In the original module, we had two transition rules. One of them processes the sent messages, and the other the received messages:

It can be seen in each of them how, for each set of strands, represented in square brackets, there is a list to the left of the operator | and one to the right. The first contains the messages to be processed, while the second contains the processed messages. At each transition, a message (sent or received) is taken from the end of the list of messages to be processed and moved to the list of processed messages. In the event that it is a sent message, the correspondence of that message will also be modified in the communication channel or intruder knowledge.

To adapt the module to protocols using non-linear arithmetic constraints on the real numbers via satisfiability, we add a conditional rule that is responsible for processing a new type of data that can appear in the strands sets: constraints. Specifically in our case, SMT constraints (type Boolean), which will be represented in the channel between the messages with the operator {_}. We will therefore now have three rules. One of them is responsible for processing the messages sent, another the messages received, and another the restrictions that occur at any given time:

Note that in this case we use variables from different sorts, SMsgListR-Ee and SMsgListR-eE, rather than the ones we used in [14]. This is because we have created a rule hierarchy, mimicking some optimizations of the Maude-NPA [9], in such a way that a more defined processing order is followed, significantly reducing the computation time in the experiments. In this way, whenever there is a constraint at the end of the list of messages to be processed in a strand set, it will be processed first. If this is not the case, it will check if there is any received message at the end of the list of messages to be processed in a strand set, and will be processed. If neither of these two cases occurs, then a sent message will be processed.

5.2 Brands and Chaum with Time

The previous module allows us, in a generic way, to specify protocols that contain SMT restrictions. To this must be added the specific equational theories of each protocol. In our case, the first protocol used is Brands and Cham with time [1], which can be seen as a simplified version of the protocol seen in Example 1, but does not take into account the coordinates of the messages. Two cryptographic primitives are combined: exclusive-or over a set of nonces and a commitment scheme. Exclusive-or is defined with the following properties:

The commitment scheme allows a participant to commit to a chosen hidden value at an early protocol stage and reveal it later. It is defined with the following properties:

The open function is defined only for the successful case. This implies the use of the kind [Boolean] rather than the sort Boolean. We also use additional operators for this protocol, which allow us to define signing, message concatenation, and the creation of nonces and secrets.

Additionally, we add several operators that will allow us to add metadata to the messages. In them, the sending and receiving times of the messages will be saved, as well as the identifier of the sender and the receiver.

Note that times will be represented as real numbers, one of the data types manageable by Maude’s SMT interface. The distance between two participants A and B is represented by a variable dab:Real.

The module defined with the previous sorts, operators and rules allows us to code the strands of the Brands and Chaum protocol of Example 1 only with time. This will be done in the call to the narrowing algorithm, with an initial state and a target state. In the initial state, the strand sets will contain a list of messages and constraints to be processed and a list of messages and constraints processed, which will be empty. In the target state, the lists will have been inverted, so that all the messages and restrictions to be processed become processed. Consider, for example, the strands of a prover and a verifier in a regular execution of the Brands and Chaum protocol with time. With our syntax, they would be specified in the initial state as follows:

We can see how the prover, Bob, will first send a commit to the verifier. Afterwards, the verifier, Alice, sends her nonce to the prover. Subsequently, the prover will send the XOR of his nonce with the received one, and then sends the secret. The verifier will open it to confirm everything is okay. Finally, the prover will send the signs messages. An @ operator appears in each message, after which the sending and receiving times of the message are saved, as well as the identifier of the sender and receiver. We can also see how SMT constraints are introduced after each received message. In them, conditions to be met are specified regarding the delivery and reception times. Conditions to satisfy relative to distances are also specified. For example, in the SMT constraint that is introduced on the strands of the prover, it is specified that the arrival time of the received message must be equal to its departure time plus the distance between the prover and the verifier. It is also specified that this distance must be greater than zero, and that the sending time of the message must be equal to or greater than the time in which the previous message was received.

Using this syntax and coding methodology, we have defined three experiments in which we test a regular execution of the protocol, a mafia-like attack pattern, and a hijacking-like attack pattern. In regular execution, we get a solution, which is expected, since if the protocol is well defined, this execution should be possible. In the case of the mafia attack, a priori, a solution is also found, which translates into a possible vulnerability. However, adding the triangle inequality $(d(a,i) + d(b,i)) > d$ as the initial constraint, together with the constraint $d(V,P)> d > 0$, no solution is found. This is because, for consistency to exist in this execution, it is necessary that $2 *d(V, I) + 2 *d(P, I) \le 2 *d$. As mentioned in Sect. 4, the initial SMT constraints can be written in one of the arguments of the narrowing command. However, it is possible to perform a hijacking attack, and that is why by specifying this pattern in one of the experiments, a solution is found. The attack occurs when an intruder located outside the neighborhood of the verifier (i.e., $d(V, I) > d$) succeeds in convincing the verifier that he is inside the neighborhood by exploiting the presence of an honest prover in the neighborhood (i.e., $d(V,P) \le d$).

5.3 Brands and Chaum with Time and Space

The second protocol that we have used for the experiments is an extension of the previous one: Brands and Chaum with time and space, detailed at a theoretical level in Example 2. In this case, the coordinates related to the sending and receiving of each message appear in the metadata of the messages and in the restrictions, that is, the coordinates of the participants. To be able to write this, a slight modification of the previous protocol specification is enough, as well as the addition of a new operator:

Once the modification is done, it is possible to encode the new strands. For example, the strands for a verifier and a prover in a regular execution of the protocol would now be as follows:

The exchange of messages is very similar to what we have seen before, but in this case the metadata is somewhat more complex, since the sending coordinates are attached to each sending time. In addition, the restrictions are also complicated, since in this case it will also be necessary to verify that the conditions required for those coordinates are satisfied at each moment. In fact, since the new constraints are non-linear arithmetic, Maude’s SMT is not capable of processing them. In order to correctly execute the traces related to this protocol, we have used a version of Maude called Maude-NRA, which provides an SMT solver (CVC4) that is capable of processing this type of arithmetic.

Once more, we have performed experiments for this protocol with a regular execution, a mafia-like attack pattern, and a hijacking-like attack pattern. The results are similar to the previous ones, although more complex. Regular execution returns a solution, since it is possible to do it without problems. The hijacking attack is again possible as well, so a solution is again returned. Regarding the mafia attack, the same thing happens: a priori it is possible, but by adding the initial SMT restrictions necessary for the trace to be consistent, the attack is impossible. These restrictions are the same as before, but in this case some relative to coordinates are also added.

6 Conclusions and Future Work

The canonical narrowing strategy with irreducibility and SMT constraints opens the door to the use of narrowing to analyze protocols that use laws of physics, such as the Brands and Chaum protocol. It is a greatly generic methodology of symbolic reachability analysis that manages to prove the existence of traces of a protocol, giving greater flexibility when defining and specifying them. In this article we have presented an implementation of canonical narrowing capable of handling SMT constraints. This allows us to carry out symbolic analysis of two versions of the Brands and Chaum protocol. Maude-NPA already handled such protocols, as shown in [1, 2], but in an ad-hoc way without the canonical narrowing presented here. We now have a new algorithm with a powerful theoretical framework behind it, which can be useful to both Maude-NPA and other symbolic protocol analysis tools. As future work, we expect to expand this canonical narrowing to more general cases, clearly increasing its power for protocol analysis.