Formal Verification of Forward-Secure Authenticated Key Exchange Scheme for Location-based Service Application
Mahesh Kumar K.M1, Pradeep R2, Sunitha N.R3
1Mahesh Kumar K.M, Department of CSE, Siddaganga Institute of Technology, Tumakuru (Karnataka), India.
2Pradeep R, Department of CSE, Siddaganga Institute of Technology, Tumakuru (Karnataka), India.
3N.R. Sunitha, Department of CSE, Siddaganga Institute of Technology, Tumakuru (Karnataka), India.
Manuscript received on 03 December 2019 | Revised Manuscript received on 11 December 2019 | Manuscript Published on 31 December 2019 | PP: 129-136 | Volume-9 Issue-2S December 2019 | Retrieval Number: B10731292S19/2019©BEIESP | DOI: 10.35940/ijitee.B1073.1292S19
Open Access | Editorial and Publishing Policies | Cite | Mendeley | Indexing and Abstracting
© The Authors. Blue Eyes Intelligence Engineering and Sciences Publication (BEIESP). This is an open-access article under the CC-BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)
Abstract: A Location-based service (LBS) is a popular information service which uses the geographical position of the user to provide service. Major challenges for wide deployment of such services is security and privacy, in our paper we propose a generic model of authenticated key exchange (AKE)protocol termed as forward-secure authenticated key exchange protocol (FSAKE) which uses elliptic curve cryptosystem. TheFSAKE protocol supports concurrent sessions and is used for the exchange of secure seed values which are used in forward-securepseudo-random number generators to generate secret keys for message authentication and symmetric encryption. The FSAKE protocol is a key evolving scheme which updates the long-termkeys (LTKs) at regular intervals and guarantees the security of the past keys and mitigates the damage caused by exposure of the current key. We make use of Scy ther model checking tool to prove the correctness of FSAKE protocol security.
Keywords: Authenticated Key Exchange, Elliptic Curve Cryptography, Forward-Security, Formal Verification, Location-Based Services, Symmetric Key Evolving Systems.
Scope of the Article: Secure Mobile and Multi-Agent Systems