Authentication by Witness Functions

TL;DR

This paper extends witness functions from proving secrecy to verifying authentication in cryptographic protocols, demonstrating their safe application and analyzing a modified Woo-Lam protocol for authentication correctness.

Contribution

It introduces the use of witness functions for authentication and provides a method to analyze protocols for authentication correctness.

Findings

The modified Woo-Lam protocol is correct with respect to authentication.

Witness functions can be safely extended from secrecy to authentication.

The paper offers a new approach to protocol analysis for authentication.

Abstract

Witness functions have recently been introduced in cryptographic protocols' literature as a new powerful way to prove protocol correctness with respect to secrecy. In this paper, we extend them to the property of authentication. We show how to use them safely and we run an analysis on a modified version of the Woo-Lam protocol. We show that it is correct with respect to authentication.

Equations

$$F(\alpha,\partial[\overline{\alpha}]m\sigma)=\left\{\begin{array}[]{ll}F(\alpha,\partial m)&\mbox{if }\alpha\in{\mathcal{A}}(\partial m),\\ F(X,\partial[\overline{X}]m)&\mbox{if }\alpha\notin{\mathcal{A}}(\partial m)\\ &\mbox{and }\alpha=X\sigma.\par\par\end{array}\right.$$

$$F^{\prime}(\alpha,\{\alpha.A.X\}_{k_{cd}})=F(\alpha,\{\alpha.{\color[rgb]{1,0,0}A}\}_{k_{{\color[rgb]{1,0,0}cd}}})=\{A,C,D\}$$

$$F^{\prime}(\alpha,\{\alpha.Y.B\}_{k_{cd}})=F(\alpha,\{\alpha.{\color[rgb]{1,0,1}B}\}_{k_{{\color[rgb]{1,0,1}cd}}})=\{B,C,D\}$$

$${\mathcal{W}}_{p,F}(\alpha ,m\sigma )=\underset{\{(m^{\prime },{\sigma }^{\prime })\in {\tilde{\mathcal{M}}}_p^{\mathcal{G}}\otimes \Gamma |m^{\prime }{\sigma }^{\prime }=m\sigma \}}{\sqcap }{F}^{\prime }(\alpha ,m^{\prime }{\sigma }^{\prime })$$

$$F^{\prime }(\alpha ,m)⊒{\mathcal{W}}_{p,F}(\alpha ,m\sigma )⊒\underset{\{(m^{\prime },{\sigma }^{\prime })\in {\tilde{\mathcal{M}}}_p^{\mathcal{G}}\otimes \Gamma |m^{\prime }{\sigma }^{\prime }=m{\sigma }^{\prime }\}}{\sqcap }{F}^{\prime }(\alpha ,m^{\prime }{\sigma }^{\prime })$$

$$\underset{\{(m^{\prime },{\sigma }^{\prime })\in {\tilde{\mathcal{M}}}_p^{\mathcal{G}}\otimes \Gamma |m^{\prime }{\sigma }^{\prime }=r^{+}{\sigma }^{\prime }\}}{\sqcap }{F}^{\prime }(\alpha ,m^{\prime }{\sigma }^{\prime })⊒┌\alpha ┐\sqcap F^{\prime }(\alpha ,R^{-})$$

$$A\in F^{\prime }(\alpha ,m)\wedge F^{\prime }(\alpha ,m)⊐\perp$$

$$\begin{array}[]{l}\begin{array}[]{lllll}{\cal A}_{G}^{1}=&\langle i.1,A&\rightarrow&I(B):&A\rangle\\ \end{array}\\ \\ \begin{array}[]{llllll}{\cal A}_{G}^{2}=&\langle i.1,A&\rightarrow&I(B):&A\rangle.\\ &\langle i.2,I(B)&\rightarrow&A:&X\rangle.\\ &\langle i.3,A&\rightarrow&I(B):&\{B.k_{ab}^{i}\}_{k_{as}}\rangle\end{array}\end{array}$$

$$\begin{array}[]{l}\begin{array}[]{lllll}{\cal B}_{G}^{1}=&\langle i.1,I(A)&\rightarrow&B:&A\rangle.\\ &\langle i.2,B&\rightarrow&I(A):&N_{b}^{i}\rangle\\ \end{array}\\ \\ \begin{array}[]{lllll}{\cal B}_{G}^{2}=&\langle i.1,I(A)&\rightarrow&B:&A\rangle.\\ &\langle i.2,B&\rightarrow&I(A):&N_{b}^{i}\rangle.\\ &\langle i.3,I(A)&\rightarrow&B:&Y\rangle.\\ &\langle i.4,B&\rightarrow&I(S):&\{A.N_{b}^{i}.Y\}_{k_{bs}}\rangle\end{array}\\ \\ \begin{array}[]{lllll}{\cal B}_{G}^{3}=&\langle i.1,I(A)&\rightarrow&B:&A\rangle.\\ &\langle i.2,B&\rightarrow&I(A):&N_{b}^{i}\rangle.\\ &\langle i.3,I(A)&\rightarrow&B:&Y\rangle.\\ &\langle i.4,B&\rightarrow&I(S):&\{A.N_{b}^{i}.Y\}_{k_{bs}}\rangle.\\ &\langle i.5,I(S)&\rightarrow&B:&\{N_{b}^{i}.\{A.Z\}_{k_{bs}}\}_{k_{bs}}\rangle\\ \end{array}\end{array}$$

$$\begin{array}[]{l}\begin{array}[]{lllll}{\cal S}_{G}^{1}=&\langle i.4,I(B)&\rightarrow&S:&\{A.U.\{B.V\}_{k_{as}}\}_{k_{bs}}\rangle.\\ &\langle i.5,S&\rightarrow&I(B):&\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}}\rangle\\ \end{array}\end{array}$$

$$S^i:\frac{X}{\{B.k_{ab}^i{\}}_{k_{as}}}$$

$$F^{\prime }(k_{ab}^i,R_{S^i}^{-})=F(k_{ab}^i,\partial [\overline{k_{ab}^i}]X)=F(k_{ab}^i,ϵ)=\top$$

$${\sigma }_1^{\prime }=\{B_1⟼B,K_{A_2{B}_1}^i⟼k_{ab}^i,K_{A_2{S}_1}⟼k_{as}\}$$

$${{\rm Y}}_{p,F}(k_{ab}^i,\{B.k_{ab}^i{\}}_{k_{as}})=\{B,A,S\}$$

$${{\rm Y}}_{p,F}(k_{ab}^i,\{B.k_{ab}^i{\}}_{k_{as}})⊒┌k_{ab}^i┐\sqcap F^{\prime }(k_{ab}^i,X)$$

$$S^i:\frac{A}{N_b^i}{S}^j:\frac{Y}{\{A.N_b^i.Y{\}}_{k_{bs}}}$$

$${{\rm Y}}_{p,F}(N_b^i,N_b^i)⊒┌N_b^i┐\sqcap F^{\prime }(N_b^i,A)$$

$${{\rm Y}}_{p,F}(N_b^i,\{A.N_b^i.Y{\}}_{k_{bs}})⊒┌N_b^i┐\sqcap F^{\prime }(N_b^i,Y)$$

$$F^{\prime }(Y,Y)=F(Y,\partial [\overline{Y}]Y)=F(Y,Y)=\perp$$

$${{\rm Y}}_{p,F}(Y,\{A.N_b^i.Y{\}}_{k_{bs}})⊒┌Y┐\sqcap F^{\prime }(Y,Y)$$

$$S^i:\frac{\{A.U.\{B.V{\}}_{k_{as}}{\}}_{k_{bs}}}{\{U.\{A.V{\}}_{k_{bs}}{\}}_{k_{bs}}}$$

$$F^{\prime }(U,\{A.U.\{B.V{\}}_{k_{as}}{\}}_{k_{bs}})$$

$${\sigma }_1^{\prime }=\{U_2⟼U,A_7⟼A,V_2⟼V,K_{B_6{S}_5}⟼k_{bs}\}$$

$${{\rm Y}}_{p,F}(U,\{U.\{A.V{\}}_{k_{bs}}{\}}_{k_{bs}})=\{A,B,S\}$$

$$F^{\prime }(V,\{A.U.\{B.V{\}}_{k_{as}}{\}}_{k_{bs}})=\{A,B,S\}$$

$$\left\{\begin{array}[]{l}\sigma_{1}^{\prime}=\{U_{2}\longmapsto U,A_{7}\longmapsto A,V_{2}\longmapsto V,{K_{B_{6}S_{5}}}\longmapsto{k_{bs}}\}\\ \sigma_{2}^{\prime}=\{U\longmapsto N_{B_{4}}^{i},A_{5}\longmapsto A,Z_{1}\longmapsto V,{K_{B_{4}S_{3}}}\longmapsto{k_{bs}}\}\\ \end{array}\right.$$

$$F^{\prime }(V,\{U_2.\{A_7.V_2{\}}_{K_{B_6{S}_5}}{\}}_{K_{B_6{S}_5}}{\sigma }_1^{\prime })$$

$$\sqcap$$

$$F^{\prime }(V,\{N_{B_4}^i.\{A_5.Z_1{\}}_{K_{B_4{S}_3}}{\}}_{K_{B_4{S}_3}}{\sigma }_2^{\prime })$$

$$F^{\prime }(V,\{U.\{A.V_2{\}}_{k_{bs}}{\}}_{k_{bs}}{\sigma }_1^{\prime })\sqcap F^{\prime }(V,\{N_b^i.\{A.V_2{\}}_{k_{bs}}{\}}_{k_{bs}}{\sigma }_2^{\prime })$$

Full text

Notice

© 2016 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

I Introduction

Cryptographic protocols are distributed programs used everywhere. They are designed to provide security assurances in communications by using cryptographic primitives. Traditional assurances include secrecy, integrity and authentication, and more recently, anonymity, atomicity, verifiability, coercion-resistance, etc. It has been clear for a long time that cryptographic protocols are prone to serious design drifts. Therefore, several formalisms [1] have been proposed to check protocols against flaws and vulnerabilities. In this paper, we focus on authentication. Authentication is the property that should be satisfied by a protocol to be secure against acceptance of a fraudulent agent by ensuring that one party is who he claims to be. A protocol can reach authentication by means of secrecy when it succeeds to provide evidence to one party that the second party manages to present a piece of data that could only have been generated by him (e.g. response to a challenge). This implies, very often, that some data can be unequivocally traced back to its origin. In some scenarios, authentication involves more than two parties where a trusted server could be used to introduce one party $B$ to another party $A$ and $A$ is assured that $B$ is trusted by the server in the required protocol semantics. It is worth mentioning that, of course, protocols can reach authentication with no need to secrecy, however, these protocols are not our target in this paper.

II Methodology

Our way to prove that a protocol is correct with respect to authentication consists in reaching two intermediate purposes:

we prove that the secret used for authentication is never disclosed to avoid any bad use of this latter by an opponent; 2. 2.

we make sure that the link between the authenticatee identity and the secret is never untied. This is to guarantee that the secret emanates from the right origin.

For that, we use the theory of witness functions [2, 3, 4, 5]. Witness functions adequately estimate the level of security of each atomic message. Before this paper, we used to use them to prove secrecy in a protocol by showing that it is increasing. That is to say, to show that the level of security of every single atomic message exchanged in the protocol is always growing and never goes down between any two consecutive steps of receiving and sending. Our contribution here is the extension of witness functions for the authentication property. For that, we give sufficient conditions for authentication based on the two mighty bounds of a witness function such, if met, the protocol is automatically declared correct with respect to authentication.

• •

in Sections III and IV, we’ll give a brief summary of the proof of correctness of increasing protocols when analyzed with safe functions and we give a guideline to build these functions;

• •

in Section V, we’ll give a short overview on witness functions and we bring out their powerful bounds;

• •

in Section VI, we’ll give sufficient conditions to ensure protocols’ correctness with respect to authentication based on witness functions;

• •

in Section VII, we’ll analyze a modified version of the Woo-Lam protocol;

• •

finally, we’ll compare our approach with similar ones and conclude.

Please notice that all the notations we will use in this paper are given in the appendix. The reader is kindly requested to see them before moving forward.

III On the correctness of increasing protocols

Hereafter, we remind an important result: ”A protocol keeps its secret inputs when analyzed with a safe function and shown increasing”.

III-A Safe functions

Definition 1

*(Well-formed Function)

Let ${F}$ be a function and ${\mathcal{C}}$ be a context of verification. ${F}$ is ${\mathcal{C}}$-well-formed iff: $\forall M,M_{1},M_{2}\subseteq{\mathcal{M}},\forall\alpha\in{\mathcal{A}}({\mathcal{M}})\mbox{:}$

[TABLE]

A well-formed function ${F}$ must return the infimum to an atom $\alpha$ that appears clear in $M$ to say that any participant knows it from $M$. It returns to an atom in the union of two sets, the minimum of the two values calculated in each set separately. It returns the supremum to any atom $\alpha$ that does not appear in $M$ to say that nobody could get it from $M$.

Definition 2

*(Full-Invariant-by-Opponent Function)

Let ${F}$ be a function and ${\mathcal{C}}$ be a context of verification. ${F}$ is full-invariant-by-Opponent iff: $\forall{M}\subseteq{\mathcal{M}},m\in{\mathcal{M}},\alpha\in{\mathcal{A}}(m)$:

${M}\models_{\mathcal{C}}m\Rightarrow({F}(\alpha,m)\sqsupseteq{F}(\alpha,{M}))\vee(\ulcorner K(I)\urcorner\sqsupseteq\ulcorner\alpha\urcorner).$

A full-invariant-by-opponent function ${F}$ is such, when it affects a security level to an atom $\alpha$ in a set of messages $M$, the opponent cannot deduce from this set some message $m$ in which this level decreases (i.e. ${F}(\alpha,m)\not\sqsupseteq{F}(\alpha,{M})$), unless he is expressly entitled to know it (i.e. $\ulcorner K(I)\urcorner\sqsupseteq\ulcorner\alpha\urcorner$).

A function ${F}$ is s said to be safe if it is well-formed and full-invariant-by-Opponent.

Definition 3

*(${F}$-Increasing Protocol)

Let ${F}$ be a function and ${\mathcal{C}}$ be a context of verification and $p$ be a protocol.

$p$ is ${F}$-increasing iff: $\forall R.r\in R_{G}(p),\sigma\in\Gamma,\alpha\in{\mathcal{A}}(r^{+}),\mbox{ we have: }{F}(\alpha,r^{+}\sigma)\sqsupseteq\ulcorner\alpha\urcorner\sqcap{F}(\alpha,R^{-}\sigma)$*

An ${F}$-increasing protocol must produce traces with atomic messages having always a security level, returned by ${F}$, higher when sending (i.e. in $r^{+}\sigma$) than when receiving (i.e. in $R^{-}\sigma$) or than its level set in the context (i.e. $\ulcorner\alpha\urcorner$), if known.

Theorem 1

*(Sececy in Increasing Protocols)

Let ${F}$ be a safe function and $p$ be an ${F}$-increasing protocol.*

$p$* keeps its secret inputs.*

Theorem 1 states that a protocol keeps its secret inputs when it is analyzed by a safe function $F$ and is shown increasing. This result is quite intuitive. In fact, if the opponent succeeds to obtain a secret $\alpha$ (clear) from the protocol then its security level given by $F$ is the infimum since $F$ is well-formed. That cannot be due to the rules of the protocol since this latter is $F\mbox{-increasing}$. That could not arise neither when the opponent uses his capabilities since $F$ is full-invariant-by-opponent. So, the secret is kept forever. The detailed proof is available in [5].

IV Guideline for Building Safe Functions

In  [4] we propose a class of safe selections: $S_{Gen}^{EK}$. Any selection $S$ in $S_{Gen}^{EK}$ must return to an atom $\alpha$ in a message $m$:

if $\alpha$ is encrypted by a key $k$ such that $k$ is the outer key that satisfies the condition $\ulcorner k^{-1}\urcorner\sqsupseteq\ulcorner\alpha\urcorner$ (we refer to it by the external protective key), a subset among $k^{-1}$ and the neighbors of $\alpha$ under the same protection by $k$; 2. 2.

for two messages linked by a function $f$ in $\Sigma$ other than an encryption by a protective key (e.g. pair), the union of two subselections in these two messages. 3. 3.

if $\alpha$ does not have a protective key in $m$, the infimum (all atoms); 4. 4.

if $\alpha$ does not appear in $m$, the supremum (the empty set);

Among the selections of $S_{Gen}^{EK}$, we spotlight three practical ones:

the selection $S_{MAX}^{EK}:$ it returns to an atom $\alpha$ in a message $m$ encrypted by the external protective key $k$, all the principal identities inside the same protection by $k$, in addition to $k^{-1}$; 2. 2.

the selection $S_{EK}^{EK}:$ it returns to an atom $\alpha$ in a message $m$ encrypted by the external protective key $k$, the key $k^{-1}$; 3. 3.

the selection $S_{N}^{EK}:$ it returns to an atom $\alpha$ in a message $m$ encrypted by the key external protective key $k$, all the principal identities inside the same protection by $k$;

Any selection $S$ in $S_{Gen}^{EK}$ when composed to a adequate homomorphism $\psi$ returns a safe function $F=\psi\circ S$. We choose the homomorphism that returns for:

an agent, its identity; 2. 2.

the key $k^{-1}$, if selected, the set of agent identities that are authorized to know it.

We denote by $F_{MAX}^{EK},F_{EK}^{EK}$ and $F_{N}^{EK}$ respectively the functions resulting from the compositions $\psi\circ S_{MAX}^{EK},\psi\circ S_{EK}^{EK}$ and $\psi\circ S_{N}^{EK}$. We prove [4] that these functions are safe. In fact, since the selection for any atom $\alpha$ is performed in an invariant section protected by the external protective key $k$, then, to alter this section (to decrease the security level of $\alpha$), the opponent must have priorly obtained the atomic key $k^{-1}$. At this point of the proof, his knowledge must satisfy: $\ulcorner K(I)\urcorner\sqsupseteq\ulcorner k^{-1}\urcorner$. Since the key $k^{-1}$ satisfies: $\ulcorner k^{-1}\urcorner\sqsupseteq\ulcorner\alpha\urcorner$ then the knowledge of the opponent must satisfy $\ulcorner K(I)\urcorner\sqsupseteq\ulcorner\alpha\urcorner$ too seeing that the comparator ”$\sqsupseteq$” is transitive. This is simply the definition of a full-invariant-by-opponent function. These functions are well-formed by construction, too.

Example 1

*Context: $\ulcorner\alpha\urcorner=\{A,B,S\}$; $m=\{C.\{\alpha.D\}_{k_{as}}\}_{k_{ab}}$; ${k_{ab}^{-1}}={k_{ab}},{k_{as}^{-1}}={k_{as}}$; $\ulcorner{k_{as}}\urcorner=\{A,S\},\ulcorner{k_{ab}}\urcorner=\{A,B\}$. We have:

$S_{MAX}^{EK}(\alpha,m)=\{C,D,{k_{ab}^{-1}}\}$ and $F_{MAX}^{EK}(\alpha,m)=\psi\circ S_{MAX}^{EK}(\alpha,m)=\{C,D\}{\cup}\ulcorner{k_{ab}^{-1}}\urcorner=\{C,D\}\cup\{A,B\}=\{A,B,C,D\}$.*

V Witness functions to eliminate the effect of variables

The functions $F\in\{F_{MAX}^{EK},F_{EK}^{EK},F_{N}^{EK}\}$ we have defined so far are not useful in practice since they operate on ground terms only. However, a static analysis should be run over messages of the generalized roles resulting from writing the protocol in a role-based specification [18]. These messages contain variables that denote a content that an agent ignores and on which he cannot perform any verification. We give here a safe way to deal with variables. But now, let us introduce derivation in Definition 4.

Definition 4

[Derivation]

[TABLE]

Derivation simply eliminates variables from a message except a variable under evaluation. The expression $\partial m$ denotes a message $m$ after removing all variables in. The aim of derivation is to deprive variables from playing any role when evaluating an atom in a message. The idea is hence to apply $F$ on the derivative message instead of the message itself. Besides, any variable is evaluated as a block with no regard to its content (i.e quantified). In fact, the reason why we do not care about the content of a variable is that if a variable, globally evaluated, is shown increasing that means that it cannot be discovered by any unauthorized party, and consequently any content inside cannot be discovered by an unauthorized party, too. If it is not increasing, then the protocol will not satisfy our sufficient conditions and hence no decision with respect to secrecy is made on, thus, with respect to authentication, too. This way of treating variables allows us to give any content of a variable (dynamically known) the same value of the variable itself (statically calculable). The way we evaluate an atom from within a derivative message is described by Definition 5.

Definition 5

*Let $m\in{\mathcal{M}}_{p}^{\mathcal{G}}$, $X\in{\mathcal{X}}_{m}$ and $m\sigma$ be a valid trace.

For all $\alpha\in{\mathcal{A}}(m\sigma)$, $\sigma\in\Gamma$, we denote by:*

[TABLE]

Since the expression $F(\alpha,\partial[\overline{\alpha}]m\sigma)$ does not depend on substitution (i.e the run $\sigma$), we denote it simply by $F^{\prime}(\alpha,m)$. Although the derivative function $F^{\prime}$ allows us to neutralize variables, which is as such an important intermediate result, using it as is to analyze protocols is not safe because it is not even a function in the protocol. In fact, when we want to evaluate the security level of $\alpha$ in the trace $\{\alpha.A.B\}_{k_{cd}}­$ for example, we must return to the generalized roles to see from which message (with variables) this trace is generated and we may realize that more than one message are able to generate it. For instance, the messages $m_{1}=\{\alpha.A.X\}_{k_{cd}}­$ and $m_{2}=\{\alpha.Y.B\}_{k_{cd}}­$ are both candidates to generate the trace $\{\alpha.A.B\}_{k_{cd}}­$ (i.e. possible sources of it). If we refer to the first source (i.e. to $m_{1}$), the security level of $\alpha$ returned by $F^{\prime}$ (with $F=F_{MAX}^{EK}$) is:

[TABLE]

Whereas, if we refer to the second source (i.e. to $m_{2}$), its security level is:

[TABLE]

Therefore, we cannot rely on $F^{\prime}$ to analyze a protocol. To overcome this insufficiency, we define the witness functions. A witness function looks for all the sources of a ground term $m\sigma$ in the finite set ${\mathcal{M}}_{p}^{\mathcal{G}}$, applies $F^{\prime}$ to all of them, and returns the minimum. This minimum must satisfy both existence and uniqueness in the security lattice. Since a secret is always evaluated under the protection of a protective key, the research of the sources of a closed message in ${\mathcal{M}}_{p}^{\mathcal{G}}$ is then restricted to encryption patterns. We denote by $\tilde{\mathcal{M}}_{p}^{\mathcal{G}}$ the set of all encryption patterns generated by the protocol (renamed).

Definition 6

[witness function] Let $m\in{\mathcal{M}}_{p}^{\mathcal{G}}$, $X\in{\mathcal{X}}_{m}$ and $m\sigma$ be a valid trace. Let $p$ be a protocol and $F$ be a safe function. We define a witness function ${\mathcal{W}}_{p,F}$ for all $\alpha\in{\mathcal{A}}(m\sigma)$, $\sigma\in\Gamma$, as follows:

[TABLE]

Using a witness function as is to analyze a protocol is a very tedious process since we cannot enumerate all the valid traces $m\sigma$ and their sources statically. For that we bind it into two bounds that do not depend on substitution (i.e on $\sigma$). The upper bound of a witness function returns a minimum set of confirmed principal identities for any $\alpha$ in $m$ whereas the lower bound returns the set of all principal identities from all the possible sources of $m$ (that are unifiable with it) including the odd ones. The lower bound hunts so any odd principal identity and interprets it as an attack. The proof is simple since we have always $\{(m^{\prime},\sigma^{\prime})\in\tilde{\mathcal{M}}_{p}^{\mathcal{G}}\otimes\Gamma|m^{\prime}\sigma^{\prime}=m\sigma\}\subseteq\{(m^{\prime},\sigma^{\prime})\in\tilde{\mathcal{M}}_{p}^{\mathcal{G}}\otimes\Gamma|m^{\prime}\sigma^{\prime}=m\sigma^{\prime}\}$ in the security lattice whatever $\sigma$. This is expressed by Proposition 1.

Proposition 1

[binding a witness function] Let $m\in{\mathcal{M}}_{p}^{\mathcal{G}}$. Let ${\mathcal{W}}_{p,F}$ be a witness function. For all $\sigma\in\Gamma$ we have:

[TABLE]

VI Sufficient conditions for authentication (Contribution)

The Lemma 1 declares a decision criterion for secrecy based on the bounds of a witness function. The upper bound returns the set of original and trusted identities only from the received message. The lower bound returns the set of all the identities including those that could be inserted by a masquerader by substituting a regular message when sent. The criterion makes sure that no odd identity could be inserted in the evaluation neighborhood of a given atom in the sent message. The proof of Lemma 1 results directly from Proposition 1 and Theorem 1.

Lemma 1

[Decision for Secrecy] Let $p$ be a protocol. Let ${\mathcal{W}}_{p,F}$ be a witness function. $p$ is correct with respect to secrecy if: $\forall R.r\in R_{G}(p),\forall\alpha\in{\mathcal{A}}{(r^{+})}$ we have:

[TABLE]

Theorem 2 forwards two conditions such, if met, a protocol is automatically declared correct for authentication. The first one ensures that the protocol does not disclose its secret inputs. An immediate outcome of this first result is that the message the verifier last receives for authentication is in a safe state and had not been subverted by a masquerader. The second one makes sure that the binding between the challenge and the identity of the identifier is not broken. Therefore, we call once again the upper bound of the witness function to confirm the originality of the claimer identity by evaluating the challenge in the message that should authenticate the claimer to the verifier. The second clause of the second condition is trivial and introduced just to make sure that the challenge is not received in a public state.

Theorem 2

[Decision for Authentication] Let $p$ be a protocol. Let ${\mathcal{W}}_{p,F}$ be a witness function. $p$ is correct with respect to authentication if:

Lemma 1 is satisfied; 2. 2.

Let $\alpha$ be the challenge in a message $m$ received by a verifier $B$ to authenticate an agent $A$. We have:

[TABLE]

It is worth mentioning that:

• •

the conditions set by Theorem 2 can be verified statically as they use the two bounds of a witness function only and both of them are statically determinable;

• •

their verification is linear under the assumption of perfect encryption since the most costly operation is unification in the lower bound of a witness function which is linear under that assumption. However, under nonempty equational theories, it will vary from one to another. In a future work, we will give new results related to this question.

VII Analysis of a modified version of the Woo-Lam Protocol with a witness function for authentication (Contribution)

The original version of the Woo-Lam protocol has been proven incorrect by several means [6, 7, 8]. Hereafter, we analyze an modified version of this protocol with a witness function and we prove that it is correct with respect to authentication. This version is denoted by $p$ in Table I.

The role-based specification of $p$ is ${\cal R}_{G}(p)=\{{\cal A}_{G}^{1},~{}{\cal A}_{G}^{2},~{}{\cal B}_{G}^{1},~{}{\cal B}_{G}^{2},~{}{\cal B}_{G}^{3},~{}{\cal S}_{G}^{1}\}$, where the generalized roles ${\cal A}_{G}^{1}$, ${\cal A}_{G}^{2}$ of $A$ are as follows:

[TABLE]

The generalized roles ${\cal B}_{G}^{1}$, ${\cal B}_{G}^{2}$, ${\cal B}_{G}^{3}$ of $B$ are as follows:

[TABLE]

The generalized role ${\cal S}_{G}^{1}$ of $S$ is as follows:

[TABLE]

Let us have a context of verification such that:

$\ulcorner k_{as}\urcorner=\{A,S\}$; $\ulcorner k_{bs}\urcorner=\{B,S\}$; $\ulcorner k_{ab}^{i}\urcorner=\{A,B,S\}$;

$\ulcorner N_{b}^{i}\urcorner=\bot$; $\forall A\in{\cal{I}},\ulcorner A\urcorner=\bot$.

Let $F=F_{MAX}^{EK}$; ${\mathcal{W}}_{p,F}={\mathcal{W}}_{{p},F_{MAX}^{EK}}$;

We denote by ${\Upsilon}_{p,F}(\alpha,m)$ the lower bound $\underset{\{{(m^{\prime},\sigma^{\prime})\in\tilde{\cal{M}}_{p}^{\cal{G}}}\otimes\Gamma{|m^{\prime}\sigma^{\prime}=m\sigma^{\prime}\}}}{\sqcap}\!\!\!\!\!\!\!\!\!\!F^{\prime}(\alpha,m^{\prime}\sigma^{\prime})$ of the witness function ${\mathcal{W}}_{p,F}(\alpha,m)$.

The set of messages generated by $p$ is ${\cal{M}}_{p}^{\cal{G}}=\{A_{1},X_{1},\{B_{1}.K_{A_{2}B_{1}}^{i}\}_{K_{A_{2}S_{1}}},A_{3},N_{B_{2}}^{i},Y_{1},$ $\{A_{4}.N_{B_{3}}^{i}.Y_{2}\}_{K_{{B_{3}S_{2}}}},\{N_{B_{4}}^{i}.\{A_{5}.Z_{1}\}_{K_{B_{4}S_{3}}}\}_{K_{B_{4}S_{3}}},\\ \{A_{6}.U_{1}.\{B_{5}.V_{1}\}_{K_{{A_{6}}S_{4}}}\}_{K_{{B_{5}}S_{4}}},\{U_{2}.\{A_{7}.V_{2}\}_{K_{B_{6}S_{5}}}\}_{K_{B_{6}S_{5}}}\}$

The variables are denoted by $X_{1},Y_{2},Z_{1},U_{1},U_{2},V_{1}$ and $V_{2}$;

After eliminating duplicates in ${\cal{M}}_{p}^{\cal{G}}$ and the messages that are not encryption patterns, we have:

$\tilde{\cal{M}}_{p}^{\cal{G}}=\{\{B_{1}.K_{A_{2}B_{1}}^{i}\}_{K_{A_{2}S_{1}}},\{A_{4}.N_{B_{3}}^{i}.Y_{2}\}_{K_{{B_{3}S_{2}}}},$ $\{N_{B_{4}}^{i}.\{A_{5}.Z_{1}\}_{K_{B_{4}S_{3}}}\}_{K_{B_{4}S_{3}}},\{A_{6}.U_{1}.\{B_{5}.V_{1}\}_{K_{{A_{6}}S_{4}}}\}_{K_{{B_{5}}S_{4}}},\\ \{U_{2}.\{A_{7}.V_{2}\}_{K_{B_{6}S_{5}}}\}_{K_{B_{6}S_{5}}}\}$

VII-A Analysis of the Generalized Roles of $A$

According to the generalized role of $A$, an agent $A$ may take part in some session $S^{i}$ in which he receives an unkown message $X$ and sends the message $\{B.k_{ab}^{i}\}_{k_{as}}$. This is described by the following rule:

[TABLE]

-Analysis of the messages exchanged in $S^{i}$:

1- For $k_{ab}^{i}$:

a- Receiving step: $R_{S^{i}}^{-}=X$ (when receiving, we use the upper bound)

[TABLE]

b- Sending step: $r_{S^{i}}^{+}=\{B.k_{ab}^{i}\}_{k_{as}}$ *(when sending , we use the lower bound)

$\forall k_{ab}^{i}.\{(m^{\prime},\sigma^{\prime})\in\tilde{\cal{M}}_{p}^{\cal{G}}\otimes\Gamma|{m^{\prime}\sigma^{\prime}=r_{S^{i}}^{+}\sigma^{\prime}}\}$

$=\forall k_{ab}^{i}.\{(m^{\prime}\sigma^{\prime})\in\tilde{\cal{M}}_{p}^{\cal{G}}\otimes\Gamma|{m^{\prime}\sigma^{\prime}=\{B.k_{ab}^{i}\}_{k_{as}}\sigma^{\prime}}\}$

$=\{(\{B_{1}.K_{A_{2}B_{1}}^{i}\}_{K_{A_{2}S_{1}}},\sigma_{1}^{\prime})\}$ such that:

[TABLE]

${\Upsilon}_{p,F}(k_{ab}^{i},\{B.k_{ab}^{i}\}_{k_{as}})$

$=\{\mbox{Definition of the lower bound of the witness function}\}$

$F^{\prime}(k_{ab}^{i},\{B_{1}.K_{A_{2}B_{1}}^{i}\}_{K_{A_{2}S_{1}}}\sigma_{1}^{\prime})$

$=\{\mbox{Setting the static neighborhood}\}$

$F^{\prime}(k_{ab}^{i},\{B.k_{ab}^{i}\}_{k_{as}}\sigma_{1}^{\prime})$

$=\{\mbox{Definition }\ref{Fder}\}$

$F(k_{ab}^{i},\partial[\overline{k_{ab}^{i}}]\{B.k_{ab}^{i}\}_{k_{as}})$

$=\{\mbox{Derivation in Definition }\ref{derivation}\}$

$F(k_{ab}^{i},\{B.k_{ab}^{i}\}_{k_{as}})$

$=\{\mbox{Since }F=F_{MAX}^{EK}\}$

$\{B,A,S\}$

Then, we have:

[TABLE]

2- Conformity with Lemma 1:

From (1) and (2) and since $\ulcorner k_{ab}^{i}\urcorner=\{B,A,S\}$ in the context, we have:

[TABLE]

Then, the generalized role of $A$ respects Lemma 1.      (I)

VII-B Analysis of the generalized roles of $B$

According to the generalized role of $B$, an agent $B$ may take part in two subsequent sessions: $S^{i}$ and $S^{j}$ such that $j>i$. In the first session $S^{i}$, the agent $B$ receives the identity $A$ and sends the nonce $N_{b}^{i}$. In the second one $S^{j}$, he receives an unknown message $Y$ and he sends the message $\{A.N_{b}^{i}.Y\}_{k_{bs}}$. This is described by the following rules:

[TABLE]

B.1- Analysis of the messages exchanged in $S^{i}$:

1- For $N_{b}^{i}$:

Since $N_{b}^{i}$ is set public in the context (i.e. $\ulcorner N_{b}^{i}\urcorner=\bot$), then, we have directly:

[TABLE]

B.2- Analysis of the messages exchanged in $S^{j}$:

1- For $N_{b}^{i}$:

Since $N_{b}^{i}$ is set public in the context (i.e. $\ulcorner N_{b}^{i}\urcorner=\bot$), then, we have directly:

[TABLE]

2- $\forall Y$:

Since when receiving, we have:

[TABLE]

Then, we have directly:

[TABLE]

3- Conformity with Lemma 1:

From (4), (5) and (6), we have: the generalized role of $B$ respects Lemma 1.                                                      (II)

VII-C Analysis of the generalized roles of $S$

According to the generalized role of $S$, an agent $S$ may take part in some session $S^{i}$ in which he receives the message $\{A.U.\{B.V\}_{k_{as}}\}_{k_{bs}}$ and sends the message $\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}}$. This is described by the following rule:

[TABLE]

1- $\forall U$:

a- Receiving step: $R_{S^{i}}^{-}=\{A.U.\{B.V\}_{k_{as}}\}_{k_{bs}}$ (when receiving, we use the upper bound)

[TABLE]

b- Sending step: $r_{S^{i}}^{+}=\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}}$ *(when sending , we use the lower bound)

$\forall U.\{(m^{\prime},\sigma^{\prime})\in\tilde{\cal{M}}_{p}^{\cal{G}}\otimes\Gamma|{m^{\prime}\sigma^{\prime}=r_{S^{i}}^{+}\sigma^{\prime}}\}$

$=\forall U.\{(m^{\prime},\sigma^{\prime})\in\tilde{\cal{M}}_{p}^{\cal{G}}\otimes\Gamma|{m^{\prime}\sigma^{\prime}=\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}}\sigma^{\prime}}\}$

$=\{(\{\{U_{2}.\{A_{7}.V_{2}\}_{K_{B_{6}S_{5}}}\}_{K_{B_{6}S_{5}}},\sigma_{1}^{\prime})\}$ such that:

[TABLE]

${\Upsilon}_{p,F}(U,\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}})$

$=\{\mbox{Definition of the lower bound of the witness function}\}$

$F^{\prime}(U,\{U_{2}.\{A_{7}.V_{2}\}_{K_{B_{6}S_{5}}}\}_{K_{B_{6}S_{5}}}\sigma_{1}^{\prime})$

$=\{\mbox{Setting the static neighborhood}\}$

$F^{\prime}(U,\{U_{2}.\{A.V\}_{k_{bs}}\}_{k_{bs}}\sigma_{1}^{\prime})$

$=\{\mbox{Definition }\ref{Fder}\}$

$F(U_{2},\partial[\overline{U_{2}}]\{U_{2}.\{A.V\}_{k_{bs}}\}_{k_{bs}})$

$=\{\mbox{Derivation in Definition }\ref{derivation}\}$

$F(U_{2},\{U_{2}.\{A\}_{k_{bs}}\}_{k_{bs}})$

$=\{\mbox{Since }F=F_{MAX}^{EK}\}$

$\{A,B,S\}$

Then, we have:

[TABLE]

2- $\forall V$:

a- Receiving step: $R_{S^{i}}^{-}=\{A.U.\{B.V\}_{k_{as}}\}_{k_{bs}}$ *(when receiving, we use the upper bound)

[TABLE]

=\left\{\begin{array}[]{ll}\{A,B,S\}&\mbox{if }k_{as}\mbox{ is the external protective key }\mbox{of }V\mbox{ in}\\ &~{}~{}\mbox{ the received message }\{A.\{{\color[rgb]{1,0,1}B}.V\}_{k_{{\color[rgb]{1,0,1}as}}}\}_{k_{bs}}\\ \\ \{A,B,S\}&\mbox{if }k_{bs}\mbox{ is the external protective key }\mbox{of }V\mbox{ in}\\ &~{}~{}\mbox{ the received message }\{{\color[rgb]{1,0,1}A}.\{{\color[rgb]{1,0,1}B}.V\}_{k_{as}}\}_{k_{{\color[rgb]{1,0,1}bs}}}\end{array}\right.

$\!\!\!\!\!\!=$ $\{A,B,S\}$

Then, we have:

[TABLE]

b- Sending step: $r_{S^{i}}^{+}=\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}}$ *(when sending , we use the lower bound)

$\forall V.\{(m^{\prime},\sigma^{\prime})\in\tilde{\cal{M}}_{p}^{\cal{G}}\otimes\Gamma|{m^{\prime}\sigma^{\prime}=r_{S^{i}}^{+}\sigma^{\prime}}\}$

$=\forall V.\{(m^{\prime},\sigma^{\prime})\in\tilde{\cal{M}}_{p}^{\cal{G}}\otimes\Gamma|{m^{\prime}\sigma^{\prime}=\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}}\sigma^{\prime}}\}$

$=\{(\{\{U_{2}.\{A_{7}.V_{2}\}_{K_{B_{6}S_{5}}}\}_{K_{B_{6}S_{5}}},\sigma_{1}^{\prime}),$

$(\{N_{B_{4}}^{i}.\{A_{5}.Z_{1}\}_{K_{B_{4}S_{3}}}\}_{K_{B_{4}S_{3}}},\sigma_{2}^{\prime})\}$ such that:

[TABLE]

${\Upsilon}_{p,F}(V,\{U.\{A.V\}_{k_{bs}}\}_{k_{bs}})$

$=\{\mbox{Definition of the lower bound of the witness function}\}$

[TABLE]

[TABLE]

[TABLE]

$=\{\mbox{Setting the static neighborhood}\}$

[TABLE]

$=\{\mbox{Definition }\ref{Fder}\}$

[TABLE]

$=\{\mbox{Derivation in Definition }\ref{derivation}\}$

[TABLE]

$=\{\mbox{Since }F=F_{MAX}^{EK}\}$

$\{A,B,S\}$

Then, we have:

[TABLE]

3- Conformity with Lemma 1:

From (7) and (8), we have:

[TABLE]

From (9) and (10), we have:

[TABLE]

From (11) and (12), we have: the generalized role of $S$ respects Lemma 1.                                                 (III)

From (I) and (II) and (III), we conclude that: $p$ respects Lemma 1.                                                       (IV)

Now that the first condition of Theorem 2 is satisfied (i.e. the protocol is proven increasing, so correct for secrecy), let us examine the second one. Indeed, the message received by the authenticator $B$ to authenticatee $A$ is $\{N_{b}^{i}.\{A.Z\}_{k_{bs}}\}_{k_{bs}}$. The challenge to be verified by $B$ is the nonce $N_{b}^{i}$. We have:

$\!\!\!\!\!F^{\prime}(N_{b}^{i},\{N_{b}^{i}.\{A.Z\}_{k_{bs}}\}_{k_{bs}}$ $\!\!\!\!\!=$ \!\!\!F(N_{b}^{i},\partial[\overline{N_{b}^{i}}]\{N_{b}^{i}.\{{\color[rgb]{1,0,1}A}.Z\}_{k_{bs}}\}_{k_{bs}}

$\!\!\!\!\!=$ \!\!\!F(N_{b}^{i},\{N_{b}^{i}.\{{\color[rgb]{1,0,1}A}\}_{k_{bs}}\}_{k_{bs}})

$\!\!\!\!\!=$ \!\!\!\{{\color[rgb]{1,0,1}A},B,S\}

Then, we can easily see that:

[TABLE]

[TABLE]

[TABLE]

From (IV) and (V) and Theorem 2, we can declare now, and only now, that: The modified version of the Woo-Lam protocol is correct with respect to authentication.

VIII Comparison with similar works

In the witness functions logic, to prove authentication, a protocol must be verified for secrecy first. For that, the upper bound of a witness function bases its calculation on safe identities collected from a piece of message that is fully invariant by opponent in order to deprives this latter from using his capabilities to forge these identities. Besides, in every single sending step of the protocol, the lower bound makes sure that the protocol does not endow the opponent of new rules that could mislead a regular agent by using suspicious messages that ’’look like” a regular one but, in fact, have been gathered from previous sessions. To do so, this bound considers all encryption patterns that might be sources of a final trace and verifies whether or not a suspicious identity could be inseminated in some variable when the protocol is running. If this is the case, the analysis is immediately aborted and no result for the protocol correctness is given with respect to secrecy. This way we treat secrecy leads to an interesting observation: ”If a protocol is correct for secrecy, then any atomic messages arrives to its destination in a safe state”. That means that its evaluation environment, based on a protective key and all the identities beyond, does not contain any suspicious identity. All of them are reliable. It turns out that the authenticator has just to make sure that the identity of the authenticatee is present, witnessing finally the origin of the authenticating message. This is made available by the upper bound that is called, once again, to provide this authentication service, too. In literature, we can point out an interesting work which is similar in some aspects to ours. It is the work of Houmani published in  [9, 10, 11, 12]. In this work, she defined two functions to estimate the level of security of atoms in messages called respectively DEK and DEKAN. The DEK function is based on the direct key only whereas DEKAN is based on the direct key and neighbors. The DEK function is very limited in practice. However, the main drawback of the DEKAN function is that it is not variable free. For instance, $\mbox{DEKAN}(\alpha,\{\alpha.A.X\}_{k_{bs}})=\{A,,B,S\}\sqcap\ulcorner X\urcorner$, where $X$ is a variable having an unknown level of security $\ulcorner X\urcorner$ in the context. The fact that a function has outputs with variables sets up a real barrier when comparing two security levels, especially when we have more than one variable in the same message. As a result, very few protocols have been shown correct with respect to secrecy and, as far as we know, no further researches have been published with respect to authentication, very likely because of variables in output. With witness functions, we do not have this problem owing to derivation used in the witness functions’ bounds that eliminate variables in output. Hence, the comparison between security levels is made possible and easier. Several tools have been proposed in the state-of-the-art of cryptographic protocols to verify authentication in security protocols. Among them, we can cite an interesting one: the AVISPA tool [13]. This tool consists of an aggregation of three model checkers and a tree automata verifier. These four components are:

• •

the Constraint-Logic-based Attack Searcher: applies constraint solving to run both protocol falsification and verification for bounded sessions;

• •

the On-the-fly Model-Checker: it carries out a protocol verification by exploring the transition system. It considers both typed and untyped protocol models;

• •

the SAT-based Model-Checker: it uses typed protocols and carries out bounded session verification by calling a SAT solvers to reduce problem input;

• •

the TA4SP: is a tree automata that carries out unbounded protocol verification by estimating the opponent knowledge using rewriting techniques.

The AVISPA tool was successful in finding new attacks, for instance, on the ISO-PK3 protocol and the IKEv2 protocol with digital signatures (a man-in-the-middle attack). However, the main drawback of model checkers remains the state explosion problem that we do not face using our approach. Another interesting tool is the ProVerif one [14, 15]. This latter uses an abstract representation of a protocol by Horn clauses and supports several cryptographic primitives described by rewrite rules or equations. The main limitation of this kind of verifiers is the halting problem where a program could never end. That is why binding sessions becomes usually a must. In our approach, we are not concerned about this problem since our approach is fully static.

IX Conclusion and future work

In this paper, we strongly believe that we are giving a new analytic direction for protocols’ verification against authentication flaws by using our recent finding: the witness functions. In a future work, we will experiment our approach on more protocols in order to know how wide is the range of protocols that could be analyzed with it and how reasonable is the rate of false negatives. A special attention will be paid to protocols that do not run in isolation in order to prevent multi-protocol attacks [16, 17]. Finally, anonymity is one of our immediate targets. In fact, this property seems to be the opposite of authentication in the sense that the link between the sender identity and the secret must be shown broken during the communication to make sure that an opponent cannot reconstruct it. This is a major concern in e-voting protocols, for example. In theory, witness functions should be useful to prove this property by setting sufficient conditions for anonymity.

Appendix: Notations

We denote by ${\cal{C}}=\langle{\cal{M}},\xi,\models,{\cal{K}},{\cal{L}}^{\sqsupseteq},\ulcorner.\urcorner\rangle$ the context of verification containing the parameters that affect the analysis of a protocol:

• $\bullet$

${\cal{M}}$: is a set of messages built from the algebraic signature $\langle\cal{N}$,$\Sigma\rangle$ where ${\cal{N}}$ is a set of atomic names (nonces, keys, principals, etc.) and $\Sigma$ is a set of functions ($enc$:​: encryption, $dec$:​: decryption, $pair$:​: concatenation (denoted by ”.” ), etc.). i.e. ${\cal{M}}=T_{\langle{\cal{N}},\Sigma\rangle}({\cal{X}})$. We use $\Gamma$ to denote the set of all substitution from ${\cal{X}}\rightarrow{\cal{M}}$. We denote by $\cal{A}$ all atomic messages (atoms) in ${\cal{M}},$ by ${\cal{A}}(m)$ the set of atomic messages in $m$ and by ${\cal{I}}$ the set of principals including the opponent $I$. We denote by $k{{}^{-1}}$ the reverse form of a key $k$ and we assume that $({k^{-1}})^{-1}=k$.

• $\bullet$

$\xi$: is the theory that describes the algebraic properties of the functions in $\Sigma$ by equations (e.g. $dec(enc(x,y),y^{-1})=x$).

• $\bullet$

$\models$: is the inference system of the opponent under the theory. Let $M$ be a set of messages and $m$ a message. $M$ $\models$ $m$ means that the opponent can infer $m$ from $M$ using his capabilities. We extend this notation to traces as follows: $\rho$ $\models$ $m$ means that the opponent can infer $m$ from the trace $\rho$.

• $\bullet$

${\cal{K}}$ : is a function from ${\cal{I}}$ to ${\cal{M}}$, that assigns to any principal a set of atomic messages describing his initial knowledge. We denote by $K_{{\cal{C}}}(I)$ the initial knowledge of the opponent, or simply $K(I)$ where the context of verification is obvious.

• $\bullet$

${\cal{L}}^{\sqsupseteq}$ : is the security lattice $({\cal{L}},\sqsupseteq,\sqcup,\sqcap,\bot,\top)$ used to assign security values to messages. A concrete example of a lattice is $(2^{\cal{I}},\subseteq,\cap,\cup,\cal{I},\emptyset)$ that will be used in this paper.

• $\bullet$

$\ulcorner.\urcorner$ : is a partial function that assigns a value of security (type) to a message in ${\cal{M}}$. Let $M$ be a set of messages and $m$ a single message. We write $\ulcorner M\urcorner\sqsupseteq\ulcorner m\urcorner$ when $\exists m^{\prime}\in M.\ulcorner m^{\prime}\urcorner\sqsupseteq\ulcorner m\urcorner$

• +

Let $p$ be a protocol, we denote by $R_{G}(p)$ the set of the generalized roles extracted from $p$. A generalized role is an abstraction of the protocol where the emphasis is put on a specific principal and all the unknown messages are replaced by variables. More details about the role-based specification could be found in [18]. We denote by ${\cal{M}}_{p}^{\cal{G}}$ the set of messages generated by $R_{G}(p)$, by ${\cal{M}}_{p}$ the set of closed messages (ground terms) generated by substitution in terms in ${\cal{M}}_{p}^{\cal{G}}$. We denote by $R^{-}$ (respectively $R^{+}$) the set of received messages (respectively sent messages) by a principal in the role $R$. Conventionally, we use uppercases for sets or sequences and lowercases for single elements. For example $M$ denotes a set of messages, $m$ a message, $R$ a role composed of sequence of steps, $r$ a step and $R.r$ the role ending by the step $r$. A valid trace is a ground term obtained by substitution in the generalized roles. We assume that the opponent has the full-control of the net and is able to defeat any operation $f$ in $\Sigma$ except encryption if he does not have the decryption key, as described in the Dolev-Yao model [19].