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
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
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 ﬁrst 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.