Extending Formal Analysis of Mobile Device Authentication
Authentication between mobile devices in ad-hoc computing environments is a challenging problem. Without pre-shared knowledge, existing applications must rely on additional communication methods, such as out-of-band or location-limited channels for device authentication. Much of the focus in development of new applications in this area seeks to reduce or eliminate the impact of this additional requirement. However, no formal analysis has been conducted to determine whether out-of-band channels are actually necessary, or more importantly, whether the protocols used to establish ad-hoc communication can be proven secure. The authors seek to answer these questions through formal analysis of authentication protocols in mobile device applications.