Secrecy by Witness-Functions Jaouhar Fattahi1 , Mohamed Mejri1 and Hanane Houmani2 1 LSI Group, Laval University, Quebec, Canada 2 University Hassan II, Morocco Abstract. In this paper, we introduce a new type of functions to analyze crypto- graphic protocols statically for the property of secrecy: the Witness-Functions. A Witness-Function is a reliable protocol-dependent function intended to prove the cor- rectness of a protocol through its growth. It bases its calculation on the static part of a message in a role-based specication and ignores the dynamic one by introducing the notion of derivative messages. It oers two interesting bounds that enable an analysis of protocols on an unbounded number of sessions. We give here the way to build these functions and we state the theorem of protocol analysis with the Witness-Functions. Keywords: Protocol, role-based specication, secrecy, sucient condition. 1 Motivation and background In this paper, we introduce a new static approach to analyze cryptographic protocols with witness-functions for the property of secrecy. Intuitively, an increasing protocol pre- serves the secret. In other words, if the security of any atomic message does not decrease between receiving and sending steps of a protocol, the secret is never leaked. For that, we should dene "good" metrics to evaluate the security of any atomic message. This way of thinking has been considered in some previous works. In [1], Steve Schneider proposed the concept of rank-functions as metrics to analyze protocols in CSP algebra. These functions were successful in analyzing Needham-Schroeder protocol. However, a such analysis requires the protocol implementation in CSP [2,3]. Besides, building rank-functions is not a trivial job and their existence is not sure [4]. In [5] Abadi, using Spi-Calculus [6,7], guarantees that: "If a protocol typechecks, then it does not leak its secret inputs". To do so, he requests from the exchanged messages to be composed of four parts having strictly the following types: {se- cret, public, any, confounder} in order to recognize the security level of every part. However, this approach cannot analyze protocols that had been implemented with no respect to this restriction. In the same vein, Houmani and al. [8,9,10,11] dened universal functions called interpretation functions able to analyze a protocol statically and operate on an abstraction of the protocol called generalized roles, that generate a space of messages with variables. An interpretation function must meet some sucient conditions to be reliable for the analysis. Obviously, less we have conditions on functions, more we have functions and more we have chance to get protocols proven correct since one function may fail to prove the growth of a protocol but another may manage to do. However, we notice that the conditions on functions were so restrictive that only two concrete functions had been proposed. We believe that the condition related to the full-invariance by substitution, which is the property-bridge between an analysis run on messages of the generalized roles and the conclusion made on valid traces, is the most restrictive one. Since the aim of our approach is to build as more reliable functions as we are able to do, we think that if we free a function from this restrictive condition, we can build more functions. Nevertheless, freeing a function from a condition may impel us to take additional precautions. In this work, we introduce the witness-functions to analyze crypto- graphic protocols. We show how to build them. We show that a witness-function oers two bounds that allow us to get rid of the restrictive condition of full-invariance by substitution in Houmani's work by using derivation techniques. We state nally the theorem of proto- col analysis with the Witness-Functions that sets an interesting criterion for the protocol correctness. Notations Hereafter, we give some denitions and conventions that will be used throughout the paper. + We denote by C = hM, ξ, |=, K, Lw , p.qi the context containing the parameters that aect the analysis of a protocol: • M : is a set of messages built from the algebraic signature hN ,Σi where N is a set of atomic names (nonces, keys, principals, etc.) and Σ is a set of allowed functions (enc:: encryption, dec:: decryption, pair:: concatenation (denoted by "." here), etc.). i.e. M = ThN ,Σi (X ). We use Γ to denote the set of all possible substitution from X → M. We denote by A all atomic messages in M, by A(m) the set of atomic messages (or atoms) in m and by I the set of agents (principals) including the intruder I . We denote by k −1 the reverse key of a key k and we consider that (k −1 )−1 = k . • ξ : is the equational theory that describes the algebraic properties of the functions in Σ by equations. e.g. dec(enc(x, y), y −1 ) = x. • |= : is the inference system of the intruder under the equational theory. Let M be a set of messages and m a message. M |= m means that the intruder is able to infer m from M using her capacity. We extend this notation to traces as following: ρ |= m means that the intruder can infer m from the messages exchanged in the trace ρ. • K : is a function from I to M, that assigns to any agent (principal) a set of atomic messages describing her initial knowledge. We denote by KC (I) the initial knowledge of the intruder, or simply K(I) where the context is clear. • Lw : is the security lattice (L, w, t, u, ⊥, >) used to attribute security levels to mes- sages. A concrete example of a lattice is (2I , ⊆, ∩, ∪, I, ∅) that will be used to attribute to a message α the set of principals that are allowed to know it. • p.q : is a partial function that assigns a value of security (type) to a message in M. Let M be a set of messages and m a message. We write pM q w pmq if ∃m0 ∈ M.pm0 q w pmq + Let p be a protocol, we denote by RG (p) the set of the generalized roles extracted from p. A generalized role is a protocol abstraction where the emphasis is put on a particular principal and all the unknown messages, and on which no verication could be done by the agent, are replaced by variables. A generalized role ends always by a sending step and an intruder I is introduced to describe that the received messages and the sent messages are probably sent or received by the intruder. More details about the role-based specication are in [12,13,14]. Hereafter, an example of a variation of N SL protocol written in a role-based specication: m1 : A −→ B : {Na .A}kb m2 : B −→ A : {B.Na }ka .{B.Nb }ka m3 : A −→ B : A.B.{Nb }kb Table 1. A variation of NSL protocol The generalized roles of this protocol in a role-based specication are RG (pNSL )= {A1G , A2G , BG1 , BG2 } where: A1G = i.1 A −→ I(B) : {Nai .A}kb 2 AG = i.1 A −→ I(B) : {Nai .A}kb i.2 I(B) −→ A : {B.Nai }ka .{B.X}ka i.3 A −→ I(B) : A.B.{X}kb BG1 = i.1 I(A) −→ B : {Y.A}kb i.2 B −→ I(A) : {B.Y }ka .{B.Nbi }ka BG2 = i.1 I(A) −→ B : {Y.A}kb i.2 B −→ I(A) : {B.Y }ka .{B.Nbi }ka i.3 I(A) −→ B : A.B.{Nbi }kb We denote by MGp the set of messages with variables generated by RG (p), by Mp the set of closed messages generated by substituting terms in MGp . We denote by R+ (respectively R− ) the set of sent messages (respectively received messages) by a honest agent in the role R. Commonly , we reserve the uppercase letters for sets or sequences of elements and the lowercase for single elements. For instance M denotes a set of messages, m a single message, R a role composed of a sequence of steps, r a step and R.r the role ending by the step r. + A valid trace is an interleaving of instantiated generalized roles where each message sent by the intruder can be produced by her using her capacity and the previous received messages. We denote by [[p]] the set of valid traces of p. + We assume that the intruder has the full-control of the net, as described in the Dolev- Yao model [15] with no restriction neither on the size of messages nor on the number of sessions. 2 Increasing protocols are correct with respect to the secrecy property To analyze a protocol, we need reliable functions to estimate the security level of every atomic message. In this section, we state sucient conditions allowing to guarantee that a function is reliable. We prove that an increasing protocol is correct with respect to the secrecy property when analyzed with such functions. 2.1 C -reliable interpretation functions Denition 21 (Well-formed interpretation function) Let F be an interpretation function. F is well-formed in C if: ∀M, M1 , M2 ⊆ M, ∀α ∈ A(M):   F (α, {α}) =⊥ F (α, M1 ∪ M2 ) = F (α, M1 ) u F (α, M2 ) F (α, M ) = >, if α ∈ / A(M )  For an atom α in a set of messages M , a well-formed interpretation function returns the bottom value "⊥" if α appears in clear in M . It returns for it in the union of two sets, the minimum "u" of the two values calculated in each set seperately. It returns the top value ">" if α does not appear at all in M . Example 22 Let m1 = {α}, m2 = {β.A}k , M = {m1 , m2 } and F a well-formed interpre- ab tation function. • F (α, M ) = F (α, {m1 } ∪ {m2 }) = F (α, {α}) u F (α, {β.A}kab )= ⊥ u > = ⊥ • F (β, M )= F (α, {m1 } ∪ {m2 })= F (β, {α}) u F (β, {β.A}kab )= > u F (β, {β.A}kab ) = F (β, {β.A}kab ) Denition 23 (Full-invariant-by-intruder interpretation function) Let F be an interpretation function. F is full-invariant-by-intruder in C if: ∀M ⊆ M, m ∈ M.M |=C m ⇒ ∀α ∈ A(m).(F (α, m) w F (α, M )) ∨ (pK(I)q w pαq) An interpretation function F is said to be full-invariant-by-intruder if when it assigns a security level to an atomic message α in a set of messages M , this level cannot be decreased by the intruder. That is to say, the intruder cannot infer another message m from M in which the level of security of α decreases (i.e. F (α, m) w F (α, M )) using her capacity in the context of verication, unless α is initially intended to be known by the intruder (i.e. pK(I)q w pαq). Denition 24 (Reliable interpretation function) Let F be an interpretation function and C be a context. F is C -reliable if F is well-formed and F is full-invariant-by-intruder in C. Denition 25 [F -increasing protocol] Let F be an interpretation function and p a protocol. p is F -increasing in C if: ∀R.r ∈ RG (p), ∀σ ∈ Γ : X → Mp we have: ∀α ∈ A(Mp ).F (α, r+ σ) w pαq u F (α, R− σ) A F -increasing protocol is a protocol where every involved principal (every substituted generalized role) never decreases the security levels of received components. When a protocol is F -increasing and F is a reliable function, it is intuitively easy to prove its correctness with respect to the secrecy property. In fact, if every agent appropriately protects her sent messages (if she initially knows the security level of a component, she has to encrypt it with at least one key having a similar or higher security level, and if she does not know its security level, she estimates it using a reliable function F ), the intruder can never reveal it. Denition 26 (Secret disclosure) Let p be a protocol and C a context. We say that p discloses a secret α ∈ A(M) in C if: ∃ρ ∈ [[p]].(ρ |=C α) ∧ (pK(I)q 6w pαq) A secret disclosure consists in exploiting a valid trace of the protocol (denoted by [[p]]) by the intruder using her knowledge K(I) in the context of verication C , to infer a secret α that she is not allowed to know (expressed by: pK(I)q 6w pαq in the denition 26). Lemma 27 Let F be a C -reliable interpretation function and p a F -increasing protocol. We have: ∀m ∈ M.[[p]] |=C m ⇒ ∀α ∈ A(m).(F (α, m) w pαq) ∨ (pK(I)q w pαq). Proof. See the proof 819 in [16]  The lemma 27 expressess an intuitive result that for any atom α in a message generated by an increasing protocol, its security level calculated by a reliable interpretation function is maintained greater than its initial value in the context, if the intruder is not initially allowed to know it. Thus, initially the atom has a certain security level. This value cannot be decreased by the intruder using her initial knowledge and received messages since a reliable function is full-invariant by intruder. In each new step of any valid trace, involved messages are better protected since the protocol is increasing. The proof is then run by induction on the size of the trace and uses the reliability properties of the interpretation function in every step. Theorem 21 (Correctness of increasing protocols) Let F be a C -reliable interpretation function and p a F -increasing protocol. p is C -correct with respect to the secrecy property. Proof. See the proof 820 in [16]  In this section, we have shown that an increasing protocol is correct with respect to the secrecy property when analyzed with an interpretation function that is full-invariant by intruder and well-formed, or simply reliable. Please notice that compared to the sucient conditions stated in [11], we have one less. Houmani in [11] requested that a protocol must be increasing on the messages of the generalized roles of the protocol (that contain variables), and demanded from the interpretation function to resist to the problem of substitution of variables. Here, we free our functions from this restrictive condition in order to be able to build more functions. We relocate this condition in our new denition of an increasing protocol, that is requested now to be increasing on valid traces. The problem of substitution migrates to the protocol and becomes less harder to deal with. 3 Building reliable interpretation functions As seen in the previous section, to analyze a protocol statically we need reliable interpre- tation functions to evaluate the level of security of each atom in a message. In this section, we propose a constructive way to build these functions. We rst show how to build a generic class of reliable selections inside the protection of the most external key (or simply the ex- ternal key), then we provide specialized selections that are instances of this class, and nally we show the way to build reliable selection-based interpretation functions. Similar techniques have been used in some previous works and especially in [8,10,11] to build functions based on the direct key of encryption and in [17] to verify correspondences for security in protocols. But rst, we introduce the notion of well-protected messages that have interesting properties that we will use in the denition of reliable selections. 3.1 Well-protected messages We denote by EC the set of encryption functions and by E C the complementary set Σ\EC in a context of verication C . In the denition 31, we dene the application keys that returns the encryption keys of any atom α in a message m. Denition 31 (Keys) Let M ⊆ M, f ∈ Σ and m ∈ M . We dene the application Keys as follows: Keys : A × M −→ P(P(A)) ∀t1 , t2 ...tn subterms of m: Keys(α, α) = {∅} Keys(α, β) = ∅, if α 6= β and β ∈ A n Keys(α, fk (t1 , ..., tn )) = {k} ⊗ ∪ Keys(α, ti ), if fk ∈ EC i=1 n Keys(α, f (t1 , ..., tn )) = ∪ Keys(α, ti ), if f ∈ E C i=1 We extend the application Keys to sets as follows: ∀M ⊆ M.Keys(α, M ) = ∪ Keys(α, m) and Keys(α, ∅) = ∅. m∈M Denition 32 (Equational theory, rewriting system and normal form) We assume that we can transform the equational theory ξ given in the context of verication to a convergent rewriting system →ξ such that: ∀m ∈ M, ∀α ∈ A(m), ∀l → r ∈→ξ , Keys(α, r) ⊆ Keys(α, l) (3.1.1) We denote by m⇓ the normal form of m in →ξ . The normal form of a message in the denition 32 is the one that has the smallest set of encryption keys and eliminates all the unnecessary keys (e.g. e(k, d(k −1 , m)) → m). This kind of rewriting systems orientation poses no problem with the most of equational theo- ries [18,19,20]. In the denition 33 we introduce the application Access where every element of Access(α, m) contains a set of required keys to decrypt α in m after elimination of unnecessary keys by the normal form dened in 32. Denition 33 (Access) Let M ⊆ M, f ∈ Σ and m ∈ M . We dene the application Accessor as follows: Access : A × M −→ P(P(A)) ∀t1 , t2 ...tn subterms of m: Access(α, α) = {∅} Access(α, β) = ∅, if α 6= β and β ∈ A n Access(α, fk (t1 , ..., tn )) = {k −1 } ⊗ ∪ Access(α, ti ), if fk ∈ EC and fk (t1 , ..., tn ) = fk (t1 , ..., tn )⇓ i=1 n Access(α, f (t1 , ..., tn )) = ∪ Access(α, ti ), if f ∈ E C and fk (t1 , ..., tn ) = fk (t1 , ..., tn )⇓ i=1 Access(α, f (t1 , ..., tn )) = Access(α, f (t1 , ..., tn )⇓ ), if not. We extend the application Access to sets as follows: ∀M ⊆ M.Access(α, M ) = ∪ Access(α, m) and Access(α, ∅) = ∅. m∈M Example 34 Let m be a message such that: m = {{A.D.α}k .α.{A.E.{C.α}k }k }k ; ab ef ab ac −1 −1 Access(α, m) = {{kac −1 , kab }, {kac }, {kac , kab , kef }}. −1 −1 −1 In the denition 35, we dene a well-protected message. Informally, a well-protected message is a message such that every atom α in it such that pαq A ⊥ is encrypted by at least one key k such that pk −1 q w pαq after elimination of unnecessary keys by the normal form dened in 32. Denition 35 (Well-protected message) Let C be context of verication, m ∈ M, M ⊆ M and α ∈ A(m) such that pαq A ⊥. We say that α is well-protected in m if: ∀K ∈ Access(α, m).pKq w pαq We say that α is well-protected in M if: ∀m ∈ M.α is well-protected in m We say that m is well-protected in C if: ∀α ∈ A(m).α is well-protected in m We say that M is well-protected in C if: ∀m ∈ M.m is well-protected in C. In the denition 36, we dene Clear(m). Informally, Clear(m) is the set of all atoms that appear in clear in m after elimination of unnecessary keys by the normal form dened in 32. Denition 36 (Clear) Let m ∈ M and M ⊂ M. Clear(m) = {α ∈ A(m)| ∅ ∈ Access(α, m)} We extend this denition to sets as follows: Clear(M ) = ∪ Clear(m) m∈M Lemma 37 Let M be a set of well-protected messages in M. We have: M |=C m ⇒ ∀α ∈ A(m).(α is well-protected in m) ∨ (pK(I)q w pαq) Proof. See the proof 912 in [16]  The lemma 37 states that from a set of well-protected messages, all atomic messages beyond the knowledge of the intruder (i.e. pK(I)q 6w pαq) remain well-protected in any message that the intruder could infer. In fact, since we operate on well-protected messages, every atom such that pαq A ⊥ is encrypted by at least one key k such that pk −1 q w pαq. So the intruder must retrieve k −1 before she sees α not well-protected in any message. Yet, the key k −1 , if it appears in M , should be in its turn encrypted by at least one key k 0 such that pk 0−1 q w pk −1 q since we operate on well-protected messages. The proof is then run by induction on the encryption keys. Lemma 38 (Lemma of non-disclosure of atomic secrets in well-protected messages) Let M be a set of well-protected messages in M and α an atomic message in M . We have: M |=C α ⇒ pK(I)q w pαq. Proof. See the proof 914 in [16]  3.2 Well-protected messages and increasing protocols The lemma 38 expresses an important result. It states that a set of well-protected messages never discloses a secret. Thus, an intruder cannot infer from this set of messages something that she is not initially allowed to know. The notion of well-protected messages is linked to the notion of increasing protocols. Indeed, having a reliable interpretation function F and a protocol p, p could not be F -increasing if it does not operate on a set of well-protected messages Mp . Thus, a F -increasing protocol does not leak secrets as established by the theroem 21. This could not happen if Mp is not well-protected. Thus, an atomic message that is not well-protected in Mp could be deduced by agents that have the decryption keys even if they are not intented to know it. To be coherent, a reliable interpretation function must give for a non-well-protected atom α in any message m in Mp a value less than pαq (e.g. F (α, m) = ⊥). 3.3 Reliable selections in well-protected messages Now, we will focus on building selections such that when they are composed to suit- able homomorphisms, provide reliable interpretation functions. The denition 39 introduces the notion of a well-formed selection and the denition 310 introduces the notion of a full- invariant-by-intruder selection. Denition 39 (Well-formed selection) Let M, M1 , M2 ⊆ M such that M, M1 and M2 are well-protected. Let S : A × M 7−→ 2A be a selection. We say that S is well-formed in C if:   S(α, {α}) = A, S(α, M1 ∪ M2 ) = S(α, M1 ) ∪ S(α, M2 ), S(α, M ) = ∅, if α ∈ / A(M )  For an atom α in a set of messages M , a well-formed selection returns all the atoms in M if M = {α}. It returns for it in the union of two sets of messages, the union of the two selections performed in each set separately. It returns the empty set if the atom does not appear in M . Denition 310 (Full-invariant-by-intruder selection) Let M ⊆ M such that M is well-protected. Let S : A × M 7−→ 2A be a selection. We say that S is full-invariant-by-intruder in C if: ∀M ⊆ M, m ∈ M, we have: M |=C m ⇒ ∀α ∈ A(m).(S(α, m) ⊆ S(α, M )) ∨ (pK(I)q w pαq) The goal of a full-invariant-by-intruder selection is to create a full-invariant-by-intruder function when composed to an appropriate homomorphism that transforms its returned values into security levels. Since a full-invariant-by-intruder function is requested to resist to any attempt of the intruder to generate a message m from any set of messages M in which the level of security of an atom, that she is not allowed to know, decreases compared to it its value in M , a full-invariant-by-intruder selection is requested to resist to any attempt of the intruder to generate a message m from any set of messages M in which the selection associated to an atom, that she is not allowed to know, could be enlarged compared to the selection associated to this atom in M . This fact is expressed by the denition 310. Denition 311 (Reliable selection) Let S : A × M 7−→ 2A be a selection and C be a context of verication. S is C -reliable if S is well-formed and S is full-invariant-by-intruder in C. 3.3.1 Reliable selections inside the protection of an external key Now, we dene a generic class of selections that we call SGen EK and we prove that any in- stance of this class is C -reliable. Then we instantiate concrete selections from this class. Denition 312 (SGen EK : selection inside the protection of an external key) We denote by SGen EK the class of all selections S that meet the following conditions: • S(α, α) = A; (3.3.1) • S(α, m) = ∅, if α 6∈ A(m); (3.3.2) • ∀α ∈ A(m), where m = fk (m1 , ..., mn ) : S(α, m) ⊆ ( ∪ A(mi )∪{k −1 }\{α}) if fk ∈ EC and pk −1 q w pαq and m = m⇓ (3.3.3) 1≤i≤n • ∀α ∈ A(m), where m = f (m1 , ..., mn ) : if fk ∈ EC and pk−1 q 6w pαq and m = m⇓ (a)   ∪ S(α, mi ) 1≤i≤n  S(α, m) = ∪ S(α, mi ) if f ∈ E C and m = m⇓ (b) (3.3.4) 1≤i≤n if m 6= m⇓ (c)   S(α, m⇓ ) • S(α, {m} ∪ M ) = S(α, m) ∪ S(α, M ) (3.3.5) For an atom α in an encrypted message m = fk (m1 , ..., mn ), a selection S as dened above returns a subset (see "⊆" in equation 3.3.3) among atoms that are neighbors of α in m inside the protection of the most external protective key k including its reverse form k −1 . The atom α itself is not selected. This set of candidate atoms is denoted by ∪ A(mi )∪{k −1 }\{α} 1≤i≤n in the equation 3.3.3. The most external protective key (or simply the external key) is the most external one that satises pk −1 q w pαq. By neighbor of α in m, we mean any atom that travels with it inside the protection of the external key. Outside the protection of the external key, we have:  no eective selection is performed;  any two messages joined by an operation other than an encryption by the external key (e.g. a concatenation or an encryption by a weak key) are assimilated to two distinct messages and the selection returns the union of the two selections performed separately in each one (see the equations 3.3.4(a) and 3.3.4(b));  the selection in two sets of messages is the union of the two selections performed sepa- rately in each one(see the equation 3.3.5);  the selection relative to a clear atom returns all atoms in M (see the equation 3.3.1);  the selection relative to an atom that does not appear in a message returns the empty set(see the equation 3.3.2). EK SGen denes a generic class of selections since it does not identify what atoms to select pre- cisely inside the protection of the external key. It identies only the atoms that are candidates for selection and among them we are allowed to return any subset. Proposition 313 Let S ∈ SGen EK and C be a context of verication. Let's have a rewriting system →ξ such that ∀m ∈ M, ∀α ∈ A(m) ∧ α 6∈ Clear(m), we have: ∀l → r ∈→ξ , S(α, r) ⊆ S(α, l) (3.3.6) We have: S is full-invariant-by-intruder in C . Proof. See the proof 107 in [16]  Remark 314 (Scope) The condition on the rewriting system →ξ given by the equation 3.3.6 in the denition 313 is introduced to make sure that the selection in the normal form is the smallest among all forms of a given message. This prevents the selection S to select atoms that may be inserted maliciously by the intruder by manipulating the equational theory. Hence, we are sure that all selected atoms by S are honest and do not come by an intruder manipulation of the mes- sage. For example, let m = {α.C}kab be a message in a homomorphic cryptography (i.e. {α.C}kab = {α}kab .{C}kab ). In the form {α.C}kab , the selection S(α, {α.C}kab ) may select C , but in the form {α}kab .{C}kab , the selection S(α, {α}kab .{C}kab ) may not. Then, we must make sure that the rewriting system →ξ we are using is oriented in such way that it chooses the form {α}kab .{C}kab rather than the form {α.C}kab because there is no guarantee that C is a honest neighbor and that it had not been inserted maliciously by the intruder using the homomorphic property in the theory. We assume that the equational theory in the context of verication allows the extraction of a convergent rewriting system that meets this condition. As for the proposition 313, it is quite easy to verify that by constuction a selection S that is instance of SGen EK is well-formed. The proof of full-invariance-by-intruder is run by induction on the tree of construction of any message. The main idea of the proof is that the selection of the candidate atoms is performed inside the encryption by the most external protective key and therfore beyond the knowledge of the intruder, thus the intruder cannot alter when she does not detain this key. Besides, according to the lemma 38, in a set of well-protected messages the intruder can never infer this key since it is atomic. The intruder cannot neither use the equational theory to alter this selection for the reasons given in the remark 314. Therefore the set of atoms returned by S cannot be altered (enlarged) by the intruder as required by a full-invariant-by-intruder selection. Example 315 Let α be an atomic message and m a message such that pαq = {A, B} and m = {A.C.α.D}kab . Let S1 , S2 and S3 be three selections such that: S1 (α, m) = {kab −1 }, S2 (α, m) = {A, C, kab } and S3 (α, m) = {A, C, D, kab }. These three selections are C -reliable. −1 −1 3.4 Instantiation of reliable selections from the class SGen EK Now that we dened a generic class of reliable selections SGen EK , we will instantiate some concrete selections from it, that are naturally reliable. Instantiating SGen EK consists in dening selections that return precise sets of atoms among the candidates allowed by SGen EK . 3.4.1 The selection SM EK AX : is the instance of the class SGen that returns for an atom EK in a message m all its neighbors, that are principal identities, inside the protection of the external protective key k in addition to its reverse form k −1 . (MAX means: the MAXimum of principal identities) 3.4.2 The selection SEK EK : is the instance of the class SGen EK that returns for an atom in a message m only the reverse form of the external protective key. (EK means: External Key) 3.4.3 The selection SN EK : is the instance of the class SGen EK that returns only its neigh- bors, that are principal identities, inside the protection of the external protective key. (N means: Neighbors) Several other selections could be dened such that the selections inside the most internal key or inside all the keys together since they are all subselections inside the external key. Example 316 Let α be an atom and m a message such that: pαq = {A, C} and m ={{{α.C}kab .B}kac .D}kad EK −1 EK −1 EK SM AX (α, m) = {C, B, kac }; SEK (α, m) = {kac }; SN (α, m) = {C, B} 3.5 Specialized C -reliable selection-based interpretation functions The following proposition gives the way to transform the elements returned by a selection to security levels. Proposition 317 Let ψ be a homomorphism dened as follows: ψ : (2A )⊆ 7→ ( Lw > if M = ∅ M 7→ u ψ(α) if not. α∈M {α} if α ∈ I (Principal Identities)  such that: ψ(α) = pαq if not. We have: FM EK AX = ψ ◦ SM AX , FEK = ψ ◦ SEK and FN EK EK EK EK EK = ψ ◦ SN are C -reliable. Proof. See the proof 1110 in [16]  The homomorphism ψ dened in the proposition 317 returns for a principal in a selection, its identity. It returns for a key its level of security in the context of verication. ψ ensures the mapping from the operator "⊆" to the operator "w" in the lattice which enables an interpretation function to inherit the full-invariance-by-intruder from its associated selection. It ensures also the mapping from the operator "∪" to the operator "u" in the lattice, which enables an interpretation function to be well-formed when its associated selection is well- formed. Generally, any function ψ ◦ S remains reliable for any selection S that is an instance of SGen EK . Example 318 Let α be an atom, m a message and kab a key such that: pαq = {A, B}; m = {A.C.α.D}kab ; −1 kab = kab ; pkab q = {A, B}; EK SEK (α, m) = {kab −1 }; SN EK (α, m) = {A, C, D}; SM EK AX (α, m) = {A, C, D, kab }; −1 FEK (α, m) = ψ ◦ SEK (α, m) = pkab q = {A, B}; FN (α, m) = ψ ◦ SN (α, m) = {A, C, D}; EK EK −1 EK EK AX (α, m) = ψ ◦ SM AX (α, m) = {A, C, D}upkab q = {A, C, D} u {A, B} = {A, C, D, B}. EK EK −1 FM 4 The Witness-Functions In the previous section, we presented a constructive way of a class of selection-based func- tions that have the required properties to analyze protocols statically. Unfortunatly, they operate only on valid traces that contain closed messages. However, a static protocol analysis should run over a nite set of messages of the generalized roles of the protocol because the set of valid traces is innite. The nite set of the generalized roles contains variables. The func- tions we dened are not "enough prepared" to analyze messages with variables because they are not supposed to be full-invariant by substitution (or stable by substitution) [21,22,23]. The full-invariance by substitution is the property-bridge that allows us to perform an anal- ysis over messages with variables and propagate the conclusion made-on to closed messages. In the following section, we deal with the substitution question. We introduce the notion of derivation to reduce the impact of variables and we build the witness-functions that operate on derivative messages rather than messages themselves. As we will see, the witness-functions provide two interesting bounds that are independent of all substitutions and hence we solve the problem of substitution. We last dene a criterion of protocol correctness based on these two bounds. The fact that the criterion is independent of all substitutions enables an analysis to be run on generalized roles and the decision made-on to be exported to valid traces. 4.1 Derivative message Let m, m1 , m2 ∈ M; X m = V ar(m); S1 , S2 ⊆ 2Xm ; α ∈ A(m); X, Y ∈ Xm and  be the empty message. Denition 41 (Derivation) We dene the derivative message as follows: ∂X  = ∂X α =α ∂X X = ∂X Y =Y ∂X f (m) = f (∂X m), f ∈ EC ∪ E C ∂{X} m = ∂X m ∂[X]m = ∂{Xm \X} m ∂S1 ∪S2 m = ∂S2 ∪S1 m= ∂S1 ∂S2 m= ∂S2 ∂S1 m For the sake of simplication, we denote by ∂m the expression ∂Xm m. The operation of derivation in the denition 41 (denoted by ∂ ) is used to eliminate variables in a message. ∂X m consists in eliminating the variable X in m. ∂[X]m consists in eliminating all variables, except X , in m. Hence, X when overlined is considered as a constant in m. ∂m consists in eliminating all the variables in m. Example 42 Let m = {A.X.Y }k where A and kab are static and X and Y are two vari- ab ables. We have: ∂m = {A}kab ; ∂X m = {A.Y }kab ; ∂[X]m = {A.X}kab Denition 43 Let m ∈ MGp , X ∈ Xm and mσ be a closed message. For all α ∈ A(mσ), σ ∈ Γ , we denote by: if α 6∈ A(mσ),  > F (α, ∂[α]mσ) = F (α, ∂m) if α ∈ A(∂m), F (X, ∂[X]m) if α ∈ A(Xσ) ∧ α ∈ / A(∂m).  A message m in a generalized role is composed of two parts: a static part and a dynamic part. The dynamic part is described by variables. For an atom α in the static part (i.e. ∂m), F (α, ∂[α]mσ) removes the variables in m and gives it the value F (α, ∂m). For anything that is not an atom of the static part, so comes by substitution of some variable X in m, F (α, ∂[α]mσ) considers it as the variable itself, treated as a constant (as a block), and gives it the value F (X, ∂[X]m). It gives the top value for any atom that does not appear in mσ . For any F such that its associated selection is an instance of the class SGenEK , F (α, ∂[α]mσ) depends only on the static part of m since α is never selected. The introduction of the derivation could suggest that we give to F (α, mσ) the value of F (α, ∂[α]mσ) and hence we neutralize the variable eects. Unfortunately, this does not happen without undesirable "side- eects" because derivation causes a "loss of details". Let's examine the following case in the example 44. Example 44 Let m1 and m2 be two messages of a generalized role of a protocol p such that m1 = {α.B.X}kad and m2 = {α.Y.C}kad and pαq = {A, D}. Let m = {α.B.C}kad be in a valid trace generated by p. ( EK {B, A, D} if m comes by the substitution of X by C in m1 FM AX (α, ∂[α]m) = {A, D, C} if m comes by the substitution of Y by B in m2 Hence FM AX (α, ∂[α]m) is not even a function on the closed message m since it may return EK more than one image for the same preimage. This leads us straightly to the witness-functions. 4.2 The Witness-Functions Denition 45 (Witness-Function) Let m ∈ MGp , X ∈ Xm and mσ be a closed message. Let p be a protocol and F be a C -reliable interpretation function. We dene a witness-function Wp,F for all α ∈ A(mσ), σ ∈ Γ , as follows: Wp,F (α, mσ) = u F (α, ∂[α]m0 σ 0 ) m0 ∈MGp ∃σ 0 ∈Γ.m0 σ 0 =mσ Wp,F is said to be a witness-function inside the protection of an external key when F is an interpretation function such that its associated selection is an instance of the class SGen EK . As seen in the example 44, the application dened in 43 is not necessary a function in the set MGp of messages generated by the generalized roles of p since a valid trace could have more than one source in MGp such that each source has a dierent static part. A witness-function is though a function since it looks for all the sources of any closed message and takes the minimum (the union). This minimum exists and is unique in the nite set MGp . Although a witness-function is protocol-dependent since it depends on messages in the generalized roles of the protocol, it is built in a standard way for any pair (protocol, interpretation function) in input. Remark 46 For a witness-function inside the protection of an external key, since its asso- ciated interpretation function calculates the security level of an atom always in a message m having an encryption pattern, i.e. when fk ∈ EC , the search of all sources of m in the set {m0 ∈ MGp |∃σ 0 ∈ Γ.m0 σ 0 = mσ} is reduced to a search in the encryption patterns in MGp . 4.3 Inheritance of reliability properties from F Proposition 47 Let Wp,F be a witness-function inside the protection of an external key. We have: Wp,F inherits reliability from F Proof. See the proof 122 in [16]  The selection associated with a witness-function inside the protection of an external key is the union of selections associated with the interpretation function F restricted to derivative messages. It is easy to verify that a witness-function is by construction well-formed. For the full-invariance-by-intruder property, since the derivation just removes variables and since each selection in the union returns a subset among acceptable candidates, then the union itself returns a subset among acceptable candidates (the union of subsets is a subset). Therefore the selection associated with a witness-function remains an instance of the class SGen EK and so full- invariant-by-intruder. Since the witness-function is the composition of the homomorphism associated with F and an instance of the class SGenEK , then it is reliable. Example 48 Let MGp = {{α.B.X}kad , {α.Y.C}kad , {A.Z}kbc }; m1 = {α.B.C}kad ; V ar(MGp ) = {X, Y, Z}. Wp,FM EK (α, m1 ) AX = {Denition 45} EK 0 0 EK 0 0 u FM AX (α, ∂[α]m σ ) = u FM AX (α, ∂[α]m σ ) m0 ∈MGp {{α.B.X}k ad ,{α.Y.C}k ad } ∃σ 0 ∈Γ.m0 σ 0 =m 1 σ 0 ={X7−→C,Y 7−→B} = {Wp,FMEK AX is well-formed from the proposition 47 } EK EK FM AX (α, ∂[α]{α.B.X}kad [X 7−→ C])uFM AX (α, ∂[α]{α.Y.C}kad [Y 7−→ B]) ={Denition 43 and derivation in 41} EK EK FM AX (α, {α.B}kad ) u FM AX (α, {α.C}kad ) = {Denition of FM AX } EK {B, A, D} ∪ {C, A, D} = {B, A, D, C} 4.4 Bounding a Witness-Function Lemma 49 Let m ∈ MGp and Wp,F be a witness-function inside the protection of an external key. ∀σ ∈ Γ, ∀α ∈ A(Mp ) we have: F (α, ∂[α]m) w Wp,F (α, mσ) w u F (α, ∂[α]m0 σ 0 ) m0 ∈MG p ∃σ 0 =mgu(m0 ,m) Proof. See the proof 124 in [16]  The upper bound of a witness-function estimates the security level of an atom from one conrmed source of the closed message, the witness-function it-self estimates it from the exact sources of the closed message (i.e. when the protocol is executed), and the lower bound estimates it from all likely sources of the closed message. The unication in the lower bound "hunts" the candidates from all the likely sources of the closed message in the protocol. 4.5 Sucient condition for protocol correctness with a Witness-Function Now, it is time to state the protocol analysis with a Witness-Function theorem that states a criterion for protocol correctness with respect to the secrecy property which is independent of all substitutions. Theorem 41 (Protocol analysis with a Witness-Function) Let Wp,F be a witness-function inside the protection of an external key. A sucient condition of correctness of p with respect to the secrecy property is: ∀R.r ∈ RG (p), ∀α ∈ A(r+ ) we have: u F (α, ∂[α]m0 σ 0 ) w pαq u F (α, ∂[α]R− ) m0 ∈MG p ∃σ 0 =mgu(m0 ,r + ) Proof. See the proof 125 in [16]  Thanks to the independence of the criterion stated by the theorem 41 of all substitutions, any decision made on the generalized roles can be transmitted to valid traces. 5 NSL protocol analysis with a witness-function Hereafter, we analyze the N SL protocol given in Table 1 with a witness-function. Let's have a context of verication such that: pAq = ⊥; pBq = ⊥; pNai q = {A, B} (secret shared between A and B ); pNbi q = {A, B} (secret shared between A and B ); pka−1 q = {A}; pkb−1 q = {B}; (L, w, t, u, ⊥, >) = (2I , ⊆, ∩, ∪, I, ∅); I = {I, A, B, A1 , A2 ,B1 , B2 , ...}; The set of messages generated by the protocol is MGp = {{NA1 .A1 }kB1 , {B2 .NA2 }kA2 , {B3 .X1 }kA3 , {X2 }kB4 , {Y1 .A4 }kB5 , {B6 .Y2 }kA5 , {B7 .NB7 }kA6 , {NB8 }kB8 } The variables are denoted by X1 , X2 , Y1 and Y2 ; The static names are denoted by NA1 , A1 , kB1 , B2 , NA2 , kA2 , B3 , kA3 , kB4 , A4 , kB5 , B6 , kA5 , B7 , NB7 , kA6 , NB8 and kB8 . After elimination of duplicates, MGp = {{NA1 .A1 }kB1 , {B2 .NA2 }kA2 , {B3 .X1 }kA3 , {X2 }kB4 , {Y1 .A4 }kB5 , {B7 .NB7 }kA6 , {NB8 }kB8 } Let's select the Witness-Function as follows: p = N SL; F = FM AX ; Wp,F (α, mσ) = EK u F (α, ∂[α]m0 σ 0 ); m0 ∈MG p ∃σ 0 .m0 σ 0 =mσ Let's denote the lower bound of the Witness-Function in the theorem 41 by: 0 Wp,F (α, r+ ) = u F (α, ∂[α]m0 σ 0 ) m0 ∈MG p ∃σ 0 =mgu(m0 ,r + ) Please notice that all messages are in their normal form since no equational theory is de- ned. Principal identities in the context are not analyzed since they are declared public. The protocol is analyzed for the property of secrecy only. 5.1 Analysis of the generalized role of A As dened in the generalized roles of p, an agent A can participate in two consequent sessions: S i and S j such that j > i. In the former session S i , the agent A receives nothing and sends the message {Nai .A}kb . In the consequent session S j , she receives the message {B.Nai }ka .{B.X}ka and she sends the message A.B.{X}kb . This is described by the following schema: 2 {B.Nai }ka .{B.X}ka Si : i Sj : {Na .A}kb A.B.{X}kb -Analysis of the messages exchanged in the session S i : 1- For any Nai : a- When sending: rS+i = {Nai .A}kb (in a sending step, the lower bound is used) ∀Nai .{m0 ∈ MGp |∃σ 0 = mgu(m0 , rS+i )} = ∀Nai .{m0 ∈ MGp |∃σ 0 = mgu(m0 , {Nai .A}kb )} = {({NA1 .A1 }kB1 , σ10 ), ({X2 }kB4 , σ20 ), ({Y1 .A4 }kB5 , σ30 )} such that:  0  σ1 = {NA1 7−→ Nai , A1 7−→ A, kB1 7−→ kb } σ 0 = {X2 7−→ Nai .A, kB4 7−→ kb }  20 σ3 = {Y1 7−→ Nai , A4 7−→ A, kB5 7−→ kb } 0 Wp,F (Nai , {Nai .A}kb ) = {Denition of the lower bound of the Witness-Function} F (Nai , ∂[Nai ]{NA1 .A1 }kB1 σ10 ) u F (Nai , ∂[Nai ]{X2 }kB4 σ20 )u F (Nai , ∂[Nai ]{Y1 .A4 }kB5 σ30 ) = {Setting the static neighborhood} F (Nai , ∂[Nai ]{Nai .A}kb σ10 ) u F (Nai , ∂[Nai ]{X2 }kb σ20 )u F (Nai , ∂[Nai ]{Y1 .A}kb σ30 ) = {Denition 43} F (Nai , {Nai .A}kb ) u F (X2 , ∂[X2 ]{X2 }kb )u F (Y1 , ∂[Y1 ]{Y1 .A}kb ) = {Derivation in the denition 41} F (Nai , {Nai .A}kb ) u F (X2 , {X2 }kb ) u F (Y1 , {Y1 .A}kb ) = {Since F = FM EK AX } {A, B} ∪ {B} ∪ {A, B} = {A, B}(1.0) b- When receiving: RS−i = ∅ (in a receiving step, the upper bound is used) F (Nai , ∂[Nai ]∅) = F (Nai , ∅) = > (1.1) 2- Compliance with the correctness criterion stated in the theorem 41: From (1.0) and (1.1), we have: Wp,F 0 (Nai , {Nai .A}kb ) = {A, B} w pNai q u F (Nai , ∅) = {A, B} (1.2) From (1.2) we have: the messages exchanged in the session S i respect the correctness criterion stated in the theorem 41. (I) -Analysis of the messages exchanged in the session S j : 1- For any X : a- When sending: rS+j = A.B.{X}kb 0 0 0 0 0 Wp,F (X, A.B.{X}kb ) = Wp,F (X, A)uWp,F (X, B)uWp,F (X, {X}kb ) = >u>uWp,F (X, {X}kb ) = Wp,F (X, {X}kb ) (2.0) 0 ∀X.{m0 ∈ MGp |∃σ 0 = mgu(m0 , {X}kb )} = {({X2 }kB4 , σ10 )} such that: σ10 = {X2 7−→ X, kB4 7−→ kb } 0 Wp,F (X, {X}kb ) = {Denition of the lower bound of the Witness-Function} F (X, ∂[X]{X2 }kB4 σ10 ) = {Setting the static neighborhood} F (X, ∂[X]{X2 }kb σ10 ) = {Denition 43} F (X2 , ∂[X2 ]{X2 }kb ) = {Derivation in the denition 41} F (X2 , {X2 }kb ) = {Since F = FM EK AX } {B} (2.1) b- When receiving: RS−j = {B.Nai }ka .{B.X}ka (in a receiving step, the upper bound is used) F (X, ∂[X]{B.Nai }ka .{B.X}ka ) =F (X, ∂[X]{B.Nai }ka ) u F (X, ∂[X]{B.X}ka ) = F (X, {B.Nai }ka ) u F (X, {B.X}ka ) = > u {A, B} = {A, B} (2.2) 3-Compliance with the correctness criterion stated in the theorem 41: From (2.0), (2.1) and (2.2), we have: 0 Wp,F (X, A.B.{X}kb ) = {B} w pXq u F (X, ∂[X]{B.Nai }ka .{B.X}ka ) = pXq ∪ {A, B} (2.3) From (2.3), we have: the messages exchanged in the session S j respect the correctness crite- rion stated in the theorem 41. (II) From (I) and (II), the messages exchanged in the generalized role of A respect the correctness criterion stated in the theorem 41. (III) 5.2 Analysis of the generalized role of B i As dened in the generalized roles of p, an agent B can participate in a session S 0 , in which she receives the message {Y.A}kb and she sends the message {B.Y }ka .{B.Nbi }ka . This is described by the following schema: i {Y.A}kb S0 : {B.Y }ka .{B.Nbi }ka 1- For any Nbi : a- When sending: r+0 i = {B.Y }ka .{B.Nbi }ka (in a sending step, the lower bound is used) S 0 0 0 Wp,F (Nbi , {B.Y }ka .{B.Nbi }ka ) =Wp,F (Nbi , {B.Y }ka ) u Wp,F (Nbi , {B.Nbi }ka ) = > u Wp,F0 0 (Nbi , {B.Nbi }ka ) = Wp,F (Nbi , {B.Nbi }ka ) (3.0) 0 G 0 0 ∀Nb .{m ∈ Mp |∃σ = mgu(m , {B.Nbi }ka )} i = {({B3 .X1 }kA3 , σ10 ), ({X2 }kB4 , σ20 ), ({B7 .NB7 }kA6 , σ30 )} such that:  0  σ1 = {B3 7−→ B, X1 7−→ Nbi , kA3 7−→ ka } σ 0 = {X2 7−→ B.Nbi , kB4 7−→ ka }  20 σ3 = {B7 7−→ B, NB7 7−→ Nbi , kA6 7−→ ka } 0 Wp,F (Nbi , {B.Nbi }ka ) = {Denition of the lower bound of the Witness-Function} F (Nbi , ∂[Nbi ]{B3 .X1 }kA3 σ10 ) u F (Nbi , ∂[Nbi ]{X2 }kB4 σ20 )uF (Nbi , ∂[Nbi ]{B7 .NB7 }kA6 σ30 ) = {Setting the static neighborhood} F (Nbi , ∂[Nbi ]{B.X1 }ka σ10 ) u F (Nbi , ∂[Nbi ]{X2 }ka σ20 )uF (Nbi , ∂[Nbi ]{B.Nbi }ka σ30 ) = {Denition 43} F (X1 , ∂[X1 ]{B.X1 }ka ) u F (X2 , ∂[X2 ]{X2 }ka )uF (Nbi , ∂[Nbi ]{B.Nbi }ka ) = {Derivation in the denition 41} F (X1 , {B.X1 }ka ) u F (X2 , {X2 }ka ) u F (Nbi , {B.Nbi }ka ) = {Since F = FM EK AX } {A, B} ∪ {A} ∪ {A, B} = {A, B} (3.1) b- When receiving: R−0 i = {Y.A}kb (in a receiving step, the upper bound is used) S F (Nbi , ∂[Nbi ]{Y.A}kb ) = > (3.2) 2- For any Y : a- When sending: r+0 i = {B.Y }ka .{B.Nbi }ka (in a receiving step, the upper bound is used) S 0 0 0 Wp,F (Y, {B.Y }ka .{B.Nbi }ka ) = Wp,F (Y, {B.Y }ka ) u Wp,F (Y, {B.Nbi }ka ) = Wp,F (Y, {B.Y }ka ) u > = Wp,F (Y, {B.Y }ka ) (3.3) 0 0 ∀Y.{m0 ∈ MGp |∃σ 0 = mgu(m0 , {B.Y }ka )} = {({B3 .X1 }kA3 , σ1 ), ({X2 }kB4 , σ2 )} such that:  0 σ1 = {B3 7−→ B, X1 7−→ Y, kA3 7−→ ka } σ20 = {X2 7−→ B.Y, kB4 7−→ ka } 0 Wp,F (Y, {B.Y }ka ) = {Denition of the lower bound of the Witness-Function} F (Y, ∂[Y ]{B3 .X1 }kA3 σ10 ) uF (Y, ∂[Y ]{X2 }kB4 σ20 ) = {Setting the static neighborhood} F (Y, ∂[Y ]{B.X1 }ka σ10 ) uF (Y, ∂[Y ]{X2 }ka σ20 ) = = {Denition 43} F (X1 , ∂[X1 ]{B.X1 }ka ) uF (X2 , ∂[X2 ]{X2 }ka ) = {Derivation in the denition 41} F (X1 , {B.X1 }ka ) u F (X2 , {X2 }ka ) = {Since F = FM EK AX } {A, B} ∪ {A} = {A, B} (3.4) b- When receiving: R−0 i = {Y.A}kb (in a receiving step, the upper bound is used) S F (Y, ∂[Y ]{Y.A}kb ) = {A, B} (3.5) 3- Compliance with the correctness criterion stated in the theorem 41: From (3.0), (3.1) and (3.2) we have: 0 Wp,F (Nbi , {B.Y }ka .{B.Nbi }ka ) = {A, B} w pNbi q u F (Nbi , ∂[Nbi ]{Y.A}kb ) = {A, B} (3.6) From (3.3), (3.4) and (3.5) we have: 0 Wp,F (Y, {B.Y }ka .{B.Nbi }ka ) = {A, B} w pY q u F (Y, ∂[Y ]{Y.A}kb ) = pY q u {A, B} (3.7) i From (3.6) and (3.7), the messages exchanged in the session S 0 respect the correctness cri- terion stated in the theorem 41. (IV) From (IV), the messages exchanged in the generalized role of B respect the correctness cri- terion stated by the theorem 41. (V) From (III) and (V), the protocol N SL respects the correctness criterion stated by the theorem 41, then it is correct with respect to the secrecy property. 6 Comparison with related works Houmani et al. in [8,9,10,11] have dened universal functions to analyze increasing pro- tocols. Even if they gave a clear guideline to build safe functions, just two functions have been dened: DEK and DEKAN. That is due to the diculty to prove that a function is full-invariant by substitution. Henceforth, with a witness-function, there is no need to re- quest the property of full-invariance by substitution from an interpretation function. The witness-function takes it in input, without this property, and solves the problem of substi- tutions locally in the protocol, thanks to its construction that depends fully on the static part of a message and thanks to its two bounds that do not depend on substitutions (bring two properties and have one for free). This enables us to build more functions, and then, to analyze more protocols. The bounds of a witness-function having an output free of variables are expected to prove the correctness of protocols that could not be proven with universal functions because of variables in output, for instance, Kerberos protocol and SET protocol with Houmanis' functions. Our approach does not need a complicated formalism as do the rank-functions suggested by Schneider in [1] that require the CSP formalism [24]. It does not need, neither, a strongly message-typing as suggested by Abadi in [5]. Our approach intersects Schneider's work and Houmani's work in the way of seeing the protocol correctness through its growth and through the need to have reliable metrics to evaluate security. Besides, all of these methods handle an unbounded number of sessions and provide a semi-decidable procedure since they decide only when the protocol is increasing. 7 Conclusion and future work In this paper, we introduced the witness-functions as a technique to analyze crypto- graphic protocols for secrecy. We gave the way to build them. In a future work, we intend to dene witness-functions based on the selection of other keys (other than the most ex- ternal key) like the most internal key or all encryption keys together. In this respect, we believe that a witness-function based on the selection of all neighbors and all encryption −1 −1 keys (i.e. S(α, {{E.α}kAB }kCD ) = {E, kAB , kCD }) could eciently deal with protocols with the Die-Hellman property in a non-empty equational theory. In this respect, we believe that the witness-functions are ready to deal with algebraic properties in convergent theo- ries. In addition, we intend to take benece of the bounds of a witness-function to con- sider exchanged messages in a protocol as keys of encryption. We intend also to experiment our witness-functions on compose protocols. Indeed, many protocols could be secure when they are analyzed separately but may show undesirable interactions when analyzed together. In this regard, similar researches had been led by V. Cortier, S. Ciobaca and S. Delaune in [25,26,27] where they suggest protocol-tags to secure compose protocols. We think that our witness-functions are prepared to deal with this question. References 1. Steve Schneider. Verifying authentication protocols in csp. IEEE Trans. Software Eng., 24(9):741758, 1998. 2. Steve Schneider. Security properties and csp. In IEEE Symposium on Security and Privacy, pages 174187, 1996. 3. Steve A. Schneider and Rob Delicata. Verifying security protocols: An application of csp. In 25 Years Communicating Sequential Processes, pages 243263, 2004. 4. James Heather and Steve Schneider. A decision procedure for the existence of a rank function. J. Comput. Secur., 13(2):317344, March 2005. 5. Martín Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46:611638, 1998. 6. Martín Abadi and Andrew D. Gordon. Reasoning about cryptographic protocols in the spi calculus. In CONCUR, pages 5973, 1997. 7. Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. In ACM Conference on Computer and Communications Security, pages 3647, 1997. 8. Hanane Houmani and Mohamed Mejri. Practical and universal interpretation functions for secrecy. In SECRYPT, pages 157164, 2007. 9. Hanane Houmani and Mohamed Mejri. Ensuring the correctness of cryptographic protocols with respect to secrecy. In SECRYPT, pages 184189, 2008. 10. Hanane Houmani and Mohamed Mejri. Formal analysis of set and nsl protocols using the interpretation functions-based method. Journal Comp. Netw. and Communic., 2012, 2012. 11. Hanane Houmani, Mohamed Mejri, and Hamido Fujita. Secrecy of cryptographic protocols under equational theory. Knowl.-Based Syst., 22(3):160173, 2009. 12. Mourad Debbabi, Y. Legaré, and Mohamed Mejri. An environment for the specication and analysis of cryptoprotocols. In ACSAC, pages 321332, 1998. 13. Mourad Debbabi, Mohamed Mejri, Nadia Tawbi, and I. Yahmadi. Formal automatic verication of authentication crytographic protocols. In ICFEM, pages 5059, 1997. 14. Mourad Debbabi, Mohamed Mejri, Nadia Tawbi, and I. Yahmadi. From protocol specications to aws and attack scenarios: An automatic and formal algorithm. In WETICE, pages 256262, 1997. 15. Danny Dolev and Andrew Chi-Chih Yao. On the security of public key protocols. IEEE Trans- actions on Information Theory, 29(2):198207, 1983. 16. Jaouhar Fattahi, Mohamed Mejri, and Hanane Houmani. The witness-functions: Proofs and intermediate results http://web_security.fsg.ulaval.ca/lab/sites/default/files/ WF/WFFMS/WFAppend.pdf. pages 128, 2014. 17. Bruno Blanchet. Automatic verication of correspondences for security protocols. Journal of Computer Security, 17(4):363434, 2009. 18. Hubert Comon-Lundh, Véronique Cortier, and Eugen Zalinescu. Deciding security properties for cryptographic protocols. application to key cycles. ACM Trans. Comput. Log., 11(2), 2010. 19. Véronique Cortier and Stéphanie Delaune. Decidability and combination results for two notions of knowledge in security protocols. J. Autom. Reasoning, 48(4):441487, 2012. 20. Véronique Cortier, Steve Kremer, and Bogdan Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning, 46(3-4):225259, 2011. 21. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. 22. Nachum Dershowitz and David A. Plaisted. Rewriting. In Handbook of Automated Reasoning, pages 535610. 2001. 23. Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors. Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of Lecture Notes in Computer Science. Springer, 2007. 24. Steve A. Schneider, Helen Treharne, and Neil Evans. Chunks: Component verication in csp||b. In IFM, pages 89108, 2005. 25. Stefan Ciobaca and Veronique Cortier. Protocol composition for arbitrary primitives. 2012 IEEE 25th Computer Security Foundations Symposium, 0:322336, 2010. 26. Véronique Cortier. Secure composition of protocols. In TOSCA, pages 2932, 2011. 27. Véronique Cortier and Stéphanie Delaune. Safely composing security protocols. Formal Methods in System Design, 34(1):136, 2009.