Security protocol verification
(TLS) is used to establish secure communication channels between clients and servers and Internet Protocol Security (IPsec) can be used to set up virtual private networks. These protocols are omnipresent and are used to access and protect numerous applications, ranging from banking to social media. Unfortunately, as history has shown, it is notoriously difficult for protocol designers to correctly design security protocols and for programmers to implement them securely. Numerous protocols, standardized and implemented, have later been successfully attacked and broken. We are developing tools that support protocol designers in their activities, particularly for creating models and analyzing their properties. Our work encompasses the development of an automated symbolic cryptographic protocol verification tool, called Tamarin. The Tamarin prover is a state-of-the-art automated symbolic cryptographic protocol verification tool. It supports both verification and falsification (attack-finding) of security protocols. The tool has helped improve standards and other proposed protocols before deployment by finding attacks, and then proving absence of those attacks after the protocols are improved. Examples include the TLS v1.3 standard, next-generation mobile communication 5G-AKA, the Attack-Resilient Public Key Infrastructure (ARPKI), group Joux, group Diffie-Hellman (GDH), and identity-based protocols. Formal guarantees underlying our symbolic protocol verification tools provide confidence that the protocols achieve their claimed security goals. Formal guarantees require a model of the protocol, its desired properties, and the capabilities of possible adversaries. Two kinds of models are well-established: concrete computational models and abstract symbolic models. Computational models are close to real-world implementations but are technical and far too complex for the average designer or implementor and quite narrow in scope, e.g., usually addressing each mode of a protocol in isolation. Conversely, methods and tools for automated security analyses of symbolic models are scalable and address the combination of all modes.
Publications
David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirovic, Ralf Sasse, Vincent StettlerA Formal Analysis of 5G Authentication.
In Proceedings of the 25th ACM SIGSAC Conference on Computer and Communications Security (CCS), 2018.
Jannik Dreier, Lucca Hirschi, Saša Radomirovic, Ralf Sasse
Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR.
In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF), 2018.
David Basin, Cas Cremers, Jannik Dreier, Ralf Sasse
Symbolically Analyzing Security Protocols using TAMARIN.
SIGLOG Newsletter October 2017, 2017.
Jannik Dreier, Charles Duménil, Steve Kremer, Ralf Sasse
Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols.
In Proceedings of the 6th Conference on Principles of Security and Trust (POST), 2017.
Andreas Lochbihler
Probabilistic Functions and Cryptographic Oracles in Higher-Order Logic.
In Proceedings of the 25th Symposium on Programming Languages and Systems (ESOP 2016), 2016.
David Basin, Sasa Radomirovic, Lara Schmid
Modeling Human Errors in Security Protocols
In Proceedings of the 29th IEEE Computer Security Foundations Symposium (CSF), 2016.
Andreas Lochbihler and Joshua Schneider
Equational Reasoning with Applicative Functors
In Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), 2016.
David Basin, Jannik Dreier, Ralf Sasse
Automated Symbolic Proofs of Observational Equivalence
In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS), 2015.
David Basin, Cas Cremers, Tiffany Hyun-Jin Kim, Adrian Perrig, Ralf Sasse, and Pawel Szalachowski
ARPKI: Attack Resilient Public-Key Infrastructure
In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS), 2014.
Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin
Automated Verification of Group Key Agreement Protocols
In Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P), 2014.
Simon Meier and Cas Cremers and David A. Basin
Efficient Construction of Machine-Checked Symbolic Protocol Security Proofs
In Journal of Computer Security, Vol. 21, no. 1, 2013.
Simon Meier, Benedikt Schmidt, Cas Cremers, David Basin
The TAMARIN Prover for the Symbolic Analysis of Security Protocols (Tool Paper)
In Proceedings of the 25th International Conference on Computer Aided Verification (CAV), 2013.
Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin
Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF), 2012.
Simon Meier and Cas Cremers and David Basin
Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs
In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF ’10), 2010.