Formal Model for Ad Hoc Pairing Covering Method Confusion
Formal Model for Ad Hoc Pairing Covering Method Confusion
Supervisor(s): | Ludwig Peuckert |
Status: | open |
Topic: | Software testing |
Type of Thesis: | Masterthesis |
DescriptionChair of IT Security / Prof. Dr. Claudia Eckert Announcement: Master Thesis in Cooperation with Fraunhofer AISEC, Garching Formal Model for Ad Hoc Pairing Covering Method ConfusionToday'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 DescriptionThis 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
Sources |