CSF on Monday, July 19th

09:00‑10:00 Security Specifications
Chair: Jon Millen
Location: AT LT2
09:00 Juan Garay, Aggelos Kiayias and Hong-Sheng Zhou
A framework for the sound specification of cryptographic tasks

Nowadays it is widely accepted to formulate the security of a protocol carrying out a given task via the ``trusted-party paradigm,'' where the protocol execution is compared with an ideal process where the outputs are computed by a trusted party that sees all the inputs. A protocol is said to securely carry out a given task if running the protocol with a realistic adversary amounts to ``emulating'' the ideal process with the appropriate trusted party. In the Universal Composability (UC) framework the program run by the trusted party is called an {\em ideal functionality}. While this simulation-based security formulation provides strong security guarantees, its usefulness is contingent on the properties and correct specification of the ideal functionality, which, as demonstrated in recent years by the coexistence of complex, multiple functionalities for the same task as well as by their ``unstable'' nature, does not seem to be an easy task.

In this paper we address this issue, by introducing a general methodology for the sound specification of ideal functionalities. First, we introduce the class of {\em canonical} ideal functionalities for a cryptographic task, which unifies the syntactic specification of a large class of cryptographic tasks under the same basic template functionality. Furthermore, this representation enables the isolation of the individual properties of a cryptographic task as separate members of the corresponding class. By endowing the class of canonical functionalities with an algebraic structure we are able to combine basic functionalities to a single final canonical functionality for a given task. Effectively, this puts forth a bottom-up approach for the specification of ideal functionalities: first one defines a set of basic constituent functionalities for the task at hand, and then combines them into a single ideal functionality taking advantage of the algebraic structure.

In our framework, the constituent functionalities of a task can be derived either directly or, following a translation strategy we introduce, from existing game-based definitions; such definitions have in many cases captured desired individual properties of cryptographic tasks, albeit in less adversarial settings. Our translation methodology entails a sequence of steps that systematically derive a corresponding canonical functionality given a game-based definition, effectively ``lifting'' the game-based definition to its composition-safe version.

We showcase our methodology by applying it to a variety of basic cryptographic tasks, including commitments, digital signatures, zero-knowledge proofs, and oblivious transfer. While in some cases our derived canonical functionalities are equivalent to existing formulations, thus attesting to the validity of our approach, in others they differ, enabling us to ``debug'' previous definitions and pinpoint their shortcomings.

09:30 Devdatta Akhawe, Adam Barth, Peifung Lam, John Mitchell and Dawn Song
Towards a formal foundation of web security

We propose a formal model of web security based on an abstraction of the web platform and use this model to analyze the security of several sample web mechanisms and applications. We identify several distinct threat models that can be used to analyze web applications, ranging from a web attacker who controls malicious web sites and clients, to stronger attackers that can control the network and/or leverage sites designed to display user-supplied content. We propose two broadly applicable security goals and study five security mechanisms. In our case studies, which include HTML5 forms, Referer validation, and a single sign-on solution, we use a SAT-based model-checking tool to find previously known vulnerabilities in two cases and three new vulnerabilities. The case study of a Kerberos-based single sign-on system illustrates key differences between network protocols and web protocols and finds a vulnerability that arises because of the way cookies, redirects, and embedded links are used.

10:30‑12:15 Language-Based Security
Chair: Matteo Maffei
Location: AT LT2
10:30 Alwen Tiu and Jeremy Dawson
Automating open bisimulation checking for the spi-calculus

We consider the problem of automating open bisimulation checking for the spi-calculus, an extension of the pi-calculus with cryptographic primitives. The notion of open bisimulation considered here is indexed by a (symbolic) environment, represented as bi-traces (i.e., pairs of symbolic traces), which encode the history of interaction between the intruder with the processes being checked for bisimilarity. A crucial part of the definition of this open bisimulation, that is, the notion of consistency of bi-traces, involves infinite quantification over a certain notion of ``respectful substitutions''. We show that one needs only to check a finite number of respectful substitutions in order to check bi-trace consistency. Our decision procedure uses techniques that have been well developed in the area of symbolic trace analysis for security protocols. More specifically, we make use of techniques for symbolic trace refinement, which transforms a symbolic trace into a finite set of symbolic traces in a certain ``solved form''. Crucially, we show that refinements of a projection of a bi-trace can be uniquely extended to refinements of the bi-trace, and that consistency of all instances of the original bi-trace can be reduced to consistency of its finite set of refinements. We then give a sound and complete procedure for deciding open-bisimilarity for finite spi-processes.

11:00 Stefan Ciobaca and Veronique Cortier
Protocol composition for arbitrary primitives

We study the composition of security protocols in a Dolev-Yao model when the protocols share secrets such as keys.

We show that if two protocols use disjoint cryptographic primitives, their composition is secure if the individual protocols are secure, even if they share data. Our result holds for any cryptographic primitives that can be modeled using equational theories, such as encryption, signature, MAC, exclusive-or and Diffie-Hellman.

Our main result transforms any trace of the combined protocol leading to an attack into an attack trace of one of the individual protocols. This allows various ways of combining protocols such as sequentially or in parallel, possibly with inner replications.

As an application, we show that a protocol using pre-established keys may use any (secure) key-exchange protocol without jeopardizing its security, provided that they do not use the same primitives. This allows us, for example, to securely compose a Diffie-Hellman key exchange protocol with any other protocol using the exchanged key, provided that the second protocol does not use Diffie-Hellman primitives.

We also explain why composing protocols which use tagged cryptographic primitives like encryption and hash functions is secure by reducing this problem to the previous one.

11:30 Martin Abadi and Gordon Plotkin
On protection by layout randomization

Layout randomization is a powerful, popular technique for software protection. We present it and study it in programming-language terms. More specifically, we consider layout randomization as part of an implementation for a high-level programming language; the implementation translates this language to a lower-level language in which memory addresses are numbers. We analyze this implementation, by relating low-level attacks against the implementation to contexts in the high-level programming language, and by establishing full abstraction results.

12:00 Andrew Myers and Michael Backes
Program chairs' report and conference close