print · login   

TMSP: Trends in Mechanized Security Proofs

EUTypes WG4 meeting / Satellite workshop of FSCD 2017, Oxford, UK, 3 September 2017

Overview

Recent cyber attacks against the US election have shown: the more valuable a target the higher the likelihood that it will be attacked. Adversaries, in particular nation states, have nearly unlimited capacity to devise cyberattacks and exploit even the smallest vulnerabilities.

In this first international workshop on Trends in Mechanized Security Proofs, we will discuss, how formal methods, logic, type theory, and automated reasoning tools can contribute to solving the security challenges of tomorrow. In particular, we have invited expert speakers to present

  • the current state of the art in mechanized security proofs,
  • rich type systems for security
  • case studies in mechanized security proofs
  • the formal modeling and adequacy of threat models
  • security proofs in the symbolic model versus semantic security proofs

This workshop is funded by the EUTypes COST project and co-organised by the DemTech project For workshop details including registration information, please visit the FCSD homepage

Program

  • 09:00 - 09:30 Registration/Tea/Coffee/Croissants/Fruit
  • 09:30 - 10:15 Formal verification of cryptographic algorithms and implementations
    Gilles Barthe, IMDEA, Spain
  • 10:15 - 11:00 Security Theorems via Model Theory
    Joshua Guttman, Worcester Polytechnic Institute, USA
  • 11:00 - 11:30 Tea/Coffee/Biscuits
  • 11:30 - 12:15 A Formal Approach to Exploiting Multi-Stage Attacks based SQL Injection and File-System Vulnerabilities of Web Applications
    Luca Vigano, King's College London, Great Britain
  • 12:15 - 13:00 Deciding behavioral equivalences in the applied pi calculus: complexity, procedures and tool
    Vincent Cheval Loria, Nancy, France
  • 13:00 - 14:00 Lunch
  • 14:00 - 14:45 Reality versus Security Proofs
    Cas Cremers Oxford University, Great Britain
  • 14:45 - 15:30 Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate
    Bruno Blanchet, INRIA, France
  • 15:30 - 16:00 Tea/Coffee/Cake
  • 16:00 - 16:45 Linear resolution for stateful protocols
    Eike Ritter, University of Birmingham, Great Britain
  • 16:45 - 17:30 PSPSP: Proper Security Proofs for Stateful Protocols
    Sebastian Mödersheim, Denmark's Technical University, Denmark

Abstracts

  • Formal verification of cryptographic algorithms and implementations - Gilles Barthe
    Computer-aided cryptography develops formal methods for the design, analysis, and verification of cryptographic algorithms and implementations. I will outline some of our most recent work along these lines.
  • Security Theorems via Model Theory - Joshua Guttmann
    We usually think of theorems as established by syntactic deduction, and many approaches to proving security are based on that core idea. However, theorems can also follow from systematic exploration of models. In this talk, we will explain how executions of security protocols and related systems can be viewed as models of suitable theories. These models have a natural structure determined by their homomorphisms. CPSA, a Cryptographic Protocol Shapes Analyzer, uses this homomorphism structure to control an enumeration of protocol executions. It identifiers a strongest security goal achieved in each scenario it analyzes. We extend this approach via more general model-finding to executions that may involve access control policies and other security mechanisms. Joint work with Dan Dougherty, Moses Liskov, John Ramsdell, and Paul Rowe.
  • A Formal Approach to Exploiting Multi-Stage Attacks based on SQL Injection and File-System Vulnerabilities of Web Applications - Luca Vigano
    We propose a formal approach that allows one to (i) reason about file-system vulnerabilities of web applications and (ii) combine file-system vulnerabilities and SQL-Injection vulnerabilities for complex, multi-stage attacks. We have developed an automatic tool that implements our approach and we show its efficiency by discussing four real-world case studies, which are witness to the fact that our tool can generate, and exploit, attacks that, to the best of our knowledge, no other tool for the security of web applications can find. This is joint work with Federico De Meo and Marco Rocchetto.
  • Deciding behavioral equivalences in the applied pi calculus: complexity, procedures and tool - Vincent Cheval
    Many security properties are naturally expressed in terms of indistinguishability. In symbolic protocol models the notion of indistinguishability can be expressed as trace equivalence in a cryptographic process calculus. Current automated verification tools are however limited even for a bounded number of sessions: they are either restricted to support only a particular set of cryptographic primitives, do not allow for protocols with else branches, or can only approximate trace equivalence, allowing for false attacks. Moreover, the complexity of these algorithms has never been studied. I will discuss in this talk about the new complexity results we established for static equivalence, trace equivalence and labelled bisimilarity. Moreover, I will also shortly present our new decision procedure for these equivalences in the case of a bounded number of sessions.
  • Reality versus Security Proofs - Cas Cremers
    The field of security proofs, both in the symbolic models and in the more traditional semantic security setting, have made huge advances in the last few decades. Parts of such analysis can now automated, and in some cases proofs and attacks can be found automatically. In this talk I introduce the Tamarin prover, highlight some of these case studies, and focus on some of the many gaps between analysis and reality that still remain.
  • Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate - Bruno Blanchet
    TLS 1.3 is the next version of the Transport Layer Security (TLS) protocol. Its clean-slate design is a reaction both to the increasing demand for low-latency HTTPS connections, and to a series of recent high-profile attacks on TLS. The hope is that a fresh protocol with modern cryptography will prevent legacy problems; the danger is that it will expose new kinds of attacks, or reintroduce old flaws that were fixed in previous versions of TLS. After 18 drafts, the protocol is nearing completion, and the working group has appealed to researchers to analyze the protocol before publication. We respond by presenting a comprehensive analysis of TLS 1.3 Draft-18: (1) We present symbolic ProVerif models for various intermediate versions of TLS 1.3 and evaluate them against a rich class of attacks to reconstruct both known and previously unpublished vulnerabilities that influenced the current design of the protocol. In particular, we test whether TLS 1.3 prevents well-known attacks on TLS 1.2, such as Logjam or the Triple Handshake, even if it is run in parallel with TLS 1.2. (2) We present a computational CryptoVerif model for TLS 1.3 Draft-18 and mechanically prove its security under standard (strong) assumptions on its cryptographic primitives. (3) We present RefTLS, an interoperable implementation of TLS 1.0-1.3 and automatically analyze its protocol core by extracting a ProVerif model from its typed JavaScript code. The talk will mainly focus on (2) and briefly sketch (1) and (3). Joint work with Karthikeyan Bhargavan and Nadim Kobeissi, published at IEEE S&P 2017
  • Linear resolution for stateful protocols - Eike Ritter
    Global mutable state raises specific problems for automated tools for security protocol verification. In particular, a system can be in exactly one state at a given time, but this property is not modelled correctly by the resolution procedure employed e.g. in ProVerif. In this talk we present a sound and complete resolution system based on linear logic which models this property correctly. We also discuss ways of using the resolution for security protocol verification. Joint work with Alessandro Bruni and Carsten Schürmann
  • PSPSP: Proper Security Proofs for Stateful Protocols - Sebastian Mödersheim
    This work combines three aspects of mechanized security proofs. (1) The most popular abstraction techniques for security protocol verification (e.g. in ProVerif) basically throws away most state information by computing an over-approximation of all facts that become true in any reachable state. While efficient for many simple protocols, this does not work on stateful protocols e.g. when we have a webserver who maintains a database. We overcome this limitation by a more refined abstraction that integrates state information into the abstraction but without destroying the spirit and efficiency of the original method. (2) Verification tools may have bugs and accidentally prove correct an insecure protocol. We want to minimize the amount of trust we have to have in tools and thus produce proofs that can be checked by the Isabelle/HOL automatically – so that we only rely on the correctness of the Isabelle core. (3) This and many other works rely on a typed model, where the intruder cannot send arbitrary ill-typed messages. There are several relative-soundness results that show (for a certain class of protocols) that if there is an attack then there is a well-typed attack, i.e., that it is sound to verify the protocol in a typed model. We have also formalized this proof in Isabelle, including a formalization of the “Lazy Intruder” technique, descovering several flaws in the existing pen-and-paper proofs. Joint work with Achim Brucker, Alessandro Bruni, and Andreas Viktor Hess

Organisers

  • Carsten Schürmann
  • Herman Geuvers