CSF on Saturday, July 17th

09:00‑10:00 Hewlett-Packard Security Lecture
Chair: Andrew Myers
Location: AT LT2
09:00 Andrew Myers
Conference welcome
09:05 Vitaly Shmatikov (University of Texas, Austin)
The end of anonymity, the beginning of privacy
10:30‑12:30 Quantitative Security
Chair: Michael Backes
Location: AT LT2
10:30 Boris Köpf and Andrey Rybalchenko
Approximation and randomization for quantitative information-flow analysis

Quantitative information-flow analysis (QIF) is an emerging technique for establishing information-theoretic confidentiality properties. Automation of QIF is an important step towards ensuring its practical applicability, since manual reasoning about program security has been shown to be a tedious and expensive task. Existing automated techniques for QIF fall short providing full coverage of all program execution, esp. in the presence of advanced programming constructs like unbounded loops and data structures. In this paper we propose a blend of approximation and randomization techniques to bear on the challenge of sufficiently precise, yet efficient computation of quantitative information flow properties. Our approach relies on a sampling method to enumerate large or unbounded secret spaces, and applies both static and dynamic program analysis techniques to deliver necessary over- and under-approximations of information-theoretic characteristics.

11:00 Hirotoshi Yasuoka and Tachio Terauchi
Quantitative information flow - verification hardness and possibilities

Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, and channel capacity. This paper investigates the hardness and possibilities of precisely checking and inferring quantitative information flow according to such definitions.

We prove that, even for just comparing two programs on which has the larger flow, none of the definitions is a k-safety property for any k, and therefore is not amenable to the self-composition technique that has been successfully applied to precisely checking non-interference. We also show a complexity theoretic gap with non-interference by proving that, for loop-free boolean programs whose non-interference is coNP-complete, the comparison problem is #P-hard for all of the definitions.

For positive results, we show that universally quantifying the distribution in the comparison problem, that is, comparing two programs according to the entropy based definitions on which has the larger flow for all distributions, is a 2-safety problem in general and is coNP-complete when restricted for loop-free boolean programs. We prove this by showing that the problem is equivalent to a simple relation naturally expressing the fact that one program is more secure than the other. We prove that the relation also refines the channel-capacity based definition, and that it can be precisely checked via the self-composition as well as the ``interleaved'' self-composition technique.

11:30 Michael Clarkson and Fred Schneider
Quantification of integrity

Two information-flow integrity measures, contamination and suppression, are introduced. The former is dual to information-flow confidentiality, and the latter is analogous to the standard model of channel reliability from information theory. As a case study, the relationship between quantitative integrity, confidentiality, and database privacy is examined.

12:00 Boris Köpf and Geoffrey Smith
Vulnerability bounds and leakage resilience of blinded cryptography under timing attacks

We establish formal bounds for the number of min-entropy bits that can be extracted in a timing attack against a cryptosystem that is protected by blinding, the state-of-the art countermeasure against timing attacks. Compared with existing bounds, our bounds are both tighter and of greater operational significance, in that they directly address the key's one-guess vulnerability. Moreover, we show that any semantically secure public-key cryptosystem remains semantically secure in the presence of timing attacks, if the implementation is protected by blinding and bucketing. This result shows that, by considering (and justifying) more optimistic models of leakage than recent proposals for leakage-resilient cryptosystems, one can achieve provable resistance against side-channel attacks for standard cryptographic primitives.

14:00‑15:00 Security Protocol Verification I
Chair: Bruno Blanchet
Location: AT LT2
14:00 Mathilde Arnaud, Véronique Cortier and Stephanie Delaune
Modeling and verifying ad hoc routing protocols

Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such networks, a central issue, ensured by routing protocols, is to find a route from one device to another. Those protocols use cryptographic mechanisms in order to prevent malicious nodes from compromising the discovered route.

Our contribution is twofold. We first propose a calculus for modeling and reasoning about security protocols, including in particular secured routing protocols. Our calculus extends standard symbolic models to take into account the characteristics of routing protocols and to model wireless communication in a more accurate way. Our second main contribution is a decision procedure for analyzing routing protocols for any network topology. By using constraint solving techniques, we show that it is possible to automatically discover (in NPTIME) whether there exists a network topology that would allow malicious nodes to mount an attack against the protocol, for a bounded number of sessions. We also provide a decision procedure for detecting attacks in case the network topology is given a priori. We demonstrate the usage and usefulness of our approach by analyzing the protocol SRP applied to DSR.

14:30 Mayla Bruso, Konstantinos Chatzikokolakis and Jerry den Hartog
Formal verification of privacy for RFID systems

RFID tags are being widely employed in a variety of applications, ranging from barcode replacement to electronic passports. Their extensive use, however, in combination with their wireless nature, introduces privacy concerns as a tag could leak information about the owner's behaviour. In this paper we define two privacy notions, unlinkability and forward privacy, using a formal model based on the applied pi calculus, and we show the relationship between them. Then we focus on a generic class of simple privacy protocols, giving sufficient and necessary conditions for unlinkability and forward privacy for this class. These conditions are based on the concept of frame independence that we develop in this paper. Finally, we apply our techniques to two identification protocols, formally proving their privacy guarantees.

15:30‑17:00 Privacy and Anonymity
Chair: Vitaly Shmatikov
Location: AT LT2
15:30 Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk and Bogdan Warinschi
Robustness guarantees for anonymity

Anonymous communication protocols must achieve two seemingly contradictory goals: privacy (informally, they must guarantee the anonymity of the parties that send/receive information), and robustness (informally, they must ensure that the messages are not tampered). However, the long line of research that defines and analyzes the security of such mechanisms focuses almost exclusively on the former property and ignores the latter.

In this paper, we initiate a rigorous study of robustness properties for anonymity protocols. We identify and formally define, using the style of modern cryptography, two related but distinct flavors of robustness. Our definitions are general ( e.g. they strictly generalize the few existent notions for particular protocols) and flexible ( e.g. they can be easily adapted to purely combinatorial/probabilistic mechanisms).

We demonstrate the use of our definitions through the analysis of several anonymity mechanisms (Crowds, broadcast-based mix-nets, DC-nets). Notably, we analyze the robustness of a protocol by Golle and Juels for the dinning cryptographers problem, identify a robustness-related weakness of the protocol, and propose and analyze a stronger version.

16:00 Myrto Arapinis, Tom Chothia, Eike Ritter and Mark Ryan
Analysing unlinkability and anonymity using the applied pi-calculus

An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets' behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi-calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced. We demonstrate that our framework can be applied to a wide range of devices by modelling the Trusted Platform Module's DAA protocol and showing that it fails both anonymity and unlinkability.

16:30 Ralf Kuesters, Tomasz Truderung and Andreas Vogt
A game-based definition of coercion-resistance and its applications

Coercion-resistance is one of the most important and intricate security requirements for voting protocols. Several definitions of coercion-resistance have been proposed in the literature, both in cryptographic settings and more abstract, symbolic models. However, unlike symbolic approaches, only very few voting protocols have been rigorously analyzed within the cryptographic setting. A major obstacle is that existing cryptographic definitions of coercion-resistance tend to be complex and limited in scope: They are often tailored to specific classes of protocols or are too demanding.

In this paper, we therefore present a simple and intuitive, yet widely applicable cryptographic definition of coercion-resistance, in the style of game-based definitions. This definition allows to precisely measure the level of coercion-resistance a protocol provides. As a proof of concept, we apply our definition to two voting systems, namely, the Bingo voting system and ThreeBallot. The results we obtain are out of the scope of existing approaches. We show that the Bingo voting system provides the same level of coercion-resistance as an ideal voting system. We also precisely measure the degradation of coercion-resistance of ThreeBallot in case the so-called short ballot assumption does not hold and show that the level of coercion-resistance ThreeBallot provides is significantly lower than that of an ideal system, even in case of short ballots.

17:00‑18:00 Five-Minute Talks
Chair: Stephen Chong
Location: AT LT2
17:00 List of talks at http://people.seas.harvard.edu/~chong/csf2010-5min/