1. Prof Liqun Chen's paper was presented at IEEE S&P 2017. It is titled "One TPM to Bind Them All: Fixing TPM2.0 for Provably Secure Anonymous Attestation", which was the result of collaboration with Jan Camenisch (IBM Research – Zurich, Switzerland), Manu Drijvers (IBM Research - Zurich and ETH Zurich, Switzerland), Anja Lehmann (IBM Research - Zurich, Switzerland), David Novick (Intel, USA), and Rainer Urian (Infineon, Germany).
Abstract: The Trusted Platform Module (TPM) is an international standard for a security chip that can be used for the management of cryptographic keys and for remote attestation. The specification of the most recent TPM 2.0 interfaces for direct anonymous attestation unfortunately has a number of severe shortcomings. In this paper, we provide a better specification of the TPM 2.0 interfaces that addresses the problems and requires only minimal changes to the current TPM 2.0 commands. We then show how to use the revised interfaces to build direct anonymous attestation schemes, and prove their security. We also discuss how to obtain other schemes addressing different use cases such as key-binding for U-Prove and e-cash.
2. Dr François Dupressoir has one paper presented at IEEE S&P 2017. It is titled "Machine-Checked Proofs of Privacy for Electronic Voting Protocols", which was the result of collaboration with Véronique Cortier (LORIA, CNRS & Inria & Université de Lorraine, France), Constantin Cătalin Drăgan (LORIA, CNRS & Inria, France), Benedikt Schmidt (IMDEA Software Institute, Spain), Pierre-Yves Strub (École Polytechnique, France), and Bogdan Warinschi (University of Bristol, UK).
Abstract: We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme. In addition, we highlight some of the lessons learned regarding the gap between pen-and-paper and machine-checked proofs, and report on the experience with formalizing the security of protocols at this scale.
3. Dr François Dupressoir has another paper accepted presented at EUROCRYPT 2017. It is titled "Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model", which was the result of collaboration with Gilles Barthe (IMDEA Software Institute, Spain), Sebastian Faust (Ruhr Universität Bochum, Germany), Benjamin Grégoire (Inria Sophia-Antipolis – Méditerranée, France), François-Xavier Standaert (Université Catholique de Louvain, Belgium), and Pierre-Yves Strub (Ecole Polytechnique, France).
Abstract: In this paper, we provide a necessary clarification of the good security properties that can be obtained from parallel implementations of masking schemes. For this purpose, we first argue that (i) the probing model is not straightforward to interpret, since it more naturally captures the intuitions of serial implementations, and (ii) the noisy leakage model is not always convenient, e.g. when combined with formal methods for the verification of cryptographic implementations. Therefore we introduce a new model, the bounded moment model, that formalizes a weaker notion of security order frequently used in the side-channel literature. Interestingly, we prove that probing security for a serial implementation implies bounded moment security for its parallel counterpart. This result therefore enables an accurate understanding of the links between formal security analyses of masking schemes and experimental security evaluations based on the estimation of statistical moments. Besides its consolidating nature, our work also brings useful technical contributions. First, we describe and analyze refreshing and multiplication algorithms that are well suited for parallel implementations and improve security against multivariate side-channel attacks. Second, we show that simple refreshing algorithms (with linear complexity) that are not secure in the continuous probing model are secure in the continuous bounded moment model. Eventually, we discuss the independent leakage assumption required for masking to deliver its security promises, and its specificities related to the serial or parallel nature of an implementation.
4. Dr Ioana Boureanu has a paper presented at Euro S&P 2017. It is titled "Content delivery over TLS: A cryptographic analysis of Keyless SSL", which was the result of collaboration with Karthikeyan Bhargavan (INRIA de Paris, France), Pierre-Alain Fouque (University of Rennes 1/ IRISA, France), Cristina Onete (INSA Rennes / IRISA, France), and Benjamin Richard (Orange Labs Chatillon, France).
Abstract: We explore the case of TLS handshakes between a client and a server, when mediated by a middle-man embodied mainly by a CDN (content delivery network). We specifically discuss the case of the so-called “Keyless SSL”; this is a commercial solution for proxying TLS 1.2 sold by Cloudflare, where the end-server retains its private key and the mediating CDN uses the server as proxy during the TLS handshake. We disclose vulnerabilities of Keyless SSL. We propose a fixed version of Keyless TLS 1.2 and a new version of Keyless TLS 1.3. We put forward a formal model for proxied authenticated key-exchanged executed over three parties, encompassing traditional as well as new, proxy-induced security requirements. In this model, we formally prove the security of our repaired Keyless TLS 1.2. and our new Keyless TLS 1.3. We discuss some efficiency aspects as well, e.g., the new Keyless TLS 1.3 is computationally lighter that the repaired Keyless TLS 1.2.