SecureScan

Research has shown that devices using the current WiFi standard are easily vulnerable to attacks which allow an adversary to compromise a user's privacy through identification and information disclosure. Many of these vulnerabilities arise as a result of the insecure design of the WiFi scanning protocol, or handshake. This project argues that the vulnerabilities present in the WiFi handshake make it unsuitable for privacy-conscious users, and contributes a new scanning protocol, SecureScan, which improves on the privacy vulnerabilities of the current WiFi implementation. The safety and liveness properties of SecureScan are shown to hold under a strong Dolev-Yao adversary, where the current WiFi implementation fails, using the Tamarin formal model checker. Furthermore, a high-level implementation of SecureScan in Python is published to demonstrate its correctness, privacy and efficiency in comparison to the current WiFi handshake. Experimental results are collected to show that SecureScan provides very strong privacy to mobile devices, approximately equivalent to being selected at random (mu_I = 0.922, sigma_I = 0.516), at the cost of requiring more time and power. Extrapolation of results infers that using a smaller key size may reduce the latency and power usage of the SecureScan handshake.

Overview

• protocol: Provides a formal specification for the SecureScan protocol using a Secure Protocol THeorY (.spthy) supported by Tamarin, an open access protocol security formal model checker. Contains a specification for the protocol as well as lemmas which demonstrate (and prove) the protocol's correctness and security in a Dolev Yao formal model and demonstrate corresponding attacks or vulnerabilities in the current WiFi standard.
• secure_scan: Provides an interface by which the SecureScan protocol can be utilised at a very high level. Consists of actors, who communicate via frames of data. AccessPoint actors have the capacity to broad their public key via a beacon, or to respond to a probe_request with a valid probe_response. Station actors have the capacity to respond to beacons with a probe_request and verify the validity of a received probe_response. See test for example usage.
• simulation: Provides a high level implementation of the protocol in Python, which performs analysis on WiFi traffic generated by both SecureScan and the current WiFi standard to quantify their security, privacy and efficiency. A Gaussian NB classifier is used to evaluate the privacy afforded to stations in the network based on their probe requests.
• plotter: Given a set of results retrieved from simulation, provides an interface by which said results can be shown in meaningful graphs.

Installation

The simulation module can be executed without installation. To install dependencies, run:

python -m pip install -r simulation/requirements.txt

The secure_scan module can be installed from TestPyPI:

python -m pip install -i https://test.pypi.org/simple/ SecureScan

Usage

The simulation module can be executed from the project's root directory:

python -m simulation

Use the -h flag to see a list of simulation parameters.

The secure_scan interface cannot be executed directly, but can be tested using pytest from the project's root directory:

python -m pytest

Development

The SecureScan protocol was developed as part of Alistair Robinson's third year dissertation in Computer Science at the University of Warwick DCS.