# Formal Analysis of SET and NSL Protocols Using the Interpretation Functions-Based Method

Authors: Hanane Houmani; Mohamed Mejri
Journal: Journal of Computer Networks and Communications
 (2012)

---

## Abstract

Most applications in the Internet such as e-banking and e-commerce use the SET and the NSL protocols to protect the communication channel between the client and the server. Then, it is crucial to ensure that these protocols respect some security properties such as confidentiality, authentication, and integrity. In this paper, we analyze the SET and the NSL protocols with respect to the confidentiality (secrecy) property. To perform this analysis, we use the interpretation functions-based method.   The main idea behind the interpretation functions-based technique is to give sufficient conditions that allow to guarantee that a cryptographic protocol respects the secrecy property. The flexibility of the proposed conditions allows the verification of daily-life protocols such as SET and NSL. Also, this method could be used under different assumptions such as a variety of intruder abilities including algebraic properties of cryptographic primitives. The NSL protocol, for instance, is analyzed with and without the homomorphism property. We show also, using the SET protocol, the usefulness of this approach to correct weaknesses and problems discovered during the analysis.


---

## Body

## 1. Motivations and Background

Intuitively, cryptographic protocols are communication protocols that involve cryptography to reach some specific security goals (authentication, secrecy, etc.). Today, these protocols are playing a key role in our daily life. Among others, they protect our banking transactions (e-commerce protocol), our access to private wired and wireless network, and our access to a variety of indispensable services (web, FTP, e-mail, etc.).Obviously, any flaws in such protocols can have heavy negative consequences on individuals and organizations. It is also a well-known fact that attacks exploiting cryptographic protocols flaws are generally very difficult to detect: tools such as intrusion detections and firewalls are helpless against them since it is difficult (even impossible some-times) to distinguish between legitimate and illegitimate users when the cryptographic protocol is flawed.Like any sensitive system, cryptographic protocols need to be seriously studied and their correctness should be rigorously analyzed and ideally proved. For that reason, formal specification and verification of security protocols have received much attention in recent years. Some of these works including comparative studies could be found in [1–10].Today and after more of thirty years of hard work, international community has a better understanding of cryptographic protocols and better support to specify and analyze them. But there remains a lot of work to do in this field. Some of the most important drawbacks of the existing results is that they are limited by either the class of protocols that they can analyze or the context (e.g., limited intruder abilities) in which they can analyze them. For instance, the method described in [11] gives an algorithm that allows to analyze the pingpong protocols in a polynomial time but only within the encryption of atomic and closed messages. Others like [12–23] are dedicated to a specific intruder capacity which is usually the standard Dolev and Yao model. These two parameters (the class of the analyzed protocols and the context in which they are analyzed) are generally hard-coded inside the approach making its adaptation to another context or others protocols very difficult. Also, in  [24], Paulson has proven that the Bull protocol preserves the secrecy by using an intruder model that does not consider any algebraic property of cryptographic primitives. However, he proved that attacks are possible on this protocol if some algebraic properties of ⊕ or of exponentiation are considered in the intruder model. Thereby, the flexibility of an approach to be adapted to different contexts of analysis is helpful to make the conditions of the analysis closer to the reality.To deal with this problem, we have introduced in [25, 26] a general and flexible approach that allows to analyze a large variety of protocols in different contexts (different intruder capacities including equational theories) based on interpretation functions. The idea is to give some metaresults (independent of a specific context) that give sufficient conditions allowing to guarantee the correctness of a protocol with respect of the secrecy (confidentiality) property.In this paper, we recall the main results of the approach and we show its efficiency and its flexibility by analyzing some famous cryptographic protocols such as SET protocol  [27–29] and NSL protocol [30] under different assumptions. In fact, we first analyze the secrecy property of the NSL protocol in the Dolev and Yao intruder model and after that we consider the homomorphism property of the encryption. This analysis allows us to prove that the NSL protocol is secure in the Dolev and Yao model whereas it is not when considering the homomorphism encryption property and some weaknesses are found. Second, we analyze the secrecy property of SET protocol which could be considered the first analysis until now that concern this protocol and the secrecy property which is very important in such protocols that allow to transmit secret information such as the card credit number.This paper is organized as follows. Section2 gives an overview of the interpretation functions-based method. The analysis of the NSL protocol in different contexts is given in Section 3. Section 4 analyzes the SET protocol. Section 5 compares the interpretation functions-based method with some similar works like the rank functions-based method [31, 32] and the typing-based method [33]. Finally, some concluding remarks are given in Section 6.


## 2. Overview of the Interpretation Functions-Based Method

As stated before, the main idea of our approach is to propose some conditions that are proven (in [25, 26]) sufficient to guarantee the secrecy property of any protocol that respects them. The proposed conditions can be easily verified in PTIME, and they state intuitively that principals involved in the protocol should not decrease the security levels of sent components. The security level of an atomic message is either given within the context of verification (input information) or estimated from received messages. The security levels estimated from received messages is calculated by using some special function called safe interpretation functions.A brief description about these notions could be found in the next sections. In fact, Section2.1 gives the intuitive definition and some examples of increasing protocols. Section 2.2 presents the notion of safe interpretation functions. After that Section 2.3 presents the definition of the secrecy property (confidentiality). Finally, Section 2.4 states the main result and show how the interpretation functions-based method could be applied to analyze the secrecy property.


### 2.1. Increasing Protocols

The sufficient condition to guarantee the secrecy property could be summarized as follows. Principals involved in the protocol should not decrease the security levels of sent components. Protocols that satisfy this condition are called in this work “increasing protocols.” For instance, the protocol described by Table1 is increasing since the security level of the message secret in step 1 is the same in step 2. Indeed, in step 1 the message secret is encrypted by the secret key of A to say that the message is originated from A and also is encrypted by the public key of B to say that the message secret is destined to B, hence the security level of the message secret is the security level that allows only B and A to know it. In the same way, we can notice that the security level of the message secret in step 2 is the security level that allows B and A to know it and hence, the protocol does not decrease the security level of message secret form step to another and so the protocol is increasing.Table 1
Example of increasing protocol.
1.A→B:{{A,B,secret}kb}ka-1
2.B→A:{{A,B,secret}ka}kb-1Let us consider the protocol described by Table2. This protocol is not increasing since the security level of the message secret in step 2 is lower than its security level in step 1. Indeed, in step 1 the message secret is encrypted by the secret key of A to say that the message is originated from A and also is encrypted by the public key of B to say that the message secret is destined to B, hence the security level of the message secret is the security level that allows only B and A to know it. In step 2, the message secret is encrypted by the secret key of B, so everybody could decrypt it and hence the security level of the message decreases from step 1 to step  2. The formal definition of decreasing protocol could be found in our previous works [25, 26].Table 2
Exemple of deacreasing protocol.
1.A→B:{{A,B,secret}kb}ka-1
2.B→A:{A,B,secret}kb-1


### 2.2. Safe Interpretation Function

To verify whether a protocol is increasing, we need a safe means to correctly estimate the security levels of received components so that we can appropriately handle them. We called it “safe interpretation function” (The name of the approach (interpretation functions-based approach) come for this notions.). Among the important features of a safe interpretation function is that its results could not be misled by the intruder manipulations. For example, if the interpretation function estimates that the security level of a componentα in a set of messages M is top secret, then the intruder can never produce M' from M such that the security level of α in M' is estimated by secret or public. A simple example of a safe interpretation function is the one that attributes a security level for a component α in a message m depending only on the direct keys encrypting α in m. This function, denoted by FDEK, will be referred later by DEK (Direct Encryption Key). Accordingly, FDEK(Nb,{S,Nb}kab) calculates the security level of Nb in the message {S,Nb}kab, and it is equal to the security level of kab. For example, if the security level of kab is {A,B} then we have
(1)FDEK(Nb,{S,Nb}kab)={A,B}.Another example of safe interpretation function, used in this paper, is the one that attributes a security level of a componentα in a message m depending on both the direct keys encrypting α in m and the neighbors of α in m (the components that can be reached from α without going outside encryptions: usually we consider neighbors that are only identities of agents). This function, denoted by FDEKAN, will be referred later by the DEKAN (direct encryption key and neighbors) function. Accordingly, FDEKAN(Nb,{S,Nb}kab) calculates the security level of Nb in the message {S,Nb}kab, and it depends on both the security level of kab and S. For example, if the security level of kab is {A,B} to design that is a shared secret between A and B, then we have
(2)FDEKAN(Nb,{S,Nb}kab)={A,B,S}.The DEK function and the DEKAN function can be used to analyze a large variety of cryptographic protocols. When the analysis fails, we should either adapt the protocol or use another safe function. However, the definition of safe functions is a complicated task. For this reason, we have introduced in [25, 26, 34] a helpful guideline allowing to define a safe interpretation function having the following form:
(3)F(α,M)=I∘S(α,M).The functionS selects from M some atomic components on which the security level of α depends. This function is called a selection function. The function I interprets what S returns as a security type. This function is called a rank function. This type of rank functions has been already introduced and used by Schneider et al. in [31, 32, 35] to attribute to a message a security level (rank).A simple way to define a selection function is to consider a term (a message in our case) as a tree where its arcs are annotated with real numbers that reflect costs or distances between nodes. After that, it will be easy to defineS as a function that selects components that are at some distance from a given component. For instance, let m be the message 〈B,{Nb,kab}kas〉 then the representation of m can be described as shown by Figure 1, where the annotations of arcs are explained later.Figure 1
The message(〈B,{Nb,kab}kas〉).Recall that the symbolenc is the encryption operator and the symbol pair is the concatenation operator. Hence, at distance 1, we could select the keys of encryption, and at distance 0 we could select components that are concatenated to some specific components.Of course, not all the interpretation functionsF which are the composition of the selection function S and a rank function I are safe (could not be misled by an intruder). In the sequel, we give some conditions that must be satisfied by the functions S and I so that their composition is safe. Intuitively, the conditions on the selection function S states that at least the direct encryption keys are selected and no components outside direct encryptions could be selected. The idea behind this condition is that only messages encrypted with a secret key could be safe from the intruder manipulations. For example S(α,{S,R,{α,A,Na,B,C}k1}k2) should return k1 and any subset in {A,Na,B,C}. To exclude components outside encryption, we attribute ∞ as a cost between any enc node and its father.In the other side, the conditions on the rank functionI state intuitively that the security level of a message, given by this function, should not be greater than its real security level. The idea behind this condition is that the rank function could not give any security level to messages. For instance, if β is a public information (according to the function ⌜·⌝ given within the context of analysis), then I cannot interpret it as secret because elsewhere β could encrypt a secret information whereas β is a public information and so such interpretation functions do give a safe means to estimate the secrurity level. An easy way to construct the rank function is to take it equal to the function ⌜·⌝.The formal definition of these functions and some sufficient conditions to construct some safe interpretation functions can be found in [25, 26, 34].As stated in Section1, there is a large variety of formal methods dedicated to the analysis of cryptographic protocols and particularly with respect to the secrecy property. One of the major differences between them is the assumptions or the restrictions required by each method from the analyzed protocol. They can analyze protocols only under some particular conditions. One of the major drawbacks of these approaches is that the proofs of the their main results are strongly connected to their assumptions making their adaptation to others assumptions a very tedious task.To overcome this drawback, we introduced in [25, 26] a more general approach that considers the context of verification (some assumptions on protocols, intruder model, etc.) as a parameter of the approach so that it will be clear how it affects any intermediary result. Intuitively, a context of verification contains all the parameters that affect the verification of cryptographic protocols. Among others, a context of verification, denoted by 𝒞 in this paper, contains the sorts of messages involved in analyzed protocols, the rules that capturing the intruder capacities, and the algebraic properties of the cryptographic primitives. As we will see later, all the results of our approach consider the context of the verification as a simple input parameter. This great flexibility is useful to change the class of protocols or the intruder capacities and use the approach without any need of reworking the proofs or the conditions. For instance, we can use the approach to analyze protocols that use either symmetric or asymmetric keys. Also, we can employ the approach with or without algebraic properties of cryptographic primitives as it will be shown later within examples.


### 2.3. Secrecy Property

In this work, the secrecy property is defined in term of information flow security. We adopt also the “no read-up” notion of Bell-La Padula [36] model stating that a subject at a given security level is not allowed to know an information having a higher security level. We suppose, without effective restrictions (notice that it is always possible to define a security lattice that reflects our needs and which is coherent with this hypothesis), that each principal has his security level captured by the highest security level of components in his initial knowledge. In other words, if an agent (including the intruder) knows a message with a security level τ, then he is also eligible to know all messages having a security level lower or equal than τ. Intuitively, we say that a protocol respects the secrecy property if the intruder cannot learn from any valid trace more than what he is eligible to know. For example, if K is the set of the intruder's initial knowledge where α has a security level denoted by ⌜α⌝, then the intruder is illegible to know an information β only if its security level  ⌜β⌝ is lower or equal to ⌜α⌝.


### 2.4. Main Result

Now, recall the sufficient conditions allowing to guaranty the correctness of a protocol with respect to the secrecy property. Informally, these conditions state that honest agents should never decrease, according to a safe interpretation function, the security level of any atomic message sent over the network. Protocols that satisfy this function are called increasing protocols. The formalization of an increasing protocol is as follows. The secrecy property of increasing protocols is guaranteed even for an unbounded number of sessions and in the presence of an active intruder who can use an unbounded number of operations to the messages that he manipulates. Indeed, we proved that, to check if a protocol respects the secrecy property, it is sufficient to verify whether a finite model of the protocol, called in this work a “roles-based specification,’’ is increasing.The verification process of the interpretation functions-based method can be summarized as described by Figure2.Figure 2
Protocol verification process.Intuitively, if the protocol is increasing according to a specific safe interpretation function, then we can deduce that the protocol respects the secrecy property; otherwise, we cannot make any statement about its correctness. Generally, if the correctness of a protocol cannot be ensured using a given safe interpretation function, it does not mean that a positive result cannot be involved using another one. However, even if the verification is not conclusive, it provides helpful information that can be used either to discover flaws or weaknesses in the analyzed protocol or to deduce another safe interpretation function allowing us to prove the secrecy property of a protocol as it will be illustrated later. Also, this verification is finite since it is conducted on a finite set of generalized roles.We believe that the sufficient conditions are not very restrictive, that is, for most of secure protocols we can construct a safe interpretation function allowing to prove the secrecy property. As shown later, even when the verification is not conclusive, the effort made to verify if the protocol is increasing could be helpful to discover flaws or weaknesses in the analyzed protocol or sometimes to have an idea about another safe interpretation function allowing to prove that it is increasing one. It is interesting to notice also that, some times, a slight modification on a protocol could make it an increasing one for a given safe interpretation function and allow to conclude that it is correct for secrecy.


### 2.5. Protocol

This section gives the syntax and semantics of a protocol and how to infer the roles-based specification from the standard description of a given protocol.


### 2.6. Syntax

Essentially, a protocol is specified by a sequence of communication steps given in the standard notation. Each step has an unique identifier and specifies the sender, the receiver, and the transmitted message. More precisely, a protocolp has to respect the following BNF grammar:
(4)p::=〈i:A→B:m〉∣p.p.The statement〈i:A→B:m〉 denotes the transmission of a message m from the principal A to the principal B in the step i of the protocol.Table3 gives an example of a protocol inspired from the Woo and Lam’s one  [37] and aims to distribute a fresh key that will be shared between two principals A and B.Table 3
Woo and Lam modified protocol.
p
WL
=
〈
1
,
A
→
B
:
A
〉
〈
2
,
B
→
A
:
N
b
〉
〈
3
,
A
→
B
:
{
N
b
,
k
a
b
}
k
a
s
〉
〈
4
,
B
→
S
:
{
A
,
{
N
b
,
k
a
b
}
k
a
s
}
k
b
s
〉
〈
5
,
S
→
B
:
{
N
b
,
k
a
b
}
K
b
s
〉


#### 2.6.1. Roles-Based Specification

To give a semantics to a protocol, we use the notion of generalized roles introduced in [38]. Intuitively, a roles-based specification is a set containing the prefixes of generalized roles. A generalized role is a protocol abstraction, where the emphasis is put on a particular principal and where all the unknown messages are replaced by variables. Also, an exponent i (the session identifier) is added to each fresh message to emphasize that these components change their values from one run to another. Intuitively, a generalized role reflects how a particular agent perceives the exchanged messages. To a given principal, different generalized roles can be attributed. These generalized roles are not necessarily prefixes of each others and show the different messages that can be accepted by a role to successfully reach a given step in the protocol. More details related to the generalized roles are in [39]. The roles-based specification (the set of generalized roles) of the Woo and Lam protocol is as follow.(i) The generalized roles ofA are 𝒜G1 and 𝒜G2 and are as follows:
(5)𝒜G1=〈i.1,A→I(B):A〉,𝒜G2=〈i.1,A→I(B):A〉〈i.2,I(B)→A:X〉〈i.3,A→I(B):{X,kabi}kas〉.If a given role cannot make any verification on a part of the received message, then this part needs to be substituted by a variable. The role ofA receives a nonce at step 2 but he cannot make any validation on it (we suppose that there are no different types for different messages). For that reason Nb has been substituted by X.(ii) The generalized roles ofB are ℬG1 and ℬG2 and are as follows:
(6)ℬG1=〈i.1,I(A)→B:A〉〈i.2,B→I(A):Nb〉,ℬG2=〈i.1,I(A)→B:A〉〈i.2,B→I(A):Nb〉〈i.3,I(A)→B:Y〉〈i.4,B→I(S):{A,Y}kbs〉.The variableY appears since the principal B receives at the third step the unknown message {Nb,kab}kas and he does not have the key kas to make any verification inside it. For a similar reason, the variable Z appears in the fifth step (the key kab is initially unknown by B and he could not make any verification on it).(iii) The generalized role ofS is
(7)𝒮G=〈i.4,I(B)→S:{A,{U,V}kas}kbs〉〈i.5,S→I(B):{U,V}kbs〉.SinceS does not initially know the value of Nb and kab, then these messages are, respectively, replaced by the fresh variables U and V.In the rest of this paper, we denote byℛG(p) the prefix closed set of generalized roles of the protocol p and if A is an agent, then ℛG(A) denotes the set of its generalized roles.


#### 2.6.2. Valid Traces

Based on generalized roles, we define the notion of avalid trace of a protocol (an acceptable execution of a protocol). A trace is considered valid if it respects the following tow conditions.(i)
Any session in the trace is an instance (a substitution) of a prefix of a generalized role.(ii)
Any message sent by the intruder should be deductible from his previous received messages, his initial knowledge, and his inference rules.For instance, the trace of Table4 is valid for the Woo and Lam protocol described by Table 3. This valid trace contains a breach of secrecy since the intruder can obtain the secret kabα that should be shared only between A and B.Table 4
Valid trace for the Woo and Lam modified protocol.
α
.
1
.
A
→
I
(
B
)
:
A
α
.
2
.
I
(
B
)
→
A
:
N
i
α
α
.
3
.
A
→
I
(
B
)
:
{
N
i
α
,
k
a
b
α
}
k
a
s
β.4.I(B)→S:{A,{Niα,kabα}kas}kis
β.5.S→I(B):{Niα,kabα}kis


#### 2.6.3. Semantics

The semantics of a protocolp executed in a context 𝒞 is given by the following definition.Definition 1 (semantics).
Let𝒞 be a context of verification and p a protocol. The semantics of p in 𝒞, denoted by [p]𝒞, is the set of valid traces of p when executed in 𝒞.


## 2.1. Increasing Protocols

The sufficient condition to guarantee the secrecy property could be summarized as follows. Principals involved in the protocol should not decrease the security levels of sent components. Protocols that satisfy this condition are called in this work “increasing protocols.” For instance, the protocol described by Table1 is increasing since the security level of the message secret in step 1 is the same in step 2. Indeed, in step 1 the message secret is encrypted by the secret key of A to say that the message is originated from A and also is encrypted by the public key of B to say that the message secret is destined to B, hence the security level of the message secret is the security level that allows only B and A to know it. In the same way, we can notice that the security level of the message secret in step 2 is the security level that allows B and A to know it and hence, the protocol does not decrease the security level of message secret form step to another and so the protocol is increasing.Table 1
Example of increasing protocol.
1.A→B:{{A,B,secret}kb}ka-1
2.B→A:{{A,B,secret}ka}kb-1Let us consider the protocol described by Table2. This protocol is not increasing since the security level of the message secret in step 2 is lower than its security level in step 1. Indeed, in step 1 the message secret is encrypted by the secret key of A to say that the message is originated from A and also is encrypted by the public key of B to say that the message secret is destined to B, hence the security level of the message secret is the security level that allows only B and A to know it. In step 2, the message secret is encrypted by the secret key of B, so everybody could decrypt it and hence the security level of the message decreases from step 1 to step  2. The formal definition of decreasing protocol could be found in our previous works [25, 26].Table 2
Exemple of deacreasing protocol.
1.A→B:{{A,B,secret}kb}ka-1
2.B→A:{A,B,secret}kb-1


## 2.2. Safe Interpretation Function

To verify whether a protocol is increasing, we need a safe means to correctly estimate the security levels of received components so that we can appropriately handle them. We called it “safe interpretation function” (The name of the approach (interpretation functions-based approach) come for this notions.). Among the important features of a safe interpretation function is that its results could not be misled by the intruder manipulations. For example, if the interpretation function estimates that the security level of a componentα in a set of messages M is top secret, then the intruder can never produce M' from M such that the security level of α in M' is estimated by secret or public. A simple example of a safe interpretation function is the one that attributes a security level for a component α in a message m depending only on the direct keys encrypting α in m. This function, denoted by FDEK, will be referred later by DEK (Direct Encryption Key). Accordingly, FDEK(Nb,{S,Nb}kab) calculates the security level of Nb in the message {S,Nb}kab, and it is equal to the security level of kab. For example, if the security level of kab is {A,B} then we have
(1)FDEK(Nb,{S,Nb}kab)={A,B}.Another example of safe interpretation function, used in this paper, is the one that attributes a security level of a componentα in a message m depending on both the direct keys encrypting α in m and the neighbors of α in m (the components that can be reached from α without going outside encryptions: usually we consider neighbors that are only identities of agents). This function, denoted by FDEKAN, will be referred later by the DEKAN (direct encryption key and neighbors) function. Accordingly, FDEKAN(Nb,{S,Nb}kab) calculates the security level of Nb in the message {S,Nb}kab, and it depends on both the security level of kab and S. For example, if the security level of kab is {A,B} to design that is a shared secret between A and B, then we have
(2)FDEKAN(Nb,{S,Nb}kab)={A,B,S}.The DEK function and the DEKAN function can be used to analyze a large variety of cryptographic protocols. When the analysis fails, we should either adapt the protocol or use another safe function. However, the definition of safe functions is a complicated task. For this reason, we have introduced in [25, 26, 34] a helpful guideline allowing to define a safe interpretation function having the following form:
(3)F(α,M)=I∘S(α,M).The functionS selects from M some atomic components on which the security level of α depends. This function is called a selection function. The function I interprets what S returns as a security type. This function is called a rank function. This type of rank functions has been already introduced and used by Schneider et al. in [31, 32, 35] to attribute to a message a security level (rank).A simple way to define a selection function is to consider a term (a message in our case) as a tree where its arcs are annotated with real numbers that reflect costs or distances between nodes. After that, it will be easy to defineS as a function that selects components that are at some distance from a given component. For instance, let m be the message 〈B,{Nb,kab}kas〉 then the representation of m can be described as shown by Figure 1, where the annotations of arcs are explained later.Figure 1
The message(〈B,{Nb,kab}kas〉).Recall that the symbolenc is the encryption operator and the symbol pair is the concatenation operator. Hence, at distance 1, we could select the keys of encryption, and at distance 0 we could select components that are concatenated to some specific components.Of course, not all the interpretation functionsF which are the composition of the selection function S and a rank function I are safe (could not be misled by an intruder). In the sequel, we give some conditions that must be satisfied by the functions S and I so that their composition is safe. Intuitively, the conditions on the selection function S states that at least the direct encryption keys are selected and no components outside direct encryptions could be selected. The idea behind this condition is that only messages encrypted with a secret key could be safe from the intruder manipulations. For example S(α,{S,R,{α,A,Na,B,C}k1}k2) should return k1 and any subset in {A,Na,B,C}. To exclude components outside encryption, we attribute ∞ as a cost between any enc node and its father.In the other side, the conditions on the rank functionI state intuitively that the security level of a message, given by this function, should not be greater than its real security level. The idea behind this condition is that the rank function could not give any security level to messages. For instance, if β is a public information (according to the function ⌜·⌝ given within the context of analysis), then I cannot interpret it as secret because elsewhere β could encrypt a secret information whereas β is a public information and so such interpretation functions do give a safe means to estimate the secrurity level. An easy way to construct the rank function is to take it equal to the function ⌜·⌝.The formal definition of these functions and some sufficient conditions to construct some safe interpretation functions can be found in [25, 26, 34].As stated in Section1, there is a large variety of formal methods dedicated to the analysis of cryptographic protocols and particularly with respect to the secrecy property. One of the major differences between them is the assumptions or the restrictions required by each method from the analyzed protocol. They can analyze protocols only under some particular conditions. One of the major drawbacks of these approaches is that the proofs of the their main results are strongly connected to their assumptions making their adaptation to others assumptions a very tedious task.To overcome this drawback, we introduced in [25, 26] a more general approach that considers the context of verification (some assumptions on protocols, intruder model, etc.) as a parameter of the approach so that it will be clear how it affects any intermediary result. Intuitively, a context of verification contains all the parameters that affect the verification of cryptographic protocols. Among others, a context of verification, denoted by 𝒞 in this paper, contains the sorts of messages involved in analyzed protocols, the rules that capturing the intruder capacities, and the algebraic properties of the cryptographic primitives. As we will see later, all the results of our approach consider the context of the verification as a simple input parameter. This great flexibility is useful to change the class of protocols or the intruder capacities and use the approach without any need of reworking the proofs or the conditions. For instance, we can use the approach to analyze protocols that use either symmetric or asymmetric keys. Also, we can employ the approach with or without algebraic properties of cryptographic primitives as it will be shown later within examples.


## 2.3. Secrecy Property

In this work, the secrecy property is defined in term of information flow security. We adopt also the “no read-up” notion of Bell-La Padula [36] model stating that a subject at a given security level is not allowed to know an information having a higher security level. We suppose, without effective restrictions (notice that it is always possible to define a security lattice that reflects our needs and which is coherent with this hypothesis), that each principal has his security level captured by the highest security level of components in his initial knowledge. In other words, if an agent (including the intruder) knows a message with a security level τ, then he is also eligible to know all messages having a security level lower or equal than τ. Intuitively, we say that a protocol respects the secrecy property if the intruder cannot learn from any valid trace more than what he is eligible to know. For example, if K is the set of the intruder's initial knowledge where α has a security level denoted by ⌜α⌝, then the intruder is illegible to know an information β only if its security level  ⌜β⌝ is lower or equal to ⌜α⌝.


## 2.4. Main Result

Now, recall the sufficient conditions allowing to guaranty the correctness of a protocol with respect to the secrecy property. Informally, these conditions state that honest agents should never decrease, according to a safe interpretation function, the security level of any atomic message sent over the network. Protocols that satisfy this function are called increasing protocols. The formalization of an increasing protocol is as follows. The secrecy property of increasing protocols is guaranteed even for an unbounded number of sessions and in the presence of an active intruder who can use an unbounded number of operations to the messages that he manipulates. Indeed, we proved that, to check if a protocol respects the secrecy property, it is sufficient to verify whether a finite model of the protocol, called in this work a “roles-based specification,’’ is increasing.The verification process of the interpretation functions-based method can be summarized as described by Figure2.Figure 2
Protocol verification process.Intuitively, if the protocol is increasing according to a specific safe interpretation function, then we can deduce that the protocol respects the secrecy property; otherwise, we cannot make any statement about its correctness. Generally, if the correctness of a protocol cannot be ensured using a given safe interpretation function, it does not mean that a positive result cannot be involved using another one. However, even if the verification is not conclusive, it provides helpful information that can be used either to discover flaws or weaknesses in the analyzed protocol or to deduce another safe interpretation function allowing us to prove the secrecy property of a protocol as it will be illustrated later. Also, this verification is finite since it is conducted on a finite set of generalized roles.We believe that the sufficient conditions are not very restrictive, that is, for most of secure protocols we can construct a safe interpretation function allowing to prove the secrecy property. As shown later, even when the verification is not conclusive, the effort made to verify if the protocol is increasing could be helpful to discover flaws or weaknesses in the analyzed protocol or sometimes to have an idea about another safe interpretation function allowing to prove that it is increasing one. It is interesting to notice also that, some times, a slight modification on a protocol could make it an increasing one for a given safe interpretation function and allow to conclude that it is correct for secrecy.


## 2.5. Protocol

This section gives the syntax and semantics of a protocol and how to infer the roles-based specification from the standard description of a given protocol.


## 2.6. Syntax

Essentially, a protocol is specified by a sequence of communication steps given in the standard notation. Each step has an unique identifier and specifies the sender, the receiver, and the transmitted message. More precisely, a protocolp has to respect the following BNF grammar:
(4)p::=〈i:A→B:m〉∣p.p.The statement〈i:A→B:m〉 denotes the transmission of a message m from the principal A to the principal B in the step i of the protocol.Table3 gives an example of a protocol inspired from the Woo and Lam’s one  [37] and aims to distribute a fresh key that will be shared between two principals A and B.Table 3
Woo and Lam modified protocol.
p
WL
=
〈
1
,
A
→
B
:
A
〉
〈
2
,
B
→
A
:
N
b
〉
〈
3
,
A
→
B
:
{
N
b
,
k
a
b
}
k
a
s
〉
〈
4
,
B
→
S
:
{
A
,
{
N
b
,
k
a
b
}
k
a
s
}
k
b
s
〉
〈
5
,
S
→
B
:
{
N
b
,
k
a
b
}
K
b
s
〉


### 2.6.1. Roles-Based Specification

To give a semantics to a protocol, we use the notion of generalized roles introduced in [38]. Intuitively, a roles-based specification is a set containing the prefixes of generalized roles. A generalized role is a protocol abstraction, where the emphasis is put on a particular principal and where all the unknown messages are replaced by variables. Also, an exponent i (the session identifier) is added to each fresh message to emphasize that these components change their values from one run to another. Intuitively, a generalized role reflects how a particular agent perceives the exchanged messages. To a given principal, different generalized roles can be attributed. These generalized roles are not necessarily prefixes of each others and show the different messages that can be accepted by a role to successfully reach a given step in the protocol. More details related to the generalized roles are in [39]. The roles-based specification (the set of generalized roles) of the Woo and Lam protocol is as follow.(i) The generalized roles ofA are 𝒜G1 and 𝒜G2 and are as follows:
(5)𝒜G1=〈i.1,A→I(B):A〉,𝒜G2=〈i.1,A→I(B):A〉〈i.2,I(B)→A:X〉〈i.3,A→I(B):{X,kabi}kas〉.If a given role cannot make any verification on a part of the received message, then this part needs to be substituted by a variable. The role ofA receives a nonce at step 2 but he cannot make any validation on it (we suppose that there are no different types for different messages). For that reason Nb has been substituted by X.(ii) The generalized roles ofB are ℬG1 and ℬG2 and are as follows:
(6)ℬG1=〈i.1,I(A)→B:A〉〈i.2,B→I(A):Nb〉,ℬG2=〈i.1,I(A)→B:A〉〈i.2,B→I(A):Nb〉〈i.3,I(A)→B:Y〉〈i.4,B→I(S):{A,Y}kbs〉.The variableY appears since the principal B receives at the third step the unknown message {Nb,kab}kas and he does not have the key kas to make any verification inside it. For a similar reason, the variable Z appears in the fifth step (the key kab is initially unknown by B and he could not make any verification on it).(iii) The generalized role ofS is
(7)𝒮G=〈i.4,I(B)→S:{A,{U,V}kas}kbs〉〈i.5,S→I(B):{U,V}kbs〉.SinceS does not initially know the value of Nb and kab, then these messages are, respectively, replaced by the fresh variables U and V.In the rest of this paper, we denote byℛG(p) the prefix closed set of generalized roles of the protocol p and if A is an agent, then ℛG(A) denotes the set of its generalized roles.


### 2.6.2. Valid Traces

Based on generalized roles, we define the notion of avalid trace of a protocol (an acceptable execution of a protocol). A trace is considered valid if it respects the following tow conditions.(i)
Any session in the trace is an instance (a substitution) of a prefix of a generalized role.(ii)
Any message sent by the intruder should be deductible from his previous received messages, his initial knowledge, and his inference rules.For instance, the trace of Table4 is valid for the Woo and Lam protocol described by Table 3. This valid trace contains a breach of secrecy since the intruder can obtain the secret kabα that should be shared only between A and B.Table 4
Valid trace for the Woo and Lam modified protocol.
α
.
1
.
A
→
I
(
B
)
:
A
α
.
2
.
I
(
B
)
→
A
:
N
i
α
α
.
3
.
A
→
I
(
B
)
:
{
N
i
α
,
k
a
b
α
}
k
a
s
β.4.I(B)→S:{A,{Niα,kabα}kas}kis
β.5.S→I(B):{Niα,kabα}kis


### 2.6.3. Semantics

The semantics of a protocolp executed in a context 𝒞 is given by the following definition.Definition 1 (semantics).
Let𝒞 be a context of verification and p a protocol. The semantics of p in 𝒞, denoted by [p]𝒞, is the set of valid traces of p when executed in 𝒞.


## 2.6.1. Roles-Based Specification

To give a semantics to a protocol, we use the notion of generalized roles introduced in [38]. Intuitively, a roles-based specification is a set containing the prefixes of generalized roles. A generalized role is a protocol abstraction, where the emphasis is put on a particular principal and where all the unknown messages are replaced by variables. Also, an exponent i (the session identifier) is added to each fresh message to emphasize that these components change their values from one run to another. Intuitively, a generalized role reflects how a particular agent perceives the exchanged messages. To a given principal, different generalized roles can be attributed. These generalized roles are not necessarily prefixes of each others and show the different messages that can be accepted by a role to successfully reach a given step in the protocol. More details related to the generalized roles are in [39]. The roles-based specification (the set of generalized roles) of the Woo and Lam protocol is as follow.(i) The generalized roles ofA are 𝒜G1 and 𝒜G2 and are as follows:
(5)𝒜G1=〈i.1,A→I(B):A〉,𝒜G2=〈i.1,A→I(B):A〉〈i.2,I(B)→A:X〉〈i.3,A→I(B):{X,kabi}kas〉.If a given role cannot make any verification on a part of the received message, then this part needs to be substituted by a variable. The role ofA receives a nonce at step 2 but he cannot make any validation on it (we suppose that there are no different types for different messages). For that reason Nb has been substituted by X.(ii) The generalized roles ofB are ℬG1 and ℬG2 and are as follows:
(6)ℬG1=〈i.1,I(A)→B:A〉〈i.2,B→I(A):Nb〉,ℬG2=〈i.1,I(A)→B:A〉〈i.2,B→I(A):Nb〉〈i.3,I(A)→B:Y〉〈i.4,B→I(S):{A,Y}kbs〉.The variableY appears since the principal B receives at the third step the unknown message {Nb,kab}kas and he does not have the key kas to make any verification inside it. For a similar reason, the variable Z appears in the fifth step (the key kab is initially unknown by B and he could not make any verification on it).(iii) The generalized role ofS is
(7)𝒮G=〈i.4,I(B)→S:{A,{U,V}kas}kbs〉〈i.5,S→I(B):{U,V}kbs〉.SinceS does not initially know the value of Nb and kab, then these messages are, respectively, replaced by the fresh variables U and V.In the rest of this paper, we denote byℛG(p) the prefix closed set of generalized roles of the protocol p and if A is an agent, then ℛG(A) denotes the set of its generalized roles.


## 2.6.2. Valid Traces

Based on generalized roles, we define the notion of avalid trace of a protocol (an acceptable execution of a protocol). A trace is considered valid if it respects the following tow conditions.(i)
Any session in the trace is an instance (a substitution) of a prefix of a generalized role.(ii)
Any message sent by the intruder should be deductible from his previous received messages, his initial knowledge, and his inference rules.For instance, the trace of Table4 is valid for the Woo and Lam protocol described by Table 3. This valid trace contains a breach of secrecy since the intruder can obtain the secret kabα that should be shared only between A and B.Table 4
Valid trace for the Woo and Lam modified protocol.
α
.
1
.
A
→
I
(
B
)
:
A
α
.
2
.
I
(
B
)
→
A
:
N
i
α
α
.
3
.
A
→
I
(
B
)
:
{
N
i
α
,
k
a
b
α
}
k
a
s
β.4.I(B)→S:{A,{Niα,kabα}kas}kis
β.5.S→I(B):{Niα,kabα}kis


## 2.6.3. Semantics

The semantics of a protocolp executed in a context 𝒞 is given by the following definition.Definition 1 (semantics).
Let𝒞 be a context of verification and p a protocol. The semantics of p in 𝒞, denoted by [p]𝒞, is the set of valid traces of p when executed in 𝒞.


## 3. Analysis of NSL Protocol

This section shows the efficiency and the flexibility of the interpretation functions-based approach when analyzing cryptographic protocols even when taking into consideration cryptographic primitives. We first analyze the NSL-protocol [30] without considering the homomorphism property and we show that it respects the secrecy property. Secondly, we show that if we consider a homomorphism encryption during the analysis, then some weaknesses could appear.


### 3.1. Analysis of NSL Protocol without the Homomorphism Property

In this section, we consider the NSL-protocol with the standard intruder model of Dolev and Yao (i.e., without algebraic properties).


#### 3.1.1. The NSL-Protocol

The Needham-Schroeder Lowe (NSL) protocol, denoted bypNSL and given in Table 5, is a mutual authentication protocol that uses asymmetric encryption.Table 5
Needham schroeder lowe protocol.
1.A→B:{A,Na}kb
2.B→A:{〈Na,Nb〉,B}ka
3.A→B:{Nb}kbThe first step of the analysis consists in fixing the context of verification which contains the message algebra, the intruder capabilities, and the security levels of all messages. Second, we define a safe interpretation function in this context. After that, the role-based specification can be analyzed to verify whether the protocol is increasing by using the defined safe interpretation function. The following paragraphs describe in detail these steps.


#### 3.1.2. NSL Context of Verification in the Dolev-Yao Model

Let𝒞NSL=〈ℳNSL,⊨NSL𝒦NSL,ℒNSL⊒,⌜·⌝NSL〉 be a context of verification where ℳNSL is (𝒩NSL,ΣNSL,ℰNSL) such that we have the following.(i)
𝒩NSL is the set of atomic messages given by BNF grammar shown in Table 6.(ii)
ΣNSL={pair,fst,snd,enc,dec} contains the set of message operators.
Hence, the set of messages ofℳNSL is defined by BNF rules shown in Table 7.(iii)
ℰNSL is an equational theory containing the following equations:
(8)fst(pair(x,y))=x,snd(pair(x,y))=y,dec(enc(x,k),k-1)=x,enc(dec(x,ka-1),ka)=x,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉.Table 6
𝒩
NSL
::=
A
(Principal Identifier)
|
N
a
(Nounce)
|
k
a
-
1
(Private key)
|
k
a
(Public key)Table 7
m
,
m
1
,
m
2
::=
𝒩
NSL
|
p
a
i
r
(
m
1
,
m
2
)
(Pair Function)
|
e
n
c
(
m
,
k
a
)
(Encryption Function)
|
d
e
c
(
m
,
k
a
-
1
)
(Decryption Function)
|
f
s
t
(
p
a
i
r
(
m
1
,
m
2
)
)
(First Function)
|
s
n
d
(
p
a
i
r
(
m
1
,
m
2
)
)
(Second Function)As usual, we can write{m}k instead of enc(m,k). Also, we can write m1,m2 or 〈m1,m2〉 instead of pair(m1,m2) and sign(m,k-1) instead of dec(m,k-1) if k-1 is a private key.Given a set of equationsℰNSL and a set of signatures ΣNSL, the intruder capacities, denoted by the relation ⊨NSL, are defined by the following rules:
(9)(knowledge)□M⊨NSLm[m∈M],(construction)M⊨NSLm1⋯M⊨NSLmnM⊨NSLf(m1,…,mn)[f∈ΣNSL],(ℰ-equality)M⊨NSLmM⊨NSLm′[m=ℰNSLm′].The initial knowledge of principals𝒦NSL can be as follows: each principal knows his identity, the identities of other principals, his public and private key, and all the public keys of the other principals. Also, each principal can generate fresh values.The security latticeℒNSL is ℒ0=(2ℐ,⊆). The security level of a message is the set of principals that are eligible to know its value. Therefore, the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ.The typing function⌜·⌝NSL could be any partial function from ℳNSL to ℒNSL that reflects the security levels of components exchanged during the protocol. In this example, we choose this function as follows:
(10)⌜·⌝=[Na↦{A,B},Nb↦{A,B},ka-1↦{A},ka↦⊥],
where A and B could be substituted by any principal identifier.


#### 3.1.3. NSL Safe Interpretation Function

We use the DEKAN function (that selects the direct encryption keys and neighbors) to analyze the NSL-protocol under the equational theoryℰNSL. More precisely, the DEKAN function is a composition of a selection function and an interpretation function, that is FNSL=INSL∘SNSL(i) The selection functionSNSL takes an atomic component α and a message m and returns keys that directly encrypt α in m with principal identities and variables that are neighbors of α in m. The notion of direct encrypting keys and neighbors are formalized using a special labeled tree representing the analyzed message m. More precisely, given a message m, we start by annotating the arcs of its corresponding tree according to schema given by Figure 3, where d is defined as follows:
(11)d={∞ifx=enc0else.This means that the distance between a node and his father is0 if it is not enc and its father is either pair or sign. If the node is enc, then the distance that separates it from its father is infinite. Finally, if the node is the encryption key of the function enc, then the distance to its father is 1. Using these distances between nodes, we consider two nodes as neighbors if the distance that separates them is equal to 0. Also, we consider a key as a direct encrypting one for α if the distance between them is equal to 1. Using these notions, SNSL(α,m) returns principal identifiers and variables in m having a distance 0 from α (neighbors) with atomic components having a distance 1 from α (direct encrypting keys). For example,
(12)SNSL(α,{β,A,{B,α,{α,Na,X}k3}k2}k1)={B,X,k2,k3}.(ii) The interpretation functionINSL interprets elements returned by SNSL as follows:
(13)INSL(∅)=⊤,INSL(S1∪S2)=INSL(S1)⊔INSL(S2),INSL({β})={{β}ifβisaprincipalidentifier,⌜β-1⌝ifβisakey,τβifβisavariable.For example, if⌜k2-1⌝={A}  and ⌜k3-1⌝={S} then,
(14)INSL({B,X,k2,k3})=τX⊔{A,B,S}.Figure 3
Safe costs assignment.Notice also that, when an equational theory is taken into consideration, a message can have different equivalent forms. In this situation, to be safe, an interpretation function should give to a message the lowest level of the messages of its class. More precisely, ifm/ℰ={m′∈ℳ∣m=ℰm'}, then, for any atomic message α, we have
(15)F(α,m)=∏m′∈m/ℰF(α,m′).To simplify the computation ofF, we usually try to transform the equational theory to a convergent inference system so that the canonical form of a message m, denoted by m↓, has always the lowest security level. In other words,
(16)F(α,m↓)⊑∏m′∈m/ℰF(α,m′).To reach this goal, we orient the equation so that the right side is greater to the left side according toF and the obtained rewriting system is convergent (the convergence can be proved based on another ordering relation that is independent of F). (Notice that if such orientation is not possible, the approach cannot be applied. However, for all the equational theories that we have already considered till now we didn't find difficulties to orient them.) For our example, it is simple to see that the following rewriting system is convergent and gives the lowest security level:
(17)fst(〈x,y〉)→x,snd(〈x,y〉)→y,dec(enc(x,k),k-1)→x,enc(dec(x,ky-1),ky)→x,〈〈m1,m2〉,m3〉→〈m1,〈m2,m3〉〉.


#### 3.1.4. NSL Role-Based Specification

The NSL role-based specification is(18)ℛG(pNSL)={𝒜G1,𝒜G2,ℬG1},
where the generalized roles 𝒜G1 and 𝒜G2 are as follows:
(19)𝒜G1=i.1.A→I(B):{A,Nai}kbi.1.A→I(B):{A,Nai}kb,𝒜G2=i.2.I(B)→A:{〈Nai,X〉,B}kai.3.A→I(B):{X}kb,
and the generalized role ℬG1 is as follows:
(20)ℬG1=i.1.I(A)→B:{A,Y}kbi.2.B→I(A):{〈Y,Nbi〉,B}ka.


#### 3.1.5. Verifying Whether the NSL Role-Based Specification Is Increasing

Now, we can verify whether the role-based specification of SET isFSET-increasing. More precisely, we need accordingly to verify that principals do not decrease the security level of components from step to another. To that end, we verify this condition on each generalized role of the protocol (i.e., on each point of view of protocol participants). To that end, we should verify whether the security level of sent messages is a subset of the security level of these messages in the received steps, that is,
(21)∀rFSET(α,r+)⊆⌜α⌝∪FSET(α,r-)∀α.From the generalized roles ofA, we deduce that
(22)𝒜G1-=∅,𝒜G1+={A,Nai}kb,𝒜G2-={〈Nai,X〉,B}ka,𝒜G2+={X}kb.Recall that we are working with the lattice of security(2ℐ,⊆), so the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ. Then, the security levels of sent and received messages in the generalized roles of A according to FNSL are as shown in Table 8.Table 8
Analysis of NSL: role ofA.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
a
i
𝒜
G
1
{
A
,
B
}
{
B
}
⊤
Yes
X
𝒜
G
2
τ
X
{
B
}
{
A
,
B
}
Yes
(
for  any
τ
X
∈
2
ℐ
)Table8 shows that the generalized roles 𝒜G1 and 𝒜G2 are FNSL-increasing.From the generalized roles ofB, we deduce that
(23)ℬG1-={A,Y}kb,ℬG1+={〈Y,Nbi〉,B}ka.Then, the security levels of sent and received messages in the generalized roles ofB according to FNSL are as in Table 9.Table 9
Analysis of NSL protocol: role ofB.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
b
i
ℬ
G
1
{
A
,
B
}
{
A
}
⊤
Yes
Y
ℬ
G
1
τ
Y
{
A
,
B
}
{
A
,
B
}
Yes
(
for  any
τ
Y
∈
2
ℐ
)Table9 shows that the generalized role ℬG1 is FNSL-increasing. Since all generalized roles of NSL are FNSL-increasing, then it is an FNSL-increasing protocol. Furthermore, since FNSL is 𝒞NSL-safe interpretation function, we conclude, from  our main result,  that NSL is 𝒞NSL-correct with respect to secrecy.


### 3.2. Analysis of the NSL-Protocol with the Homomorphism Property

This section presents the analysis of the Needham-Schroeder Lowe (NSL) protocol with the homomorphism property of encryption:(24)enc(g(x,y))=g′(enc(x),enc(y)),
where g and g' are any operators (usually the same) from the message algebra. For example, enc(m1·m2)=enc(m1)·enc(m2) is satisfied when using block ciphers with Electronic Code Block (ECB) and when m1 has the same size as requested by the encryption system (64 bits for DES). In fact, the ECB consists of splitting the message into blocks of n-bits and encrypting each of them separately. Many asymmetric systems like RSA, Elgamal, Benaloh, and Paillier are also homomorphic for some algebraic operators.Related works that take into consideration the homomorphism property in the analysis of cryptographic protocols are rare and most of them do not deal with an unbounded number of sessions. Among the important results obtained in this direction are those described in [40–42] which address the intruder deduction problem and propose a PTIME-decision procedure for it. Despite the importance of the result, the resolution of the intruder deduction problem is not enough to analyze a protocol that can exhibit an infinite number of sessions.The interpretation functions-based method does not suffer from this problem since it is proved that if the protocol is increasing then it is sufficient to guarantee its correctness for the secrecy property under an unbounded number of sessions. In the sequel, we show how the homomorphism property can affect the analysis of a protocol like NSL.


#### 3.2.1. NSL Context of Verification with the Homomorphism Property

First, we need to change the context of verification𝒞NSL used in the previous section, so that we consider the homomorphism property. Let 𝒞NSL' be a context of verification such as 𝒞NSL'=〈(𝒩NSL,ΣNSL,ℰNSL'),⊨NSL𝒦NSL,ℒNSL⊒,⌜·⌝NSL〉 where all items are the same as those defined in the context 𝒞NSL except the equational theory ℰNSL' that includes homomorphism of encryption and it is as follows:
(25)fst(pair(x,y))=x,snd(pair(x,y))=y,dec(enc(x,k),k-1)=x,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉,enc(〈x,y〉,z)=〈enc(x,z),enc(y,z)〉.The last two equations ofℰNSL' reflect the homomorphic property of the encryption enc and the signature sign with respect to the concatenation operator 〈·〉.


#### 3.2.2. NSL Safe Interpretation Function with the Homomorphism Property

We use the DEKAN function (that selects the direct encryption keys and neighbors) to analyze the Needham-Schroeder Lowe protocol under the equational theoryℰNSL'. With the homomorphism property, the DEKAN function becomes equal to the DEK function (that selects direct encryption keys). Indeed, the selection is forbidden beyond encryption and the selection is always calculated on the message m↓ (the canonical form of m according to the rewriting system obtained from the equational theory ℰNSL', when the equality is replaced by →) instead of m. For example, with the homomorphism property the message {α1,…,αn}k, where α1,…,αn are atomic, is always reduced, by the homomorphism property, to {α1}k,…,{αn}k. To calculate the security level of a component αi in the message {α1,…,αn}k, the DEKAN function is applied on its canonical form that is {α1}k,…,{αn}k. It follows that the neighbors are never chosen, and we conclude that the DEKAN function behaves as the DEK function.


#### 3.2.3. Verifying Whether the NSL Role-Based Specification Is Increasing

From the generalized roles ofA, we deduce that
(26)𝒜G1-=∅,𝒜G1+={A,Nai}kb,𝒜G2-={〈Nai,X〉,B}ka,𝒜G2+={X}kb.The security levels of sent and received messages in the generalized roles ofA using the DEKAN function FNSL are as shown in Table 10.Table 10
Analysis of NSL protocol: role ofA.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
a
i
𝒜
G
1
{
A
,
B
}
{
B
}
⊤
Yes
X
𝒜
G
2
τ
X
{
B
}
{
A
}
NoTable10 shows that the generalized role 𝒜G2 is not increasing. Indeed, the message X is sent with the security level {B} which is not always in its security level ⌜X⌝∪{A} estimated from the received messages. In this case, we can never find a safe interpretation function that guarantees the correctness of the protocol simply because the protocol is flawed and it could be attacked as shown by Table 11. Notice that message of step 1.2 could be generated by the intruder from the message 2.2 using the homomorphic property. In fact, {Na1,Nb2,B}ka={Na1,Nb2}ka,{B}ka and since the intruder can produce {I}ka, then using the homomorphic property he can produce {Na1,Nb2,I}ka by simply concatenating {Na1,Nb2}ka with {I}ka.Table 11
Flaw in the NSL-protocol under the homomorphic assumption.
1.1.A→I:{A,Na1}ki
2.1. I(A)→B:{A,Na1}kb
2.2. B→I(A):{Na1,Nb2,B}ka
1.2.I→A:{Na1,Nb2,I}ka
1.3.A→I:{Nb2}ki
2.3. I(A)→B:{Nb2}kbThis is because the DEKAN function (that selects direct encryption keys and neighbors) with the homomorphism property acts as the DEK function (that selects the direct encryption keys only) and does not select the neighbors. Therefore, to correct this protocol in the presence of such property, we should find a means (different from the concatenation, such as signatures), allowingA to conclude that Nb is from B. To overcome this problem, we suggest the use of signatures to indicate the correct security level of sent messages. For instance, we can replace the message {A,Na}kb at step 1 of the NSL-protocol with the message {{Na}ka-1}kb. In this case, signing the message Na by ka-1 is a safe way to indicate that it comes from the agent A. In the same way, we can replace the message of step 2 of the NSL-protocol by the message {{〈Na,Nb〉}kb-1}ka. Notice that if signature is also homomorphic like encryption, operators like hash functions can be used to forge such type of inseparable links between some elements.From the generalized roles ofB, we deduce that
(27)ℬG1-={A,Y}kb,ℬG1+={〈Y,Nbi〉,B}ka.
Then, the security level of sent and received messages in the generalized roles of B using the DEKAN function FNSL is as shown in Table 12.Table 12
Analysis of NSL protocol: role ofB.
α
r
⌜
α
⌝
0
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
?
⌜
α
⌝
0
∪
F
NSL
(
α
,
r
-
)
N
b
i
ℬ
G
1
{
A
,
B
}
{
A
}
⊤
Yes
Y
ℬ
G
1
⊤
{
A
}
{
B
}
NoTable12 shows that the generalized role ℬG1 is not increasing. Indeed, the message Y is sent with the security level {A} which is not in its security level {B} estimated from the received messages. As for the role of A, we suggest to replace the message {A,Na}kb of step 1 of the NSL-protocol with the message {{Na}ka-1}kb. In this case, signing the message Na by ka-1 is a safe way to indicate that it comes from the agent A. In the same way, we can replace the message of step 2 of the NSL-protocol with the message {{〈Na,Nb〉}kb-1}ka.Therefore, the NSL-protocol is not increasing and, so, we cannot deduce anything about its correctness for the secrecy property. However, the protocol, with the changes suggested above, is increasing and it is therefore correct for the secrecy property even in the presence of the homomorphism property. Table13 summarizes these changes.Table 13
Needham schroeder lowe protocol: corrected version.
1.A→B:{{Na}ka-1}kb
2.B→A:{{〈Na,Nb〉}kb-1}ka
3.A→B:{Nb}kbBy using the DEK function or the DEKAN function, this new version of the Needham-Schroeder-Lowe protocol is increasing and then respects the secrecy property. Indeed, with this versionNa is received with the security level {A,B} and so it could be sent to A. Also, Nb is received with security level {A,B} and so it could be sent to B.


## 3.1. Analysis of NSL Protocol without the Homomorphism Property

In this section, we consider the NSL-protocol with the standard intruder model of Dolev and Yao (i.e., without algebraic properties).


### 3.1.1. The NSL-Protocol

The Needham-Schroeder Lowe (NSL) protocol, denoted bypNSL and given in Table 5, is a mutual authentication protocol that uses asymmetric encryption.Table 5
Needham schroeder lowe protocol.
1.A→B:{A,Na}kb
2.B→A:{〈Na,Nb〉,B}ka
3.A→B:{Nb}kbThe first step of the analysis consists in fixing the context of verification which contains the message algebra, the intruder capabilities, and the security levels of all messages. Second, we define a safe interpretation function in this context. After that, the role-based specification can be analyzed to verify whether the protocol is increasing by using the defined safe interpretation function. The following paragraphs describe in detail these steps.


### 3.1.2. NSL Context of Verification in the Dolev-Yao Model

Let𝒞NSL=〈ℳNSL,⊨NSL𝒦NSL,ℒNSL⊒,⌜·⌝NSL〉 be a context of verification where ℳNSL is (𝒩NSL,ΣNSL,ℰNSL) such that we have the following.(i)
𝒩NSL is the set of atomic messages given by BNF grammar shown in Table 6.(ii)
ΣNSL={pair,fst,snd,enc,dec} contains the set of message operators.
Hence, the set of messages ofℳNSL is defined by BNF rules shown in Table 7.(iii)
ℰNSL is an equational theory containing the following equations:
(8)fst(pair(x,y))=x,snd(pair(x,y))=y,dec(enc(x,k),k-1)=x,enc(dec(x,ka-1),ka)=x,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉.Table 6
𝒩
NSL
::=
A
(Principal Identifier)
|
N
a
(Nounce)
|
k
a
-
1
(Private key)
|
k
a
(Public key)Table 7
m
,
m
1
,
m
2
::=
𝒩
NSL
|
p
a
i
r
(
m
1
,
m
2
)
(Pair Function)
|
e
n
c
(
m
,
k
a
)
(Encryption Function)
|
d
e
c
(
m
,
k
a
-
1
)
(Decryption Function)
|
f
s
t
(
p
a
i
r
(
m
1
,
m
2
)
)
(First Function)
|
s
n
d
(
p
a
i
r
(
m
1
,
m
2
)
)
(Second Function)As usual, we can write{m}k instead of enc(m,k). Also, we can write m1,m2 or 〈m1,m2〉 instead of pair(m1,m2) and sign(m,k-1) instead of dec(m,k-1) if k-1 is a private key.Given a set of equationsℰNSL and a set of signatures ΣNSL, the intruder capacities, denoted by the relation ⊨NSL, are defined by the following rules:
(9)(knowledge)□M⊨NSLm[m∈M],(construction)M⊨NSLm1⋯M⊨NSLmnM⊨NSLf(m1,…,mn)[f∈ΣNSL],(ℰ-equality)M⊨NSLmM⊨NSLm′[m=ℰNSLm′].The initial knowledge of principals𝒦NSL can be as follows: each principal knows his identity, the identities of other principals, his public and private key, and all the public keys of the other principals. Also, each principal can generate fresh values.The security latticeℒNSL is ℒ0=(2ℐ,⊆). The security level of a message is the set of principals that are eligible to know its value. Therefore, the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ.The typing function⌜·⌝NSL could be any partial function from ℳNSL to ℒNSL that reflects the security levels of components exchanged during the protocol. In this example, we choose this function as follows:
(10)⌜·⌝=[Na↦{A,B},Nb↦{A,B},ka-1↦{A},ka↦⊥],
where A and B could be substituted by any principal identifier.


### 3.1.3. NSL Safe Interpretation Function

We use the DEKAN function (that selects the direct encryption keys and neighbors) to analyze the NSL-protocol under the equational theoryℰNSL. More precisely, the DEKAN function is a composition of a selection function and an interpretation function, that is FNSL=INSL∘SNSL(i) The selection functionSNSL takes an atomic component α and a message m and returns keys that directly encrypt α in m with principal identities and variables that are neighbors of α in m. The notion of direct encrypting keys and neighbors are formalized using a special labeled tree representing the analyzed message m. More precisely, given a message m, we start by annotating the arcs of its corresponding tree according to schema given by Figure 3, where d is defined as follows:
(11)d={∞ifx=enc0else.This means that the distance between a node and his father is0 if it is not enc and its father is either pair or sign. If the node is enc, then the distance that separates it from its father is infinite. Finally, if the node is the encryption key of the function enc, then the distance to its father is 1. Using these distances between nodes, we consider two nodes as neighbors if the distance that separates them is equal to 0. Also, we consider a key as a direct encrypting one for α if the distance between them is equal to 1. Using these notions, SNSL(α,m) returns principal identifiers and variables in m having a distance 0 from α (neighbors) with atomic components having a distance 1 from α (direct encrypting keys). For example,
(12)SNSL(α,{β,A,{B,α,{α,Na,X}k3}k2}k1)={B,X,k2,k3}.(ii) The interpretation functionINSL interprets elements returned by SNSL as follows:
(13)INSL(∅)=⊤,INSL(S1∪S2)=INSL(S1)⊔INSL(S2),INSL({β})={{β}ifβisaprincipalidentifier,⌜β-1⌝ifβisakey,τβifβisavariable.For example, if⌜k2-1⌝={A}  and ⌜k3-1⌝={S} then,
(14)INSL({B,X,k2,k3})=τX⊔{A,B,S}.Figure 3
Safe costs assignment.Notice also that, when an equational theory is taken into consideration, a message can have different equivalent forms. In this situation, to be safe, an interpretation function should give to a message the lowest level of the messages of its class. More precisely, ifm/ℰ={m′∈ℳ∣m=ℰm'}, then, for any atomic message α, we have
(15)F(α,m)=∏m′∈m/ℰF(α,m′).To simplify the computation ofF, we usually try to transform the equational theory to a convergent inference system so that the canonical form of a message m, denoted by m↓, has always the lowest security level. In other words,
(16)F(α,m↓)⊑∏m′∈m/ℰF(α,m′).To reach this goal, we orient the equation so that the right side is greater to the left side according toF and the obtained rewriting system is convergent (the convergence can be proved based on another ordering relation that is independent of F). (Notice that if such orientation is not possible, the approach cannot be applied. However, for all the equational theories that we have already considered till now we didn't find difficulties to orient them.) For our example, it is simple to see that the following rewriting system is convergent and gives the lowest security level:
(17)fst(〈x,y〉)→x,snd(〈x,y〉)→y,dec(enc(x,k),k-1)→x,enc(dec(x,ky-1),ky)→x,〈〈m1,m2〉,m3〉→〈m1,〈m2,m3〉〉.


### 3.1.4. NSL Role-Based Specification

The NSL role-based specification is(18)ℛG(pNSL)={𝒜G1,𝒜G2,ℬG1},
where the generalized roles 𝒜G1 and 𝒜G2 are as follows:
(19)𝒜G1=i.1.A→I(B):{A,Nai}kbi.1.A→I(B):{A,Nai}kb,𝒜G2=i.2.I(B)→A:{〈Nai,X〉,B}kai.3.A→I(B):{X}kb,
and the generalized role ℬG1 is as follows:
(20)ℬG1=i.1.I(A)→B:{A,Y}kbi.2.B→I(A):{〈Y,Nbi〉,B}ka.


### 3.1.5. Verifying Whether the NSL Role-Based Specification Is Increasing

Now, we can verify whether the role-based specification of SET isFSET-increasing. More precisely, we need accordingly to verify that principals do not decrease the security level of components from step to another. To that end, we verify this condition on each generalized role of the protocol (i.e., on each point of view of protocol participants). To that end, we should verify whether the security level of sent messages is a subset of the security level of these messages in the received steps, that is,
(21)∀rFSET(α,r+)⊆⌜α⌝∪FSET(α,r-)∀α.From the generalized roles ofA, we deduce that
(22)𝒜G1-=∅,𝒜G1+={A,Nai}kb,𝒜G2-={〈Nai,X〉,B}ka,𝒜G2+={X}kb.Recall that we are working with the lattice of security(2ℐ,⊆), so the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ. Then, the security levels of sent and received messages in the generalized roles of A according to FNSL are as shown in Table 8.Table 8
Analysis of NSL: role ofA.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
a
i
𝒜
G
1
{
A
,
B
}
{
B
}
⊤
Yes
X
𝒜
G
2
τ
X
{
B
}
{
A
,
B
}
Yes
(
for  any
τ
X
∈
2
ℐ
)Table8 shows that the generalized roles 𝒜G1 and 𝒜G2 are FNSL-increasing.From the generalized roles ofB, we deduce that
(23)ℬG1-={A,Y}kb,ℬG1+={〈Y,Nbi〉,B}ka.Then, the security levels of sent and received messages in the generalized roles ofB according to FNSL are as in Table 9.Table 9
Analysis of NSL protocol: role ofB.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
b
i
ℬ
G
1
{
A
,
B
}
{
A
}
⊤
Yes
Y
ℬ
G
1
τ
Y
{
A
,
B
}
{
A
,
B
}
Yes
(
for  any
τ
Y
∈
2
ℐ
)Table9 shows that the generalized role ℬG1 is FNSL-increasing. Since all generalized roles of NSL are FNSL-increasing, then it is an FNSL-increasing protocol. Furthermore, since FNSL is 𝒞NSL-safe interpretation function, we conclude, from  our main result,  that NSL is 𝒞NSL-correct with respect to secrecy.


## 3.1.1. The NSL-Protocol

The Needham-Schroeder Lowe (NSL) protocol, denoted bypNSL and given in Table 5, is a mutual authentication protocol that uses asymmetric encryption.Table 5
Needham schroeder lowe protocol.
1.A→B:{A,Na}kb
2.B→A:{〈Na,Nb〉,B}ka
3.A→B:{Nb}kbThe first step of the analysis consists in fixing the context of verification which contains the message algebra, the intruder capabilities, and the security levels of all messages. Second, we define a safe interpretation function in this context. After that, the role-based specification can be analyzed to verify whether the protocol is increasing by using the defined safe interpretation function. The following paragraphs describe in detail these steps.


## 3.1.2. NSL Context of Verification in the Dolev-Yao Model

Let𝒞NSL=〈ℳNSL,⊨NSL𝒦NSL,ℒNSL⊒,⌜·⌝NSL〉 be a context of verification where ℳNSL is (𝒩NSL,ΣNSL,ℰNSL) such that we have the following.(i)
𝒩NSL is the set of atomic messages given by BNF grammar shown in Table 6.(ii)
ΣNSL={pair,fst,snd,enc,dec} contains the set of message operators.
Hence, the set of messages ofℳNSL is defined by BNF rules shown in Table 7.(iii)
ℰNSL is an equational theory containing the following equations:
(8)fst(pair(x,y))=x,snd(pair(x,y))=y,dec(enc(x,k),k-1)=x,enc(dec(x,ka-1),ka)=x,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉.Table 6
𝒩
NSL
::=
A
(Principal Identifier)
|
N
a
(Nounce)
|
k
a
-
1
(Private key)
|
k
a
(Public key)Table 7
m
,
m
1
,
m
2
::=
𝒩
NSL
|
p
a
i
r
(
m
1
,
m
2
)
(Pair Function)
|
e
n
c
(
m
,
k
a
)
(Encryption Function)
|
d
e
c
(
m
,
k
a
-
1
)
(Decryption Function)
|
f
s
t
(
p
a
i
r
(
m
1
,
m
2
)
)
(First Function)
|
s
n
d
(
p
a
i
r
(
m
1
,
m
2
)
)
(Second Function)As usual, we can write{m}k instead of enc(m,k). Also, we can write m1,m2 or 〈m1,m2〉 instead of pair(m1,m2) and sign(m,k-1) instead of dec(m,k-1) if k-1 is a private key.Given a set of equationsℰNSL and a set of signatures ΣNSL, the intruder capacities, denoted by the relation ⊨NSL, are defined by the following rules:
(9)(knowledge)□M⊨NSLm[m∈M],(construction)M⊨NSLm1⋯M⊨NSLmnM⊨NSLf(m1,…,mn)[f∈ΣNSL],(ℰ-equality)M⊨NSLmM⊨NSLm′[m=ℰNSLm′].The initial knowledge of principals𝒦NSL can be as follows: each principal knows his identity, the identities of other principals, his public and private key, and all the public keys of the other principals. Also, each principal can generate fresh values.The security latticeℒNSL is ℒ0=(2ℐ,⊆). The security level of a message is the set of principals that are eligible to know its value. Therefore, the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ.The typing function⌜·⌝NSL could be any partial function from ℳNSL to ℒNSL that reflects the security levels of components exchanged during the protocol. In this example, we choose this function as follows:
(10)⌜·⌝=[Na↦{A,B},Nb↦{A,B},ka-1↦{A},ka↦⊥],
where A and B could be substituted by any principal identifier.


## 3.1.3. NSL Safe Interpretation Function

We use the DEKAN function (that selects the direct encryption keys and neighbors) to analyze the NSL-protocol under the equational theoryℰNSL. More precisely, the DEKAN function is a composition of a selection function and an interpretation function, that is FNSL=INSL∘SNSL(i) The selection functionSNSL takes an atomic component α and a message m and returns keys that directly encrypt α in m with principal identities and variables that are neighbors of α in m. The notion of direct encrypting keys and neighbors are formalized using a special labeled tree representing the analyzed message m. More precisely, given a message m, we start by annotating the arcs of its corresponding tree according to schema given by Figure 3, where d is defined as follows:
(11)d={∞ifx=enc0else.This means that the distance between a node and his father is0 if it is not enc and its father is either pair or sign. If the node is enc, then the distance that separates it from its father is infinite. Finally, if the node is the encryption key of the function enc, then the distance to its father is 1. Using these distances between nodes, we consider two nodes as neighbors if the distance that separates them is equal to 0. Also, we consider a key as a direct encrypting one for α if the distance between them is equal to 1. Using these notions, SNSL(α,m) returns principal identifiers and variables in m having a distance 0 from α (neighbors) with atomic components having a distance 1 from α (direct encrypting keys). For example,
(12)SNSL(α,{β,A,{B,α,{α,Na,X}k3}k2}k1)={B,X,k2,k3}.(ii) The interpretation functionINSL interprets elements returned by SNSL as follows:
(13)INSL(∅)=⊤,INSL(S1∪S2)=INSL(S1)⊔INSL(S2),INSL({β})={{β}ifβisaprincipalidentifier,⌜β-1⌝ifβisakey,τβifβisavariable.For example, if⌜k2-1⌝={A}  and ⌜k3-1⌝={S} then,
(14)INSL({B,X,k2,k3})=τX⊔{A,B,S}.Figure 3
Safe costs assignment.Notice also that, when an equational theory is taken into consideration, a message can have different equivalent forms. In this situation, to be safe, an interpretation function should give to a message the lowest level of the messages of its class. More precisely, ifm/ℰ={m′∈ℳ∣m=ℰm'}, then, for any atomic message α, we have
(15)F(α,m)=∏m′∈m/ℰF(α,m′).To simplify the computation ofF, we usually try to transform the equational theory to a convergent inference system so that the canonical form of a message m, denoted by m↓, has always the lowest security level. In other words,
(16)F(α,m↓)⊑∏m′∈m/ℰF(α,m′).To reach this goal, we orient the equation so that the right side is greater to the left side according toF and the obtained rewriting system is convergent (the convergence can be proved based on another ordering relation that is independent of F). (Notice that if such orientation is not possible, the approach cannot be applied. However, for all the equational theories that we have already considered till now we didn't find difficulties to orient them.) For our example, it is simple to see that the following rewriting system is convergent and gives the lowest security level:
(17)fst(〈x,y〉)→x,snd(〈x,y〉)→y,dec(enc(x,k),k-1)→x,enc(dec(x,ky-1),ky)→x,〈〈m1,m2〉,m3〉→〈m1,〈m2,m3〉〉.


## 3.1.4. NSL Role-Based Specification

The NSL role-based specification is(18)ℛG(pNSL)={𝒜G1,𝒜G2,ℬG1},
where the generalized roles 𝒜G1 and 𝒜G2 are as follows:
(19)𝒜G1=i.1.A→I(B):{A,Nai}kbi.1.A→I(B):{A,Nai}kb,𝒜G2=i.2.I(B)→A:{〈Nai,X〉,B}kai.3.A→I(B):{X}kb,
and the generalized role ℬG1 is as follows:
(20)ℬG1=i.1.I(A)→B:{A,Y}kbi.2.B→I(A):{〈Y,Nbi〉,B}ka.


## 3.1.5. Verifying Whether the NSL Role-Based Specification Is Increasing

Now, we can verify whether the role-based specification of SET isFSET-increasing. More precisely, we need accordingly to verify that principals do not decrease the security level of components from step to another. To that end, we verify this condition on each generalized role of the protocol (i.e., on each point of view of protocol participants). To that end, we should verify whether the security level of sent messages is a subset of the security level of these messages in the received steps, that is,
(21)∀rFSET(α,r+)⊆⌜α⌝∪FSET(α,r-)∀α.From the generalized roles ofA, we deduce that
(22)𝒜G1-=∅,𝒜G1+={A,Nai}kb,𝒜G2-={〈Nai,X〉,B}ka,𝒜G2+={X}kb.Recall that we are working with the lattice of security(2ℐ,⊆), so the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ. Then, the security levels of sent and received messages in the generalized roles of A according to FNSL are as shown in Table 8.Table 8
Analysis of NSL: role ofA.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
a
i
𝒜
G
1
{
A
,
B
}
{
B
}
⊤
Yes
X
𝒜
G
2
τ
X
{
B
}
{
A
,
B
}
Yes
(
for  any
τ
X
∈
2
ℐ
)Table8 shows that the generalized roles 𝒜G1 and 𝒜G2 are FNSL-increasing.From the generalized roles ofB, we deduce that
(23)ℬG1-={A,Y}kb,ℬG1+={〈Y,Nbi〉,B}ka.Then, the security levels of sent and received messages in the generalized roles ofB according to FNSL are as in Table 9.Table 9
Analysis of NSL protocol: role ofB.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
b
i
ℬ
G
1
{
A
,
B
}
{
A
}
⊤
Yes
Y
ℬ
G
1
τ
Y
{
A
,
B
}
{
A
,
B
}
Yes
(
for  any
τ
Y
∈
2
ℐ
)Table9 shows that the generalized role ℬG1 is FNSL-increasing. Since all generalized roles of NSL are FNSL-increasing, then it is an FNSL-increasing protocol. Furthermore, since FNSL is 𝒞NSL-safe interpretation function, we conclude, from  our main result,  that NSL is 𝒞NSL-correct with respect to secrecy.


## 3.2. Analysis of the NSL-Protocol with the Homomorphism Property

This section presents the analysis of the Needham-Schroeder Lowe (NSL) protocol with the homomorphism property of encryption:(24)enc(g(x,y))=g′(enc(x),enc(y)),
where g and g' are any operators (usually the same) from the message algebra. For example, enc(m1·m2)=enc(m1)·enc(m2) is satisfied when using block ciphers with Electronic Code Block (ECB) and when m1 has the same size as requested by the encryption system (64 bits for DES). In fact, the ECB consists of splitting the message into blocks of n-bits and encrypting each of them separately. Many asymmetric systems like RSA, Elgamal, Benaloh, and Paillier are also homomorphic for some algebraic operators.Related works that take into consideration the homomorphism property in the analysis of cryptographic protocols are rare and most of them do not deal with an unbounded number of sessions. Among the important results obtained in this direction are those described in [40–42] which address the intruder deduction problem and propose a PTIME-decision procedure for it. Despite the importance of the result, the resolution of the intruder deduction problem is not enough to analyze a protocol that can exhibit an infinite number of sessions.The interpretation functions-based method does not suffer from this problem since it is proved that if the protocol is increasing then it is sufficient to guarantee its correctness for the secrecy property under an unbounded number of sessions. In the sequel, we show how the homomorphism property can affect the analysis of a protocol like NSL.


### 3.2.1. NSL Context of Verification with the Homomorphism Property

First, we need to change the context of verification𝒞NSL used in the previous section, so that we consider the homomorphism property. Let 𝒞NSL' be a context of verification such as 𝒞NSL'=〈(𝒩NSL,ΣNSL,ℰNSL'),⊨NSL𝒦NSL,ℒNSL⊒,⌜·⌝NSL〉 where all items are the same as those defined in the context 𝒞NSL except the equational theory ℰNSL' that includes homomorphism of encryption and it is as follows:
(25)fst(pair(x,y))=x,snd(pair(x,y))=y,dec(enc(x,k),k-1)=x,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉,enc(〈x,y〉,z)=〈enc(x,z),enc(y,z)〉.The last two equations ofℰNSL' reflect the homomorphic property of the encryption enc and the signature sign with respect to the concatenation operator 〈·〉.


### 3.2.2. NSL Safe Interpretation Function with the Homomorphism Property

We use the DEKAN function (that selects the direct encryption keys and neighbors) to analyze the Needham-Schroeder Lowe protocol under the equational theoryℰNSL'. With the homomorphism property, the DEKAN function becomes equal to the DEK function (that selects direct encryption keys). Indeed, the selection is forbidden beyond encryption and the selection is always calculated on the message m↓ (the canonical form of m according to the rewriting system obtained from the equational theory ℰNSL', when the equality is replaced by →) instead of m. For example, with the homomorphism property the message {α1,…,αn}k, where α1,…,αn are atomic, is always reduced, by the homomorphism property, to {α1}k,…,{αn}k. To calculate the security level of a component αi in the message {α1,…,αn}k, the DEKAN function is applied on its canonical form that is {α1}k,…,{αn}k. It follows that the neighbors are never chosen, and we conclude that the DEKAN function behaves as the DEK function.


### 3.2.3. Verifying Whether the NSL Role-Based Specification Is Increasing

From the generalized roles ofA, we deduce that
(26)𝒜G1-=∅,𝒜G1+={A,Nai}kb,𝒜G2-={〈Nai,X〉,B}ka,𝒜G2+={X}kb.The security levels of sent and received messages in the generalized roles ofA using the DEKAN function FNSL are as shown in Table 10.Table 10
Analysis of NSL protocol: role ofA.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
a
i
𝒜
G
1
{
A
,
B
}
{
B
}
⊤
Yes
X
𝒜
G
2
τ
X
{
B
}
{
A
}
NoTable10 shows that the generalized role 𝒜G2 is not increasing. Indeed, the message X is sent with the security level {B} which is not always in its security level ⌜X⌝∪{A} estimated from the received messages. In this case, we can never find a safe interpretation function that guarantees the correctness of the protocol simply because the protocol is flawed and it could be attacked as shown by Table 11. Notice that message of step 1.2 could be generated by the intruder from the message 2.2 using the homomorphic property. In fact, {Na1,Nb2,B}ka={Na1,Nb2}ka,{B}ka and since the intruder can produce {I}ka, then using the homomorphic property he can produce {Na1,Nb2,I}ka by simply concatenating {Na1,Nb2}ka with {I}ka.Table 11
Flaw in the NSL-protocol under the homomorphic assumption.
1.1.A→I:{A,Na1}ki
2.1. I(A)→B:{A,Na1}kb
2.2. B→I(A):{Na1,Nb2,B}ka
1.2.I→A:{Na1,Nb2,I}ka
1.3.A→I:{Nb2}ki
2.3. I(A)→B:{Nb2}kbThis is because the DEKAN function (that selects direct encryption keys and neighbors) with the homomorphism property acts as the DEK function (that selects the direct encryption keys only) and does not select the neighbors. Therefore, to correct this protocol in the presence of such property, we should find a means (different from the concatenation, such as signatures), allowingA to conclude that Nb is from B. To overcome this problem, we suggest the use of signatures to indicate the correct security level of sent messages. For instance, we can replace the message {A,Na}kb at step 1 of the NSL-protocol with the message {{Na}ka-1}kb. In this case, signing the message Na by ka-1 is a safe way to indicate that it comes from the agent A. In the same way, we can replace the message of step 2 of the NSL-protocol by the message {{〈Na,Nb〉}kb-1}ka. Notice that if signature is also homomorphic like encryption, operators like hash functions can be used to forge such type of inseparable links between some elements.From the generalized roles ofB, we deduce that
(27)ℬG1-={A,Y}kb,ℬG1+={〈Y,Nbi〉,B}ka.
Then, the security level of sent and received messages in the generalized roles of B using the DEKAN function FNSL is as shown in Table 12.Table 12
Analysis of NSL protocol: role ofB.
α
r
⌜
α
⌝
0
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
?
⌜
α
⌝
0
∪
F
NSL
(
α
,
r
-
)
N
b
i
ℬ
G
1
{
A
,
B
}
{
A
}
⊤
Yes
Y
ℬ
G
1
⊤
{
A
}
{
B
}
NoTable12 shows that the generalized role ℬG1 is not increasing. Indeed, the message Y is sent with the security level {A} which is not in its security level {B} estimated from the received messages. As for the role of A, we suggest to replace the message {A,Na}kb of step 1 of the NSL-protocol with the message {{Na}ka-1}kb. In this case, signing the message Na by ka-1 is a safe way to indicate that it comes from the agent A. In the same way, we can replace the message of step 2 of the NSL-protocol with the message {{〈Na,Nb〉}kb-1}ka.Therefore, the NSL-protocol is not increasing and, so, we cannot deduce anything about its correctness for the secrecy property. However, the protocol, with the changes suggested above, is increasing and it is therefore correct for the secrecy property even in the presence of the homomorphism property. Table13 summarizes these changes.Table 13
Needham schroeder lowe protocol: corrected version.
1.A→B:{{Na}ka-1}kb
2.B→A:{{〈Na,Nb〉}kb-1}ka
3.A→B:{Nb}kbBy using the DEK function or the DEKAN function, this new version of the Needham-Schroeder-Lowe protocol is increasing and then respects the secrecy property. Indeed, with this versionNa is received with the security level {A,B} and so it could be sent to A. Also, Nb is received with security level {A,B} and so it could be sent to B.


## 3.2.1. NSL Context of Verification with the Homomorphism Property

First, we need to change the context of verification𝒞NSL used in the previous section, so that we consider the homomorphism property. Let 𝒞NSL' be a context of verification such as 𝒞NSL'=〈(𝒩NSL,ΣNSL,ℰNSL'),⊨NSL𝒦NSL,ℒNSL⊒,⌜·⌝NSL〉 where all items are the same as those defined in the context 𝒞NSL except the equational theory ℰNSL' that includes homomorphism of encryption and it is as follows:
(25)fst(pair(x,y))=x,snd(pair(x,y))=y,dec(enc(x,k),k-1)=x,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉,enc(〈x,y〉,z)=〈enc(x,z),enc(y,z)〉.The last two equations ofℰNSL' reflect the homomorphic property of the encryption enc and the signature sign with respect to the concatenation operator 〈·〉.


## 3.2.2. NSL Safe Interpretation Function with the Homomorphism Property

We use the DEKAN function (that selects the direct encryption keys and neighbors) to analyze the Needham-Schroeder Lowe protocol under the equational theoryℰNSL'. With the homomorphism property, the DEKAN function becomes equal to the DEK function (that selects direct encryption keys). Indeed, the selection is forbidden beyond encryption and the selection is always calculated on the message m↓ (the canonical form of m according to the rewriting system obtained from the equational theory ℰNSL', when the equality is replaced by →) instead of m. For example, with the homomorphism property the message {α1,…,αn}k, where α1,…,αn are atomic, is always reduced, by the homomorphism property, to {α1}k,…,{αn}k. To calculate the security level of a component αi in the message {α1,…,αn}k, the DEKAN function is applied on its canonical form that is {α1}k,…,{αn}k. It follows that the neighbors are never chosen, and we conclude that the DEKAN function behaves as the DEK function.


## 3.2.3. Verifying Whether the NSL Role-Based Specification Is Increasing

From the generalized roles ofA, we deduce that
(26)𝒜G1-=∅,𝒜G1+={A,Nai}kb,𝒜G2-={〈Nai,X〉,B}ka,𝒜G2+={X}kb.The security levels of sent and received messages in the generalized roles ofA using the DEKAN function FNSL are as shown in Table 10.Table 10
Analysis of NSL protocol: role ofA.
α
r
⌜
α
⌝
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
NSL
(
α
,
r
-
)
N
a
i
𝒜
G
1
{
A
,
B
}
{
B
}
⊤
Yes
X
𝒜
G
2
τ
X
{
B
}
{
A
}
NoTable10 shows that the generalized role 𝒜G2 is not increasing. Indeed, the message X is sent with the security level {B} which is not always in its security level ⌜X⌝∪{A} estimated from the received messages. In this case, we can never find a safe interpretation function that guarantees the correctness of the protocol simply because the protocol is flawed and it could be attacked as shown by Table 11. Notice that message of step 1.2 could be generated by the intruder from the message 2.2 using the homomorphic property. In fact, {Na1,Nb2,B}ka={Na1,Nb2}ka,{B}ka and since the intruder can produce {I}ka, then using the homomorphic property he can produce {Na1,Nb2,I}ka by simply concatenating {Na1,Nb2}ka with {I}ka.Table 11
Flaw in the NSL-protocol under the homomorphic assumption.
1.1.A→I:{A,Na1}ki
2.1. I(A)→B:{A,Na1}kb
2.2. B→I(A):{Na1,Nb2,B}ka
1.2.I→A:{Na1,Nb2,I}ka
1.3.A→I:{Nb2}ki
2.3. I(A)→B:{Nb2}kbThis is because the DEKAN function (that selects direct encryption keys and neighbors) with the homomorphism property acts as the DEK function (that selects the direct encryption keys only) and does not select the neighbors. Therefore, to correct this protocol in the presence of such property, we should find a means (different from the concatenation, such as signatures), allowingA to conclude that Nb is from B. To overcome this problem, we suggest the use of signatures to indicate the correct security level of sent messages. For instance, we can replace the message {A,Na}kb at step 1 of the NSL-protocol with the message {{Na}ka-1}kb. In this case, signing the message Na by ka-1 is a safe way to indicate that it comes from the agent A. In the same way, we can replace the message of step 2 of the NSL-protocol by the message {{〈Na,Nb〉}kb-1}ka. Notice that if signature is also homomorphic like encryption, operators like hash functions can be used to forge such type of inseparable links between some elements.From the generalized roles ofB, we deduce that
(27)ℬG1-={A,Y}kb,ℬG1+={〈Y,Nbi〉,B}ka.
Then, the security level of sent and received messages in the generalized roles of B using the DEKAN function FNSL is as shown in Table 12.Table 12
Analysis of NSL protocol: role ofB.
α
r
⌜
α
⌝
0
F
NSL
(
α
,
r
+
)
F
NSL
(
α
,
r
-
)
F
NSL
(
α
,
r
+
)
⊆
?
⌜
α
⌝
0
∪
F
NSL
(
α
,
r
-
)
N
b
i
ℬ
G
1
{
A
,
B
}
{
A
}
⊤
Yes
Y
ℬ
G
1
⊤
{
A
}
{
B
}
NoTable12 shows that the generalized role ℬG1 is not increasing. Indeed, the message Y is sent with the security level {A} which is not in its security level {B} estimated from the received messages. As for the role of A, we suggest to replace the message {A,Na}kb of step 1 of the NSL-protocol with the message {{Na}ka-1}kb. In this case, signing the message Na by ka-1 is a safe way to indicate that it comes from the agent A. In the same way, we can replace the message of step 2 of the NSL-protocol with the message {{〈Na,Nb〉}kb-1}ka.Therefore, the NSL-protocol is not increasing and, so, we cannot deduce anything about its correctness for the secrecy property. However, the protocol, with the changes suggested above, is increasing and it is therefore correct for the secrecy property even in the presence of the homomorphism property. Table13 summarizes these changes.Table 13
Needham schroeder lowe protocol: corrected version.
1.A→B:{{Na}ka-1}kb
2.B→A:{{〈Na,Nb〉}kb-1}ka
3.A→B:{Nb}kbBy using the DEK function or the DEKAN function, this new version of the Needham-Schroeder-Lowe protocol is increasing and then respects the secrecy property. Indeed, with this versionNa is received with the security level {A,B} and so it could be sent to A. Also, Nb is received with security level {A,B} and so it could be sent to B.


## 4. Analysis of the SET Protocol

Electronic commerce, commonly denoted by e-commerce, or eCommerce, consists in buying and selling goods or services over the Internet. To make a purchase, a customer usually submits his credit card number to a merchant protected according to a specific cryptographic protocol such as SET and SSL.Many researchers have addressed the problem of analyzing the SET protocol during the last years. For example, Paulson et al. tried in [43, 44] to prove some security properties (authentication and repudiation properties) during the purchase phase as well as during the cardholder registration one by using the inductive approach and the theorem prover “Isabelle.’’ However, the analysis was very difficult and could not be achieved because of the complexity of the exchanged messages and the complexity of targeted properties. However, they discovered some flaws related to repudiation and authentication properties. In [45], the authors present some weaknesses in the purchase phase of the SET protocol and propose their correct version. The weaknesses concern the repudiation property. However, no results concerning the secrecy property have been given till now. In the following, we show the efficiency of the interpretation function-based method when analyzing such difficult protocol and how it could be used to give a correct version of this protocol.The SET protocol [27–29] has been proposed by a consortium of credit card and software companies. It aims to protect sensitive cardholder information, to ensure payment integrity, and confidentiality, and to authenticate merchants and cardholders. It contains five subprotocols: cardholder registration; merchant and payment gateway registration; purchase request; payment authorization and transaction payment. We focus here on the analysis of the purchase phase which involves three parties: the cardholder (C); the merchant (M) and a payment gateway (G). The formal description of the purchase phase of SET, denoted in the sequel by pSET, is defined by Table 14.Table 14
SET protocol.
1.C→M:C,Nc
2.M→C:{M,C,XID,Nc,NM,CA(G)}kM-1
3.C→M:OI,DualSign,{PI}kG
4.M→G:{{AuthReqData,LinkOIPI}kM-1}kG,DualSign,{PI}kG
5.G→M:{{M,C,XID,AuthRRTags,PurchAmt,
AuthCode}kG-1}kM
6.M→C:{M,C,XID,NC,AuthCode}kM-1TheOI, PI, DualSign, and LinkOIPI are as follows:
(28)OI:=OIData,H(PIData),OIData:=M,C,XID,NM,NC,HOD,HOD:=H(OrderDesc,PurchAmt),PIData:=PIHead,PANData,PIHead≔M,C,XID,HOD,PurchAmt,MerID,H(XID,CardSecret),PANData:=PAN,PANSecret,PI:=PIHead,H(OIData),PANData,DualSign:={H(PIData),H(OIData)}kc-1,LinkOIPI:=H(AuthReqData,DualSign,{PI}KG),AuthReqData≔H(OIData),HOD,M,C,XID,AuthRRTags.P
A
N is the cardholder's primary account number, and PANSecret is a secret number known by the cardholder and used to prove his identity when making purchases. The OrderDesc is the description of the customer's detailed order and PurchAmt is the total amount of the purchase order. The intuitive meaning of each step is as follows.  (i)
Initialization request (step 1): before starting the purchase, the cardholder and the merchant agree upon the order description and its price. This shopping step is out of the SET protocol. The cardholder then sends to the merchant his local ID (C) and a fresh random challenge Nc.(ii)
Initialization response (step 2): The merchantM generates a transaction ID (XID) and sends it to the costumer with the gateway's public encryption key certificate (CA(G)).(iii)
Order request (step 3): after validating the signature of the merchant and the certificates of the gateway, the cardholder sends an order request which contains the payment instruction (PI), the order information (OI), and the dual signature (DualSign) to the merchant.(iv)
Authorization request (step 4): the message sent during this step containsPI and DualSign sent by the cardholder, the hash codes H(OIData) and HOD. This information enables the gateway to verify the dual signature, the different IDs involved in the transaction, and the authorization request/response tags (authRRTags) that should be returned in the authorization response. The purpose of AuthRRTags is to match the request/response paired messages; it contains the merchant's financial ID and some optional data that are used by the merchant's bank to authorize the transaction.(v)
Authorization response (step 5): if bothPI and OI agree, the gateway proceeds to the transaction authorization using the existing financial networks. If the authorization is allowed, the gateway sends the authorization response containing authRRTags copied from step 4, the purchase amount, and the transaction status (a boolean value).(vi)
Purchase response (step 6): the merchant verifies the gateway's signature and whether the IDs and theauthRRTags in the response match with those sent in his request message. Then, he forwards to the cardholder the authorization status combined with IDs and challenges involved in the transaction.In the following, we focus on verifying the secrecy property of this protocol by using the interpretation functions-based method. To that end, we follow the steps described by Figure2. First, we define the context of verification and a safe interpretation function for it. After that, the role-based specification is generated to verify whether this protocol is increasing.


### 4.1. SET Context of Verification in the Dolev-Yao Model

Let𝒞SET=〈(𝒩SET,ΣSET),F0,𝒦SET,ℒSET⊒,⌜·⌝SET〉 be a context of verification where 𝒩SET is the set of atomic messages given by BNF grammar shown in Table 15 and ΣSET={enc,dec,pair,fst,snd,hash}.Table 15
n
::=
A
(Principal Identifier)
|
N
a
(Nounce)
|
k
a
-
1
(Private key)
|
k
a
(Public key)As usual, we write{m}k instead of enc(m,k) or sign(m,k). Also, we write m1,m2 instead of pair(m1,m2), H(m) instead of hash(m) and sign(m,k-1) instead of dec(m,k-1) if k-1 is a private key. Hence, the set of messages ℳSET is the set of messages that respect BNF rules shown in Table 16.Table 16
m
,
m
1
,
m
2
::=
n
|
e
n
c
(
m
,
k
a
)
(Encryption Function)
|
d
e
c
(
m
,
k
a
-
1
)
(Signature Function)
|
p
a
i
r
(
m
1
,
m
2
)
(Pair Function)
|
f
s
t
(
p
a
i
r
(
m
1
,
m
2
)
)
(First Function)
|
s
n
d
(
p
a
i
r
(
m
1
,
m
2
)
)
(Second Function)
|
H
(
m
)
(Hash Function)LetℰSET be the equational theory containing the following equations:
(29)fst(〈x,y〉)=x,snd(〈x,y〉)=y,dec(enc(x,k),k-1)=x,enc(dec(x,k-1),k)=x,check(sign(m,ka-1),ka)=ok,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉.The intruder model⊨SET is the famous Dolev-Yao model for asymmetric key given as follows:
(30)(knowledge)□M⊨SETm[m∈M],(construction)M⊨SETm1⋯M⊨SETmnM⊨SETf(m1,…,mn)[f∈ΣSET],(ℰ-equality)M⊨SETmM⊨SETm′[m=ℰSETm′].The initial knowledge of principals𝒦SET is as follows. Each principal knows his identity, the identities of other principals, his public and private key, all the public keys of the other principals and his card numbers (its PAN and its PANSecret). Also, each principal can generate fresh values.The security latticeℒSET is the same as the one defined in the   NSL-example, that is, ℒSET=ℒ0=(2ℐ,⊆). The security level of a message is simply the set of principals that are eligible to know its value. Therefore, the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ.The typing relation⌜·⌝SET (or shortly denoted by ⌜·⌝ if there is no confusion) is a partial function from ℳSET to ℒSET defined as follows:
(31)[Nc↦⊥,PurchAmt↦⊥,MerID↦⊥,CardSecret↦{C,G},PANSecret↦{C,G},PAN↦{C,G},XID↦⊥,NM↦⊥,CA(G)↦⊥,AuthRRTags↦{M,G},AuthCode↦⊥].


### 4.2. SET Safe Interpretation Function in the Dolev-Yao Model

We use an extended version of the DEKAN function to deal with hash functions. To that end, we follow the guideline defined in Section2.2. In fact, the guideline states that we have to consider the interpretation function as a composition of a selection and rank function (i.e., FSET=ISET∘SSET). In this example, we consider the selection function SSET that allows to select principal identifiers that are at distance 0 (neighbors) and component at distance 1 (encryption keys). A hashed message is considered in this example as a black box for the selection function. This means that selection function could not select components from a hashed message and this done by making the hashed components at distance strictly greater than 1 (the maximum distance that the selection function can reach to select components). Also, to have a safe function, we forbid the selection of components that are beyond an encryption operator. To that end, we set distances so that any two components separated by an encryption are at distance equal to ∞. More precisely, the selection function SSET could be defined by considering the costs between nodes in messages as described by Figure 4, where d is as follows:
(32)d={∞ifx∈{enc,hash}0else.Figure 4
Safe costs assignment.The DEKAN functionFSET, used to analyze the SET protocol, could be built by composing the selection function and the rank function as follows:
(33)FSET=ISET∘SSET,
where ISET gives the rank{A} to any principal identity A that is selected as a neighbor and the rank  ⌜k-1⌝ to the keys k which are selected as direct keys of encryption.


### 4.3. SET Roles-Based Specification

For more details about how we compute a roles-based specification from a protocol and a context of verification, we refer the reader to Section2.6.1. Following the steps described in Section 2.6.1, the SET roles-based specification is
(34)ℛG(pSET)={𝒞G1,𝒞G2,𝒞G3,ℳG1,ℳG2,ℳG3,𝒢G1},
where 𝒞G1, 𝒞G2, and 𝒞G3 (the generalized roles of C) are as follows:
(35)𝒞G1=i.1.C→I(M):C,Nci,𝒞G2={i.1.C→I(M):C,Nci,i.2.I(M)→C:{M,C,X1,Nci,X2,CA(G)}kM-1,i.3.C→I(M):IOGC,DualSignGC,{PIGC}kG,𝒞G3={i.1.C→I(M):C,Nci,i.2.I(M)→C:{M,C,X1,Nci,X2,CA(G)}kM-1,i.3.C→I(M):IOGC,DualSignGC,{PIGC}kG,i.6.I(M)→C:{M,C,X1,NCi,X3}kM-1.TheOIGC, DualSignGC, and PIGC are, respectively, OI, DualSign, and PI in which XID, NM and Nc are, respectively, replaced by X1, X2, and Nci. The generalized roles of M (ℳG1, ℳG2, and ℳG3) are as follows:
(36)ℳG1={i.1.I(C)→M:C,Y1,i.2.M→I(C):{M,C,XIDi,Y1,NMi,CA(G)}kM-1,ℳG2={i.1.I(C)→M:C,Y1,i.2.M→I(C):{M,C,XIDi,Y1,NMi,CA(G)}kM-1,i.3.I(C)→M:OIDataGM,Y7,DualSignGM,Y8,i.4.M→I(G):{{AuthReqData,LinkOIPI}kM-1}kG,DualSignGM,Y8,ℳG3={i.1.I(C)→M:C,Y1,i.2.M→I(C):{M,C,XIDi,Y1,NMi,CA(G)}kM-1,i.3.I(C)→M:OIDataGM,Y7,DualSignGM,Y8,i.4.M→I(G):{{AuthReqDataGM,LinkOIPIGM}kM-1}kG,DualSignGM,Y8,i.5.I(G)→M:{{M,C,XIDi,authRRTags,Y3,Y9}kG-1}kM,i.6.M→I(C):{M,C,XIDi,Y1,Y9}kM-1.TheOIDataGM, DualSignGM, AuthReqDataGM and LinkOIPIGM are as follows:
(37)OIDataGM≔M,C,XIDi,NMi,Y1,Y2,DualSignGM≔{Y7,H(OIDataGM)}kc-1,LinkOIPIGM:=H(AuthReqData,DualSignGM,Y8),AuthReqDataGM≔H(OIDataGM),Y2,M,C,XIDi,AuthRRTags.The generalized role ofG (𝒢G1) is as follows:
(38)𝒢G1={i.4.I(M)→G:{{AuthReqDataGG,LinkOIPIGG}kM-1}kG,DualSignGG,{PIGG}kG,i.5.G→I(M):{{M,C,Z1,Z11,Z6,AuthCode}kG-1}kM.ThePIGG, DualSignGG, AuthReqDataGG, and LinkOIPIGG are as follows:
(39)PIDataGG≔PIHeadGG,PANDataGGPIHeadGG≔M,C,Z1,Z4,Z6,MerID,Z8PANDataGG≔Z9,Z10PIGG≔PIHeadGG,Z12,PANDataGGDualSignGG≔{H(PIDataGG),Z12}kc-1LinkOIPIGG≔H(AuthReqDataGG,DualSignGG,{PI}KG)AuthReqDataGG:=Z12,Z4,M,C,Z1,Z11.


### 4.4. Verifying Whether the SET Role-Based Specification is Increasing

Now, we can verify whether the role-based specification of SET isFSET-increasing. More precisely, we need accordingly to verify that principals do not decrease the security level of components from step to another. To that end, we verify this condition on the each generalized role of the protocol (i.e., on each point of view of protocol participants). To that end, we should verify whether the security level of sent messages is a subset of the security level of these messages in the receieved steps that is,
(40)∀r·FSET(α,r+)⊆⌜α⌝∪FSET(α,r-).(i) Let us start with the generalized roles ofC. According to the definition of r+ and r-, we have
(41)𝒞G1-=∅,𝒞G1+=C,Nci,𝒞G2-={M,C,X1,Nci,X2,CA(G)}kM-1,𝒞G2+=IOGC,DualSignGC,{PIGC}kG.From the definition ofFSET and 𝒞G2+, it follows that, for all atomic message α, we have that
(42)FSET(α,𝒞G2+)=FSET(α,IODataGC,{PIHead,PANData}kG).Now, the security levels of sent and received messages in the generalized roles ofC using the FSET function are as shown in Table 17.Table 17
SET analysis: role ofC.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
N
c
i
𝒞
G
1
⊥
⊥
⊤
Yes
N
c
i
𝒞
G
2
⊥
⊥
⊤
Yes
X
1
𝒞
G
2
τ
X
1
⊥
⊥
Yes
X
2
𝒞
G
2
τ
X
2
⊥
⊥
Yes
PurchAmt
𝒞
G
2
⊥
{
C
,
G
}
∪
τ
X
1
⊤
Yes
MerID
𝒞
G
2
⊥
⊥
⊤
Yes
CardSecret
𝒞
G
2
{
C
,
G
}
{
C
,
M
,
G
}
∪
τ
X
1
⊤
No
PAN
𝒞
G
2
{
C
,
G
}
{
C
,
M
,
G
}
∪
τ
X
1
⊤
No
PANSecret
𝒞
G
2
{
C
,
G
}
{
C
,
M
,
G
}
∪
τ
X
1
⊤
NoFrom the analysis of the role ofC shown in Table 17, we deduce that its generalized roles are not increasing. This is due to the fact that an unknown message X1 is put beside the secret components CardSecret, PAN, and PANSecret and this lowers their security level. Moreover, putting the identity M beside CardSecret, PAN, and PANSecret means that these messages could be known by M according to our interpretation function. Therefore, if X1 (XID in the description of the protocol step 3) and M are hashed in PIHead, then this role can be proved increasing. More precisely, we redefine PIHead as follows:
(43)PIHead=C,HOD,PurchAmt,MerID,H(M,XID),H(CardSecret).(ii) From the generalized roles ofM, we deduce that
(44)ℳG1-=C,Y1,ℳG1+={M,C,XIDi,Y1,NMi,CA(G)}kM-1,ℳG2-=ℳG1-∪{OIDataGM,Y7,DualSignGM,Y8},ℳG2+={{AuthReqData,LinkOIPI}kM-1}kG,DualSignGM,Y8,ℳG3-=ℳG2-∪{{{M,C,XIDi,AuthRRTags,Y3,Y9}kG-1}kM},ℳG3+={M,C,XIDi,Y1,Y9}kM-1.The security levels of sent and received messages in the generalized roles of M using the DEKAN function are as shown in (Table 18).Table 18
SET analysis: role ofM.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
Y
1
ℳ
G
1
τ
Y
1
⊥
⊥
Yes
X
I
D
i
ℳ
G
1
⊥
⊥
⊤
Yes
N
M
i
ℳ
G
1
⊥
⊥
⊤
Yes
C
A
(
G
)
ℳ
G
1
⊥
⊥
⊤
Yes
Y
2
ℳ
G
2
τ
Y
2
⊥
⊥
Yes
X
I
D
i
ℳ
G
2
⊥
⊥
⊥
Yes
AuthRRTags
ℳ
G
2
{
M
,
G
}
⊥
⊤
NoFrom Table19, we can deduce that the generalized roles of M are not increasing. This is because the message AuthRRTags is sent at step 4 of the generalized role ℳG2, with the security level {C,M,G}, which is not greater than its real security level ({M,G}). This is since the identity C is beside AuthRRTags and that means that this message is for C which also lowers the security level of AuthRRTags. One way to make this role increasing is as follows. We remove (or put it beyond the encryption) the identity C from the message AuthReqData of step 4 of the generalized role. More precisely, we redefine AuthReqData as follows:
(45)AuthReqData=H(OIData),HOD,M,XID,AuthRRTags.(iii) From the generalized roles ofG, we deduce that
(46)𝒢G1-={{AuthReqDataGG,LinkOIPIGG}kM-1}kG,DualSignGG,{PIGG}kG𝒢G1+={{M,C,Z1,Z11,Z6,AuthCode}kG-1}kM.Table 19
SET analysis: role ofM.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
Y
8
ℳ
G
2
τ
Y
8
⊥
⊥
Yes
X
I
D
i
ℳ
G
3
⊥
{
M
,
C
,
G
}
∪
τ
Y
2
{
M
,
C
,
Y
3
}
∪
τ
Y
9
Yes
Y
1
ℳ
G
3
τ
Y
1
⊥
⊥
Yes
Y
9
ℳ
G
3
τ
Y
9
⊥
⊥
YesThen, the security levels of sent and received messages in the generalized roles ofM using the DEKAN function are as in Table 20.Table 20
SET analysis: role ofG WLMV:prot.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
Z
1
𝒢
G
1
τ
Z
1
{
M
,
C
,
G
}
∪
τ
Z
6
∪
τ
Z
11
{
M
,
C
,
G
,
τ
Z
4
}
∪
τ
Z
6
∪
τ
Z
8
∪
τ
Z
11
∪
τ
Z
12
Yes
Z
6
𝒢
G
1
τ
Z
6
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
11
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
4
∪
τ
Z
8
∪
τ
Z
11
∪
τ
Z
12
Yes
Z
11
𝒢
G
1
τ
Z
11
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
6
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
4
∪
τ
Z
12
No
AuthCode
𝒢
G
1
⊥
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
4
∪
τ
Z
6
⊤
YesFrom Table20, we can deduce that the generalized roles of G are not increasing. This is since the messages Z11 (AuthRRTags) and Z6 (PurchAmt) are neighbors in step five while it is not the case in the step four. So, to make this role increasing we should put  Z6 (PurchAmt) beyond the encryption that contains AuthRRTags in step five. For instance, we replace the message of step five as follows:
(47)5.G→M:{{M,C,XID,AuthRRTags,AuthCode}kG-1}kM,{{M,C,XID,PurchAmt,AuthCode}kG-1}kM.To sum up, we propose hereafter a secure version of the SET protocol for the secrecy property. It replaces the message of step5 by message 5' in Table 21.Table 21
A Secure version of the SET protocol.
1.C→M:C,Nc
2.M→C:{M,C,XID,Nc,NM,CA(G)}kM-1
3.C→M:OI,DualSign,{PI}kG
4.M→G:{{AuthReqData,LinkOIPI}kM-1}kG,DualSign,
{PI}kG
5.G→M:{{M,C,XID,AuthRRTags,PurchAmt,
AuthCode}kG-1}kM
5
′. G→M:{{M,XID,AuthRRTags,AuthCode}kG-1}kM,
{{M,C,XID,PurchAmt,AuthCode}kG-1}kM
6.M→C:{M,C,XID,NC,AuthCode}kM-1Also, theOI, PI, DualSign, and LinkOIPI messages are as follows:
(48)OI≔OIData,H(PIData),OIData≔M,C,XID,NM,NC,HOD,HOD≔H(OrderDesc,PurchAmt),PIData≔PIHead,PANData,PIHead(oldversion)≔C,HOD,PurchAmt,MerID,M,XID,H(XID,CardSecret),PIHead≔C,HOD,PurchAmt,MerID,H(M,XID),H(CardSecret),PANData≔PAN,PANSecret,PI≔PIHead,H(OIData),PANData,DualSign≔{H(PIData),H(OIData)}kC-1,LinkOIPI≔H(AuthReqData,DualSign,{PI}KG),AuthReqData≔H(OIData),HOD,M,C,XID,AuthRRTags.
Such modifications allow to prove, by using the DEKAN function, that the new version is increasing and therefore respects the secrecy property.


## 4.1. SET Context of Verification in the Dolev-Yao Model

Let𝒞SET=〈(𝒩SET,ΣSET),F0,𝒦SET,ℒSET⊒,⌜·⌝SET〉 be a context of verification where 𝒩SET is the set of atomic messages given by BNF grammar shown in Table 15 and ΣSET={enc,dec,pair,fst,snd,hash}.Table 15
n
::=
A
(Principal Identifier)
|
N
a
(Nounce)
|
k
a
-
1
(Private key)
|
k
a
(Public key)As usual, we write{m}k instead of enc(m,k) or sign(m,k). Also, we write m1,m2 instead of pair(m1,m2), H(m) instead of hash(m) and sign(m,k-1) instead of dec(m,k-1) if k-1 is a private key. Hence, the set of messages ℳSET is the set of messages that respect BNF rules shown in Table 16.Table 16
m
,
m
1
,
m
2
::=
n
|
e
n
c
(
m
,
k
a
)
(Encryption Function)
|
d
e
c
(
m
,
k
a
-
1
)
(Signature Function)
|
p
a
i
r
(
m
1
,
m
2
)
(Pair Function)
|
f
s
t
(
p
a
i
r
(
m
1
,
m
2
)
)
(First Function)
|
s
n
d
(
p
a
i
r
(
m
1
,
m
2
)
)
(Second Function)
|
H
(
m
)
(Hash Function)LetℰSET be the equational theory containing the following equations:
(29)fst(〈x,y〉)=x,snd(〈x,y〉)=y,dec(enc(x,k),k-1)=x,enc(dec(x,k-1),k)=x,check(sign(m,ka-1),ka)=ok,〈〈m1,m2〉,m3〉=〈m1,〈m2,m3〉〉.The intruder model⊨SET is the famous Dolev-Yao model for asymmetric key given as follows:
(30)(knowledge)□M⊨SETm[m∈M],(construction)M⊨SETm1⋯M⊨SETmnM⊨SETf(m1,…,mn)[f∈ΣSET],(ℰ-equality)M⊨SETmM⊨SETm′[m=ℰSETm′].The initial knowledge of principals𝒦SET is as follows. Each principal knows his identity, the identities of other principals, his public and private key, all the public keys of the other principals and his card numbers (its PAN and its PANSecret). Also, each principal can generate fresh values.The security latticeℒSET is the same as the one defined in the   NSL-example, that is, ℒSET=ℒ0=(2ℐ,⊆). The security level of a message is simply the set of principals that are eligible to know its value. Therefore, the supremum of this lattice ⊤ is equal to ∅ and the infimum ⊥ is equal to ℐ.The typing relation⌜·⌝SET (or shortly denoted by ⌜·⌝ if there is no confusion) is a partial function from ℳSET to ℒSET defined as follows:
(31)[Nc↦⊥,PurchAmt↦⊥,MerID↦⊥,CardSecret↦{C,G},PANSecret↦{C,G},PAN↦{C,G},XID↦⊥,NM↦⊥,CA(G)↦⊥,AuthRRTags↦{M,G},AuthCode↦⊥].


## 4.2. SET Safe Interpretation Function in the Dolev-Yao Model

We use an extended version of the DEKAN function to deal with hash functions. To that end, we follow the guideline defined in Section2.2. In fact, the guideline states that we have to consider the interpretation function as a composition of a selection and rank function (i.e., FSET=ISET∘SSET). In this example, we consider the selection function SSET that allows to select principal identifiers that are at distance 0 (neighbors) and component at distance 1 (encryption keys). A hashed message is considered in this example as a black box for the selection function. This means that selection function could not select components from a hashed message and this done by making the hashed components at distance strictly greater than 1 (the maximum distance that the selection function can reach to select components). Also, to have a safe function, we forbid the selection of components that are beyond an encryption operator. To that end, we set distances so that any two components separated by an encryption are at distance equal to ∞. More precisely, the selection function SSET could be defined by considering the costs between nodes in messages as described by Figure 4, where d is as follows:
(32)d={∞ifx∈{enc,hash}0else.Figure 4
Safe costs assignment.The DEKAN functionFSET, used to analyze the SET protocol, could be built by composing the selection function and the rank function as follows:
(33)FSET=ISET∘SSET,
where ISET gives the rank{A} to any principal identity A that is selected as a neighbor and the rank  ⌜k-1⌝ to the keys k which are selected as direct keys of encryption.


## 4.3. SET Roles-Based Specification

For more details about how we compute a roles-based specification from a protocol and a context of verification, we refer the reader to Section2.6.1. Following the steps described in Section 2.6.1, the SET roles-based specification is
(34)ℛG(pSET)={𝒞G1,𝒞G2,𝒞G3,ℳG1,ℳG2,ℳG3,𝒢G1},
where 𝒞G1, 𝒞G2, and 𝒞G3 (the generalized roles of C) are as follows:
(35)𝒞G1=i.1.C→I(M):C,Nci,𝒞G2={i.1.C→I(M):C,Nci,i.2.I(M)→C:{M,C,X1,Nci,X2,CA(G)}kM-1,i.3.C→I(M):IOGC,DualSignGC,{PIGC}kG,𝒞G3={i.1.C→I(M):C,Nci,i.2.I(M)→C:{M,C,X1,Nci,X2,CA(G)}kM-1,i.3.C→I(M):IOGC,DualSignGC,{PIGC}kG,i.6.I(M)→C:{M,C,X1,NCi,X3}kM-1.TheOIGC, DualSignGC, and PIGC are, respectively, OI, DualSign, and PI in which XID, NM and Nc are, respectively, replaced by X1, X2, and Nci. The generalized roles of M (ℳG1, ℳG2, and ℳG3) are as follows:
(36)ℳG1={i.1.I(C)→M:C,Y1,i.2.M→I(C):{M,C,XIDi,Y1,NMi,CA(G)}kM-1,ℳG2={i.1.I(C)→M:C,Y1,i.2.M→I(C):{M,C,XIDi,Y1,NMi,CA(G)}kM-1,i.3.I(C)→M:OIDataGM,Y7,DualSignGM,Y8,i.4.M→I(G):{{AuthReqData,LinkOIPI}kM-1}kG,DualSignGM,Y8,ℳG3={i.1.I(C)→M:C,Y1,i.2.M→I(C):{M,C,XIDi,Y1,NMi,CA(G)}kM-1,i.3.I(C)→M:OIDataGM,Y7,DualSignGM,Y8,i.4.M→I(G):{{AuthReqDataGM,LinkOIPIGM}kM-1}kG,DualSignGM,Y8,i.5.I(G)→M:{{M,C,XIDi,authRRTags,Y3,Y9}kG-1}kM,i.6.M→I(C):{M,C,XIDi,Y1,Y9}kM-1.TheOIDataGM, DualSignGM, AuthReqDataGM and LinkOIPIGM are as follows:
(37)OIDataGM≔M,C,XIDi,NMi,Y1,Y2,DualSignGM≔{Y7,H(OIDataGM)}kc-1,LinkOIPIGM:=H(AuthReqData,DualSignGM,Y8),AuthReqDataGM≔H(OIDataGM),Y2,M,C,XIDi,AuthRRTags.The generalized role ofG (𝒢G1) is as follows:
(38)𝒢G1={i.4.I(M)→G:{{AuthReqDataGG,LinkOIPIGG}kM-1}kG,DualSignGG,{PIGG}kG,i.5.G→I(M):{{M,C,Z1,Z11,Z6,AuthCode}kG-1}kM.ThePIGG, DualSignGG, AuthReqDataGG, and LinkOIPIGG are as follows:
(39)PIDataGG≔PIHeadGG,PANDataGGPIHeadGG≔M,C,Z1,Z4,Z6,MerID,Z8PANDataGG≔Z9,Z10PIGG≔PIHeadGG,Z12,PANDataGGDualSignGG≔{H(PIDataGG),Z12}kc-1LinkOIPIGG≔H(AuthReqDataGG,DualSignGG,{PI}KG)AuthReqDataGG:=Z12,Z4,M,C,Z1,Z11.


## 4.4. Verifying Whether the SET Role-Based Specification is Increasing

Now, we can verify whether the role-based specification of SET isFSET-increasing. More precisely, we need accordingly to verify that principals do not decrease the security level of components from step to another. To that end, we verify this condition on the each generalized role of the protocol (i.e., on each point of view of protocol participants). To that end, we should verify whether the security level of sent messages is a subset of the security level of these messages in the receieved steps that is,
(40)∀r·FSET(α,r+)⊆⌜α⌝∪FSET(α,r-).(i) Let us start with the generalized roles ofC. According to the definition of r+ and r-, we have
(41)𝒞G1-=∅,𝒞G1+=C,Nci,𝒞G2-={M,C,X1,Nci,X2,CA(G)}kM-1,𝒞G2+=IOGC,DualSignGC,{PIGC}kG.From the definition ofFSET and 𝒞G2+, it follows that, for all atomic message α, we have that
(42)FSET(α,𝒞G2+)=FSET(α,IODataGC,{PIHead,PANData}kG).Now, the security levels of sent and received messages in the generalized roles ofC using the FSET function are as shown in Table 17.Table 17
SET analysis: role ofC.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
N
c
i
𝒞
G
1
⊥
⊥
⊤
Yes
N
c
i
𝒞
G
2
⊥
⊥
⊤
Yes
X
1
𝒞
G
2
τ
X
1
⊥
⊥
Yes
X
2
𝒞
G
2
τ
X
2
⊥
⊥
Yes
PurchAmt
𝒞
G
2
⊥
{
C
,
G
}
∪
τ
X
1
⊤
Yes
MerID
𝒞
G
2
⊥
⊥
⊤
Yes
CardSecret
𝒞
G
2
{
C
,
G
}
{
C
,
M
,
G
}
∪
τ
X
1
⊤
No
PAN
𝒞
G
2
{
C
,
G
}
{
C
,
M
,
G
}
∪
τ
X
1
⊤
No
PANSecret
𝒞
G
2
{
C
,
G
}
{
C
,
M
,
G
}
∪
τ
X
1
⊤
NoFrom the analysis of the role ofC shown in Table 17, we deduce that its generalized roles are not increasing. This is due to the fact that an unknown message X1 is put beside the secret components CardSecret, PAN, and PANSecret and this lowers their security level. Moreover, putting the identity M beside CardSecret, PAN, and PANSecret means that these messages could be known by M according to our interpretation function. Therefore, if X1 (XID in the description of the protocol step 3) and M are hashed in PIHead, then this role can be proved increasing. More precisely, we redefine PIHead as follows:
(43)PIHead=C,HOD,PurchAmt,MerID,H(M,XID),H(CardSecret).(ii) From the generalized roles ofM, we deduce that
(44)ℳG1-=C,Y1,ℳG1+={M,C,XIDi,Y1,NMi,CA(G)}kM-1,ℳG2-=ℳG1-∪{OIDataGM,Y7,DualSignGM,Y8},ℳG2+={{AuthReqData,LinkOIPI}kM-1}kG,DualSignGM,Y8,ℳG3-=ℳG2-∪{{{M,C,XIDi,AuthRRTags,Y3,Y9}kG-1}kM},ℳG3+={M,C,XIDi,Y1,Y9}kM-1.The security levels of sent and received messages in the generalized roles of M using the DEKAN function are as shown in (Table 18).Table 18
SET analysis: role ofM.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
Y
1
ℳ
G
1
τ
Y
1
⊥
⊥
Yes
X
I
D
i
ℳ
G
1
⊥
⊥
⊤
Yes
N
M
i
ℳ
G
1
⊥
⊥
⊤
Yes
C
A
(
G
)
ℳ
G
1
⊥
⊥
⊤
Yes
Y
2
ℳ
G
2
τ
Y
2
⊥
⊥
Yes
X
I
D
i
ℳ
G
2
⊥
⊥
⊥
Yes
AuthRRTags
ℳ
G
2
{
M
,
G
}
⊥
⊤
NoFrom Table19, we can deduce that the generalized roles of M are not increasing. This is because the message AuthRRTags is sent at step 4 of the generalized role ℳG2, with the security level {C,M,G}, which is not greater than its real security level ({M,G}). This is since the identity C is beside AuthRRTags and that means that this message is for C which also lowers the security level of AuthRRTags. One way to make this role increasing is as follows. We remove (or put it beyond the encryption) the identity C from the message AuthReqData of step 4 of the generalized role. More precisely, we redefine AuthReqData as follows:
(45)AuthReqData=H(OIData),HOD,M,XID,AuthRRTags.(iii) From the generalized roles ofG, we deduce that
(46)𝒢G1-={{AuthReqDataGG,LinkOIPIGG}kM-1}kG,DualSignGG,{PIGG}kG𝒢G1+={{M,C,Z1,Z11,Z6,AuthCode}kG-1}kM.Table 19
SET analysis: role ofM.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
Y
8
ℳ
G
2
τ
Y
8
⊥
⊥
Yes
X
I
D
i
ℳ
G
3
⊥
{
M
,
C
,
G
}
∪
τ
Y
2
{
M
,
C
,
Y
3
}
∪
τ
Y
9
Yes
Y
1
ℳ
G
3
τ
Y
1
⊥
⊥
Yes
Y
9
ℳ
G
3
τ
Y
9
⊥
⊥
YesThen, the security levels of sent and received messages in the generalized roles ofM using the DEKAN function are as in Table 20.Table 20
SET analysis: role ofG WLMV:prot.
α
r
⌜
α
⌝
F
SET
(
α
,
r
+
)
F
SET
(
α
,
r
-
)
F
SET
(
α
,
r
+
)
⊆
⌜
α
⌝
∪
F
SET
(
α
,
r
-
)
Z
1
𝒢
G
1
τ
Z
1
{
M
,
C
,
G
}
∪
τ
Z
6
∪
τ
Z
11
{
M
,
C
,
G
,
τ
Z
4
}
∪
τ
Z
6
∪
τ
Z
8
∪
τ
Z
11
∪
τ
Z
12
Yes
Z
6
𝒢
G
1
τ
Z
6
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
11
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
4
∪
τ
Z
8
∪
τ
Z
11
∪
τ
Z
12
Yes
Z
11
𝒢
G
1
τ
Z
11
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
6
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
4
∪
τ
Z
12
No
AuthCode
𝒢
G
1
⊥
{
M
,
C
,
G
}
∪
τ
Z
1
∪
τ
Z
4
∪
τ
Z
6
⊤
YesFrom Table20, we can deduce that the generalized roles of G are not increasing. This is since the messages Z11 (AuthRRTags) and Z6 (PurchAmt) are neighbors in step five while it is not the case in the step four. So, to make this role increasing we should put  Z6 (PurchAmt) beyond the encryption that contains AuthRRTags in step five. For instance, we replace the message of step five as follows:
(47)5.G→M:{{M,C,XID,AuthRRTags,AuthCode}kG-1}kM,{{M,C,XID,PurchAmt,AuthCode}kG-1}kM.To sum up, we propose hereafter a secure version of the SET protocol for the secrecy property. It replaces the message of step5 by message 5' in Table 21.Table 21
A Secure version of the SET protocol.
1.C→M:C,Nc
2.M→C:{M,C,XID,Nc,NM,CA(G)}kM-1
3.C→M:OI,DualSign,{PI}kG
4.M→G:{{AuthReqData,LinkOIPI}kM-1}kG,DualSign,
{PI}kG
5.G→M:{{M,C,XID,AuthRRTags,PurchAmt,
AuthCode}kG-1}kM
5
′. G→M:{{M,XID,AuthRRTags,AuthCode}kG-1}kM,
{{M,C,XID,PurchAmt,AuthCode}kG-1}kM
6.M→C:{M,C,XID,NC,AuthCode}kM-1Also, theOI, PI, DualSign, and LinkOIPI messages are as follows:
(48)OI≔OIData,H(PIData),OIData≔M,C,XID,NM,NC,HOD,HOD≔H(OrderDesc,PurchAmt),PIData≔PIHead,PANData,PIHead(oldversion)≔C,HOD,PurchAmt,MerID,M,XID,H(XID,CardSecret),PIHead≔C,HOD,PurchAmt,MerID,H(M,XID),H(CardSecret),PANData≔PAN,PANSecret,PI≔PIHead,H(OIData),PANData,DualSign≔{H(PIData),H(OIData)}kC-1,LinkOIPI≔H(AuthReqData,DualSign,{PI}KG),AuthReqData≔H(OIData),HOD,M,C,XID,AuthRRTags.
Such modifications allow to prove, by using the DEKAN function, that the new version is increasing and therefore respects the secrecy property.


## 5. Comparison with Related Works

The interpretation functions-based method is flexible framework allowing to verify different classes of protocols against a variety of intruder models. This flexibility gives to it a great advantage when compared to the related works where almost all the approaches can deal only with a specific class of protocols and under some specific assumptions. When using the interpretation functions-based method, we do not have any restriction neither on the class of protocols that we can analyze nor on the intruder model and the algebraic properties. We are limited only by our capacity to find a suitable and safe interpretation function for the protocol that we want to analyze under a selected intruder model (context of verification).Also, the analysis of protocols using the interpretation function-based method can help to discover the algebraic properties that should not be satisfied by an operator of encryption to guarantee the correctness of the analyzed protocol. This information is useful for the implementation of the protocol when time comes to select a specific encryption system. For instance, the commutativity property of the “exclusive or” and the “nilpotence” property should not be combined since they allow to decrypt a message without knowing the key.Moreover, the interpretation function-based method has the significant advantage to ensure the correctness of cryptographic protocols for unbound number of sessions without any restriction neither on the number of principals nor on the size of exchanged messages. In fact, may existing approaches restrict their results by either limiting the number of sessions, the sizes of messages, or/and the number of involved principals to be able to overcome infinite number of traces that can be exhibited by a protocol. Other works tried to find a finite number of traces that are representative for all the others, that is, the analysis of the selected traces is enough to conclude about the correctness of the protocol. However, finding this representative and finite set of traces, if it exists, can be as complicated as the original problem even for some particular class of protocols. There are, however, some tentatives to analyze protocols without restriction on their traces, but they still suffer from some heavy restrictions both on the class of protocols that they can analyze and on the intruder model that they use.In the remaining part of this section, we focus on the typing-based method [33] and the rank function-based method [32] which have some similarities with the interpretation functions-based method.


### 5.1. Typing-Based Method

In 1997, Abadi introduced in [33] a typing system to verify the secrecy property. This system uses three types {secret,public,any} as security levels and verifies whether the sent messages during the protocol are appropriately protected, that is, according to their security levels. The approach uses the Spi-calculus as a formal language to specify the analyzed protocol. Then, a typing system is applied on the protocol: if it typechecks we conclude that it ensures the secrecy property.Compared to interpretation functions-based method, the secrecy by typing approach has the following restrictions.(i)
The exchanged messages have to respect some particular form. They must always be composed of four separated parts having the following type{secret,public,any,confounder}. This restriction helps to recognize the parts that are “secret,’’ “public,’’ and “any’’ (component with unknown security level) of messages. But, this involves that this approach cannot be applied to analyze existing protocols which have not been developed with this restriction in mind. The interpretation functions-based method, on the other side, does not require any particular form related to the exchanged messages during a protocol.(ii)
The secrecy by typing approach uses only the the Dolev and Yao model for the intruder, while interpretation functions-based method can deal with different intruder models.


### 5.2. Rank Functions-Based Method

In 1997, Schneider suggested, in  [31, 32], an interesting approach to verify the cryptographic protocols, specified as a process in CSP [46]. A protocol is considered as correct for the secrecy property if all its exchanged messages have a suitable rank according to a well-designed rank function. A message is either secret or public and the result returned by the ranking function should be in harmony with these security levels, that is, it assigns ranks (negative value) to secret messages different from the ones (positive value) assigned to public messages.The main ideas behind   the typing system, the interpretation function, and the rand function approach are the same, that is, find someway to evaluate the security levels of exchanged messages and then evaluate if they are appropriately protected to guaranty the correctness of the protocol for the secrecy property. However, there are some fundamental differences between them. Hereafter, we focus on the difference between the approach presented in this paper and the rank function.(i)
For each protocol, we need to define a suitable rank function which is a complicated task. There are no universal functions, like DEK or DEKAN for the interpretation function approach, that are independent of the analyzed protocols. A rank function is extracted from the analyzed protocol itself and should respect some specific conditions (like safe condition for the interpretation function). Though the author makes a great effort, in  [35, 47], to help find rank functions, the task remains complicated. On the other hand, in [25], the interpretation functions-based method gives a guideline which helps to define in an easier way safe interpretation functions.(ii)
The results given within the rank function approach are linked to a specific intruder ability. The approach based on interpretation function, on the other hand, is more flexible since it can handle a large variety of intruder abilities without reworking proofs.(iii)
When using a given interpretation function to analyze a protocol, even if we are unable to ensure its correctness the result is generally very helpful to either adapt the protocol or to build another interpretation function. This is not generally the case with the rank function approach.


## 5.1. Typing-Based Method

In 1997, Abadi introduced in [33] a typing system to verify the secrecy property. This system uses three types {secret,public,any} as security levels and verifies whether the sent messages during the protocol are appropriately protected, that is, according to their security levels. The approach uses the Spi-calculus as a formal language to specify the analyzed protocol. Then, a typing system is applied on the protocol: if it typechecks we conclude that it ensures the secrecy property.Compared to interpretation functions-based method, the secrecy by typing approach has the following restrictions.(i)
The exchanged messages have to respect some particular form. They must always be composed of four separated parts having the following type{secret,public,any,confounder}. This restriction helps to recognize the parts that are “secret,’’ “public,’’ and “any’’ (component with unknown security level) of messages. But, this involves that this approach cannot be applied to analyze existing protocols which have not been developed with this restriction in mind. The interpretation functions-based method, on the other side, does not require any particular form related to the exchanged messages during a protocol.(ii)
The secrecy by typing approach uses only the the Dolev and Yao model for the intruder, while interpretation functions-based method can deal with different intruder models.


## 5.2. Rank Functions-Based Method

In 1997, Schneider suggested, in  [31, 32], an interesting approach to verify the cryptographic protocols, specified as a process in CSP [46]. A protocol is considered as correct for the secrecy property if all its exchanged messages have a suitable rank according to a well-designed rank function. A message is either secret or public and the result returned by the ranking function should be in harmony with these security levels, that is, it assigns ranks (negative value) to secret messages different from the ones (positive value) assigned to public messages.The main ideas behind   the typing system, the interpretation function, and the rand function approach are the same, that is, find someway to evaluate the security levels of exchanged messages and then evaluate if they are appropriately protected to guaranty the correctness of the protocol for the secrecy property. However, there are some fundamental differences between them. Hereafter, we focus on the difference between the approach presented in this paper and the rank function.(i)
For each protocol, we need to define a suitable rank function which is a complicated task. There are no universal functions, like DEK or DEKAN for the interpretation function approach, that are independent of the analyzed protocols. A rank function is extracted from the analyzed protocol itself and should respect some specific conditions (like safe condition for the interpretation function). Though the author makes a great effort, in  [35, 47], to help find rank functions, the task remains complicated. On the other hand, in [25], the interpretation functions-based method gives a guideline which helps to define in an easier way safe interpretation functions.(ii)
The results given within the rank function approach are linked to a specific intruder ability. The approach based on interpretation function, on the other hand, is more flexible since it can handle a large variety of intruder abilities without reworking proofs.(iii)
When using a given interpretation function to analyze a protocol, even if we are unable to ensure its correctness the result is generally very helpful to either adapt the protocol or to build another interpretation function. This is not generally the case with the rank function approach.


## 6. Conclusion

By analyzing the SET and the NSL protocols, this paper is an attempt to show that the interpretation functions-based method is an efficient technique to analyze and to ensure the correctness of cryptographic protocols for the secrecy property. Based on some special functions called “Interpretation Functions,’’ this technique allows to guarantee the secrecy property under an unbound number of sessions and without any restriction on the size of messages sent by the intruder. To verify the secrecy property, it is sufficient to check whether a finite specification of the protocol, called generalized roles, respects some precise conditions. Intuitively, these conditions state that involved principals could not decrease, for a safe interpretation function, the security levels of exchanged messages. Another interesting feature of this approach is that it can handle different verification contexts with different intruder abilities including algebraic properties.As future works, we want to implement the approach, extend it to authentication property, and propose more safe interpretation functions.



---

*Source: 254942-2012-11-25.xml*