Paper 2021/1598

Modelling IBE-based Key Exchange Protocol using Tamarin Prover

Srijanee Mookherji, Vanga Odelu, and Rajendra Prasath


Tamarin Prover is a formal security analysis tool that is used to analyse security properties of various authentication and key exchange protocols. It provides built-ins like Diffie-Hellman, Hashing, XOR, Symmetric and Asymmetric encryption as well as Bilinear pairings. The shortfall in Tamarin Prover is that it does not support elliptic curve point addition operation. In this paper, we present a simple IBE (Identity-Based Encryption) based key exchange protocol and tamarin model. For modelling, we define a function to replace the point addition operation by the concept of pre-computation. We demonstrate that the security model functions for theoretical expectation and is able to resist Man-In-The-Middle (MITM) Attack. This model can be used to analyse the formal security of authentication and key exchange protocols designed based-on the IBE technique.

Available format(s)
Cryptographic protocols
Publication info
Preprint. MINOR revision.
Tamarin ProverKey Exchange ProtocolIdentity Based EncryptionMan-In-The-Middle attackElliptic Curve Point Addition Operation
Contact author(s)
srijanee mookherji @ iiits in
odelu vanga @ iiits in
rajendra prasath @ iiits in
2021-12-09: received
Short URL
Creative Commons Attribution


      author = {Srijanee Mookherji and Vanga Odelu and Rajendra Prasath},
      title = {Modelling IBE-based Key Exchange Protocol using Tamarin Prover},
      howpublished = {Cryptology ePrint Archive, Paper 2021/1598},
      year = {2021},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.