Modelling Identity-Based Authentication and Key Exchange Protocol Using the Tamarin Prover

In real-time applications, authentication plays a vital role in enabling secure communications. The authentication protocols need to be formally verified under a defined threat model. Unless the protocols are verified for the intended security, the purpose of employing such protocols may eventually fail. There are multiple ways to formally verify the security of the authentication protocols including the use of automatic verification tools like the Tamarin Prover. The Tamarin Prover tool supports equational theories along with built-in functions. However, this tool does not support some mathematical operations such as elliptic curve point addition. It is necessary to have point addition in Identity-Based Encryption (IBE)-based authentication protocols. Chen–Kudla modelled the point addition operation in the Tamarin Prover using a technique based on concatenation. However, this technique is not applicable to all identity-based protocols including IBE-based authentication protocols. In this paper, we present a modelling technique known as normalised precomputation for point addition using a hash function. We analyse the security of a simple identity-based encryption-based key exchange protocol under extended Canetti and Krawczyk’s (eCK) adversary model. Our analysis shows that the proposed technique is secure and retains the properties of point addition. Therefore, the technique can be applied to different IBE-based authentication protocols where point addition operation is necessary.