FIRST PhD School 2006 at the IT University of Copenhagen
Verification of Protocols for Security and Mobility (VPSM)
FIRST PhD School 2006 at the IT University of Copenhagen Verification of Protocols for Security and Mobility (VPSM) |
|
|
Group fotos and other fotos are available here This one-week PhD school will give young researchers, doctoral students and others a comprehensive overview of contemporary automatic verification methods and tools. The participants will meet a variety of techniques including: static analysis, (on-the-fly, probabilistic, and real-time) model checking, and Coloured Petri Nets. The emphasis will be put on verification of protocols for security and mobility. The school will offer lectures by key researchers in automatic verification, security and mobility. The exercise classes will introduce the students to state-of-the-art tools for automatic verification. Lecturers
Session 1 >> Hanne and Flemming Nielson: Validation of Cryptographic
Protocols using Static Analysis. [ABSTRACT][Slides] |
Location: IT University of Copenhagen Host: Jens Christian Godskesen Dates: 9 - 13 October 2006 Fee: DKK 750 (€ 100) Note: the
fee does not cover accommodation. The max. number of participants is 50 ("first come, first served"). List of participants. Links to sites with tools and texts will be available shortly. ECTS: 3,5 Sponsored by: FIRST Graduate School
Useful links: Accommodation: Facilities at ITU
Last updated 31.08.2006 |
ABSTRACTS:
Title: Validation of cryptographic protocols using static analysis
Speakers: Hanne Riis Nielson and Flemming Nielson
In the past a number of cryptographic protocols have been developed for exchanging messages over insecure networks. This has proved to be a surprisingly difficult task as many protocols have been shown to be flawed long after they have been published. A famous example is the Needham Schroeder key exchange protocol that was published in 1978 and became the basis for many other protocols - yet Denning and Sacco discovered an attack on the protocol in 1981 and in 1995 Lowe found another attack. In this lecture we show how to perform a systematic expansion of protocol narrations into terms of a process calculus. In this way we ensure that the detailed checks that need to be performed in a protocol are indeed made precise. We then apply static analysis technology to develop an automatic validation procedure and we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric and asymmetric key exchange protocols. The analysis is proved sound with respect to a formal semantics and it is implemented using advanced tree automata techniques.
About the speakers: Flemming Nielson is Professor at the Techinical University of Copenhagen and is head of the Computer Science and Engineering division. His main interests are modelling and validation of safe and secure systems; in particular program analysis, operational semantics, and security. Hanne Riis Nielson is Professor at the Techinical University of Copenhagen. She is a member of the Safe and Secure Systems group. Her interests are within the analysis and verification of safe and secure systems; in particular the design, construction and application of advanced tools based on formal techniques.
Title: Model Checking Security Protocols using OFMC and the AVISPA Tool
Speaker: David Basin
This course provides an introduction to automated methods and tools for formally specifying and analyzing security protocols. In the first part, we introduce security protocols, some of the difficulties in reasoning about them, and briefly survey the different kinds of formal methods available to tackle this problem. In the second part, we present OFMC, the On-the-Fly Model Checker developed at ETH Zurich and the AVISPA tool, a state-of-the-art tool for analyzing security protocols. We explain the theory behind these tools and show how they can be used to reason about complex Internet protocols, like those under development by standardization bodies like the IETF.
About the speaker: David Basin holds the chair in Information Security at ETH Zurich. His group developed the OFMC model checker and parts of the AVISPA tool. His interests are Formal Methods, Software Engineering, and Information Security.
Title: Probabilistic Model Checking of Randomised Distributed Protocols Using PRISM
Speaker: Marta Kwiatkowska
Probabilistic model checking is a formal technique for the analysis of systems which exhibit stochastic behaviour. Randomisation is frequently used as a symmetry breaker in distributed coordination, security and communication protocols. Probabilistic model checking enables a rannge of quantitative analyses of models of such protocols against specifications such as "the worst-case probability of intrusion within 10 seconds" or "the minimum expected power consumption over all possible schedulings". This course will provide an introduction to the area of probabilistic model checking by giving an overview of the models, specification notations and techniques available for their automatic verification. The course will be based on the state-of-the-art probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism/) and will be amply illustrated by real-world protocols that have been modelled and analysed in PRISM, such as the Bluetooth device discovery, Zeroconf link-local addressing, probabilistic anonymity and randomised leader election.
About the speaker: Marta Kwiatkowska is Professor of Computer Science at the University of Birmingham, UK. She led the development of the PRISM model checker which has been used to analyse over 50 protocols at Birmingham and elsewhere. Her interests are automatic verification, probabilistic modelling and model checking, and modelling of biological processes.
Relevant literature: As introductions, explaining how to use PRISM and results of modelling case studies: Probabilistic model checking in practice: Case studies with PRISM, Quantitative analysis with the probabilistic model checker PRISM. More specifically, for protocol modelling: A Formal Analysis of Bluetooth Device Discovery, Analysis of Probabilistic Contract Signing, Using Probabilistic Model Checking for Dynamic Power Management.
Title: Real Time Validation of Embedded Systems Using UPPAAL
Speakers: Gerd Behrmann and Kim G Larsen
This course will provide a thorough tutorial on the tool UPPAAL and the newly emerged UPPAAL Cora (see www.uppaal.com). UPPAAL is a tool for modelling, simulating and verifying real-time systems. The modelling language is based on timed automata allowing system behaviour to be described as a networks of timed automata extended with data variables which may be manipulated by a rich C-like programming language. The simulator is a validation tool which enables examination of possible dynamic executions of a system during early design stages and thus provides an inexpensive mean of fault detection prior to verification by the model-checker which covers the exhaustive dynamic behavior of the system.
UPPAAL Cora is a branch of UPPAAL targeted towards optimal scheduling and planning problems with numerous applications to embedded systems. The modelling formalism is that of priced timed automata allowing models to be annotated with information describing how various types of costs and rewards (e.g. energy, throughput) may accumulate during the behaviour of a model.
In the course we explain the theories, algorithms and data structure underlying UPPAAL and UPPAAL Cora and we show how to apply the tools to the analysis of a number of non-trivial real time systems (including a leader election algorithm for mobile ad-hoc networks recently proposed by Leslie Lamport). The course will include demo's and hands-on experiments with the tools.
About the speakers: Kim Guldstrand Larsen is Professor at Aalborg University, Department of Computer Science, and he is director of CISS - Center for Embedded Software Systems. His interests are semantics of concurrency and in particular in validation and verification of embedded, real-time and hybrid systems. Gerd Behrmann is Associate Professor at Aalborg University, Department of Computer Science, and he is the prime architect behind the verification tool UPPAAL. His interests are on theoretical and practical aspects of semi-automatic debugging of software and software systems using model checking and other formal methods.
Relevant litterature: In particular the two first papers in this reading material.
Title: Modelling and Verification of Communication Protocols using Coloured Petri Nets
Speaker: Lars M. Kristensen
This course provides an introduction to the Coloured Petri Nets modelling language for simulation and verification of concurrent systems. Coloured Petri Nets (CP-nets) is a graphical modelling language combining Petri Nets and the functional programming language Standard ML. Petri Nets provides the primitives for modelling concurrency, synchronisation and non-determinism. The Standard ML language provides the primitives for modelling data manipulation and for creating compact models.
The first part of the course will give an introduction to the basic concepts of CP-nets and an overview of how CP-nets can be used for simulation, verification, and performance analysis of concurrent and mobile systems. It will also present selected industrial projects in the area of communication protocols for concurrency and mobility, where CP-nets and the supporting computer tool CPN Tools have been used for modelling and verification of the protocols. The second part of the course will be a hands-on workshop, where the participants will be able to experiment with CPN Tools. The course assumes no prior knowledge of Petri Nets and Standard ML.
About the speaker: Lars M. Kristensen is an associate professor at the Department of Computer Science, University of Aarhus. He is a member of the Coloured Petri Nets Research Group developing CPN Tools. His interests are in the areas of protocol engineering, formal methods, and mobile ad-hoc networks.
Relevant literature: Colouered Petri Net and CPN Tools for Modelling and Validation of Concurrent Systems. , Specification and Validation of an Edge Router Discovery Protocol for Ad Hoc Networks , Model-based Prototyping of an Interoperability Protocol for Mobile Ad-hoc Networks .
