Automated analysis of security protocol implementations

McMahon Stone, Christopher (2021). Automated analysis of security protocol implementations. University of Birmingham. Ph.D.

Preview

McMahonStone2021PhD.pdf
Text - Accepted Version
Available under License All rights reserved.
Download (2MB) | Preview

Abstract

Security protocols, or cryptographic protocols, are crucial to the functioning of today’s technology-dependant society. They are a fundamental innovation, without which much of our online activity, mobile communication and even transport signalling would not be possible. The reason for their importance is simple, communication over shared or publicly accessible networks is vulnerable to interception, manipulation, and impersonation. It is the role of security protocols to prevent this, allowing for safe and secure communication.

Our reliance on these protocols for such critical tasks, means it is essential to engineer them with great care, just like we do with bridges or a safety-critical aircraft engine control system, for example. As with all types of engineering, there are two key elements to this process – design and implementation. In this thesis we produce techniques to analyse the latter. In particular, we develop automated tooling which helps to identify incorrect or vulnerable behaviour in the implementations of security protocols.

The techniques we present follow a theme of trying to infer as much as we can about the protocol logic implemented in a system, with as little access to it’s inner workings as possible. In general, we do this through observations of protocol messages on the network, executing the system, but treating it as a black-box. Within this particular framework, we design two new techniques – one which identifies a specific vulnerability in TLS/SSL, and another, more general approach, which systematically extracts a protocol behaviour model from protocols like the WiFi security handshakes. We then argue that it his framework limits the potential of model extraction, and proceed to develop a solution to this problem by utilising grey-box insights. Our proposed approach, which we test on a variety of security protocols, represents a paradigm shift in the well established model learning field.

Throughout this thesis, as well as presenting general results from testing the efficacy of our tools, we also present a number of vulnerabilities we discover in the process. This ranges from major banking apps vulnerable to Man-In-The-Middle attacks, to CVE assigned ciphersuite downgrades in popular WiFi routers.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):