Formal Verification of Forward-Secure Authenticated Key Exchange Scheme for Location-based Service Application

Abstract

A Location-based service (LBS) is a popularinformation service which uses the geographical position of theuser to provide service. Major challenges for wide deploymentof 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 exchangeprotocol (FSAKE) which uses elliptic curve cryptosystem. TheFSAKE protocol supports concurrent sessions and is used fortheexchange of secure seed values which are used in forward-securepseudo-random number generators to generate secret keys formessage authentication and symmetric encryption. The FSAKEprotocol is a key evolving scheme which updates the long-termkeys (LTKs) at regular intervals and guarantees the security ofthe past keys and mitigates the damage caused by exposure ofthe current key. We make use of Scyther model checking tool toprove the correctness of FSAKE protocol security.