Papers & Software





Comète-Parsifal Seminar (Abstracts 2011)


2012 2011 2010 2009 2008 2007 2006 2005 2004
Wed Dec 14, 14:30Geoffrey Smith More Theory and Applications of Min-Entropy Leakage
Wed Dec 07, 14:30Geoffrey Smith Quantifying Information Flow Using Min-Entropy
Fri Oct 22, 10:30 Flavio Garcia On the (in)security of widely-used contactless smartcards
Fri Oct 21, 11:00Geoffrey Smith Min-Entropy as a Resource
Tue Oct 04, 14:30Marco Stronati Calculi and constraints
Mon Sep 19, 14:30Myrto Arapinis Keeping track of your friends and enemies: privacy threats of new mobile technologies
Tue Jun 07, 14:30Romain Beauxis The Failure of Noise-Based Non-Continuous Audio Captchas
Fri Mar 11, 14:30 Alexandra Silva Sound and Complete Axiomatization of Trace Semantics for Probabilistic Transition Systems
Wed Mar 09, 15:00Alejandro Diaz-Caro Algebraic type systems
Wed Mar 02, 14:00Kazunori Ueda Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting
Tue Mar 01, 14:30 Marco Giunti On the Effectiveness of Typed Equivalences for Security in Pi Calculus
Wed Feb 02, 14:45Gurvan Le Guernic CFlow: a security-preserving cryptography-implicit compiler for distributed programs (A Demo with a Pinch of Theory)


Dec 14 2011, 14:30
Speaker: Geoffrey Smith
Title: More Theory and Applications of Min-Entropy Leakage [Slides] "

Building on the definitions and theory of min-entropy leakage discussed in our first talk, in this talk we will discuss several recent developments in the area. We will first discuss bounds on the min-entropy leakage of a cascade of channels, in which the output of one channel is used as the input to another. These bounds will then be applied to prove the effectiveness of certain countermeasures against timing attacks on public-key cryptography. Finally, we will discuss a static analysis approach for computing upper bounds on the min-entropy leakage of deterministic imperative programs---the approach is based on determining what patterns hold for each pair of bits in the program's output, and then using these patterns to bound the number of possible output values.

Dec 07 2011, 14:30
Speaker: Geoffrey Smith"
Title: Quantifying Information Flow Using Min-Entropy [Slides]

One of the most fundamental issues in computer security is to prevent the leakage of secret information to public outputs. But while it is sometimes possible to stop such leakage completely, it is perhaps more typical that some leakage is unavoidable. For instance an ATM machine that rejects an incorrect PIN thereby reveals that the secret PIN differs from the one that was entered. More subtly, the amount of time taken by a cryptographic operation may reveal information about the secret key. Hence the last decade has seen growing interest in quantitative theories of information flow, to allow us to talk about 'how much' information is leaked and (perhaps) allow us to tolerate 'small' leaks.

But while it is tempting to measure leakage using classic information-theoretic concepts like Shannon entropy and mutual information, these turn out not to provide very satisfactory security guarantees. As a result, several researchers have developed an alternative theory based on Rényi's min-entropy. In this theory, leakage is measured in terms of a secret's Bayes vulnerability to being guessed in one try by an adversary; note that this is the complement of the Bayes Risk. In this talk, we will describe the basic theory of min-entropy leakage in deterministic and probabilistic systems, including comparisons with mutual information leakage, results on min-capacity, and results on channels in cascade. We will also discuss algorithms for calculating leakage in systems, and mention some applications, such as bounds on timing attacks on cryptography.

Nov 25 2011, 14:30
Speaker: Flavio Garcia
Title: On the (in)security of widely-used contactless smartcards

Over the last few years, much attention has been paid to the (in)security of the cryptographic mechanisms used in contactless smartcards. Experience has shown that the secrecy of proprietary ciphers does not contribute to its cryptographic strength. Most notably the Mifare Classic, which has widespread application in public transport ticketing and access control systems, has been thoroughly broken in the last few years. Other prominent examples include KeeLoq and Hitag2 used in car keys and the CryptoRF used in access control and payment systems.

This talk briefly summarizes the latest developments on this field, with focus on our own contribution. Then, we will show that the security of other widely-used smartcards proposed as a secure successor of the Mifare Classic provide no (significantly) better security.


The secrecy of certain values (such as sender identities, keys, and nonces) is crucial to the achievement of various security goals. We can view this secrecy as a “resource” that may gradually be “consumed” by information leaks in a system. Let a secret S be modeled as a random variable with some a priori distribution, assumed publicly known. Min-entropy measures S’s secrecy based on its Bayes vulnerability to be guessed correctly in one try by an adversary. If a system manipulates S and produces an output O, then the amount of secrecy “consumed” can be defined as the amount by which observing O decreases S’s min-entropy. In this talk, we explore the intuition of min-entropy as a resource, in both deterministic and probabilistic systems. We focus on compositionality results that bound the amount of leakage of a compound system based on the leakage of its components, showing for example that n repeated independent runs, using the same value of S each time, leak at most O(log n) bits; we apply this result to the scenario of timing attacks against blinded cryptography. We deal mostly with the “static” perspective of leakage averaged over all runs, but also comment on the “dynamic” perspective of leakage in a single run.
Oct 04 2011, 14:30
Speaker: Marco Stronati
Title: Calculi and constraints

The world of logic programming always looked with a keen eye to con- currency in order to solve its constraints problems and, on the other hand, the process calculi community considered constraints the perfect candidate for its missing data structure. It is not until 1990 that this marriage found his form in the Concurrent Constraint Programming by Saraswat but with the advent of new semantic foundations and new refined tools a much due update arrived only in recent years.

A first hint of how natural was the use of constraints in Pi calculus was the use of fusions in the fusion calculus and Pi-F: with the new feature the semantic gets actually simpler. Montanari and Buscemi built their Concurrent Constraint Pi calculus extending the use of constraints from just names to a framework of possibilities and merging seamlessly the use of names and constraints thanks to the use of a constraint semiring model. The latest work in the field was developed again by the Uppsala school, extending and abstracting even more on the experience of CC-Pi to the point of building a framework for name passing calculi with constraints, complete with a coherent set of bisimilarities for both concrete and symbolic semantics, which subsumes the previous presented calculi.

Sep 19 2011, 14:30
Speaker: Myrto Arapinis
Title: Keeping track of your friends and enemies: privacy threats of new mobile technologies

oint work with Loretta Mancini, Eike Ritter, and Mark Ryan.

The proliferation of portable computing devices, such as mobile phones, Bluetooth devices, and RFID tags, has lead to a range of new computer security problems. In order to fulfil their goals, these devices need to report our movements to service providers such as mobile phone network operators, banks, and governments. While most of users accept that the service providers can track their physical movements, few would be happy if an arbitrary third party could do so. Such a possibility would enable all kinds of undesirable behaviours, ranging from criminal stalking to more mundane monitoring of spouse or employee movements. For this reason, protocols have been designed to prevent third parties from identifying wireless messages as coming from a particular user. These protocols usually include cryptography and make use of temporary identifiers, in an effort to achieve the aim of untraceability by third parties.

At CSF'10, we presented a formal framework for analysing untraceability/unlinkability in the applied pi calculus. We used our framework to show that French e-Passports are traceable, while British ones aren't. In this talk, I will present you our work on the analysis of Universal Mobile Telecommunication System (UMTS) protocols. I will show you a problem we have identified with the UMTS authentication and key establishment protocol: although mobile phones use temporary identities to identify themselves to the Network, a replayed message can be used to identify a particular mobile phone. Our attack exploits the fact that the victim's phone will reply with subtly different error messages, depending on whether the replayed request is associated with it or with a different phone. To thwart this attack, we propose a modification of the protocol, and verify the proposed fix using our framework and the ProVerif tool.

Jun 07 2011, 14:30
Speaker: Romain Beauxis
Title: The Failure of Noise-Based Non-Continuous Audio Captchas

CAPTCHAs, which are automated tests intended to distinguish humans from programs, are used on many web sites to prevent bot-based account creation and spam. To avoid imposing undue user friction, CAPTCHAs must be easy for humans and difficult for machines. However, the scientific basis for successful CAPTCHA design is still emerging. In this talk, we will examine the widely used class of audio CAPTCHAs based on distorting non-continuous speech with certain classes of noise and demonstrates that virtually all current schemes, including ones from Microsoft, Yahoo, and eBay, are easily broken. More generally, we describe a set of fundamental techniques, packaged together in our Decaptcha system, that effectively defeat a wide class of audio CAPTCHAs based on non-continuous speech. Decaptcha's performance on actual observed and synthetic CAPTCHAs indicates that such speech CAPTCHAs are inherently weak and, because of the importance of audio for various classes of users, alternative audio CAPTCHAs must be developed.
Mar 11 2011, 14:30
Speaker: Alexandra Silva
Title: Sound and Complete Axiomatization of Trace Semantics for Probabilistic Transition Systems

We present the first sound and complete axiomatization of trace semantics for probabilistic tran- sition systems. Our approach is coalgebraic, which opens the door to axiomatize other types of systems. In order to prove soundness and completeness, we employ determinization and show that coalgebraic traces can be recovered via determinization, a result interesting in itself. The approach is also applicable to labelled transition systems, for which we can recover the known axiomatization of trace semantics (work of Rabinovich).
Mar 09 2011, 15:00
Speaker: Alejandro Diaz-Caro
Title: Algebraic type systems

In this talk I will present several extensions to the System F, for the sake of type the linear-algebraic lambda-calculus, a lambda-calculus enriched with a vectorial structure. The first type system is a straightforward extension of System F, which just types the calculus without any further adornment. The second one is a type system accounting for scalars, which can serve as a guarantee that the normal form of a term is of the form Σαi.ti with Σαi=1. The following system includes 'sums of types' reflecting that of the terms --showing that sums in the algebraic calculus behaves as a special kind of pairs. Eventually the last type system combines the previous two. We give counterexamples of why this kind of vectorial type system cannot be made in Curry style and show the clues of a future vectorial type system in Church style suitable to specialize the calculus into a quantum calculus.
Mar 02 2011, 14:00
Speaker: Kazunori Ueda
Title: Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting

Fine-grained reformulation of the lambda calculus is expected to solve several difficulties with the notion of substitutions -- definition, implementation and cost properties.  However, previous attempts including those using explicit substitutions and those using Interaction Nets were not ideally simple when it came to the encoding of the pure (as opposed to weak) lambda calculus.  We present a fine-grained and highly asynchronous encoding of the pure lambda calculus using LMNtal, a hierarchical graph rewriting language, and discuss its properties.  The membrane construct of LMNtal plays an essential role in encoding local names and and their operations that consist of (i) ordering between names, (ii) checking of name equality, (iii) detection of garbage names (names with no references), and (iv) fusion of two names, all of which are essential in our encoding.  The encoding has been tested using our publicly available LMNtal implementation, and the talk will also introduce its features including a state space visualizer/explorer and a model checker.
Mar 01 2011, 14:30
Speaker: Marco Giunti
Title: On the Effectiveness of Typed Equivalences for Security in Pi Calculus

Starting from the seminal work of Pierce and Sangiorgi there has been a lot of interest on type techniques for analyzing  the access to communication channels in pi calculi. Among these, typed behavioral equivalences have been suggested as a powerful method for reason on the security of processes immersed in an hostile context. While in this approach the behavior of the attacker is constrained by strong (static) typing, in previous work we argued that it is unclear whether such reasoning could be deployed in open contexts, for which no assumption on trust and behavior may be made. On contrast, we showed that a management of capabilities based on lightweight dynamic typing could be effectively implemented in untyped contexts by providing a fully abstract translation of an high level typed calculus into a low-level cryptographic (applied-pi) calculus.

In this talk we introduce a separation result stating that the reasoning based on dynamic typing do comport of loss of expressiveness w.r.t. static typing. To this aim, we show that a fully abstract encoding from the typed (asynchronous) pi calculus to our high level typed calculus could not exist under any reasonable condition. We argue that this result injects doubt on the effectiveness of the reasoning based on typed behavioral equivalences for process calculi.

Feb 02 2011, 14:45
Speaker: Gurvan Le Guernic
Title: CFlow: a security-preserving cryptography-implicit compiler for distributed programs (A Demo with a Pinch of Theory)

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues. We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract information-flow policy for accessing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing. We build a translation from source programs with high-level security policies to cryptographic implementations. The translation enforces the correct usage of cryptographic primitives against active adversaries. From an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We show type soundness for a variant of the non-interference property, then show that our translation preserves typability. We rely on concrete primitives and hypotheses for cryptography. We model these primitives as commands in our target language.

Page maintainer: Andres Aristizabal