Formal Model for Ad Hoc Pairing Covering Method Confusion

Description

Chair of IT Security / Prof. Dr. Claudia Eckert

Announcement: Master Thesis in Cooperation with Fraunhofer AISEC, Garching

Formal Model for Ad Hoc Pairing Covering Method Confusion

Today's general-purpose ecosystems for ad hoc pairing (e.g., Bluetooth) consist of multiple pairing methods, which are required to support a large variety of devices. The interworking of different pairing methods, however, supposes the threat of Method Confusion as shown in [1]. While no solution to the Method Confusion exists today, a prerequisite is an approach to reliably analyze the security of such a fix. 

A promising approach to proof security properties is Formal Verification, which was applied successfully multiple times in the past. The application of Formal Verification is elaborate and, thus, the first formal model to analyze a whole ad hoc ecosystem was developed only recently in [2]. The approach, however, has two limitations: it is focused on the Bluetooth ecosystem only, and, more important, it can only detect Method Confusion partially.  

Task Description

This thesis aims to expand the approach in [2] and develop a general model for formal verification of ad hoc pairing capable to detect Method Confusion. First, the discrepancies in the given model are discovered and resolved. Afterward, the model is adapted for ad hoc pairing in general. Eventually, the model is applied to analyze potential fixes for the Method Confusion Attack. 

Requirements

• Knowledge of Protocol Security
• Ideally obtained from the lectures IT-Security and Secure Mobile Systems
• First experiences in Formal Verification or Model Checking

Sources

• [1] Method Confusion Attack on Bluetooth Pairing
• [2] Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities