Block lecture on Week 9, 2006


1 AP (1.5 ECTS), ends with "Arvestus" (pass/fail examination). To pass, a number of exercises have to be solved after the course.


Day Time Lecture hall
Mon, February 27th 10:15 - 12:00 Liivi 2-207 Slides
Tue, February 28th 14:15 - 16:00 Slides
Wed, March 1st 12:15 - 14:00 Liivi 2-122 Slides
14:00 - 15:00 Liivi 2-403
Thu, March 2nd 16:15 - 18:00 Liivi 2-207 Slides

Target audience

Graduate and advanced undergraduate students interested in information security and cryptology


Michael Backes, Computer Science department of Saarland University, Germany


In recent times, the analysis of cryptographic protocols has been getting more and more attention, and the demand for general frameworks for representing cryptographic protocols has been rising. To allow for a faithful analysis of cryptographic protocols, it is well-known that such models have to capture probabilistic behaviors, complexity-theoretically bounded adversaries as well as a reactive environment of the protocol, i.e., continuous interaction with the users and the adversaries.

We present a rigorous model for reactive systems in asynchronous networks that lives up to these requirements. It supports abstract specification and the composition of secure systems, which enables modular proofs of security and has the potential to link the rigorous proof techniques of cryptography with tool-supported formal proof techniques. The model follows the general simulatability approach, which is the cryptographic notion of a secure refinement. Integrity, strong confidentiality, and liveness properties can be expressed in the model, and we show that they are preserved under simulatability. As the foundation for cryptographically sound protocol analysis, we present an ideal cryptographic library — the so-called BPW model — which allows for analyzing and expressing cryptographic protocols in an idealized setting that is suitable for formal proof tools while nevertheless coming with a provably secure implementation. We use this result to derive the first cryptographically sound security proofs of several well-known protocols such as Needham-Schroeder-Lowe public-key protocol.

We furthermore show that the BPW model can be faithfully implemented in the theorem prover Isabelle/HOL. The main challenge for designing a practical formalization of this model was to cope with the complexity of providing such strong guarantees between formal verification and cryptographic realizations. We reduce this complexity by abstracting the library into a sound, light-weight formalization that enables both concise property specifications and efficient application of our proof strategies and their supporting proof tools. This yields the first tool-supported framework for symbolically verifying security protocols that enjoys the strong cryptographic soundness guarantees provided by reactive simulatability.

Supported by

Estonian Information Technology Foundation, Tiger University programme.