# ESSM: Formal Analysis Framework for Protocol to Support Algebraic Operations and More Attack Capabilities

Authors: Xuyang Miao; Chunxiang Gu; Siqi Lu; Yanan Shi
Journal: Security and Communication Networks
 (2021)

---

## Abstract

The strand space model has been proposed as a formal method for verifying the security goals of cryptographic protocols. However, only encryption and decryption operations and hash functions are currently supported for the semantics of cryptographic primitives. Therefore, we establish the extended strand space model (ESSM) framework to describe algebraic operations and advanced threat models. Based on the ESSM, we add algebraic semantics, including the Abelian group and the XOR operation, and a threat model based on algebraic attacks, key-compromise impersonation attacks, and guess attacks. We implement our model using the automatic analysis tool, Scyther. We demonstrate the effectiveness of our framework by analysing several protocols, in particular a three-factor agreement protocol, with which we can identify new attacks while providing trace proofs.


---

## Body

## 1. Introduction

In recent years, formal analysis has been widely applied to different types of protocol security analyses [1, 2], including 5G authentication and key agreement (AKA) protocol [3, 4], transport-layer security (TLS) version 1.3 [5, 6], Signal Messaging Protocol [7], Secure Forwarding Protocols [8], and Multifactor Authentication Protocols [9]. Theoretical research on the formal analysis is under way, and great progress has been made in observation equivalencies [10] and equality theory [11].Automatic analysis of algebraic attributes in security protocols is gaining increasing attention in formal analysis. Among the existing formal symbol-based analysis tools, several support algebraic property analyses are based on various theories. For example, the On-the-fly Modal Checker [12] explores the state space based on a requirement-driven approach. The Constraint Logic-based Attack Searcher [13] runs protocols in all possible aspects on a limited session set based on constraint logic, converting traces into constraints. The Tree Automata based on Automatic Approximations for the Analysis of Security Protocols [14] uses tree automata based on automatic approximation analysis with a rule-tree language with rewriting to approximate intruder knowledge. ProVerif, an automatic cryptographic protocol verifier [15], verifies that a protocol satisfies a set of given user attributes based on an overapproximation technology (such as the abstraction generated by a new nonce). The Tamarin Prover, a security protocol verification tool that supports both falsification and unbounded verification in the symbolic model [16], supports the Diffie-Helman (DH) method [17] and exclusive-OR (XOR) [18] theory based on protocol descriptions of multiset rewriting systems.Scyther [19] used the strand space model to represent protocol roles and applied a pattern-based reverse search algorithm to perform bounded or unbounded attribute verification on the protocol [20]. In [21], Cremers proposed a method to approximately describe the DH operation using IKEv1 and IKEv2 protocols using an auxiliary protocol.The strand space model [22] is a practical formal method of analysing security protocols. The theoretical basis of the strand space model was built upon the Dolev-Yao model [23] proposed by Febrag et al., which transforms the role of the state and overall process of protocol operation into a set and directed graph to determine if attack nodes existed by deducing the set.Automatic analysis tools using the strand space model as their theoretical bases include Athena [24], Scyther, Maude’s Naval Research Laboratory Protocol Analyzer (NPA) [25], Cryptographic Protocol Shape Analyzer (CPSA) [26], and the Tamarin Prover. The strand space model is widely used for protocol analysis. Yang et al. [27] solved the representation selection problem of a strand space model, allowing protocol selection along different paths and integrated syntax and transformation rules of process algebra into Maude NPA strands. Basin and Cremers [28] extended strand space model support to an adversary model and modelled the attacker in Scyther-compromise. Dong and Niu [29] extended the anonymity analysis framework and qualitatively analysed the differences of degrees of anonymity.In this research, our contributions are as follows.We establish the Extended Strand Space Model (ESSM) framework with algebraic strands to represent protocol operations and use different bundles to represent different attacker behaviours. The model has scalability and protocol adaptability, and it can select attacker capabilities according to the specific protocol and communication environment while accurately modelling attacker behaviours.We establish the semantic description of the algebraic capability of the strand space, extending the attacker’s ability to obtain messages with algebraic properties. The attacker can obtain previously ignored information in protocols supporting the XOR and Abelian groups.We establish a semantic support mechanism for special attacks against attackers. The models of algebraic attacks, key leakage attacks, and guessing attacks are carried out in specific environments.The correctness of the added semantic logic is verified using Scyther’s engineering implementation of ESSM. The applicability and correctness of the framework are illustrated by comparing the number of detection paths with the ability to detect attacks before and after addition.The rest of this paper is organized as follows. In Section2, we briefly review the basic definition of strand space model. The third section elaborates the establishment of the ESSM framework. Section 4 shows the performance of ESSM using real protocol analyses. Section 5 concludes the paper and discusses future work. The source code of the protocol formal model can be obtained from https://github.com/mmmxy555/ESSM.


## 2. Strand Space Theory

This section briefly introduces the basic concepts of strand space theory, the attacker model, and security attribute representation.


### 2.1. Basic Concepts

In the strand space model, the behaviours of the protocol participant and attacker are described as strands, and the set of these strands constitutes the strand space. The symbols are shown in Table1.Table 1
Symbols in strand space.
SymbolSpecificationAgentRoles involved in protocol operationKABLong term symmetric keys of principalsA and BKALong term public key of subjectaKA−1Long term private key of principalaxKEncrypt datax with key Ka,bConnection of dataa and BPProtocol intruderWe mark the set of all elements appearing in the protocol interaction asA. We refer to the elements of A as terms, which can contain one or more subterms. t1⊂t expresses that element t1 is a subterm of t, where t and t1 are both terms.Binaryσ,a is a symbolic term in which a∈A, and σ∈+,−, which is expressed as +a or −a. +a means that the principal sends term a, and −a indicates that the principal receives term a.Definition 1 (strand).
A strand is a finite sequence containing several symbolic terms. A strands, with n symbolic terms, can be expressed as s=〈σ1,a1,…,σn,an〉. We define the set of strands as S and set all strands in protocol P as si1≤i≤t, where si∈SP.
The strand space model was used to construct the Needham-Schroeder public key (NSPK) protocol.(i)
Initiator strand:InitA,B,NA,NB=+NA,AKB,−NA,NBKA,+NBKB.(ii)
Responder strand:RespA,B,NA,NB=−NA,AKB,+NA,NBKA,−NBKB.
The strand space digraph of the protocol can be obtained by associating the collusion of each role through a causal connection. For example, in NSPK, the strand space digraph is given as Figure1.Figure 1
Strand space digraph of NSPK.


### 2.2. Protocol Attacker Description

An attacker’s ability follows the attacker model defined by Dolev and Yao using discard, generate, and combine messages. In the strand space model, the attacker’s ability is realized via a combination of an attacker’s atomic operations, as defined in Table2.Table 2
Attacker operation of strand space.
SymbolSpecificationStrandMGenerate text messages+tFReceive messages−gTReceive and send messages−g,+g,+gCConnect received messages−g,−h,+ghSSeparating received messages−gh,+g,+hKSend key+KEEncrypted message−K,−h,+hKDDecrypt message−K−1,−hK,+hBundle is a structure in the strand space, composed of some strands, connected by some binary with opposite signs but the same terms. Figure1 can be seen as a bundle composed of two strands. The three symbol terms of each strand satisfy the same terms but opposite signs. This establishes a connection between the two strands to form a bundle.Using initial knowledge and atomic operations, the attacker can completely control the channel, eavesdrop, tamper, or redirect messages and expand the known information of the attacker via encryption and decryption.


### 2.3. Representation of Security Attributes

We mainly consider that the attacker can obtain secret information protected in the protocol through a combination of attacker strands and initial knowledge. The confidentiality of secret informationx means that there is no node, n (e.g., a normal node or an attacker node), and considers unprotected x as its term. The definition of confidentiality is as follows.Definition 2 (secrecy).
A valuex is secret in a strand space Σ if, for every bundle C in Σ and for every node n∈C, the termn≠x.
Additionally, authentication can also be assured. A protocol satisfies the requirement of authentication, which indicates that each subject of the protocol receives the terms that should be accepted according to the protocol expectation.Definition 3 (authentication).
A protocol guarantees a participant’s (B (e.g., the responder)) agreement for certain data terms x, with participant A if, in a strand space Σ, for every bundle C, containing a responder strand using x in Σ, there exists a unique initiator strand using x in C.
A weaker noninjective agreement does not ensure uniqueness.


## 2.1. Basic Concepts

In the strand space model, the behaviours of the protocol participant and attacker are described as strands, and the set of these strands constitutes the strand space. The symbols are shown in Table1.Table 1
Symbols in strand space.
SymbolSpecificationAgentRoles involved in protocol operationKABLong term symmetric keys of principalsA and BKALong term public key of subjectaKA−1Long term private key of principalaxKEncrypt datax with key Ka,bConnection of dataa and BPProtocol intruderWe mark the set of all elements appearing in the protocol interaction asA. We refer to the elements of A as terms, which can contain one or more subterms. t1⊂t expresses that element t1 is a subterm of t, where t and t1 are both terms.Binaryσ,a is a symbolic term in which a∈A, and σ∈+,−, which is expressed as +a or −a. +a means that the principal sends term a, and −a indicates that the principal receives term a.Definition 1 (strand).
A strand is a finite sequence containing several symbolic terms. A strands, with n symbolic terms, can be expressed as s=〈σ1,a1,…,σn,an〉. We define the set of strands as S and set all strands in protocol P as si1≤i≤t, where si∈SP.
The strand space model was used to construct the Needham-Schroeder public key (NSPK) protocol.(i)
Initiator strand:InitA,B,NA,NB=+NA,AKB,−NA,NBKA,+NBKB.(ii)
Responder strand:RespA,B,NA,NB=−NA,AKB,+NA,NBKA,−NBKB.
The strand space digraph of the protocol can be obtained by associating the collusion of each role through a causal connection. For example, in NSPK, the strand space digraph is given as Figure1.Figure 1
Strand space digraph of NSPK.


## 2.2. Protocol Attacker Description

An attacker’s ability follows the attacker model defined by Dolev and Yao using discard, generate, and combine messages. In the strand space model, the attacker’s ability is realized via a combination of an attacker’s atomic operations, as defined in Table2.Table 2
Attacker operation of strand space.
SymbolSpecificationStrandMGenerate text messages+tFReceive messages−gTReceive and send messages−g,+g,+gCConnect received messages−g,−h,+ghSSeparating received messages−gh,+g,+hKSend key+KEEncrypted message−K,−h,+hKDDecrypt message−K−1,−hK,+hBundle is a structure in the strand space, composed of some strands, connected by some binary with opposite signs but the same terms. Figure1 can be seen as a bundle composed of two strands. The three symbol terms of each strand satisfy the same terms but opposite signs. This establishes a connection between the two strands to form a bundle.Using initial knowledge and atomic operations, the attacker can completely control the channel, eavesdrop, tamper, or redirect messages and expand the known information of the attacker via encryption and decryption.


## 2.3. Representation of Security Attributes

We mainly consider that the attacker can obtain secret information protected in the protocol through a combination of attacker strands and initial knowledge. The confidentiality of secret informationx means that there is no node, n (e.g., a normal node or an attacker node), and considers unprotected x as its term. The definition of confidentiality is as follows.Definition 2 (secrecy).
A valuex is secret in a strand space Σ if, for every bundle C in Σ and for every node n∈C, the termn≠x.
Additionally, authentication can also be assured. A protocol satisfies the requirement of authentication, which indicates that each subject of the protocol receives the terms that should be accepted according to the protocol expectation.Definition 3 (authentication).
A protocol guarantees a participant’s (B (e.g., the responder)) agreement for certain data terms x, with participant A if, in a strand space Σ, for every bundle C, containing a responder strand using x in Σ, there exists a unique initiator strand using x in C.
A weaker noninjective agreement does not ensure uniqueness.


## 3. Extended Strand Space Model

### 3.1. ESSM Framework

We extend the semantics of the strand space model and propose the ESSM framework shown in Figure2.Figure 2
ESSM framework.The definitions of strand and bundle inherit the definition of the strand space model. In ESSM, a strand can be divided into three types: role, algebra, and attack.The role strand represents the sending and receiving message strands fulfilling the role of the protocol interaction. The algebra strand includes a newly defined algebraic operation strand. The attacker strand contains the original attack capability and extension capability modules.Per the role-interaction rules defined for the protocol, the role strands describe the order of receiving and sending messages through protocol subjects. The algebra strand is a novel type added in ESSM which can be modularized and extended; it describes the conversion rules of algebraic operations in the protocol. Algebraic operations can be shared by the principal and the attacker, and the agent can use algebraic operations and basic encryption and decryption rules,E and D, to complete the internal operations of the agent. Simultaneously, the equivalent relationship of the algebraic operation can be modelled. For attackers, algebraic operations can be used to acquire more terms in the ESSM than those in the original strand space model. The basic attacker strand inherits the semantics of M, F, T, and other penetrator strands in the strand space model. In the extension module, the problems existing in the specific protocol can be combined with the model.We use three disjoint sets to represent all the strands in protocolP. SroleP, SalgebraP, and SattackP refer to the set of all role, algebra, and attack strands in P, respectively. Then, the strand set satisfies SroleP∪SalgebraP∪SattackP=SP.The extended strands must satisfy the basic rules of obtaining terms, meaning that the terms obtained by an attacker must have appeared before.Definition 4 (extended strands).
Strand−term1,−term2,…,−termn,+termobtain is a legal extended strand, if, for all subterm⊂termobtain, there exists a number i1≤i≤n that satisfies subterm⊂termi.
An extended strand space is a graph of three types of collusions connected by causal dependency. This graph is the set space of all roles, algebra operations, and attacks. We use the rules of confidentiality and authentication in the SSM to determine whether the security attributes of a protocol are satisfied.
In ESSM, the concept of algebraic rule strands that support some algebraic operations in the interaction behaviour of agents is introduced. Simultaneously, attackers can use these algebraic rule strands to carry out attacks. The algebraic operations commonly used in the XOR operation and Abelian group operations are semantically modelled such that ESSM can be used in protocols that support algebraic operations.
In the extended model, the attacker’s ability is abstracted into descriptions of the attacker’s behaviours using different atomic rules. This modular design enables us to define attacker models for specific protocols.
Furthermore, the algebraic and attacker rules in ESSM are extensible. Thus, ESSM can be further extended by the systematic description of atomic rules for added algebraic operations or attack capabilities.
Compared with the original strand space model, our extended framework has two advantages.
One is the formal description of algebraic properties. Traditional analysis ignores the nature of algebraic operations when there are algebraic operations in the protocol and cannot detect attacks carried out by attackers using algebraic operations. Our extension can search for this type of attack and expand the types of protocols that can be analysed.
The second is a custom description of attack capabilities. The traditional SSM is based on the Dolev-Yao attacker model, assuming that the cryptographic primitives are unbreakable. In fact, attackers may have attacks such as KCI attacks and weak password guessing. These are not considered in traditional analysis. In our extension, we can consider different problems according to the possible problems of the protocol. The attack models can be freely combined to find the problems in the protocol.


### 3.2. Algebraic Attribute Addition

The basic strand space model does not support algebraic operations (e.g., XOR or Abelian groups), and attackers have no way of locating attacks related to algebraic properties. Instead, a one-way function is used to model the XOR and Abelian groups abstractly, such that the strand space model can support protocol analysis using algebraic operations, and attackers can use algebraic operation strands to detect problems with algebraic operations in protocols.For the addition of different modules, we introduce new types of terms and functions. When the type of the term matches the type of the function parameter, the newly added strand can be applied. At the same time, the new type of strand is also compatible with the operations of traditional SSM attackers. For example, forNum type terms, the attacker can also perform operations such as generation and eavesdropping.


#### 3.2.1. XOR Operation

The XOR operation requires the establishment of an algebraic model that satisfies the following operational relations. Fora,b,c∈Num,(1)a⊕0=a,a⊕0=a,a⊕b=b⊕a,a⊕b⊕c=a⊕b⊕c.We use a hash function combined with a new set of decryption semantics to achieve the XOR operation. Owing to the unidirectionality of the hash function, the attacker can constructxora,b when a and b are known. However, terms a and b cannot be obtained through xora,b.Definition 5 (XOR operation).
One-way functionxor:Num∗Num⟶Num; xora,b denotes the exclusive xor of terms a and b.
The attacker can generatexora,b through a and b, and if xora,b and b are known, the attacker can calculate a⊕b⊕b=a to obtain term a, which cannot be described by the hash function. Thus, a new model of the attacker’s derivation ability is needed.
We built an XOR operation module, which is shown in Table3. For the protocol containing the XOR operation, we can add an XOR operation semantic module to model the protocol. Attackers can obtain information in an algebraic operation.
In rule XOR-Z, we construct a constantz, which represents the zero element, which is included in the initial knowledge by the subject and attacker in the protocol description. In rule XOR-G, attackers can apply XOR to construct the XOR values of two known terms. In rule XOR-S, the attacker can obtain xorb,a using the known XOR value xora,b. Moreover, these two terms are independent in the strand space model, and the exchange law of the XOR operation can be constructed using this rule. In rule XOR-D, an attacker can obtain the second term b, by knowing the XOR value xora,b, and the first term a. In rule XOR-O, an attacker can obtain the term XOR from the zero element. In rule XOR-C, the attacker can apply the binding law to combine the XOR values of the three elements.
We do not have a decryption rule for the first term of the XOR model, because it can be implemented by applying the XOR-S and XOR-D rules.
Inferring that the attacker knowsxora,b and b, term a can be obtained using these known values. The attacker first applies the XOR-S rule −xora,b,+xorb,a, gets xorb,a, and passes the XOR-D rule −xorb,a,−b,+a to obtain term a.Table 3
Strands of XOR operation module.
Rule nameSpecificationStrandXOR-ZInitial knowledge+zXOR-GGenerate XOR terms−a,−b,+xora,bXOR-SCommutative rule of XOR−xora,b,+xorb,aXOR-DReflexive rule of XOR−xora,b,−a,+bXOR-ZObtains the term XOR with 0−xora,z,+aXOR-CAssociative rule of XOR operation−xorxora,b,c,+xora,xorb,c


#### 3.2.2. Abelian Group Operation

In security protocols, the application of an Abelian group is embodied in the key agreement algorithms, DH, and the elliptic-curve DH (ECDH). Using the multiplicative group onZp∗ and the additive group on an elliptic curve, we analyse the properties of the Abelian group, describe the operation of the Abelian group in ESSM, and model the ability of attackers to obtain terms from the operation.We describe the semantics of the multiplication group onZp∗ as follows: for the primitive element g over Zp∗,(2)gxy≡gx∗ymodp,gx∗y≡gy∗xmodp,gx∗gy≡gy+xmodp,gx+y≡gy+xmodp.First, two one-way functions, add and mul, are defined to represent the addition and multiplication operations of the two variables.Definition 6 (add operation).
One-way functionadd:Z∗Z⟶Z; adda,b denotes the addition of terms a and b.Definition 7 (mul operation).
One-way functionmul:Z∗Z⟶Z; mula,b denotes multiplication of terms a and b.
Similar to the XOR operation, attackers can construct add and mul function values that support exchange to deduce the value of another element by knowing the whole function value and one element. We define these three algebraic properties as gen, swap, and decrypt, as shown in Table4.
For the equivalence relations in the Abelian group having different forms on both sides, we use the equivalence relationgxy≡gx∗y. Because it is impossible to describe the equivalence relation in the strand space model, a bidirectional derivation relationship should be considered, such as gxy≡gx∗y and gx∗gy≡gy+x. This equivalence relation is expressed as a bidirectional strand space model. For the subject and attacker of the protocol, we establish the semantic rules in Table 5.
We describe the DH key exchange protocol in the strand space by applying the semantics of the multiplication group onZp∗. Via the key exchange, the two parties can establish a shared key, expg,mulx,y. The strand representations of protocol roles A and B are as follows:(1)
InitiatorA’s strand: InitA,B,x=+expg,x,−expg,y,+mesexpg,mulx,y.(2)
ResponderB’s strand: RespA,B,y=−expg,x,+expg,y,−mesexpg,mulx,y.
In the role strand of this protocol, the third message betweenA and B is not trivial, because both parties need to obtain expg,mulx,y. The message is then encrypted and decrypted. Term expg,mulx,y is obtained by adding the semantics. Considering principal A as an example, the process of obtaining the shared key is as shown in Figure 3.
RoleA applies the DH-G rule to obtain the term expg,y. A obtains the term expexpg,y,x by combining the initial knowledge of x. DH-L1 rules are then applied to obtain the term expg,muly,x. Then, DH-S1 rules are applied to obtain the term expg,mulx,y. At this point, role A obtains the symmetric key established by both parties, and role B can obtain the term expg,mulx,y using similar methods. Roles A and B interact with the third node using the shared key.
Similarly, we establish the operation rules of the Abelian group on an elliptic curve, assuming thatP is a point on the elliptic curve E, and x,y∈Z. P has the following properties:(3)x×y×P=x∗y×P,x∗y×P=y∗x×P,x×P+y×P=x+y×P,x+y×P=y+x×P.
We define addition and multiplication on elliptic curves as ecadd and ecmul, which are distinguishable from add and mul which are defined above.Table 4
Strands of ADD and MUL operation module.
Rule nameSpecificationStrandADD-GGenerative addition terms−a,−b,+adda,bADD-SCommutative rule of addition−adda,b,+addb,aADD-DInverse rule of addition−adda,b,−a,+bMUL-GGenerative multiplication terms−a,−b,+mula,bMUL-SCommutative rule of multiplication−mula,b,+mulb,aMUL-DInverse rule of multiplication−mula,b,−a,+bTable 5
Strands of DH operation module.
Rule nameSpecificationStrandDH-KInitial knowledge+gDH-GPerform power module operation−a,−b,+expa,bDH-S1Commutative rule of multiplication−expg,mula,b,+expg,mulb,aDH-S2Commutative rule of addition−expg,adda,b,+expg,addb,aDH-L1Deduction rule L1−expexpg,a,b,+expg,mula,bDH-L2Deduction rule L2−expg,mula,b,+expexpg,a,bDH-R1Deduction rule R1−expg,mula,b,+expexpg,a,bDH-R2Deduction rule R2−expg,adda,b,+mulexpg,a,expg,bFigure 3
The path for legal agent to obtain shared key.Definition 8 (ecadd, ecmul operation).
One-way functionecadd:Point×Point⟶Point; ecmul:Z×Point⟶Point; ecadda,b denotes the addition operation of terms a and b of type point, and the term type obtained is point; ecmula,b represents multiplication operation of the term of type Z and the term of type point, and the term type obtained is point.
Similarly, the operation rules of the elliptic curve are established in Table6.Table 6
Strands of ECDH operation module.
Rule nameSpecificationStrandECDH-KInitial knowledge+PECDH-GPerform multiplication−a,−P,+ecmula,PECDH-S1Addition exchange rule−ecmuladda,b,P,+ecmuladdb,a,PECDH-S2Multiplication exchange rules−ecmulmula,b,P,+ecmulmulb,a,PECDH-L1Deduction rule L1−ecmula,ecmulb,P,+ecmulmula,b,PECDH-L2Deduction rule L2−ecaddecmula,P,ecmulb,P,+ecmuladda,b,PECDH-R1Deduction rule R1−ecmulmula,b,P,+ecmula,ecmulb,PECDH-R2Deduction rule R2−ecmuladda,b,P,+ecaddecmula,P,ecmulb,P


### 3.3. Attacker Capability

In this section, we extend the attacker attack model using modularization. Based on the classic Dolev-Yao model, in the first section, we model a variety of attacks based on algebraic properties, including small group attacks, Lim-Lee attacks, and others that need to be combined with group properties. The second section introduces the extension of the key-compromise impersonation (KCI) attack, which can describe the situation of specific information exposure. The third section considers the influence of guessing attacks on security protocols and formalizes the attack.


#### 3.3.1. Attack Based on Algebraic Form

In this section, we describe the algebraic attacks which have been already shown to exist, including subgroup attacks and Lim-Lee attacks. We reveal that the attacker can destroy algebraic properties in a specific environment to obtain secret information.(1) Small-Group Attack. The small-group attack was first proposed by van Oorschot and Wiener [30]. This type of attack takes advantage of the structural characteristics of a group to replace the key negotiated by both sides of the communication. The negotiated key can be obtained without affecting the normal communication between the two sides.In the implementation, if the Abelian group used in the protocol isZp∗, order p−1 is a composite number. If the order of group G used in the protocol is a composite number, n=r∗ω, assuming that r is a small factor of n, and G has subgroups gt∗, meaning that gt is a multiplicative group whose generator order is r. There are only r elements in this group.If the shared secret key negotiated by both parties is in groupgt∗, the attacker can guess the real key exhaustively when the two parties communicate with each other using key encryption.Considering the simple DH as an example, the attack process is as follows:(1)
RoleA initiates DH key exchange with role B, generates a random number x, and calculates the public key, gx.(2)
The attacker interceptsgx and calculates gωx sent to B.(3)
RoleB receives message gωx. Subsequently, random number y is generated and the public key gy is calculated and sent to C. The negotiated key is calculated as ZBA=gωxy=gωxy.(4)
The attacker interceptsgy and calculates gωy sent to A.(5)
RoleA receives a message gωy. Then, the key is calculated as ZAB=gωyx=gωxy.(6)
RolesA and B use ZAB as a session key for message passing, and the attacker eavesdrops the encrypted message and guesses to verify the session key, gωxy.Assuming that the order of groupG used in the protocol is a composite number, the attacker can decompose it to obtain ω. Then, for all gxω for symmetric key messages, attackers can obtain x and key gx by the exhaustive computation of gωx. We ignore the details of the exhaustive computation and assume that the attacker can decompose a large integer, n. We model the derivation relationship of the attacker in Table 7. For the operation relationship of DH, we extend the derivation in the previous section.Table 7
Strands of small group attack module.
Rule nameSpecificationStrandSS-GGenerating elements on subgroups−expg,a,+expg,mula,ωSS-VGuess the elements on a subgroup−mesexpg,mula,ω,+expg,mula,ωRule SS-G means that the attacker will use the term on groupexpg,a through the operation of the ω-power module on the subgroups to obtain terms expg,mula,ω. The SS-V rule indicates that the attacker obtains the elements, expg,mula,ω, on the subgroup via exhaustive verification using the elements in the subgroup as the term for key encryption. The type of term a is not limited. For example, the key negotiated by both sides of DH protocol under the attack of small groups can be expg,mulmulx,y,ω. In this case, a in the formula means mulx,y.(2) Lim-Lee Attack. Owing to the discovery of small group attacks, a preventive measure uses the prime, q, subgroup of Zp∗. However, Lim and Lee found an attack method having prime order [31] against the group. Thus, the attacker can obtain the private key of the responder role by actively participating in the operation of the protocol.Taking simple DH as an example, the attack process is as follows:(1)
AttackerC initiates a DH key exchange with role B to generate random numbers x∈Zq∗ and calculate the public key, gx. Simultaneously, β is generated. The order of β is r and it satisfies r|p−1/q. C sends β∗gx to role B.(2)
RoleB receives the message, β∗gx. Subsequently, random number, y, is generated, and the public key, gy, is calculated and sent to C. The negotiated key is ZBC=β∗gxy=βy∗gxy.(3)
AttackerC receives gy and calculates ZCB=gyx=gx∗y=ZBC/βy, because βy is the only r available for the attacker to use to obtain the correct partial information, ymodr, by verification.(4)
By tryingβ corresponding to different r, the attacker can obtain equations with different moduli, and the complete information of y can be obtained using the Chinese remainder theorem.Assuming that the group used in the protocol is a prime group of orderq and that the attacker can participate in and initiate the protocol, we define a strand space model for the attacker to execute the Lim-Lee attack in Table 8.Table 8
Strands of Lim-Lee attack module.
Rule nameSpecificationStrandLL-GGenerating elements outside the group−expg,a,+mulβ,expg,aLL-VGuess the elements of validationmesexpmulβ,expg,a,y,+modyLL-CComputing termy using CRT−mody,+yRule LL-G converts the elements,expg,a, of a group beyond the group to obtain mulβ,expg,a, where the order of β is r and it satisfies r|p−1/q. Rule LL-V obtains the information of ymodr by guessing its verification, ignoring the specific guessing process, and it assumes that the attacker’s guessing ability can calculate the data of scale r. Rule LL-C uses the Chinese remainder theorem to recover the complete information of y, thereby creating a sample. Moreover, the attacker must use different ri of βi, conduct intrusion behaviours, and obtain one term, ymodri, at a time. Through different ri, it combines complete information on y. We abstract this process, and, to preserve the principle of attack, we express this process as the term, y, calculated by ymodri. The attacker only needs to execute one intrusion to obtain term y.


#### 3.3.2. KCI Attack

It is possible for an attacker to break through a device to obtain its long-term private key, or in a protocol using a smart card, to obtain the smart card of a legitimate subject leading to a smart-card loss attack. We define this behaviour semantically and describe it as a KCI attack.An attacker can obtain the long-term private key, session key, or some state in communication by corroding the agent or via cryptanalysis. We model this ability as a message,mes, which the attacker steals from the role strand. Hence, the derivation relation of some information in the message that cannot be obtained directly can then be obtained. The term, key, can be symmetric or asymmetric, encrypted or hashed, or more complex. The attackable information must be included in the role strands. Thus, this method has a certain applicability that further indicates the situation of secret information disclosure (e.g., role long-term private key, session key, and smart card). The corresponding disclosure rules must be generated alongside specific protocols. Here, only the framework of the attacker rules is given in Table 9.Table 9
Strands of KCI attack module.
Rule nameSpecificationStrandRevealGet some key from encryption−meskey,+keyRevealGet some terms from encryption−meskey,+mesRevealGet some keys from hash−hashkey,+keyNote that these rules must be implemented in combination with specific protocol role strands. For details, refer to the KCI attack and impersonal attack in the MTI protocol in the next section, as well as the analysis of the three-factor authentication protocol. For specific protocols, the terms of disclosure can be specified.


#### 3.3.3. Guessing Attack

Guessing attacks include two parts. First, an attacker intercepts a message related to the value to be guessed. Then, the attacker matches the correct guess value by traversing the dictionary. The default value to be guessed is a password. For the first part, the attacker must have a detection method that can verify the conjecture.(i)
Password as encryption keyIf the attacker can obtain a message pair similar toterm and termpw, the attacker can generate termpw′ by constructing pw′ and encrypting semantic E to verify that the generated key pw′ is correct by comparing whether termpw′ and termpw are consistent.(ii)
Password contained in a hashIf the attacker can obtain ahashpw,term1,…,termn and knows termi1≤i≤n, the attacker can guess the password, pw′, and construct a hash, hashpw′,term1,…,termn. The original hash value is compared to verify the guess.In the second part, the success rate of guess attack depends on the complexity of the password set by the agent and the size of the dictionary used. Theoretically, if the password is in the dictionary, it can be successfully cracked. In the theoretical description of guessing attacks, the attacker has enough elements in the dictionary to carry out a guessing attack on any message that meets the requirements.However, the situation in the real protocol may be more complex. For example, the password is used as the key after hashing or multiple hashings, which can be regarded as the multiple effects of the basic situation. In short, the attacker can crack the weak password after obtaining a message that meets the guessing condition. The formal description of this ability is shown in Table10.Table 10
Strands of guessing attack module.
Rule nameSpecificationStrandGS-EGuess password from encryption−apw,−a,+pwGS-HGuess password from hash−hasha,pw,−a,+pwIn accordance with the description of a KCI attack, the definition of the attacker strand of a guessing attack should be combined with a specific protocol. In rules GS-E and GS-H, only the description method of the guessing attack is described. It is thus necessary to combine the strand of the subject to customize the ability of the attacker to carry out a guessing attack.


## 3.1. ESSM Framework

We extend the semantics of the strand space model and propose the ESSM framework shown in Figure2.Figure 2
ESSM framework.The definitions of strand and bundle inherit the definition of the strand space model. In ESSM, a strand can be divided into three types: role, algebra, and attack.The role strand represents the sending and receiving message strands fulfilling the role of the protocol interaction. The algebra strand includes a newly defined algebraic operation strand. The attacker strand contains the original attack capability and extension capability modules.Per the role-interaction rules defined for the protocol, the role strands describe the order of receiving and sending messages through protocol subjects. The algebra strand is a novel type added in ESSM which can be modularized and extended; it describes the conversion rules of algebraic operations in the protocol. Algebraic operations can be shared by the principal and the attacker, and the agent can use algebraic operations and basic encryption and decryption rules,E and D, to complete the internal operations of the agent. Simultaneously, the equivalent relationship of the algebraic operation can be modelled. For attackers, algebraic operations can be used to acquire more terms in the ESSM than those in the original strand space model. The basic attacker strand inherits the semantics of M, F, T, and other penetrator strands in the strand space model. In the extension module, the problems existing in the specific protocol can be combined with the model.We use three disjoint sets to represent all the strands in protocolP. SroleP, SalgebraP, and SattackP refer to the set of all role, algebra, and attack strands in P, respectively. Then, the strand set satisfies SroleP∪SalgebraP∪SattackP=SP.The extended strands must satisfy the basic rules of obtaining terms, meaning that the terms obtained by an attacker must have appeared before.Definition 4 (extended strands).
Strand−term1,−term2,…,−termn,+termobtain is a legal extended strand, if, for all subterm⊂termobtain, there exists a number i1≤i≤n that satisfies subterm⊂termi.
An extended strand space is a graph of three types of collusions connected by causal dependency. This graph is the set space of all roles, algebra operations, and attacks. We use the rules of confidentiality and authentication in the SSM to determine whether the security attributes of a protocol are satisfied.
In ESSM, the concept of algebraic rule strands that support some algebraic operations in the interaction behaviour of agents is introduced. Simultaneously, attackers can use these algebraic rule strands to carry out attacks. The algebraic operations commonly used in the XOR operation and Abelian group operations are semantically modelled such that ESSM can be used in protocols that support algebraic operations.
In the extended model, the attacker’s ability is abstracted into descriptions of the attacker’s behaviours using different atomic rules. This modular design enables us to define attacker models for specific protocols.
Furthermore, the algebraic and attacker rules in ESSM are extensible. Thus, ESSM can be further extended by the systematic description of atomic rules for added algebraic operations or attack capabilities.
Compared with the original strand space model, our extended framework has two advantages.
One is the formal description of algebraic properties. Traditional analysis ignores the nature of algebraic operations when there are algebraic operations in the protocol and cannot detect attacks carried out by attackers using algebraic operations. Our extension can search for this type of attack and expand the types of protocols that can be analysed.
The second is a custom description of attack capabilities. The traditional SSM is based on the Dolev-Yao attacker model, assuming that the cryptographic primitives are unbreakable. In fact, attackers may have attacks such as KCI attacks and weak password guessing. These are not considered in traditional analysis. In our extension, we can consider different problems according to the possible problems of the protocol. The attack models can be freely combined to find the problems in the protocol.


## 3.2. Algebraic Attribute Addition

The basic strand space model does not support algebraic operations (e.g., XOR or Abelian groups), and attackers have no way of locating attacks related to algebraic properties. Instead, a one-way function is used to model the XOR and Abelian groups abstractly, such that the strand space model can support protocol analysis using algebraic operations, and attackers can use algebraic operation strands to detect problems with algebraic operations in protocols.For the addition of different modules, we introduce new types of terms and functions. When the type of the term matches the type of the function parameter, the newly added strand can be applied. At the same time, the new type of strand is also compatible with the operations of traditional SSM attackers. For example, forNum type terms, the attacker can also perform operations such as generation and eavesdropping.


### 3.2.1. XOR Operation

The XOR operation requires the establishment of an algebraic model that satisfies the following operational relations. Fora,b,c∈Num,(1)a⊕0=a,a⊕0=a,a⊕b=b⊕a,a⊕b⊕c=a⊕b⊕c.We use a hash function combined with a new set of decryption semantics to achieve the XOR operation. Owing to the unidirectionality of the hash function, the attacker can constructxora,b when a and b are known. However, terms a and b cannot be obtained through xora,b.Definition 5 (XOR operation).
One-way functionxor:Num∗Num⟶Num; xora,b denotes the exclusive xor of terms a and b.
The attacker can generatexora,b through a and b, and if xora,b and b are known, the attacker can calculate a⊕b⊕b=a to obtain term a, which cannot be described by the hash function. Thus, a new model of the attacker’s derivation ability is needed.
We built an XOR operation module, which is shown in Table3. For the protocol containing the XOR operation, we can add an XOR operation semantic module to model the protocol. Attackers can obtain information in an algebraic operation.
In rule XOR-Z, we construct a constantz, which represents the zero element, which is included in the initial knowledge by the subject and attacker in the protocol description. In rule XOR-G, attackers can apply XOR to construct the XOR values of two known terms. In rule XOR-S, the attacker can obtain xorb,a using the known XOR value xora,b. Moreover, these two terms are independent in the strand space model, and the exchange law of the XOR operation can be constructed using this rule. In rule XOR-D, an attacker can obtain the second term b, by knowing the XOR value xora,b, and the first term a. In rule XOR-O, an attacker can obtain the term XOR from the zero element. In rule XOR-C, the attacker can apply the binding law to combine the XOR values of the three elements.
We do not have a decryption rule for the first term of the XOR model, because it can be implemented by applying the XOR-S and XOR-D rules.
Inferring that the attacker knowsxora,b and b, term a can be obtained using these known values. The attacker first applies the XOR-S rule −xora,b,+xorb,a, gets xorb,a, and passes the XOR-D rule −xorb,a,−b,+a to obtain term a.Table 3
Strands of XOR operation module.
Rule nameSpecificationStrandXOR-ZInitial knowledge+zXOR-GGenerate XOR terms−a,−b,+xora,bXOR-SCommutative rule of XOR−xora,b,+xorb,aXOR-DReflexive rule of XOR−xora,b,−a,+bXOR-ZObtains the term XOR with 0−xora,z,+aXOR-CAssociative rule of XOR operation−xorxora,b,c,+xora,xorb,c


### 3.2.2. Abelian Group Operation

In security protocols, the application of an Abelian group is embodied in the key agreement algorithms, DH, and the elliptic-curve DH (ECDH). Using the multiplicative group onZp∗ and the additive group on an elliptic curve, we analyse the properties of the Abelian group, describe the operation of the Abelian group in ESSM, and model the ability of attackers to obtain terms from the operation.We describe the semantics of the multiplication group onZp∗ as follows: for the primitive element g over Zp∗,(2)gxy≡gx∗ymodp,gx∗y≡gy∗xmodp,gx∗gy≡gy+xmodp,gx+y≡gy+xmodp.First, two one-way functions, add and mul, are defined to represent the addition and multiplication operations of the two variables.Definition 6 (add operation).
One-way functionadd:Z∗Z⟶Z; adda,b denotes the addition of terms a and b.Definition 7 (mul operation).
One-way functionmul:Z∗Z⟶Z; mula,b denotes multiplication of terms a and b.
Similar to the XOR operation, attackers can construct add and mul function values that support exchange to deduce the value of another element by knowing the whole function value and one element. We define these three algebraic properties as gen, swap, and decrypt, as shown in Table4.
For the equivalence relations in the Abelian group having different forms on both sides, we use the equivalence relationgxy≡gx∗y. Because it is impossible to describe the equivalence relation in the strand space model, a bidirectional derivation relationship should be considered, such as gxy≡gx∗y and gx∗gy≡gy+x. This equivalence relation is expressed as a bidirectional strand space model. For the subject and attacker of the protocol, we establish the semantic rules in Table 5.
We describe the DH key exchange protocol in the strand space by applying the semantics of the multiplication group onZp∗. Via the key exchange, the two parties can establish a shared key, expg,mulx,y. The strand representations of protocol roles A and B are as follows:(1)
InitiatorA’s strand: InitA,B,x=+expg,x,−expg,y,+mesexpg,mulx,y.(2)
ResponderB’s strand: RespA,B,y=−expg,x,+expg,y,−mesexpg,mulx,y.
In the role strand of this protocol, the third message betweenA and B is not trivial, because both parties need to obtain expg,mulx,y. The message is then encrypted and decrypted. Term expg,mulx,y is obtained by adding the semantics. Considering principal A as an example, the process of obtaining the shared key is as shown in Figure 3.
RoleA applies the DH-G rule to obtain the term expg,y. A obtains the term expexpg,y,x by combining the initial knowledge of x. DH-L1 rules are then applied to obtain the term expg,muly,x. Then, DH-S1 rules are applied to obtain the term expg,mulx,y. At this point, role A obtains the symmetric key established by both parties, and role B can obtain the term expg,mulx,y using similar methods. Roles A and B interact with the third node using the shared key.
Similarly, we establish the operation rules of the Abelian group on an elliptic curve, assuming thatP is a point on the elliptic curve E, and x,y∈Z. P has the following properties:(3)x×y×P=x∗y×P,x∗y×P=y∗x×P,x×P+y×P=x+y×P,x+y×P=y+x×P.
We define addition and multiplication on elliptic curves as ecadd and ecmul, which are distinguishable from add and mul which are defined above.Table 4
Strands of ADD and MUL operation module.
Rule nameSpecificationStrandADD-GGenerative addition terms−a,−b,+adda,bADD-SCommutative rule of addition−adda,b,+addb,aADD-DInverse rule of addition−adda,b,−a,+bMUL-GGenerative multiplication terms−a,−b,+mula,bMUL-SCommutative rule of multiplication−mula,b,+mulb,aMUL-DInverse rule of multiplication−mula,b,−a,+bTable 5
Strands of DH operation module.
Rule nameSpecificationStrandDH-KInitial knowledge+gDH-GPerform power module operation−a,−b,+expa,bDH-S1Commutative rule of multiplication−expg,mula,b,+expg,mulb,aDH-S2Commutative rule of addition−expg,adda,b,+expg,addb,aDH-L1Deduction rule L1−expexpg,a,b,+expg,mula,bDH-L2Deduction rule L2−expg,mula,b,+expexpg,a,bDH-R1Deduction rule R1−expg,mula,b,+expexpg,a,bDH-R2Deduction rule R2−expg,adda,b,+mulexpg,a,expg,bFigure 3
The path for legal agent to obtain shared key.Definition 8 (ecadd, ecmul operation).
One-way functionecadd:Point×Point⟶Point; ecmul:Z×Point⟶Point; ecadda,b denotes the addition operation of terms a and b of type point, and the term type obtained is point; ecmula,b represents multiplication operation of the term of type Z and the term of type point, and the term type obtained is point.
Similarly, the operation rules of the elliptic curve are established in Table6.Table 6
Strands of ECDH operation module.
Rule nameSpecificationStrandECDH-KInitial knowledge+PECDH-GPerform multiplication−a,−P,+ecmula,PECDH-S1Addition exchange rule−ecmuladda,b,P,+ecmuladdb,a,PECDH-S2Multiplication exchange rules−ecmulmula,b,P,+ecmulmulb,a,PECDH-L1Deduction rule L1−ecmula,ecmulb,P,+ecmulmula,b,PECDH-L2Deduction rule L2−ecaddecmula,P,ecmulb,P,+ecmuladda,b,PECDH-R1Deduction rule R1−ecmulmula,b,P,+ecmula,ecmulb,PECDH-R2Deduction rule R2−ecmuladda,b,P,+ecaddecmula,P,ecmulb,P


## 3.2.1. XOR Operation

The XOR operation requires the establishment of an algebraic model that satisfies the following operational relations. Fora,b,c∈Num,(1)a⊕0=a,a⊕0=a,a⊕b=b⊕a,a⊕b⊕c=a⊕b⊕c.We use a hash function combined with a new set of decryption semantics to achieve the XOR operation. Owing to the unidirectionality of the hash function, the attacker can constructxora,b when a and b are known. However, terms a and b cannot be obtained through xora,b.Definition 5 (XOR operation).
One-way functionxor:Num∗Num⟶Num; xora,b denotes the exclusive xor of terms a and b.
The attacker can generatexora,b through a and b, and if xora,b and b are known, the attacker can calculate a⊕b⊕b=a to obtain term a, which cannot be described by the hash function. Thus, a new model of the attacker’s derivation ability is needed.
We built an XOR operation module, which is shown in Table3. For the protocol containing the XOR operation, we can add an XOR operation semantic module to model the protocol. Attackers can obtain information in an algebraic operation.
In rule XOR-Z, we construct a constantz, which represents the zero element, which is included in the initial knowledge by the subject and attacker in the protocol description. In rule XOR-G, attackers can apply XOR to construct the XOR values of two known terms. In rule XOR-S, the attacker can obtain xorb,a using the known XOR value xora,b. Moreover, these two terms are independent in the strand space model, and the exchange law of the XOR operation can be constructed using this rule. In rule XOR-D, an attacker can obtain the second term b, by knowing the XOR value xora,b, and the first term a. In rule XOR-O, an attacker can obtain the term XOR from the zero element. In rule XOR-C, the attacker can apply the binding law to combine the XOR values of the three elements.
We do not have a decryption rule for the first term of the XOR model, because it can be implemented by applying the XOR-S and XOR-D rules.
Inferring that the attacker knowsxora,b and b, term a can be obtained using these known values. The attacker first applies the XOR-S rule −xora,b,+xorb,a, gets xorb,a, and passes the XOR-D rule −xorb,a,−b,+a to obtain term a.Table 3
Strands of XOR operation module.
Rule nameSpecificationStrandXOR-ZInitial knowledge+zXOR-GGenerate XOR terms−a,−b,+xora,bXOR-SCommutative rule of XOR−xora,b,+xorb,aXOR-DReflexive rule of XOR−xora,b,−a,+bXOR-ZObtains the term XOR with 0−xora,z,+aXOR-CAssociative rule of XOR operation−xorxora,b,c,+xora,xorb,c


## 3.2.2. Abelian Group Operation

In security protocols, the application of an Abelian group is embodied in the key agreement algorithms, DH, and the elliptic-curve DH (ECDH). Using the multiplicative group onZp∗ and the additive group on an elliptic curve, we analyse the properties of the Abelian group, describe the operation of the Abelian group in ESSM, and model the ability of attackers to obtain terms from the operation.We describe the semantics of the multiplication group onZp∗ as follows: for the primitive element g over Zp∗,(2)gxy≡gx∗ymodp,gx∗y≡gy∗xmodp,gx∗gy≡gy+xmodp,gx+y≡gy+xmodp.First, two one-way functions, add and mul, are defined to represent the addition and multiplication operations of the two variables.Definition 6 (add operation).
One-way functionadd:Z∗Z⟶Z; adda,b denotes the addition of terms a and b.Definition 7 (mul operation).
One-way functionmul:Z∗Z⟶Z; mula,b denotes multiplication of terms a and b.
Similar to the XOR operation, attackers can construct add and mul function values that support exchange to deduce the value of another element by knowing the whole function value and one element. We define these three algebraic properties as gen, swap, and decrypt, as shown in Table4.
For the equivalence relations in the Abelian group having different forms on both sides, we use the equivalence relationgxy≡gx∗y. Because it is impossible to describe the equivalence relation in the strand space model, a bidirectional derivation relationship should be considered, such as gxy≡gx∗y and gx∗gy≡gy+x. This equivalence relation is expressed as a bidirectional strand space model. For the subject and attacker of the protocol, we establish the semantic rules in Table 5.
We describe the DH key exchange protocol in the strand space by applying the semantics of the multiplication group onZp∗. Via the key exchange, the two parties can establish a shared key, expg,mulx,y. The strand representations of protocol roles A and B are as follows:(1)
InitiatorA’s strand: InitA,B,x=+expg,x,−expg,y,+mesexpg,mulx,y.(2)
ResponderB’s strand: RespA,B,y=−expg,x,+expg,y,−mesexpg,mulx,y.
In the role strand of this protocol, the third message betweenA and B is not trivial, because both parties need to obtain expg,mulx,y. The message is then encrypted and decrypted. Term expg,mulx,y is obtained by adding the semantics. Considering principal A as an example, the process of obtaining the shared key is as shown in Figure 3.
RoleA applies the DH-G rule to obtain the term expg,y. A obtains the term expexpg,y,x by combining the initial knowledge of x. DH-L1 rules are then applied to obtain the term expg,muly,x. Then, DH-S1 rules are applied to obtain the term expg,mulx,y. At this point, role A obtains the symmetric key established by both parties, and role B can obtain the term expg,mulx,y using similar methods. Roles A and B interact with the third node using the shared key.
Similarly, we establish the operation rules of the Abelian group on an elliptic curve, assuming thatP is a point on the elliptic curve E, and x,y∈Z. P has the following properties:(3)x×y×P=x∗y×P,x∗y×P=y∗x×P,x×P+y×P=x+y×P,x+y×P=y+x×P.
We define addition and multiplication on elliptic curves as ecadd and ecmul, which are distinguishable from add and mul which are defined above.Table 4
Strands of ADD and MUL operation module.
Rule nameSpecificationStrandADD-GGenerative addition terms−a,−b,+adda,bADD-SCommutative rule of addition−adda,b,+addb,aADD-DInverse rule of addition−adda,b,−a,+bMUL-GGenerative multiplication terms−a,−b,+mula,bMUL-SCommutative rule of multiplication−mula,b,+mulb,aMUL-DInverse rule of multiplication−mula,b,−a,+bTable 5
Strands of DH operation module.
Rule nameSpecificationStrandDH-KInitial knowledge+gDH-GPerform power module operation−a,−b,+expa,bDH-S1Commutative rule of multiplication−expg,mula,b,+expg,mulb,aDH-S2Commutative rule of addition−expg,adda,b,+expg,addb,aDH-L1Deduction rule L1−expexpg,a,b,+expg,mula,bDH-L2Deduction rule L2−expg,mula,b,+expexpg,a,bDH-R1Deduction rule R1−expg,mula,b,+expexpg,a,bDH-R2Deduction rule R2−expg,adda,b,+mulexpg,a,expg,bFigure 3
The path for legal agent to obtain shared key.Definition 8 (ecadd, ecmul operation).
One-way functionecadd:Point×Point⟶Point; ecmul:Z×Point⟶Point; ecadda,b denotes the addition operation of terms a and b of type point, and the term type obtained is point; ecmula,b represents multiplication operation of the term of type Z and the term of type point, and the term type obtained is point.
Similarly, the operation rules of the elliptic curve are established in Table6.Table 6
Strands of ECDH operation module.
Rule nameSpecificationStrandECDH-KInitial knowledge+PECDH-GPerform multiplication−a,−P,+ecmula,PECDH-S1Addition exchange rule−ecmuladda,b,P,+ecmuladdb,a,PECDH-S2Multiplication exchange rules−ecmulmula,b,P,+ecmulmulb,a,PECDH-L1Deduction rule L1−ecmula,ecmulb,P,+ecmulmula,b,PECDH-L2Deduction rule L2−ecaddecmula,P,ecmulb,P,+ecmuladda,b,PECDH-R1Deduction rule R1−ecmulmula,b,P,+ecmula,ecmulb,PECDH-R2Deduction rule R2−ecmuladda,b,P,+ecaddecmula,P,ecmulb,P


## 3.3. Attacker Capability

In this section, we extend the attacker attack model using modularization. Based on the classic Dolev-Yao model, in the first section, we model a variety of attacks based on algebraic properties, including small group attacks, Lim-Lee attacks, and others that need to be combined with group properties. The second section introduces the extension of the key-compromise impersonation (KCI) attack, which can describe the situation of specific information exposure. The third section considers the influence of guessing attacks on security protocols and formalizes the attack.


### 3.3.1. Attack Based on Algebraic Form

In this section, we describe the algebraic attacks which have been already shown to exist, including subgroup attacks and Lim-Lee attacks. We reveal that the attacker can destroy algebraic properties in a specific environment to obtain secret information.(1) Small-Group Attack. The small-group attack was first proposed by van Oorschot and Wiener [30]. This type of attack takes advantage of the structural characteristics of a group to replace the key negotiated by both sides of the communication. The negotiated key can be obtained without affecting the normal communication between the two sides.In the implementation, if the Abelian group used in the protocol isZp∗, order p−1 is a composite number. If the order of group G used in the protocol is a composite number, n=r∗ω, assuming that r is a small factor of n, and G has subgroups gt∗, meaning that gt is a multiplicative group whose generator order is r. There are only r elements in this group.If the shared secret key negotiated by both parties is in groupgt∗, the attacker can guess the real key exhaustively when the two parties communicate with each other using key encryption.Considering the simple DH as an example, the attack process is as follows:(1)
RoleA initiates DH key exchange with role B, generates a random number x, and calculates the public key, gx.(2)
The attacker interceptsgx and calculates gωx sent to B.(3)
RoleB receives message gωx. Subsequently, random number y is generated and the public key gy is calculated and sent to C. The negotiated key is calculated as ZBA=gωxy=gωxy.(4)
The attacker interceptsgy and calculates gωy sent to A.(5)
RoleA receives a message gωy. Then, the key is calculated as ZAB=gωyx=gωxy.(6)
RolesA and B use ZAB as a session key for message passing, and the attacker eavesdrops the encrypted message and guesses to verify the session key, gωxy.Assuming that the order of groupG used in the protocol is a composite number, the attacker can decompose it to obtain ω. Then, for all gxω for symmetric key messages, attackers can obtain x and key gx by the exhaustive computation of gωx. We ignore the details of the exhaustive computation and assume that the attacker can decompose a large integer, n. We model the derivation relationship of the attacker in Table 7. For the operation relationship of DH, we extend the derivation in the previous section.Table 7
Strands of small group attack module.
Rule nameSpecificationStrandSS-GGenerating elements on subgroups−expg,a,+expg,mula,ωSS-VGuess the elements on a subgroup−mesexpg,mula,ω,+expg,mula,ωRule SS-G means that the attacker will use the term on groupexpg,a through the operation of the ω-power module on the subgroups to obtain terms expg,mula,ω. The SS-V rule indicates that the attacker obtains the elements, expg,mula,ω, on the subgroup via exhaustive verification using the elements in the subgroup as the term for key encryption. The type of term a is not limited. For example, the key negotiated by both sides of DH protocol under the attack of small groups can be expg,mulmulx,y,ω. In this case, a in the formula means mulx,y.(2) Lim-Lee Attack. Owing to the discovery of small group attacks, a preventive measure uses the prime, q, subgroup of Zp∗. However, Lim and Lee found an attack method having prime order [31] against the group. Thus, the attacker can obtain the private key of the responder role by actively participating in the operation of the protocol.Taking simple DH as an example, the attack process is as follows:(1)
AttackerC initiates a DH key exchange with role B to generate random numbers x∈Zq∗ and calculate the public key, gx. Simultaneously, β is generated. The order of β is r and it satisfies r|p−1/q. C sends β∗gx to role B.(2)
RoleB receives the message, β∗gx. Subsequently, random number, y, is generated, and the public key, gy, is calculated and sent to C. The negotiated key is ZBC=β∗gxy=βy∗gxy.(3)
AttackerC receives gy and calculates ZCB=gyx=gx∗y=ZBC/βy, because βy is the only r available for the attacker to use to obtain the correct partial information, ymodr, by verification.(4)
By tryingβ corresponding to different r, the attacker can obtain equations with different moduli, and the complete information of y can be obtained using the Chinese remainder theorem.Assuming that the group used in the protocol is a prime group of orderq and that the attacker can participate in and initiate the protocol, we define a strand space model for the attacker to execute the Lim-Lee attack in Table 8.Table 8
Strands of Lim-Lee attack module.
Rule nameSpecificationStrandLL-GGenerating elements outside the group−expg,a,+mulβ,expg,aLL-VGuess the elements of validationmesexpmulβ,expg,a,y,+modyLL-CComputing termy using CRT−mody,+yRule LL-G converts the elements,expg,a, of a group beyond the group to obtain mulβ,expg,a, where the order of β is r and it satisfies r|p−1/q. Rule LL-V obtains the information of ymodr by guessing its verification, ignoring the specific guessing process, and it assumes that the attacker’s guessing ability can calculate the data of scale r. Rule LL-C uses the Chinese remainder theorem to recover the complete information of y, thereby creating a sample. Moreover, the attacker must use different ri of βi, conduct intrusion behaviours, and obtain one term, ymodri, at a time. Through different ri, it combines complete information on y. We abstract this process, and, to preserve the principle of attack, we express this process as the term, y, calculated by ymodri. The attacker only needs to execute one intrusion to obtain term y.


### 3.3.2. KCI Attack

It is possible for an attacker to break through a device to obtain its long-term private key, or in a protocol using a smart card, to obtain the smart card of a legitimate subject leading to a smart-card loss attack. We define this behaviour semantically and describe it as a KCI attack.An attacker can obtain the long-term private key, session key, or some state in communication by corroding the agent or via cryptanalysis. We model this ability as a message,mes, which the attacker steals from the role strand. Hence, the derivation relation of some information in the message that cannot be obtained directly can then be obtained. The term, key, can be symmetric or asymmetric, encrypted or hashed, or more complex. The attackable information must be included in the role strands. Thus, this method has a certain applicability that further indicates the situation of secret information disclosure (e.g., role long-term private key, session key, and smart card). The corresponding disclosure rules must be generated alongside specific protocols. Here, only the framework of the attacker rules is given in Table 9.Table 9
Strands of KCI attack module.
Rule nameSpecificationStrandRevealGet some key from encryption−meskey,+keyRevealGet some terms from encryption−meskey,+mesRevealGet some keys from hash−hashkey,+keyNote that these rules must be implemented in combination with specific protocol role strands. For details, refer to the KCI attack and impersonal attack in the MTI protocol in the next section, as well as the analysis of the three-factor authentication protocol. For specific protocols, the terms of disclosure can be specified.


### 3.3.3. Guessing Attack

Guessing attacks include two parts. First, an attacker intercepts a message related to the value to be guessed. Then, the attacker matches the correct guess value by traversing the dictionary. The default value to be guessed is a password. For the first part, the attacker must have a detection method that can verify the conjecture.(i)
Password as encryption keyIf the attacker can obtain a message pair similar toterm and termpw, the attacker can generate termpw′ by constructing pw′ and encrypting semantic E to verify that the generated key pw′ is correct by comparing whether termpw′ and termpw are consistent.(ii)
Password contained in a hashIf the attacker can obtain ahashpw,term1,…,termn and knows termi1≤i≤n, the attacker can guess the password, pw′, and construct a hash, hashpw′,term1,…,termn. The original hash value is compared to verify the guess.In the second part, the success rate of guess attack depends on the complexity of the password set by the agent and the size of the dictionary used. Theoretically, if the password is in the dictionary, it can be successfully cracked. In the theoretical description of guessing attacks, the attacker has enough elements in the dictionary to carry out a guessing attack on any message that meets the requirements.However, the situation in the real protocol may be more complex. For example, the password is used as the key after hashing or multiple hashings, which can be regarded as the multiple effects of the basic situation. In short, the attacker can crack the weak password after obtaining a message that meets the guessing condition. The formal description of this ability is shown in Table10.Table 10
Strands of guessing attack module.
Rule nameSpecificationStrandGS-EGuess password from encryption−apw,−a,+pwGS-HGuess password from hash−hasha,pw,−a,+pwIn accordance with the description of a KCI attack, the definition of the attacker strand of a guessing attack should be combined with a specific protocol. In rules GS-E and GS-H, only the description method of the guessing attack is described. It is thus necessary to combine the strand of the subject to customize the ability of the attacker to carry out a guessing attack.


## 3.3.1. Attack Based on Algebraic Form

In this section, we describe the algebraic attacks which have been already shown to exist, including subgroup attacks and Lim-Lee attacks. We reveal that the attacker can destroy algebraic properties in a specific environment to obtain secret information.(1) Small-Group Attack. The small-group attack was first proposed by van Oorschot and Wiener [30]. This type of attack takes advantage of the structural characteristics of a group to replace the key negotiated by both sides of the communication. The negotiated key can be obtained without affecting the normal communication between the two sides.In the implementation, if the Abelian group used in the protocol isZp∗, order p−1 is a composite number. If the order of group G used in the protocol is a composite number, n=r∗ω, assuming that r is a small factor of n, and G has subgroups gt∗, meaning that gt is a multiplicative group whose generator order is r. There are only r elements in this group.If the shared secret key negotiated by both parties is in groupgt∗, the attacker can guess the real key exhaustively when the two parties communicate with each other using key encryption.Considering the simple DH as an example, the attack process is as follows:(1)
RoleA initiates DH key exchange with role B, generates a random number x, and calculates the public key, gx.(2)
The attacker interceptsgx and calculates gωx sent to B.(3)
RoleB receives message gωx. Subsequently, random number y is generated and the public key gy is calculated and sent to C. The negotiated key is calculated as ZBA=gωxy=gωxy.(4)
The attacker interceptsgy and calculates gωy sent to A.(5)
RoleA receives a message gωy. Then, the key is calculated as ZAB=gωyx=gωxy.(6)
RolesA and B use ZAB as a session key for message passing, and the attacker eavesdrops the encrypted message and guesses to verify the session key, gωxy.Assuming that the order of groupG used in the protocol is a composite number, the attacker can decompose it to obtain ω. Then, for all gxω for symmetric key messages, attackers can obtain x and key gx by the exhaustive computation of gωx. We ignore the details of the exhaustive computation and assume that the attacker can decompose a large integer, n. We model the derivation relationship of the attacker in Table 7. For the operation relationship of DH, we extend the derivation in the previous section.Table 7
Strands of small group attack module.
Rule nameSpecificationStrandSS-GGenerating elements on subgroups−expg,a,+expg,mula,ωSS-VGuess the elements on a subgroup−mesexpg,mula,ω,+expg,mula,ωRule SS-G means that the attacker will use the term on groupexpg,a through the operation of the ω-power module on the subgroups to obtain terms expg,mula,ω. The SS-V rule indicates that the attacker obtains the elements, expg,mula,ω, on the subgroup via exhaustive verification using the elements in the subgroup as the term for key encryption. The type of term a is not limited. For example, the key negotiated by both sides of DH protocol under the attack of small groups can be expg,mulmulx,y,ω. In this case, a in the formula means mulx,y.(2) Lim-Lee Attack. Owing to the discovery of small group attacks, a preventive measure uses the prime, q, subgroup of Zp∗. However, Lim and Lee found an attack method having prime order [31] against the group. Thus, the attacker can obtain the private key of the responder role by actively participating in the operation of the protocol.Taking simple DH as an example, the attack process is as follows:(1)
AttackerC initiates a DH key exchange with role B to generate random numbers x∈Zq∗ and calculate the public key, gx. Simultaneously, β is generated. The order of β is r and it satisfies r|p−1/q. C sends β∗gx to role B.(2)
RoleB receives the message, β∗gx. Subsequently, random number, y, is generated, and the public key, gy, is calculated and sent to C. The negotiated key is ZBC=β∗gxy=βy∗gxy.(3)
AttackerC receives gy and calculates ZCB=gyx=gx∗y=ZBC/βy, because βy is the only r available for the attacker to use to obtain the correct partial information, ymodr, by verification.(4)
By tryingβ corresponding to different r, the attacker can obtain equations with different moduli, and the complete information of y can be obtained using the Chinese remainder theorem.Assuming that the group used in the protocol is a prime group of orderq and that the attacker can participate in and initiate the protocol, we define a strand space model for the attacker to execute the Lim-Lee attack in Table 8.Table 8
Strands of Lim-Lee attack module.
Rule nameSpecificationStrandLL-GGenerating elements outside the group−expg,a,+mulβ,expg,aLL-VGuess the elements of validationmesexpmulβ,expg,a,y,+modyLL-CComputing termy using CRT−mody,+yRule LL-G converts the elements,expg,a, of a group beyond the group to obtain mulβ,expg,a, where the order of β is r and it satisfies r|p−1/q. Rule LL-V obtains the information of ymodr by guessing its verification, ignoring the specific guessing process, and it assumes that the attacker’s guessing ability can calculate the data of scale r. Rule LL-C uses the Chinese remainder theorem to recover the complete information of y, thereby creating a sample. Moreover, the attacker must use different ri of βi, conduct intrusion behaviours, and obtain one term, ymodri, at a time. Through different ri, it combines complete information on y. We abstract this process, and, to preserve the principle of attack, we express this process as the term, y, calculated by ymodri. The attacker only needs to execute one intrusion to obtain term y.


## 3.3.2. KCI Attack

It is possible for an attacker to break through a device to obtain its long-term private key, or in a protocol using a smart card, to obtain the smart card of a legitimate subject leading to a smart-card loss attack. We define this behaviour semantically and describe it as a KCI attack.An attacker can obtain the long-term private key, session key, or some state in communication by corroding the agent or via cryptanalysis. We model this ability as a message,mes, which the attacker steals from the role strand. Hence, the derivation relation of some information in the message that cannot be obtained directly can then be obtained. The term, key, can be symmetric or asymmetric, encrypted or hashed, or more complex. The attackable information must be included in the role strands. Thus, this method has a certain applicability that further indicates the situation of secret information disclosure (e.g., role long-term private key, session key, and smart card). The corresponding disclosure rules must be generated alongside specific protocols. Here, only the framework of the attacker rules is given in Table 9.Table 9
Strands of KCI attack module.
Rule nameSpecificationStrandRevealGet some key from encryption−meskey,+keyRevealGet some terms from encryption−meskey,+mesRevealGet some keys from hash−hashkey,+keyNote that these rules must be implemented in combination with specific protocol role strands. For details, refer to the KCI attack and impersonal attack in the MTI protocol in the next section, as well as the analysis of the three-factor authentication protocol. For specific protocols, the terms of disclosure can be specified.


## 3.3.3. Guessing Attack

Guessing attacks include two parts. First, an attacker intercepts a message related to the value to be guessed. Then, the attacker matches the correct guess value by traversing the dictionary. The default value to be guessed is a password. For the first part, the attacker must have a detection method that can verify the conjecture.(i)
Password as encryption keyIf the attacker can obtain a message pair similar toterm and termpw, the attacker can generate termpw′ by constructing pw′ and encrypting semantic E to verify that the generated key pw′ is correct by comparing whether termpw′ and termpw are consistent.(ii)
Password contained in a hashIf the attacker can obtain ahashpw,term1,…,termn and knows termi1≤i≤n, the attacker can guess the password, pw′, and construct a hash, hashpw′,term1,…,termn. The original hash value is compared to verify the guess.In the second part, the success rate of guess attack depends on the complexity of the password set by the agent and the size of the dictionary used. Theoretically, if the password is in the dictionary, it can be successfully cracked. In the theoretical description of guessing attacks, the attacker has enough elements in the dictionary to carry out a guessing attack on any message that meets the requirements.However, the situation in the real protocol may be more complex. For example, the password is used as the key after hashing or multiple hashings, which can be regarded as the multiple effects of the basic situation. In short, the attacker can crack the weak password after obtaining a message that meets the guessing condition. The formal description of this ability is shown in Table10.Table 10
Strands of guessing attack module.
Rule nameSpecificationStrandGS-EGuess password from encryption−apw,−a,+pwGS-HGuess password from hash−hasha,pw,−a,+pwIn accordance with the description of a KCI attack, the definition of the attacker strand of a guessing attack should be combined with a specific protocol. In rules GS-E and GS-H, only the description method of the guessing attack is described. It is thus necessary to combine the strand of the subject to customize the ability of the attacker to carry out a guessing attack.


## 4. Implementation and Experimental Results

We implemented support for ESSM and applied Scyther to test a set of protocols that use algebraic operations and an extended attack capability. In this section, we describe our implementation and experimental results.


### 4.1. Implementation

We implemented the ESSM model using Scyther (version 1.1.3). Our implementation used auxiliary rules as additional input, combined with the definition of the protocol body to form a Security Protocol Description Language (SPDL) file as the input for Scyther model checking. We expanded the original protocol in algebraic operation and attack ability including (1) the running rules of the protocol body, (2) added algebraic operation rules, (3) added attacker rules, and (4) defining the security attributes of the check. Additionally, options can be added to Scyther, such as outputting proof procedures and limiting the number of computing processes.Our implementation followed the ESSM construction described in Section3 by precisely formalizing the algebraic properties and the attacker’s special attack ability.Considering the XOR attribute as an example, the following describes the process of converting the atomic rule of the XOR operation into the auxiliary rule input of Scyther.We used an auxiliary protocol to represent an algebraic operation or attack capability module. Under each auxiliary protocol, each role represents an atomic rule. Attackers call a combination of several rules in different auxiliary protocols to implement their attack behaviours. Specific auxiliary protocol input files should be established according to specific protocol interactions for some special attacks, such as key disclosure and guessing attacks.Moreover, without these auxiliary protocols, the interaction of protocol entities modelled by the original Scyther can work normally. However, Scyther cannot find the problems in the protocol. Compared with the original protocol modelling, using ESSM to model and analyse the protocol can find potential algebraic logic problems and special attack paths within the protocol.


### 4.2. Sample Protocol

We used extended strand space semantics to describe several protocols (e.g., three-factor authentication). We found known attack paths and revealed new ones.Taking the three-factor authentication protocol proposed by Zhang et al. [32] as an example, two attack paths were successfully analysed using the extended algebraic property semantics and the attacker’s ability. One was found by Mao et al. [33], and the other is the undiscovered attack path. The discovery of the two attack paths combined the XOR, key-compromise attack, and guessing attack ability rules added to the ESSM.


#### 4.2.1. Protocol Description

During the registration stage, the user sends the protected identity information to the server, and the server stores it and issues a smart card for authentication. It should be noted that the communication in the registration phase is based on the secure channel, and the attacker cannot obtain any information in the registration phase.(1)
UserU selects identity ID and password PW and inputs biometric B to the terminal. The terminal calculates C1=hID,PW,hBioB and generates random number r1 for calculating C2=B⊕r1. User U sends a registration request message C1,C2 to server S.(2)
After receiving the registration request message from userU, server S uses the server’s private key, s, to calculate M=hhBioC2‖s, generates random number r2, and calculates W=hhBioC2⊕r2, X=hIDSC‖C1‖M⊕r2, and Y=M⊕C1. The server stores C2,W0,W in the database and initializes W0 to null. The server writes to the smart card IDSC,h⋅,hBio⋅,X,Y and gives it to user U.(3)
Z=r1⊕hBioB is calculated after receiving the smart card. Z is written to it for completing registration.The login authentication phase is described as follows:(1)
UserU inputs accounts for ID′, password PW′, and biometric B′ and inserts the smart card at the same time.(2)
UserU generates a random number r3 and calculates C1∗=hID′PW′hBioB′, M∗=Y⊕hC1∗, r2∗=X⊕hIDSCC1∗M∗, and r1∗=Z⊕hBioB.(3)
C3=hBioB′⊕r1∗⊕r2∗, C4=B′⊕r1∗⊕hM∗‖r3, and C5=r3⊕hBioB′⊕r1∗ are calculated to send a login request C3,C4,C5 to server S.(4)
The server performs dynamic verification by matchingC3 and the data in the database. For more details, please refer to the original article [32].(5)
ServerS generates a random number r4, calculates M′=hhBioC2‖s, r3∗=C5⊕hBioC2, and B′⊕r1∗=C4⊕hM′‖r3∗, and checks B⊕r1∗ and C2. If the validation passes, the server computes C6=r4⊕hB⊕r1∗ and C7=hB⊕r1∗r3∗r4∗. Both C6,C7 are sent to user U.(6)
UserU receives C6,C7 and calculates r4∗=C6⊕hB⊕r1∗, verifying C7=?hB⊕r1∗r3∗r4∗. After verification, the user calculates the session key, SK=hM∗r3r4∗, and C8=hhBioB⊕r1∗⊕r4∗⊕r4∗, and sends the authentication message, C8, to the server.(7)
Server receivesC8 after validation and accepts session key SK after successful verification; then it sends a key confirmation message, C9=hSK‖r4, to the user.(8)
Server receivesC9 after validation. After successful verification, both parties establish a common session key, SK.


#### 4.2.2. Strand Space Analysis of Protocol

We used the XOR operation in this protocol. Mao’s analysis of the protocol included smart card and guess attacks. We added the corresponding key-compromise and guess attack modules. The behaviours of the main body of the protocol are described as shown in Figure4.Figure 4
Role strands of 3FA.The terms are defined as follows:C1=hIDu,PW,HbioB, C2=xorB,r1, M=hHbioc2,s, X=xorhIDs,c1,M,r2, Y=xorM,c1, Z=xorr1,HbioB, SmartCard=IDs,X,Y,Z, C3=HbioxorB,r1,r2, C4=xorB,r1,hM,r3, C5=xorr3,HbioxorB,r1, C6=xorr4,hxorB,r1, C7=hxorB,r1,r3,r4, SK=hM,r3,r4, C8=hxorHbioxorB,r1,r4,r4, and C9=hSK,r4.In [33], the attack on user ID and PW required the attacker to obtain the user’s smart card, know the user’s biometrics, and could guess attacks. Using the framework of key-compromise and guessing attacks defined in the previous section, combined with the principal behaviours of the protocol, we modelled the attacker’s ability.The attacker knows the user’s biometrics and smart cards. For the first time, biometrics appear in the first node. The smart card is divided into two parts.Z can be obtained via the XOR of r1 and HbioB in the first node, and the rest is sent to the user at the second node on the server. Therefore, we describe an attacker’s key-compromise attack on smart cards and biometrics as Reveal:(i)
Reveal:−C1,C2kUser,Server,−SmartCardkUser,Server,+SmartCard,B.Modelling guessing attacks requires consideration of the terms, includingIDu and password. Term C1=hIDu,PW,HbioB contains IDu and password. Furthermore, we need to obtain term B to estimate C1. Because of term Y=xorM,C1, the known terms C1 and Y can obtain M by using rule XOR-D, thus conjecturing M. Two effective guessing chains can be obtained by constantly exploring the possible guessing paths. For example, in the first guess chain, we provided a set of guess values for IDu and PW, IDuGuess and PWGuess, respectively. Then, combined with term B, C1 and the conjecture can be obtained using C1Guess=hIDuGuess,PWGuess,HbioB. Unless we obtain the conjecture value of C4, we cannot determine if the conjecture value is successful by comparison.Through two guessing chains shown in Figure5, the rules of attacker guessing attack are stated as follows:(1)
GS-1:−C3,B,Y,IDsc,X,r1,+PW,IDu.(2)
GS-2:−C4,B,Y,r1,r3,+PW,IDu.Figure 5
Two guessing chains of Zhang’s protocol.Thesmartcard and B obtained by combining guessing rules and key disclosures can guess the user’s ID and password. The process is as follows:Path 1 (Figure6)(1)
The attacker obtainssmartcard and B using the Reveal rule.(2)
XOR-D rule−xorr1,HbioB,−HbioB,+r1 is applied to obtain term r1.(3)
F rule −C3 is applied to obtain term C3.(4)
According to the GS-1 rule, usingIDsc, X, Y, B is obtained by Reveal, r1 is obtained by XOR operation, and C3 is eavesdropped using the normal protocol process. A guessing attack is carried out to obtain the terms, ID and PW, of the attacker.Path 2 (Figure7)(1)
The attacker obtainssmartcard and B using the Reveal rule.(2)
XOR-D rule−xorr1,HbioB,−HbioB,+r1 is applied to obtain term r1.(3)
HbioxorB,r1 is constructed by B and r1.(4)
XOR-D rule−xorr3,HbioxorB,r1,−HbioxorB,r1,+r3 is applied to obtain term r3.(5)
TheF receive rule −C4 is applied to obtain term C4.(6)
According to the GS-2 rule, usingY and B obtained by Reveal, r1 and r3 obtained by the XOR operation and C4 from normal protocol flow are used to carry out a guessing attack to obtain the legal user’s term ID and PW.Figure 6
Attack path 1 of Zhang’s protocol.Figure 7
Attack path 2 of Zhang’s protocol.The first path was first discovered by Mao, and the second attack path was discovered by our addition of semantics to ESSM for the first time.


### 4.3. Experiment

We make a formal analysis of six groups of protocols, including TMN protocol [34], MTI-C (1), MTI-A (0), and MTI-C (0) in MTI protocol family [35], WPA-PSK protocol [36] in 802.11i standard, and three-factor authentication protocol proposed by Zhang.We applied our method to a group of protocols using algebraic logic or special attack ideas. The results obtained by running our implementation on Scyther v. 1.1.3 are presented in Table11, which lists the analysis results using the original Scyther and using ESSM modelling, including the declaration of security attributes and the number of search states.Table 11
Experiment result of several protocols.
ProtocolOriginal modelESSM modelSearch queriesDetected attacksSemantics usedSearch queriesDetected attacksTMN2658SafeXOR191948Algebraic attackMTI-C (1)263550SafeDH SS493270Small subgroup attackMTI-A (0)1649SafeDH KCI331160Impersonal attackMTI-C (0)322SafeDH KCI2585KCI attackWPA-PSK269SafeGuess55446Guessing attackZhang’s5684SafeXOR KCI Guess6349113Combination attackThe code restores the process of protocol interaction and abstracts the storage verification process of the server. We then declare the confidentiality of ID and PW. By adding auxiliary protocols (e.g., Smartcard Lost, XOR operation, and Offline Password Guess), two paths not meeting the confidentiality requirements can be automatically searched.Through the experimental results, we can find that the search path of the model search after adding ESSM semantics is richer, more attacks can be found, and the protocol environment can be restored more realistically. The increase of search path shows two facts.(1)
The semantic extension of ESSM is real and effective and has certain effect on many types of protocols.(2)
The contrast of the experimental results before and after the expansion is too large, which leads to the state explosion problem to a certain extent. The current model detection technology still has no effective solution to the state explosion problem, especially for algebraic operations.The semantic extension of ESSM is real and effective and has certain effect on many protocols.


## 4.1. Implementation

We implemented the ESSM model using Scyther (version 1.1.3). Our implementation used auxiliary rules as additional input, combined with the definition of the protocol body to form a Security Protocol Description Language (SPDL) file as the input for Scyther model checking. We expanded the original protocol in algebraic operation and attack ability including (1) the running rules of the protocol body, (2) added algebraic operation rules, (3) added attacker rules, and (4) defining the security attributes of the check. Additionally, options can be added to Scyther, such as outputting proof procedures and limiting the number of computing processes.Our implementation followed the ESSM construction described in Section3 by precisely formalizing the algebraic properties and the attacker’s special attack ability.Considering the XOR attribute as an example, the following describes the process of converting the atomic rule of the XOR operation into the auxiliary rule input of Scyther.We used an auxiliary protocol to represent an algebraic operation or attack capability module. Under each auxiliary protocol, each role represents an atomic rule. Attackers call a combination of several rules in different auxiliary protocols to implement their attack behaviours. Specific auxiliary protocol input files should be established according to specific protocol interactions for some special attacks, such as key disclosure and guessing attacks.Moreover, without these auxiliary protocols, the interaction of protocol entities modelled by the original Scyther can work normally. However, Scyther cannot find the problems in the protocol. Compared with the original protocol modelling, using ESSM to model and analyse the protocol can find potential algebraic logic problems and special attack paths within the protocol.


## 4.2. Sample Protocol

We used extended strand space semantics to describe several protocols (e.g., three-factor authentication). We found known attack paths and revealed new ones.Taking the three-factor authentication protocol proposed by Zhang et al. [32] as an example, two attack paths were successfully analysed using the extended algebraic property semantics and the attacker’s ability. One was found by Mao et al. [33], and the other is the undiscovered attack path. The discovery of the two attack paths combined the XOR, key-compromise attack, and guessing attack ability rules added to the ESSM.


### 4.2.1. Protocol Description

During the registration stage, the user sends the protected identity information to the server, and the server stores it and issues a smart card for authentication. It should be noted that the communication in the registration phase is based on the secure channel, and the attacker cannot obtain any information in the registration phase.(1)
UserU selects identity ID and password PW and inputs biometric B to the terminal. The terminal calculates C1=hID,PW,hBioB and generates random number r1 for calculating C2=B⊕r1. User U sends a registration request message C1,C2 to server S.(2)
After receiving the registration request message from userU, server S uses the server’s private key, s, to calculate M=hhBioC2‖s, generates random number r2, and calculates W=hhBioC2⊕r2, X=hIDSC‖C1‖M⊕r2, and Y=M⊕C1. The server stores C2,W0,W in the database and initializes W0 to null. The server writes to the smart card IDSC,h⋅,hBio⋅,X,Y and gives it to user U.(3)
Z=r1⊕hBioB is calculated after receiving the smart card. Z is written to it for completing registration.The login authentication phase is described as follows:(1)
UserU inputs accounts for ID′, password PW′, and biometric B′ and inserts the smart card at the same time.(2)
UserU generates a random number r3 and calculates C1∗=hID′PW′hBioB′, M∗=Y⊕hC1∗, r2∗=X⊕hIDSCC1∗M∗, and r1∗=Z⊕hBioB.(3)
C3=hBioB′⊕r1∗⊕r2∗, C4=B′⊕r1∗⊕hM∗‖r3, and C5=r3⊕hBioB′⊕r1∗ are calculated to send a login request C3,C4,C5 to server S.(4)
The server performs dynamic verification by matchingC3 and the data in the database. For more details, please refer to the original article [32].(5)
ServerS generates a random number r4, calculates M′=hhBioC2‖s, r3∗=C5⊕hBioC2, and B′⊕r1∗=C4⊕hM′‖r3∗, and checks B⊕r1∗ and C2. If the validation passes, the server computes C6=r4⊕hB⊕r1∗ and C7=hB⊕r1∗r3∗r4∗. Both C6,C7 are sent to user U.(6)
UserU receives C6,C7 and calculates r4∗=C6⊕hB⊕r1∗, verifying C7=?hB⊕r1∗r3∗r4∗. After verification, the user calculates the session key, SK=hM∗r3r4∗, and C8=hhBioB⊕r1∗⊕r4∗⊕r4∗, and sends the authentication message, C8, to the server.(7)
Server receivesC8 after validation and accepts session key SK after successful verification; then it sends a key confirmation message, C9=hSK‖r4, to the user.(8)
Server receivesC9 after validation. After successful verification, both parties establish a common session key, SK.


### 4.2.2. Strand Space Analysis of Protocol

We used the XOR operation in this protocol. Mao’s analysis of the protocol included smart card and guess attacks. We added the corresponding key-compromise and guess attack modules. The behaviours of the main body of the protocol are described as shown in Figure4.Figure 4
Role strands of 3FA.The terms are defined as follows:C1=hIDu,PW,HbioB, C2=xorB,r1, M=hHbioc2,s, X=xorhIDs,c1,M,r2, Y=xorM,c1, Z=xorr1,HbioB, SmartCard=IDs,X,Y,Z, C3=HbioxorB,r1,r2, C4=xorB,r1,hM,r3, C5=xorr3,HbioxorB,r1, C6=xorr4,hxorB,r1, C7=hxorB,r1,r3,r4, SK=hM,r3,r4, C8=hxorHbioxorB,r1,r4,r4, and C9=hSK,r4.In [33], the attack on user ID and PW required the attacker to obtain the user’s smart card, know the user’s biometrics, and could guess attacks. Using the framework of key-compromise and guessing attacks defined in the previous section, combined with the principal behaviours of the protocol, we modelled the attacker’s ability.The attacker knows the user’s biometrics and smart cards. For the first time, biometrics appear in the first node. The smart card is divided into two parts.Z can be obtained via the XOR of r1 and HbioB in the first node, and the rest is sent to the user at the second node on the server. Therefore, we describe an attacker’s key-compromise attack on smart cards and biometrics as Reveal:(i)
Reveal:−C1,C2kUser,Server,−SmartCardkUser,Server,+SmartCard,B.Modelling guessing attacks requires consideration of the terms, includingIDu and password. Term C1=hIDu,PW,HbioB contains IDu and password. Furthermore, we need to obtain term B to estimate C1. Because of term Y=xorM,C1, the known terms C1 and Y can obtain M by using rule XOR-D, thus conjecturing M. Two effective guessing chains can be obtained by constantly exploring the possible guessing paths. For example, in the first guess chain, we provided a set of guess values for IDu and PW, IDuGuess and PWGuess, respectively. Then, combined with term B, C1 and the conjecture can be obtained using C1Guess=hIDuGuess,PWGuess,HbioB. Unless we obtain the conjecture value of C4, we cannot determine if the conjecture value is successful by comparison.Through two guessing chains shown in Figure5, the rules of attacker guessing attack are stated as follows:(1)
GS-1:−C3,B,Y,IDsc,X,r1,+PW,IDu.(2)
GS-2:−C4,B,Y,r1,r3,+PW,IDu.Figure 5
Two guessing chains of Zhang’s protocol.Thesmartcard and B obtained by combining guessing rules and key disclosures can guess the user’s ID and password. The process is as follows:Path 1 (Figure6)(1)
The attacker obtainssmartcard and B using the Reveal rule.(2)
XOR-D rule−xorr1,HbioB,−HbioB,+r1 is applied to obtain term r1.(3)
F rule −C3 is applied to obtain term C3.(4)
According to the GS-1 rule, usingIDsc, X, Y, B is obtained by Reveal, r1 is obtained by XOR operation, and C3 is eavesdropped using the normal protocol process. A guessing attack is carried out to obtain the terms, ID and PW, of the attacker.Path 2 (Figure7)(1)
The attacker obtainssmartcard and B using the Reveal rule.(2)
XOR-D rule−xorr1,HbioB,−HbioB,+r1 is applied to obtain term r1.(3)
HbioxorB,r1 is constructed by B and r1.(4)
XOR-D rule−xorr3,HbioxorB,r1,−HbioxorB,r1,+r3 is applied to obtain term r3.(5)
TheF receive rule −C4 is applied to obtain term C4.(6)
According to the GS-2 rule, usingY and B obtained by Reveal, r1 and r3 obtained by the XOR operation and C4 from normal protocol flow are used to carry out a guessing attack to obtain the legal user’s term ID and PW.Figure 6
Attack path 1 of Zhang’s protocol.Figure 7
Attack path 2 of Zhang’s protocol.The first path was first discovered by Mao, and the second attack path was discovered by our addition of semantics to ESSM for the first time.


## 4.2.1. Protocol Description

During the registration stage, the user sends the protected identity information to the server, and the server stores it and issues a smart card for authentication. It should be noted that the communication in the registration phase is based on the secure channel, and the attacker cannot obtain any information in the registration phase.(1)
UserU selects identity ID and password PW and inputs biometric B to the terminal. The terminal calculates C1=hID,PW,hBioB and generates random number r1 for calculating C2=B⊕r1. User U sends a registration request message C1,C2 to server S.(2)
After receiving the registration request message from userU, server S uses the server’s private key, s, to calculate M=hhBioC2‖s, generates random number r2, and calculates W=hhBioC2⊕r2, X=hIDSC‖C1‖M⊕r2, and Y=M⊕C1. The server stores C2,W0,W in the database and initializes W0 to null. The server writes to the smart card IDSC,h⋅,hBio⋅,X,Y and gives it to user U.(3)
Z=r1⊕hBioB is calculated after receiving the smart card. Z is written to it for completing registration.The login authentication phase is described as follows:(1)
UserU inputs accounts for ID′, password PW′, and biometric B′ and inserts the smart card at the same time.(2)
UserU generates a random number r3 and calculates C1∗=hID′PW′hBioB′, M∗=Y⊕hC1∗, r2∗=X⊕hIDSCC1∗M∗, and r1∗=Z⊕hBioB.(3)
C3=hBioB′⊕r1∗⊕r2∗, C4=B′⊕r1∗⊕hM∗‖r3, and C5=r3⊕hBioB′⊕r1∗ are calculated to send a login request C3,C4,C5 to server S.(4)
The server performs dynamic verification by matchingC3 and the data in the database. For more details, please refer to the original article [32].(5)
ServerS generates a random number r4, calculates M′=hhBioC2‖s, r3∗=C5⊕hBioC2, and B′⊕r1∗=C4⊕hM′‖r3∗, and checks B⊕r1∗ and C2. If the validation passes, the server computes C6=r4⊕hB⊕r1∗ and C7=hB⊕r1∗r3∗r4∗. Both C6,C7 are sent to user U.(6)
UserU receives C6,C7 and calculates r4∗=C6⊕hB⊕r1∗, verifying C7=?hB⊕r1∗r3∗r4∗. After verification, the user calculates the session key, SK=hM∗r3r4∗, and C8=hhBioB⊕r1∗⊕r4∗⊕r4∗, and sends the authentication message, C8, to the server.(7)
Server receivesC8 after validation and accepts session key SK after successful verification; then it sends a key confirmation message, C9=hSK‖r4, to the user.(8)
Server receivesC9 after validation. After successful verification, both parties establish a common session key, SK.


## 4.2.2. Strand Space Analysis of Protocol

We used the XOR operation in this protocol. Mao’s analysis of the protocol included smart card and guess attacks. We added the corresponding key-compromise and guess attack modules. The behaviours of the main body of the protocol are described as shown in Figure4.Figure 4
Role strands of 3FA.The terms are defined as follows:C1=hIDu,PW,HbioB, C2=xorB,r1, M=hHbioc2,s, X=xorhIDs,c1,M,r2, Y=xorM,c1, Z=xorr1,HbioB, SmartCard=IDs,X,Y,Z, C3=HbioxorB,r1,r2, C4=xorB,r1,hM,r3, C5=xorr3,HbioxorB,r1, C6=xorr4,hxorB,r1, C7=hxorB,r1,r3,r4, SK=hM,r3,r4, C8=hxorHbioxorB,r1,r4,r4, and C9=hSK,r4.In [33], the attack on user ID and PW required the attacker to obtain the user’s smart card, know the user’s biometrics, and could guess attacks. Using the framework of key-compromise and guessing attacks defined in the previous section, combined with the principal behaviours of the protocol, we modelled the attacker’s ability.The attacker knows the user’s biometrics and smart cards. For the first time, biometrics appear in the first node. The smart card is divided into two parts.Z can be obtained via the XOR of r1 and HbioB in the first node, and the rest is sent to the user at the second node on the server. Therefore, we describe an attacker’s key-compromise attack on smart cards and biometrics as Reveal:(i)
Reveal:−C1,C2kUser,Server,−SmartCardkUser,Server,+SmartCard,B.Modelling guessing attacks requires consideration of the terms, includingIDu and password. Term C1=hIDu,PW,HbioB contains IDu and password. Furthermore, we need to obtain term B to estimate C1. Because of term Y=xorM,C1, the known terms C1 and Y can obtain M by using rule XOR-D, thus conjecturing M. Two effective guessing chains can be obtained by constantly exploring the possible guessing paths. For example, in the first guess chain, we provided a set of guess values for IDu and PW, IDuGuess and PWGuess, respectively. Then, combined with term B, C1 and the conjecture can be obtained using C1Guess=hIDuGuess,PWGuess,HbioB. Unless we obtain the conjecture value of C4, we cannot determine if the conjecture value is successful by comparison.Through two guessing chains shown in Figure5, the rules of attacker guessing attack are stated as follows:(1)
GS-1:−C3,B,Y,IDsc,X,r1,+PW,IDu.(2)
GS-2:−C4,B,Y,r1,r3,+PW,IDu.Figure 5
Two guessing chains of Zhang’s protocol.Thesmartcard and B obtained by combining guessing rules and key disclosures can guess the user’s ID and password. The process is as follows:Path 1 (Figure6)(1)
The attacker obtainssmartcard and B using the Reveal rule.(2)
XOR-D rule−xorr1,HbioB,−HbioB,+r1 is applied to obtain term r1.(3)
F rule −C3 is applied to obtain term C3.(4)
According to the GS-1 rule, usingIDsc, X, Y, B is obtained by Reveal, r1 is obtained by XOR operation, and C3 is eavesdropped using the normal protocol process. A guessing attack is carried out to obtain the terms, ID and PW, of the attacker.Path 2 (Figure7)(1)
The attacker obtainssmartcard and B using the Reveal rule.(2)
XOR-D rule−xorr1,HbioB,−HbioB,+r1 is applied to obtain term r1.(3)
HbioxorB,r1 is constructed by B and r1.(4)
XOR-D rule−xorr3,HbioxorB,r1,−HbioxorB,r1,+r3 is applied to obtain term r3.(5)
TheF receive rule −C4 is applied to obtain term C4.(6)
According to the GS-2 rule, usingY and B obtained by Reveal, r1 and r3 obtained by the XOR operation and C4 from normal protocol flow are used to carry out a guessing attack to obtain the legal user’s term ID and PW.Figure 6
Attack path 1 of Zhang’s protocol.Figure 7
Attack path 2 of Zhang’s protocol.The first path was first discovered by Mao, and the second attack path was discovered by our addition of semantics to ESSM for the first time.


## 4.3. Experiment

We make a formal analysis of six groups of protocols, including TMN protocol [34], MTI-C (1), MTI-A (0), and MTI-C (0) in MTI protocol family [35], WPA-PSK protocol [36] in 802.11i standard, and three-factor authentication protocol proposed by Zhang.We applied our method to a group of protocols using algebraic logic or special attack ideas. The results obtained by running our implementation on Scyther v. 1.1.3 are presented in Table11, which lists the analysis results using the original Scyther and using ESSM modelling, including the declaration of security attributes and the number of search states.Table 11
Experiment result of several protocols.
ProtocolOriginal modelESSM modelSearch queriesDetected attacksSemantics usedSearch queriesDetected attacksTMN2658SafeXOR191948Algebraic attackMTI-C (1)263550SafeDH SS493270Small subgroup attackMTI-A (0)1649SafeDH KCI331160Impersonal attackMTI-C (0)322SafeDH KCI2585KCI attackWPA-PSK269SafeGuess55446Guessing attackZhang’s5684SafeXOR KCI Guess6349113Combination attackThe code restores the process of protocol interaction and abstracts the storage verification process of the server. We then declare the confidentiality of ID and PW. By adding auxiliary protocols (e.g., Smartcard Lost, XOR operation, and Offline Password Guess), two paths not meeting the confidentiality requirements can be automatically searched.Through the experimental results, we can find that the search path of the model search after adding ESSM semantics is richer, more attacks can be found, and the protocol environment can be restored more realistically. The increase of search path shows two facts.(1)
The semantic extension of ESSM is real and effective and has certain effect on many types of protocols.(2)
The contrast of the experimental results before and after the expansion is too large, which leads to the state explosion problem to a certain extent. The current model detection technology still has no effective solution to the state explosion problem, especially for algebraic operations.The semantic extension of ESSM is real and effective and has certain effect on many protocols.


## 5. Conclusion

In this paper, an ESSM framework was proposed, because it has a more complete semantic description than does the original strand space model, including the internal operation of protocol subject behaviours, the support of algebraic operation, and its modelling of the DY attacker ability. The proposed ESSM supports the transformation of algebraic operation rules at the symbol level and the expansion of a special attack capability. We added XOR- and Abelian-group operations to the algebraic operation module and added the description semantics of an algebraic attack, a KCI attack, and a guessing attack in special situations to the attacker module. The framework presented good expansibility. Furthermore, only ability rules needed to be added to the corresponding modules. Then, the corresponding protocols could be modelled and analysed in the strand space. We used ESSM to model and analyse different types of protocols that use algebraic rules and have special attack problems. We found no security or authentication problems in the strand space model, but we did encounter issues in the ESSM model. Simultaneously, we used Scyther to extend the modelling of ESSM and analysed several protocols automatically. The analysis showed that Scyther v. 1.1.3 found all problems in the protocol after modelling with ESSM. Moreover, we found a new guessing tool path using Mao’s three-factor authentication protocol.We observed that, with the extension of automation tools, the number of search paths for protocols increased. On one hand, it reflects that our model more comprehensively considers the problems in the protocol and has more search paths. On the other hand, it exposes the state explosion problem of model-checking methods, especially when dealing with algebraic operations that lead to many useless queries in the state space search. This problem will be solved in future studies.



---

*Source: 8273172-2021-12-07.xml*