Formal Analysis of Secure Device Pairing Protocols
Trung Nguyen, Jean Leneutre · 2014
The need to secure communications between personal devices is increasing nowadays, especially in the context of Internet of Things. Authentication between devices which have no prior common knowledge is a challenging problem. One solution consists in using a pre-authenticated auxiliary channel, human assisted or location limited, usually called out-of-band channel. A large number of device pairing protocols using an out-of-band channel were proposed, but they usually suffer from a lack of formal analysis. In this paper, we introduce a formal model, conceived as an extension of Strand Spaces, to analyze such protocols. We use it to analyze a device pairing protocol with unilateral out-of-band channel proposed by Wong & Stajano. This leads us to discover some vulnerabilities in this protocol. We propose a modified version of the protocol together with a correctness proof in our model.