Cryptology ePrint Archive: Report 2021/1598

Modelling IBE-based Key Exchange Protocol using Tamarin Prover

Srijanee Mookherji and 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.

Category / Keywords: cryptographic protocols / Tamarin Prover, Key Exchange Protocol, Identity Based Encryption, Man-In-The-Middle attack, Elliptic Curve Point Addition Operation

Date: received 7 Dec 2021

Contact author: srijanee mookherji at iiits in, odelu vanga at iiits in, rajendra prasath at iiits in

Available format(s): PDF | BibTeX Citation

Version: 20211209:031307 (All versions of this report)

Short URL: ia.cr/2021/1598


[ Cryptology ePrint archive ]