Abstracts

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.

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.

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.

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.

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.