Keywords

1 Introduction

A secure communication is a problem that the cryptography research community has been working on for a long time. Authentication and Key Exchange (AKE) is an essential part of a secure communication. The problem dealt with in an authenticated communication is that of an adversary \(\mathcal {A}\) which has the power to modify, delete, delay and introduce false messages or impersonate a participant in the communication. Key exchange in an authenticated communication allows two parties to generate a shared secret. Authentication protocols use various key exchange techniques like Diffie–Hellman Key Exchange (DHKE) protocol [5] to establish a secret session key [6, 17]. When it comes to a multi-server environment, such authentication protocols may have a major limitations such as the clients may need to store public keys of every single server [31]. To overcome the limitations, identity-based key exchange protocols were introduced [4, 15, 22]. The idea has been applied to design many key exchange protocols [3, 18]. In an identity-based cryptosystem, user identities are used as public keys. A trusted third-party generates a private key for the user using the user identity and a master key. The public key is the user identity, thus users do not need to store multiple public keys.

The extended Canetti–Krawczyk (eCK) [10] adversary model is a widely accepted adversary model. It is used to verify the various required security properties for AKE protocols. A protocol is considered as secure, if an adversary \(\mathcal {A}\), who is in control of communication between two parties, is unable to distinguish session key from a random value. It can do so, only if it calls certain queries that reveal various secret information that are part of the protocol communication. In the eCK adversary model, the adversary is able to call Ephemeral Key Reveal Query, Long-Term Key Reveal Query and Session Key Reveal Query. The Ephemeral Key Reveal Query allows an \(\mathcal {A}\) to capture all the session-specific temporary secret information. The Long-Term Key Reveal Query reveals the long-term secret keys of a party to the adversary and The Session Key Reveal Query reveals the current session key between two parties. However, the adversary is allowed to call the queries one at a time.

The Tamarin Prover is an automatic formal security analysis tools which supports features like Diffie–Hellman, hashing, bilinear pairing and so on. The shortfall of the tool is that it does not support elliptic curve point addition [21]. The developers provide a modelling example for the Chen–Kudla protocol [3] where they use ordered concatenation in place of point addition. However, the same approach cannot be implemented for all AKE protocols using point addition operations. We introduce a generalised ID-based Authentication and Key Exchange (ID-AKE) protocol in this paper that uses point addition operations. We model the same in the Tamarin Prover tool using a different modelling technique and analyse it under the eCK adversary model.

In the upcoming sections, we define the required mathematical preliminaries in Sect. 2. Next, we describe the literature review on modelling AKE protocols using the Tamarin Prover in Sect. 3. We discuss the problem of replacing point addition operation with an ordered concatenation in Sect. 4. The contributions of the paper are presented in Sect. 5. In Sect. 6, the summary of a generalised ID-AKE protocol and its Tamarin Prover model is given. We demonstrate that the proposed modelling technique ensures that ID-AKE protocol is secure under the eCK adversary model and it retains the properties of point addition. Finally, Sect. 7 concludes the paper.

2 Mathematical Background

In this section, we discuss the required mathematical preliminaries used to design the ID-AKE protocol.

2.1 Bilinear Pairings

Bilinear pairings can be defined by assuming that \(G_1\) is an additive cyclic group of prime order q, \(G_2\) is a multiplicative cyclic group of prime order q. Let, P be the generator of \(G_1\), the bilinear pairing equation \({e}: G_1 \times G_1 \rightarrow G_2\) satisfies the following properties [29]:

  • Bilinearity: \({e}(aP, bQ) = {e}(P, Q)^{ab}\), for all \(P, Q \in G_1\) and for all \(a, b \in Z^{*}_{q}\).

  • Computability: For all \(P, Q \in G_1\), e(P, Q) can be efficiently computed.

  • Non-degeneracy: There exists \(P, Q \in G_1\) with \({e}(P, Q) \ne 1\), where 1 is the multiplicative identity of \(G_2\).

2.2 Hash Function

A one-way hash function is a function \(h:\{0,1\}^* \rightarrow \{0,1\}^n\) satisfying the following conditions [13, 16]:

  • The input \(x \{0,1\}^{*}\) is of arbitrary length binary string and the output \(h(x) \in \{0,1\}^{n}\) is a binary string of fixed length with n bits.

  • One-wayness: Given a \(y = h(x) \in \{0,1\}^n\), it is hard to compute x in \(\{0,1\}^{*}\).

  • Collision-Resistant: Given \(x \in \{0,1\}^{*}\), finding \(y \in \{0,1\}^{*}\) where \(x \ne x\) such that \(h(x) = h(y)\) is infeasible to compute.

2.3 Message Authentication Code

Let \(M \in \{0,1\}^{*}\) be a message of variable length, \(K \in \mathcal {K}\), where \(\mathcal {K}\) is the key space, be a secret key shared between two parties. We define a message authentication code, say, \(MAC: \mathcal {K} \times \{0,1\}^* \rightarrow \{0,1\}^n\), and the function \(C = MAC(K,M)\), where \(C \in \{0,1\}^{n}\) is a fixed length binary string. The MAC satisfies the following properties [24]:

  • Without key K, it is hard to verify the message authentication code M.

  • For a given C, it is hard to compute the M and K due to one-wayness of the MAC.

3 Related Works

Many AKE protocols have been designed till now using the concepts of the DHKE protocol [1, 7]. Shamir [22] introduced the identity-based key exchange protocol to overcome the problem of storing multiple public keys. Using the same concept, many ID-AKE protocols were proposed [3, 9, 14, 30]. The identity of the parties was used as their public keys. The DHKE protocol is a simple and essential protocol that is still being used widely to design AKE protocols. To study the modelling techniques used in the Tamarin Prover, studying the DHKE protocol model is of utmost importance. The DHKE protocol model is coded in [12] and its vulnerability is tested against the Man-In-The-Middle (MITM) attack under the eCK adversary model. In the MITM attack, an adversary \(\mathcal {A}\) is able to impersonate one or both the participants without their knowledge and finally establish a shared secret key with the participants [8].

In various Tamarin Prover documentations [11, 20, 21], the authors have described about a few AKE protocols like Joux protocol [9], Chen–Kudla protocol [3], RYY protocol [19], etc. that use point addition. The protocols are modelled using different modelling techniques and the codes are present in the ‘The Tamarin Prover Github Repository’[25]. For formalising the Joux protocol, they used the multiset of identities of the participants. A study of the technique is presented in Sect. 3.2. Next, as stated in [21], Chen–Kudla KA protocol is modelled using an ordered concatenation instead of point addition. The Chen–Kudla protocol’s modelling technique is thoroughly explained in Sect. 3.3. An exhaustive study of three protocols [3, 5, 9] is presented in order to look through the different modelling techniques incorporated to formalise them. Also, the paper focusses on their potential of being used in a generalised case. A comparative study of the protocols is presented in Table 1. The study summarises the protocols based on the cryptographic primitives used, the protocol specifications, the modelling techniques and various security properties used for verification.

3.1 Diffie–Hellman Key Exchange Protocol

The DHKE protocol is reviewed and the Tamarin Prover model is presented in this section. We consider two parties: Alice and Bob. Alice and Bob choose a secret \(a \in (1 \le a \le p-1)\) , \( b \in (1 \le b \le p-1)\), respectively, over a finite field GF(p) with prime p. \(A = g^a \mod p\) and \(B = g^b \mod p\) are computed by Alice and Bob, respectively. A is sent to Bob by Alice and B is sent to Alice by Bob. They compute the shared session key \(SessK = SessKA = SesskB = g^{ab} \mod p\).

Man-In-The-Middle Attack in the DHKE Protocol: The DHKE protocol is vulnerable to the MITM attack [8]. Let us assume that an adversary \(\mathcal {A}\) intercepts the message \(M1 = \langle A\rangle \) from Alice and replaces it with \(X = g^x\) finally sending \(M2 = \langle X \rangle \) to Bob. Bob sends \(M3 = \langle B\rangle \) which is again intercepted by the \(\mathcal {A}\) and passed onto Alice without any changes. At the end, \(\mathcal {A}\) establishes a session with Bob using \(SessK = g^{xb}\), and therefore impersonating Alice. The DHKE protocol is modelled and tested using the Tamarin Prover in [12]. The model is tested for MITM vulnerability using the simple Lemma 1 which is shown and elaborated in Fig. 1.

Lemma 1

For all cases, session keys that are created at an instance i1, the adversary, \(\mathcal {K}\) must not be able to compute a session key at an instance i2.

Fig. 1
figure 1

A simple MITM lemma

Full size image

The tool produced an analysis stating that the protocol is vulnerable to the MITM attack. The Tamarin Prover tool traces for the possibility of the MITM attack and is able to find a counterexample where an adversary, \(\mathcal {K}\), is able to compute the session key, thus turning the lemma red. Here, the adversary sends a fake \(g^a\). Therefore, we can conclude that an adversary is able to perform an MITM attack.

3.2 The Joux Protocol Using Signatures (SIGJOUX)

In this section, we review the three-party authentication protocol proposed by Joux [9], which is a variation of the Diffie–Hellman protocol. This uses bilinear pairing.

  • Three parties: Alice, Bob and Carol participate in one round tripartite DHKE.

  • Each of them select random values a, b and c, respectively. They also choose long-term keys ka, kb, kc, respectively, \(\ni 1 \le (a,b,c) \le p-1\) over the finite field GF(p) with prime p. Finally, they compute \(A = aP\), \(B = bP\) and \(C = cP\). Here, \({e}: G_1 \times G_1 \rightarrow G_2 \ni {e}(xP , yP ) = {e}(P , P )_{xy}\).

  • Alice, Bob and Carol simultaneously sign a message with their chosen long-term keys and send the following to two other parties : \(SigA:sign_{ka}(ID_B,ID_C,A)\), \(SigB:sign_{kb}(ID_A,ID_C,B)\) and \(SigC:sign_{kc}(ID_A,ID_B,C)\).

  • On receiving the same, each party is able to compute their own shared secret keys, SessKA: \(h({e}(B,C)^a,ID_A,\) \(ID_B,\) \(ID_C)\), SessKB: \(h({e}(A,C)^b,ID_A,ID_B,\) \(ID_C)\) and SessKC: \(h({e}(A,B)^c,ID_A,ID_B,ID_C)\).

  • Finally, the shared secret is \(SessK = SessKA = SessKB = SessKC = {e}(P,P)^{abc}\) where \({e}(P,P)^{abc} \in G_2\).

The entire code Joux.spthy is present in the Tamarin Prover Github repository [27]. The ephemeral key, ekA, is denoted with \(\sim {ekA}\) which denotes that it is a fresh value and the rule Proto1 will generate a fresh ekA for every session. The !Ltk() ensures that the fact will remain constant at all times. While modelling the Session Key generation we can see that, for each party, the IDs are denoted by $ which means that they are public. For each party, the IDs of the other two are added using the multiset operator ‘+’ as per the multiset rewriting rules for formalising a protocol.

The Tamarin Prover modelling formalises the protocol by using multiset rewriting rules. Alice, A, chooses her ephemeral key ekA. The other two parties are Bob, B, and Carol, C. The signing key ltkA is used to sign his own public identity \(\$A\), the multiset of the public identities of the two parties \(\$B,\$C\) along with the public ephemeral key [ekA]P. Pstate\((x, A, B+C)\), which is the protocol state fact, denotes that a session is executed. In the second rule, A checks the signatures of the other two parties, extracts their XB and XC which are the public ephemeral keys of B and C, respectively, and computes the shared key as \({e}(XB , XC)^{ekA}\). The protocol succeeds in providing Perfect Forward Secrecy with Long-Term Key Reveal model if A accepts the session key generated with B and C. However, it fails to provide the same if there is an Ephemeral Key Reveal modelled for the protocol.

3.3 Chen–Kudla Key Agreement Protocol

We study the Chen–Kudla Key Agreement Protocol in this section. It is an ID-based key exchange protocol that uses the concepts of bilinear pairing and point addition. A Key Generation Centre (KGC) is there that is responsible for the registration of users \(\mathcal {U}\). The key exchange protocol is a two-party communication.

  • In the KGC setup phase, the KGC randomly selects a secret key, Key, which acts as the long-term key and computes public key \(Pub = KeyP\) \(\ni P\in G_1\). Here, P is a generator of \(G_1\) and \(Key \in Z_q^*\).

  • In the key exchange phase, Alice (A) and Bob (B) are considered as two users. KGC computes \(H_A = h(ID_A)\), \(S_A = KeyH_A\) for Alice, \(H_B = h(ID_B)\), \(S_B = KeyH_B\) for Bob. KGC sends \(S_A\) and \(S_B\) to Alice and Bob, respectively. Here \(H_A,H_B \in G_1\). h() is the hash function \(\ni h\{0,1\}^* \rightarrow G_1\).

  • A computes \(A = aP\) and B computes \(B = bP\), where a and b are randomly selected ephemeral secrets. A is sent to Bob by Alice. B is sent to Alice by Bob.

  • Alice then generates \(SessKA = {e}(S_A,B){e}(aH_B,Pub)\) and Bob generates \(SessKB = {e}(S_B,A){e}(bH_A,Pub)\) which results in the computation of \(SessKey = SessKA = SessKB = {e}(bH_A+aH_B,Pub)\).

The Chen–Kudla protocol is modelled in the Tamarin Prover by replacing the point addition operation with an ordered concatenation. The complete code Chen_Kudla.spthy is available in the Tamarin Prover Github Repository [26]. The shared secret key \(sessK = {e}(ex[hp(\$B)]+ey[hp(\$A)],P_s)\) is written as \(({e}(hp(\$B),mpk)^{~ex})\) (e(skA, Y)) using the concepts of bilinearity [2] that states that \({e}(P+Q,Y) = {e}(PY){e}(QY)\). The protocol model works aptly when the adversary \(\mathcal {A}\) is restricted from revealing the ephemeral key of the test session and its significant matching session. This is true even if no Long-Term Key Reveal Query is called by \(\mathcal {A}\). On removing the Ephemeral Key Reveal Query restriction, the protocol fails to provide key secrecy.

Comparative Study: A comparative study of the protocols is presented in Table 1. The protocols [3, 5, 9] and the generalised ID-AKE protocol are compared with respect to the cryptographic primitives used to design the protocols, the Tamarin Prover modelling technique used and the various security properties achieved by the protocols.

Table 1 Comparative study of modelling protocols in the Tamarin Prover
Full size table

4 Problem with Ordered Concatenation in ID-AKE

The Tamarin Prover does not provide the provision of performing point addition. Also, it does not support computation of equalities such as \((c)[(a)P+(b)]P = [(ca)P+(cb)P]\) [21]. Here, for example, the Tamarin Prover model for Chen–Kudla Key Agreement Protocol (Chen_Kudla.spthy) present in the repository [26], bilinear terms having point addition are replaced with an ordered concatenation [21] as discussed in Sect. 3.3. There are many ID-AKE protocols that are designed using the point addition operation [14, 23, 28]. The same approach cannot be used in such cases where point addition is used to secure the master key of a Trusted Key Distribution Centre (TKGC). The point addition operation is used to generate the authentication message of the participants in the communication by using the public key of the TKGC. Using the concept of concatenation would not help in achieving security of the master key. This is because, for performing the concatenation operation, the master key needs to be used directly.

We present a generalised ID-based authentication and key exchange (ID-AKE) protocol and model it using the Tamarin Prover in this paper. The detailed description is presented in Sect. 6. The protocol uses the concept of bilinear pairing and point addition. Subsequently, to model the generalised ID-AKE protocol, we embrace the technique of normalisation and define a unary public function hf/1 that works similarly to a hash function in Tamarin Prover. Along with this, some precomputations need to be performed in order to ensure the KGC’s secret key security. The technique is illustrated in detail in Sect. 6.2.

5 Contributions of the Paper

The research contributions of the paper are as follows:

  • We present a comparative study of the Tamarin Prover modelling techniques used to model authentication protocols that use point addition operations.

  • We discuss a generalised ID-AKE protocol that uses point addition operation and present a technique using normalisation and precomputation to model the same.

  • Under the eCK adversary model, we test the security properties using the proposed technique. The result shows that the proposed technique is able to achieve the properties of point addition without compromising security of the original protocol.

6 A Generalised ID-AKE Protocol

We provide a summary of the generalised ID-AKE protocol in this section. We discuss about the modelling strategy used and the normalisation and precomputations needed to successfully model the protocol.

6.1 Authentication and Key Exchange Protocol

We begin with the Key Generation Centre setup phase as shown in Table  2. The Key Generation Centre (KGC) chooses a master private key, Key and generates public key \(Pub=KeyP\).

A user requests for registration in the user registration phase (Table 2). The KGC computes \(K_U =\frac{1}{h(ID_U)+Key} P\) and sends \(\langle ID_U, K_U \rangle \), which the user keeps safe. In the proposed protocol, we assume that two users Alice, A and Bob, B register with the KGC. The KGC sends \(\langle ID_A, K_A \rangle \) to Alice and \(\langle ID_B, K_B \rangle \) to Bob. Here, \(K_A = \frac{1}{h(ID_A)+Key} P\) and \(K_B = \frac{1}{h(ID_B)+Key} P\).

In the authentication and key exchange phase (Table 3), Alice chooses secret a and computes \(A = a(h(ID_B)P + Pub)\). Alice then sends \(\langle M1 = A \rangle \) to Bob. Similarly, Bob chooses secret b, computes \(B = b(h(ID_A)P + Pub)\) and \(SessKB = {e}(A,K_B)^{y}\). Bob then sends \(\langle M2 = MAC(SessKB,A,B)\rangle \) to Alice. Thus, Alice authenticates Bob.

Alice further computes \(SessKA = {e}(B,K_A)^{x}\) and sends \(\langle M3 = MAC(SessKA,\) B,  \(A)\rangle \) back to Bob. Hence, authenticating herself to Bob and establishing a secret session key \(SessK = SessKA = SessKB = {e}(P,P)^{ab}\).

Table 2 ID-AKE—registration phase
Full size table
Table 3 Alice and Bob authentication and key exchange phase
Full size table

6.2 Modelling ID-AKE Using the Tamarin Prover

In this section, we describe about the normalisation and precomputations that are required in our modelling technique. We discuss the Tamarin Prover model and verify the protocol security under the eCK adversary model using the Tamarin Prover.

Normalisation and precomputation: In the designed ID-AKE, to model the point addition operation, normalisation needs to be performed. The public key for the participants needs to be pre-computed by the KGC. The importance of point addition in this protocol is that the operation is used to construct the ID-based public key without revealing the private key of the KGC. This is achieved by point adding the public key of the KGC. The point addition operation provides the required hardness to secure the private key.

For the normalisation of the initial point addition operation, we introduce a public unary function hf/1 that is against multiple inputs the function provides a single output. We use inv denoting field inverse and pmult denoting point multiplication. The normalisation in the protocol is performed as follows:

  • For \(K_A = \frac{1}{h(ID_A)+Key} P\) the point addition part is normalised as \(TempKa = hf(ID_A,Key)\). Next, \(K_A\) is computed as \(K_A = pmult(inv(hf(ID_A,Key)),'P')\).

  • For \(K_B = \frac{1}{h(ID_B)+Key} P\) the point addition part is normalised as \(TempKb = hf(ID_B,Key)\). Next, \(K_B\) is computed as \(K_B = pmult(inv(hf(ID_B,Key)),'P')\).

In the AKE phase, \(A = a(h(ID_B)P + Q) \) and \(B = b(h(ID_A)P + Q)\) are the ephemeral public key that needs to be computed at Alice and Bob’s end, respectively. In order to use the normalisations TempKa and TempKb for computation of A and B, Alice and Bob need to have the knowledge of \(`Key'\) which is the long-term key of KGC. It is highly undesirable from protocol security point of view. Thus, we pre-compute the values \(ap = pmult(TempKa,'P')\) and \(bp = pmult(TempKb,'P')\) at the KGC’s end and send it to Alice and Bob as public keys. With ap Bob computes \(B = pmult(~b,ap)\) and with bp Alice computes \(A = pmult(~a,bp)\) which are the ephemeral public key used for authentication.

The Tamarin Prover Code: The Tamarin Prover model for the generalised ID-AKE is explained below: The program IDAKE.spthy starts with the header ‘theory IDbasedAKE’ which is the theory name. The next line has ‘begin’ which means start of the protocol modelling. The third line calls the bulitins that are required for the modelling. The fourth line describes the public functions hf/1 and mac/2 used to model the protocol. The code is shown in Fig. 2.

Fig. 2
figure 2

ID-AKE—Tamarin Prover model—the Tamarin Prover code header

Full size image

The rule ‘TrustedKGC’ is depicted in Fig. 3. It is defined to compute the public key and long-term key (ltk) of the KGC (key generation centre). For every session, the rule will generate a fresh persistent long-term key \(\sim \)Key as registered with !Ltk() which acts as the master key. Persistent fact !PubK() is used to compute the public key.

Fig. 3
figure 3

ID-AKE—Tamarin Prover model—rule for KGC setup

Full size image

The code presented in Fig. 4 shows the Rules ‘AliceReg’ and ‘BobReg’ which are used to model the long-term key generation for Alice and Bob using the master key of the KGC. According to the protocol, the key of the user is computed by using the concept of normalisation. Point addition is replaced by the singular public function hf/1 and TempKa and TempKb is computed accordingly. With the normalised value, the long-term key for Alice and Bob is computed and registered using !Ltk(). For the precomputation, the public key is registered using !PubA() and !PubB() which contains the normalised value.

Fig. 4
figure 4

ID-AKE—Tamarin Prover model—rule for user registration

Full size image

Rules ‘Alice’ and ‘Bob’ present the computation of values of A and B. The computations are done using the Ephemeral keys a and b. The code is presented in Fig. 5. A and B (as per the protocol) are computed using the KGC’s public key. Thus, the long-term key of the KGC remains a secret. For modelling the same the normalised pre-computed values ap and bp have been used and ephemeral keys \(\sim \)a and \(\sim \)b have been registered using !Ephk().

Fig. 5
figure 5

ID-AKE—Tamarin Prover model—rule for generation of ephemeral public key

Full size image

Rules ‘AliceSession’ and ‘BobSession’ as shown in Fig. 6 are used to generate the session keys sesska and sesskb using the persistent fact !SessionKey(), MAC(), which is used to authenticate each other is also computed. An equality check is done for the MAC() values that are exchanged using the equality restrictions (presented in Fig. 7). A SessionID() and a MatchingSession() is associated for every session created by the above rules. Session_Created() denotes that the rule ran and a session is created and Accept() fact states that the shared session key sesska and sesskb has been accepted [11].

Fig. 6
figure 6

ID-AKE—Tamarin Prover model—rule for session key generation

Full size image
Fig. 7
figure 7

ID-AKE—Tamarin Prover model—restrictions and key reveal models

Full size image

Security Properties: To analyse the modelled protocol under the eCK adversary model, we design Lemmas 10 and 3. The lemma codes are presented in Figs. 8 and 9.

Lemma 2

MITM : The lemma states that for all sessions created and the adversary, \(\mathcal {K}\), has not called the Long-Term Key Reveal Query or the Session Key Reveal Query, it implies that \(\mathcal {K}\) is not able to compute the shared secret session key.

Fig. 8
figure 8

ID-AKE—Tamarin Prover model—MITM lemma

Full size image
Fig. 9
figure 9

ID-AKE—Tamarin Prover model—session key secrecy lemma

Full size image

Lemma 3

Session Key Secrecy: The lemma states that there does not exist an accepted test session and the adversary, \(\mathcal {K}\), does not have the shared session key. Also, the adversary has not called a Session Reveal Query. If the adversary has found a matching session it implies that the following queries have not been called:

  • A Session Key Reveal Query for the obtained matching session.

  • A Long-Term Key Reveal Query for Alice and Ephemeral Key Reveal Query for Alice’s matching session.

  • A Long-Term Key Reveal Query for Bob and Ephemeral Key Reveal Query for Bob’s session ID.

  • A Long-Term Key Reveal Query for both Alice and Bob.

  • An Ephemeral Key Reveal Query for obtained matching session and the parties’ session ID.

Finally, if the adversary did not find a matching session, it implies that there does not exist an Ephemeral Key Reveal Query for matching session. Also there does not exist a Long-Term Key Reveal call for Bob, thus stating that Bob has not been compromised.

Fig. 10
figure 10

The Tamarin Prover model visualisation for ID-AKE protocol

Full size image

Model Visualisation: Once Lemmas 2 and 3 are solved in the Tamarin Prover, the colour of the proof turns green as shown in Fig. 10. It is an indication that there were no traces found for any adversary computing the secret session key, k. Thus, we suggest that the designed ID-AKE protocol using the technique of precomputation and normalisation resists MITM attack and provides session key secrecy under the eCK adversary model.

7 Conclusion

In this paper, we study the designing techniques of security models using Tamarin Prover for various authentication protocols. It is observed that the point addition operation modelled in the literature is not applicable to many of the IBE-based protocols. In this work, we present a generalised IBE-based key exchange protocol and modelled it using the proposed normalised precomputation technique with the help of hash function. The Tamarin Prover simulations showed that the proposed technique provides security under the eCK adversary model. In conclusion, the proposed model can be applied to IBE-based protocols where the point addition operation is used.