Design and Formal Analysis of an Authentication Protocol, eWMDP on Wearable Devices

Abstract

For wearable devices, this paper proposes an authentication protocol eWMDP. We formally model and analyze it. In the execution model of the protocol, a Dolev-Yao adversary is constituted. With the above, various security properties can be defined for measuring security performance. Our protocol can achieve the injective-auth property, in which case it surpasses another existing wearable authentication protocol-WMDP. In addition, our analysis work is confirmed by Scyther and tamain-prover, and the two protocols are implemented on PC and on Ti CC3200 LAUNCHPAD widely used in wearable devices in the meanwhile. The results of experiments highlight the higher transmission efficiency of eWMDP under various configurations, including different platforms, sorts of combinations of encryption algorithms and hash algorithms, and sending packets in different sizes.

Keywords

• Security protocol
• formal analysis
• wearable device protocol
• scyther
• tamarin-prover