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:
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).
The following members are involved in the project:
The project is supported by the National Research Fund, Luxembourg.