[TYPES/announce] Last Call for Participation: Trends in Mechanized Security Proofs, TMSP'17

[Carsten Schuermann]

NB: The EARLY BIRD registration deals expire on 6 August, 2017.  All participants have to register.


LAST CALL FOR PARTICIPATION

TMSP'17
First International Workshop on Trends in Mechanized Secruity Proofs
(collocated  with FCSD, 2017)
Oxford, UK
3 September 2017

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 (eutypes.cs.ru.nl <http://eutypes.cs.ru.nl/>) and co-organised by the DemTech project (www.demtech.dk <http://www.demtech.dk/>).  For workshop details including registration information, please visit FCSD homepage (//www.cs.ox.ac.uk/conferences/fscd2017/index.html <http://www.cs.ox.ac.uk/conferences/fscd2017/index.html>)

Best regards,
-- Herman Geuvers and Carsten Schürmann


PROGRAMME

0900-0930 REGISTRATION/TEA/COFFEE/CROISSANTS/FRUIT

0930-1015 Formal verification of cryptographic algorithms and implementations
 Gilles Barthe, IMDEA, Spain

1015-1100 Security Theorems via Model Theory
 Joshua Guttman, Worcester Polytechnic Institute, USA

1100-1130 TEA/COFFEE/BISCUITS

1130-1215 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

1215-1300 Deciding behavioral equivalences in the applied pi calculus: complexity, procedures and tool
 Vincent Cheval
 Loria, Nancy, France

1300-1400 LUNCH

1400-1445 Reality versus Security Proofs
 Cas Cremers
 Oxford University, Great Britain

1445-1530 Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate
 Bruno Blanchet, INRIA, France

1530-1600 TEA/COFFEE/CAKE

1600-1645 Linear resolution for stateful protocols
          Eike Ritter, University of Birmingham, Great Britain

1645-1730 PSPSP: Proper Security Proofs for Stateful Protocols
          Sebastian Mödersheim, Denmark's Technical University, Denmark


ABSTRACTS

-------------------------------------------------------------------
Title:   Formal verification of cryptographic algorithms and implementations
Speaker: Gilles Barthe

Abstract: 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.

-------------------------------------------------------------------
Title:   Security Theorems via Model Theory
Speaker: Joshua Guttmann

Abstract: 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.


-------------------------------------------------------------------
Title: A Formal Approach to Exploiting Multi-Stage Attacks based on SQL Injection and File-System Vulnerabilities of Web Applications
Speaker: Luca Vigano

Abstract: 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.


-------------------------------------------------------------------
Title: Deciding behavioral equivalences in the applied pi calculus: complexity, procedures and tool 
Speaker: Vincent Cheval

Abstract: 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. 

 
-------------------------------------------------------------------
Title: Reality versus Security Proofs 
Speaker: Cas Cremers

Abstract: 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.

 
-------------------------------------------------------------------
Title: Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate
Speaker: Bruno Blanchet

Abstract: 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

-------------------------------------------------------------------
Title:   Linear resolution for stateful protocols
Speaker: Eike Ritter

Abstract: 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


-------------------------------------------------------------------
Title:  PSPSP: Proper Security Proofs for Stateful Protocols
Speaker:  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




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20170803/0595306b/attachment-0001.html>