Security games


General information

Project name:Security Games (S-GAMES)
Starting date - closing date: 1 November 2009 - 31 October 2012
Participating groups: ICR, SaToSS


Information security is not a static black-and-white system feature. Rather, it is a dynamic balance between a service provider trying to keep his system secure and an adversary trying to penetrate or abuse the service. Such interplay can be considered as a game between the adversary and the service provider and the field of game theory provides methods and tools to analyse such interactions.

Game theory has a long history in many different disciplines with their own goals, methodologies and culture. Games for verification and design have been studied in computer science for the last ten years. This fundamental research into extending and complementing traditional verification approaches from formal methods with game theoretic reasoning is paving the way for more effective verification tools.

These developments are of particular interest to the field of security, in which formal verification has always played an important role. The purpose of the project is to study how these new developments can be used to strengthen current analysis and verification techniques in information security.

The project will have two main lines of research:

  1. A study of the use of game-theoretic methods in the field of security, resulting in requirements on game-theoretic methods for security.
  2. The development of novel verification methods based on the combined use of formal verification techniques and a game theoretic approach, and its application to the field of security.

For the first line, we have selected two areas in security for which the application of these techniques seems particularly promising: fair exchange protocols and attack/defence analysis. An example of a fair exchange protocol is a contract signing protocol. The purpose of such a protocol is to allow two parties to digitally sign a contract, while preventing any of the parties to gain an advantage by cheating the other (e.g. by not signing a contract that has already been signed by one's partner). The second area is the analysis of attack/defence strategies. Our aim is to design and analyse strategies for a defender to optimally defend against possible attacks, given e.g. some budget constraints.

The second line will focus on the interplay of finite and infinite games, mathematical logic and automata theory, in particular on analysis techniques for infinite-state systems, linear-time model checking, and game models for protocols. It will build on the foundations laid in the last decade.

This is a joint project of Prof. Dr. Leon van der Torre and Prof. Dr. Sjouke Mauw, both from the Computer Science and Communication Research Unit at the University of Luxembourg. It will strongly build upon the current expertise of the two groups in logic and in formal methods in security.

The proposed project will be executed in the context of EUROPEAN SCIENCE FOUNDATION, PESC Research Networking Programme, Games for Design and Verification (GAMES), which Luxembourg recently joined (Prof. Leon van der Torre is member of the steering committee and Prof. Sjouke Mauw is project member).

Team members

The following members are involved in the project:

Financial support

The project is supported by the National Research Fund, Luxembourg.