Security Games
Coordinating Institution:
Université du Luxembourg
From: 01/04/2009
To: 31/03/2012
Budget: 314,000.00€
Contact(s):
Jamroga Wojciech
,
Mauw Sjouke
,
Van der Torre Leon
Summary
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 has 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) 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. The second line focuses 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.
Refereed Scientific Publications:
- Nils Bulling and Wojciech Jamroga (2010), Model Checking Agents with Memory Is Harder than It Seemed. Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2010. To appear.
- Mehdi Dastani and Wojciech Jamroga (2010), Reasoning about Strategies of Multi-Agent Programs. Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2010. To appear.
- Nils Bulling and Wojciech Jamroga (2009), Model Checking ATL+ Is Harder than It Seemed. Proceedings of the 7th European Workshop on Multi-Agent Systems EUMAS'09.
- Mehdi Dastani and Wojciech Jamroga (2009), Reasoning about Strategic Properties of Multi-Agent Programs. Proceedings of the 7th European Workshop on Multi-Agent Systems EUMAS'09.
- Inanc Seylan and Wojciech Jamroga (2009), Coalition Description Logic for Individuals. Proceedings of the 6th Workshop on Methods for Modalities M4M-6, pp. 146-162.