FOSAD 2010 Timetable: download the program (PDF).
The program includes 8 monographic courses of 4 hours each and
an open session (Wed 8 September) with the
- 15:00-16:00 Michael Goldsmith (Warwick University, UK)
Bigraphs and Spygraphs
- 16:15-16:45 Alejandro Hernandez (Technical University of Denmark)
Aspect-Orientation and Security Policies for Distributed Systems
- 16:45-17:15 Patrick Schweitzer (University of Luxembourg)
Foundations of Attack-Defence Trees
- 17:15-17:45 Tim Muller (University of Luxembourg)
Semantics for Trust
Verification of security protocols: from symbolic models to cryptography
(part 1 -
Security protocols are short programs aiming at securing
communications over a network. They are widely used in our everyday
life. Their verification using symbolic models has shown its interest
for detecting attacks and proving security properties. In particular,
several automatic tools have been developed. However, the guarantees
that the symbolic approach offers have been quite unclear compared to
the computational approach that considers issues of complexity and
probability. This later approach captures a strong notion of security,
guaranteed against all probabilistic polynomial-time attacks.
In this course, we will first overview several techniques used for
symbolically verifying security protocols. In a second part of the
presentation, we will present recent results that aim at obtaining
the best of both worlds: fully automated proofs and strong, clear
security guarantees. The approach consists in proving that symbolic
models are *sound* with respect to computational ones, that is, that any
potential attack is indeed captured at the symbolic level.
Bayesian approaches to the traffic analysis of anonymous communications.
Analysis of security APIs
(part 1 -
Security APIs are Application Programming Interfaces to trusted systems
such as cryptographic devices, online games, services on the web, etc.
They should allow untrusted applications to access sensitive resources
in a controlled way, e.g. signing a message using a cryptographic device
without accessing the signature key, or modifying the status of an
online game without cheating on the game rules. In practice, however,
the flexibility required by these programming interfaces gives rise to
attacks originated by 'unexpected' sequences of API invocation. It is
possible, for example, to extract sensitive keys from PKCS#11
cryptographic tokens or guess a bank user PIN while it is checked inside
a tamper-resistant Hardware Security Module, through a few suitable API
calls to the device.
In this course, we will review practical attacks on security APIs and we
will introduce formal techniques to detect and fix them. We will
describe Tookan, a tool that reverse engineers real cryptographic tokens
and performs a formal analysis of the resulting model, finding possible
attacks and testing them on the real device. We will finally show how to
apply Tookan to break and fix a software simulator of a PKCS#11 token.
Cryptographic verification of protocol implementations by typechecking.
Type systems are effective tools for verifying the security of cryptographic protocols and
implementations. They provide automation, modularity and scalability, and have been applied
to large protocols. In this tutorial, I present and illustrate types for authenticity and
secrecy, first using symbolic models for cryptography, then relying on computational
The tutorial is based on joint work with Karthik Bhargavan and Andy Gordon. Programming
tools and examples are available here.
- We introduce refinement types (that is, types carrying formulas to record invariants) for
programs written in F# and verified by F7, an SMT-based type checker.
- We use types for declaring cryptographic invariants. We develop symbolic libraries for a
range of cryptographic primitives, and we review a few case studies of protocol code.
- We adapt our libraries to rely on standard computational assumptions. For each primitive,
computational soundness follows from a code-based game-hopping argument in F#.
Key exchange and provable security.
Usage control in distributed systems.
Theory and design of low-latency anonymity systems.
(part 1 -
part 2 -
part 3 -
Privacy-preserving set operations.