Paper 2021/1598
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.
Metadata
- Available format(s)
-
PDF
- 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
- 2021-12-09: received
- Short URL
- https://ia.cr/2021/1598
- License
-
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}
}
