Formal Security Analysis of Cryptographic Protocols

Cryptographic protocols are distributed algorithms that allow entities to perform security-related functions over a (potentially untrusted) network. Such protocols are ubiquitous, and their security is essential to almost any IT system.

It is quite challenging to create secure protocols as even small non-obvious mistakes can have fatal consequences. For example, the (very simple) Needham-Schroeder key exchange protocol contains a severe security flaw that went unnoticed for 17 years. For modern security protocols, such as TLS, it is even harder to ensure security. These protocols tend to be much more complex and are typically embedded into environments that introduce their own quirks and subtleties.

Formal methods provide a systematic way to perform comprehensive analyses of such protocols concisely and rigorously. They allow us to specify security goals precisely and enable us to prove that a protocol indeed guarantees such properties. Using this approach, we can find attacks (if a proof fails), develop fixes, and formally verify whether our fixes are sufficient. Moreover, we can even exclude unknown classes of attacks on the systems we analyse.

Although this field has been quite active in research for several decades now, there are still many open research questions to answer: Existing tools and approaches often struggle with analyses of complex protocols. Proofs are often quite laborious and are susceptible to human errors. Furthermore, modern environments such as Web, Mobile, and IoT also introduce their own complexity and pitfalls and blend into each other, creating new subtleties which can be an additional source of security issues. Hence, we need to develop new methods and techniques to tackle this complexity, mechanise and automate such security analyses to more extent, and take the characteristics of modern environments into account.

We are looking for applications from highly talented candidates with a background in computer science, information security, mathematics, or a related field interested in logic, proofs, and formal analysis techniques. We value strong analytical skills and solid programming knowledge. Prospective applicants are welcome to discuss with Dr Guido Schmitz