Christoph Sprenger, ETH Zurich
From 12.00 until 13.30
At ETH Zurich, CNB/F/110
Universitätstrasse 6, 8092 Zurich
Abstract
In this talk, I will present a stepwise refinement framework for developing security protocols that are secure-by-construction. It is based on our previously proposed refinement strategy, which transforms abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style adversary. As intermediate levels of abstraction, we employ message-less guard protocols and channel protocols communicating over channels with security properties. In recent work, we substantially extended this framework. First, we strengthened the adversary by allowing him to compromise different resources of protocol participants, such as their long-term keys or their session keys. This enables the systematic development of protocols that ensure strong properties such as perfect-forward secrecy. Second, we broadened the class of protocols supported to include those with non-atomic keys and equationally defined cryptographic operators. Third, we implemented channels in a parametric way, under a set of assumptions that any concrete implementation must satisfy. This approach sheds light on the conditions that are needed for such implementations to be secure and makes security proofs more modular. These extensions required a major redesign of our original framework. We have implemented our method in Isabelle/HOL and used it to develop key agreement protocols including signed Diffie-Hellman and the core of IKEv1 and SKEME.
Joint work with Joseph Lallemand and David Basin