Modeling and analysis of LEAP, a key management protocol for wireless sensor networks

A formal analysis of a key management protocol, called LEAP (Localized Encryption and Authentication Protocol), intended for wireless sensor networks is presented in this paper. LEAP is modeled using the high level formal language HLSPL and checked using the AVISPA tool for attacks on the security and authenticity of the exchanges. We focus on the protocol's establishment of pairwise keys for nearest neighbors and for multi-hop neighbors. We then use this foundation to test the protocol's method of cluster key redistribution. Finally, we check LEAP's use of μTESLA, an authentication protocol utilized a one-way key chain and delayed key disclosure, which LEAP uses for authentication of node revocation messages.