Paper 2021/1598 Original: eprint.iacr.org/2021/1598 ↗
Modelling IBE-based Key Exchange Protocol using Tamarin Prover
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.
- History
- 2021-12-09: last updated
- 2021-12-09: published
- Short URL
- https://ia.cr/2021/1598
- License
- https://creativecommons.org/licenses/by/4.0/
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},
url = {https://eprint.iacr.org/2021/1598}
}