Research overview
Security protocols are an essential component in every secure communication. The SSL/TLS protocol, for example, plays a central role in securing communication over the web. The design of secure communication protocols is a challenging problem, both in the theoretical development and in implementation of tools to find attacks automatically. To ensure a protocol is secure one needs to anticipate all potential attacks, and an accurate model of potential attackers is crucial in increasing the coverage of attack surface. We have developed precise formal models of (potential) attackers and tools and techniques to automatically find attacks on security protocols under these attacker models. Two examples of such tools developed within our research group are:
- Proverif-ATP (https://github.com/darrenldl/ProVerif-ATP), which is built on top of the Proverif tool that has been widely used to verify real-world protocols.
- Tamgram (https://github.com/tamgram/tamgram), which is a high-level security protocol modelling language that translates to the backend verifier Tamarin, one of the most widely used security protocol verifiers.
Our current research includes:
- Scaling up the automation of protocol verification to handle complex real-world protocols.
Extending the attacker models in the state-of-the art protocol verifiers to improve their attack detection capabilities.