Formal analysis of PKM using scyther tool

Owing to the natural characteristics of wireless communication, anyone can intercept or inject frames, making wireless communication much more vulnerable to attacks than its wired equivalents. In this paper we focused on the PKM protocol which provides the authorization process and secure distribution of keying data from the base station to mobile station. Concentrating on PKMv2, we give a formal analysis of this version and we found that is vulnerable to replay, DoS, Man-in-the middle attacks. We propose a new methodology to prevent the authorization protocol from such attacks by using nonce and timestamp together.