Extending Formal Analysis of Mobile Device Authentication

William Claycomb

CERT Program*

Software Engineering Institute

Pittsburgh, PA, USA

claycomb@cert.org

Dongwan Shin

Computer Science and Engineering

New Mexico Tech

Socorro, NM, USA

doshin@nmt.edu

Abstract

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 outof-

band channels are actually necessary, or more importantly, whether the protocols used to establish

ad-hoc communication can be proven secure. We seek to answer these questions through formal

analysis of authentication protocols in mobile device applications. Specifically, we use BAN logic

to show that device authentication using a single channel is not possible, and propose a BAN logic

extension to help prove correct existing authentication protocols. We demonstrate our analysis by

applying our extensions to existing mobile device authentication applications.

*CERT and CERT Coordination Center are registered in the U.S. Patent

and Trademark Office by Carnegie Mellon University.