Formal analysis of device authentication applications in ubiquitous computing

Authentication between mobile devices in ad-hoc computing environments is a challenging problem. Without pre-shared knowledge, existing applications rely on additional communication methods, such as out-of-band or location-limited channels for device authentication. However, no formal analysis has been conducted to determine whether out-of-band channels are actually necessary. We answer this question through formal analysis, and use BAN logic to show that device authentication using a single channel is not possible.