### Modelling IBE-based Key Exchange Protocol using Tamarin Prover

Srijanee Mookherji, Vanga Odelu, and Rajendra Prasath

##### Abstract

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)
Category
Cryptographic protocols
Publication info
Preprint. MINOR revision.
Keywords
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
History
Short URL
https://ia.cr/2021/1598

CC BY

BibTeX

@misc{cryptoeprint:2021/1598,
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{https://eprint.iacr.org/2021/1598}},
url = {https://eprint.iacr.org/2021/1598}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.