FCS-PrivMod on Thursday, July 15th

09:00‑10:00 Session 4
Chair: Véronique Cortier
Location: AT LT1
09:00 Hubert Comon-Lundh (CNRS & ENS de Cachan)
Symbolic and computational proofs of security
10:30‑12:30 Session 5
Chair: Bart Jacobs
Location: AT LT1
10:30 Karthikeyan Bhargavan, Cédric Fournet and Nataliya Guts
Pre- and Post-conditions for Security Typechecking

We verify implementations of cryptographic protocols that manipulate recursive data structures, such as lists. Our main applications are X.509 certificate chains and XML digital signatures. These applica- tions are beyond the reach of automated provers such as ProVerif, since they require some form of induction. They can be verified using the F7 refinement typechecker, at the cost of annotating each data-processing function with logical formulas embedded in its type. However, this en- tails the duplication of many library functions, so that each instance can be given its own type. We propose a more flexible method for verifying ML programs that use cryptography and recursion. We annotate standard library func- tions (such as list processing functions) with precise, yet reusable types that refer to the pre- and post-conditions of their functional arguments, using generic logical predicates. We use these predicates both to spec- ify higher-order functions and to track security events in programs and cryptographic libraries. We implement our method by extending the F7 typechecker with automated support for these predicates. We evaluate our approach experimentally by verifying a series of security libraries and protocols.

11:00 Morten Dahl and Hans Hüttel
Don't Let The Opponents Grind You Down

The use of safety type systems for static verication of cryptographic protocols has seen widespread use in recent years; the approach has been that of type checking. To facilitate proof generation, type inference is also a desirable property of these type systems and has been studied by a number of authors. However, it is popular for safety type systems with symmetric cryptography to employ two sets of typing rules in order to also capture the behaviour and interaction of an adversary. This complicates type inference, since there now is a choice of which rule to use. A possible approach, followed by Kikuchi and Kobayashi, is to redesign the type system so that the choice disappears. In this paper we show that this is not necessary: we construct a polynomial time algorithm for choosing which rule to apply in the original type system. We present our approach in the setting of the type system of Authenticity by Typing for Security Protocols by Gordon and Jerey, but it can be successfully applied to several safety type systems with symmetric cryptography and opponent typing.

11:30 Radha Jagadeesan, Alan Jeffrey, Corin Pitcher and James Riely
Confidential Safety via Correspondence Assertions

We study confidential safety, a notion of secrecy that arises naturally in adversarial systems. We provide a formal definition in the context of a concurrent while-language. We provide techniques for establishing confidential safety, building on three ingredients:

(1) We develop a novel view of correspondence assertions that focuses on their confidentiality (in contrast to the traditional view of correspondence assertions that uses their integrity to derive secrecy and authentication properties of protocols). (2) We establish the confidentiality of a correspondence assertion using techniques reminiscent of information flow, and incorporating cryptography using confounders. (3) We prove protocols are confidentially safe using techniques based on frame-bisimulation that exploit the noninterference properties of well-typed programs.

12:00 Sreekanth Malladi
Protocol independence through disjoint encryption under Exclusive-OR

Protocol interaction has been a notorious problem for security. Gutman-Thayer proved that, attacks due to protocol interaction can be prevented, by ensuring that encrypted messages are distinguishable across protocols, under a free algebra. In this paper, we prove that a similar suggestion prevents those attacks under commonly used operators such as Exclusive-OR, that induce equational theories and break the free algebra assumption.

14:00‑15:00 Session 6
Chair: Vitaly Shmatikov
Location: AT LT1
14:00 Michael Clarkson (Cornell University)
Privacy in Electronic Voting
15:30‑17:00 Session 7
Chair: Catuscia Palamidessi
Location: AT LT1
15:30 Morten Dahl, Stéphanie Delaune and Graham Steel
Formal Analysis of Privacy for Vehicular Mix-Zones

Safety critical applications for newly proposed vehicle to ve- hicle ad-hoc networks (VANETs) rely on a beacon signal which poses a threat to privacy, since it could allow a vehicle to be tracked. Mix- zones, where vehicles encrypt their transmissions and then change their identifiers, have been proposed as a solution to this problem. In this work, we describe a formal analysis of mix-zones. We model a mix-zone and propose a formal definition of privacy for such a zone. We give a set of necessary conditions for any mix-zone protocol to preserve privacy. We analyse, using the ProVerif tool, a particular proposal for key distribution in mix zones, the CMIX protocol. We show that in many scenarios, it does not preserve privacy.

16:00 Tom Chothia, Konstantinos Chatzikokolakis and Apratim Guha
Calculating Information Leakage from System Tests: Mix Nodes and e-Passports

Information theoretic measures have proved a popular way to quantify security for system models. In this paper we show that measures of information leakage based on mutual information and capacity can be calculated, automatically, from trial runs of a system alone. This makes it possible to apply theoretical work on the measurement of information leakage directly to real computer systems. We find a confidence interval for the estimation of information leakage and propose a statistical test to distinguish zero leakage from a very small non-zero leakage. We illustrate our method by analysing a running mix node and e-passports from a number of countries.