ETH scientists present approach to improve communication security

At home, in the office and in public – online security is at the forefront of everyone’s mind. In their recently published book, Cas Cremers and Sjouke Mauw present a new methodology that can help prevent intruders from reading, modifying, or inserting communications.

There are countless ways in which we nowadays use the internet: we send e-mails or facebook messages, we shop online, we pay our bills online. In all these cases, we rely on the internet’s safety. The more important the internet gets in almost all areas of both our work and private life, the more urgent the internet’s safety becomes. In “Operational Semantics and Verification of Security Protocols”, the authors Cas Cremers, senior scientist at ETH’s Institute of Information Security, and Sjouke Mauw, professor of Security and Trust of Software Systems at the University of Luxembourg, describe an approach that can improve internet security and thus protects our private e-mails and – even more importantly – our credit card information.

To secure data communication, we need security protocols. Such protocols run in the background of a program or browser and mostly users do not even realize they exist. When you see the lock symbol in your browser during a purchase, you are using a security protocol. Similarly, you use such a protocol when you connect to the university’s network from home via VPN. In fact, most of the networked devices we use on a daily basis critically depend on such protocols in order to prevent others from eavesdropping or modifying our messages.

Many protocols depend on the use of cryptographic keys. These keys must be kept secret in order to achieve a secure communication – for example in order to make sure that credit card details cannot be intercepted by anybody else. Unfortunately, many protocols contain errors in their design, which allow an attacker to read or modify private communication. To tackle this problem, Cremers and Mauw developed a formal approach to security protocols. Mauw elaborates: "We are convinced that the problems concerning security protocols are of a very fundamental nature. This led us to work on our rigorous and mathematical approach, which in the end resulted in a very practical tool." Thus, the two researchers also implemented a tool from their algorithm – a tool that is already actively used in several countries.

During the last decade, there has been a growing realization that formal approaches are invaluable in assessing and improving the security of systems. For the coming decade, the authors predict a significant uptake of these methods. "Governments and companies have historically relied only on manual inspection by experts," says Cremers. "We are now providing the evidence that our methods can help to significantly improve security, and often find problems that were missed by security experts."

The book “Operational Semantics and Verification of Security Protocols” covers the methodological background as well as case studies to show how the methodology can be applied. It is well-suited for teaching courses in the area of information security at the Master's level. The exercises at the end of each chapter allow students to practice with these concepts. Additionally, the book provides a good starting point for PhD students or researchers who want to understand the analysis tools, develop new protocols, or analyze existing ones. It also includes an extensive related work section that can serve as a springboard for research.