Systematic Analysis of Security Protocol Implementations

Security protocols play a crucial role in protecting all the digital communications and interactions we rely on in our modern society. This includes many Internet-based services,  but also traditional telecom such as GSM, using our bank cards in ATMs or in shops, or using RFID cards in public transport. However, implementing such protocols so that they are secure has proven to be a great challenge, and flaws are uncovered on a regular basis, even in the leading implementations of the most important protocols. The prime example here is TLS, which is used to secure all HTTPS Internet connections. Leading implementations of TLS suffered from embarrassing security flaws, such as the infamous Heartbleed attack in the OpenSSL implementation, which affected millions of web servers worldwide. While great strides have been made in the past 15 years in the formal analysis of abstract security protocols (resulting in mature automated analysis tools such as ProVerif), the long list of security flaws discovered in implementations of protocols such as TLS clearly shows that when it comes to implementing such protocols, we still lack the tools and techniques to ensure correctness and security.

To address this problem, this workshop brings together researchers from different communities - computer security, cryptography, software engineering, and formal methods. The participants include researchers who are used to looking at security and security protocols (from an IT security or a more cryptographic perspective), but also researchers who work on generic software engineering techniques, e.g. for testing, or on formal methods as a way to model and analyse systems. The goal of the workshop is to identify gaps in the current analyses of implementations of security protocols and explore how recent scientific advances in the different fields can be combined to improve the state-of-the-art in security analysis techniques.