Information Security Group

Search

EN

Formalising computational soundness for protocol implementations

Members

Introduction

Security protocols specify how agents or systems exchange information so as to achieve security guarantees. These protocols usually involve cryptography and aim to authenticate agents and their messages, exchange session keys, protect the confidentiality of transmitted data, etc. They are omnipresent and provide the cornerstone of security in distributed settings like the Internet; SSL/TLS (for secure connections to servers), Kerberos (for distributed authorization and authentication), and IPSec (for building virtual private networks) are three popular examples.

Unfortunately, as history has shown, it is notoriously difficult for protocol designers to correctly design security protocols and for implementors to implement them securely; numerous protocols, standardized and implemented, have been later successfully attacked and broken by adversaries or researchers playing in that role. Development and verification methods with formal guarantees can support designers and implementors in their work. They provide confidence that the protocols achieve their claimed security goals, especially when the methods rely on machine support at all stages of development. 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 have been developed by cryptographers to prove computational security guarantees as studied in the cryptographic literature. The resulting proofs are very technical and far too complex for the average designer or implementor, and preliminary tool support for tiny protocols is just emerging. In contrast, for the symbolic models, security properties can be stated concisely, and methods and tools for automated security analyses are plentiful and scalable. It seems therefore promising to explore the use of symbolic methods. However, there are two huge gaps:

  1. the gap between symbolic protocol models and their implementations, and
  2. the gap between symbolic attackers and computational security.

Computational soundness results can fill the second gap: they relate guarantees established for high-level symbolic models to cryptographic notions of security. The existing results, however, are complex constructions with subtle proofs, numerous assumptions, and confusing restrictions. Still, it seems worthwhile to further explore this direction: Computational soundness combines the best of both worlds and turns symbolic analysers from debuggers into verification tools with strong guarantees. At the same time, such results narrow the first gap because they transform symbolic models into computational ones, which are closer to real-world implementations.

Objectives

We envision a tool chain that supports protocol designers all the way from symbolic models via computational soundness to prototype implementations. The tool chain will help to ensure that new protocol designs come with security proofs and reference implementations that are correct by construction. This project focuses on the formal foundations underlying this tool chain: computational soundness results and the correctness of the soundness arguments. The constructions and proofs will be formalised in the proof assistant external page Isabelle/HOL. This maximises confidence in their correctness because Isabelle mechanically checks that all steps are indeed correct and it exposes all assumptions needed for the proof. This will yield the first formalisation of computational soundness results. At the same time, it will clarify the existing results and their limitations and try to generalise and lift them, respectively; formalisation supports this as it directly exposes all assumptions and restrictions and clarifies their role.

On the symbolic level, the formalisation will connect to the existing tool scyther-proof for symbolic protocol verification. The approach and the tool both benefit from the combination: On the one hand, the pool of protocol models which has been previously developed is available — we will apply our results to them and evaluate the feasibility of our approach. On the other hand, the results of the formalisation will substantially enhance the usefulness and impact of the tool because they will enable their use for computational verification instead of just debugging symbolic models.

As the computational models are close to real-world implementations, code generation bridges the remaining gap. The formalisation will be designed such that the computational models are directly executable using Isabelle’s code generator. This way, one automatically obtains an executable implementation that achieves the proven security goals. In particular, the implementation cannot introduce errors that enable the attacker to break the security guarantees. For future protocol designs, the approach will produce secure prototypes that can serve as reference implementations for standardisation.

Publications

Software

JavaScript has been disabled in your browser