Formal Analysis of Secure Device Pairing Protocols

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.