Complexity of automatic verification of cryptographic protocols
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.
In this work, we study the complexity of deciding equivalence properties, for several classes of protocols and several equivalences.
How (not) to use TLS between 3 parties
In this talk, we will explore the case of TLS between a client and a server, being mediated in particular way by a middle-man embodied by a CDN, i.e., a content delivery network.
We specifically discuss the case of the so-called “Keyless SSL”, where the server retains its private key and the mediating CDN uses the server as proxy during the TLS handshake. We disclose vulnerabilities on this design and discuss different repairs.
Throughout, we emphasise on what we believe to be the (old and reinforced, as well as the new) security requirements and model needed when lifting TLS from the classical 2-party setting to the 3-party one.
Private and Scalable Execution of SQL Aggregates on a Secure Decentralized Architecture (to appear in ACM TODS'16)
Current applications, from complex sensor systems (e.g. quantified self) to online e-markets acquire vast quantities of personal information which usually end-up on central servers where they are exposed to prying eyes. Conversely, decentralized architectures helping individuals keep full control of their data, complexify global treatments and queries, impeding the development of innovative services.
In this presentation, we will show how to reconcile individual's privacy on one side and global benefits for the community and business perspectives on the other side. We promote the idea of pushing the security to secure hardware devices controlling the data at the place of their acquisition. Thanks to these tangible physical elements of trust, secure distributed querying protocols can reestablish the capacity to perform global computations, such as SQL aggregates, without revealing any sensitive information to central servers. In this presentation, we will show how to secure the execution of such queries in the presence of honest-but-curious and malicious attackers.
We will also discuss how the resulting querying protocols can be integrated in a concrete decentralized architecture. Cost models and experiments on SQL/AA, our distributed prototype running on real tamper- resistant hardware, demonstrate that this approach can scale to nationwide applications.
Frédéric BOISSONNET - ESPE Clermont Auvergne