Game-theory and Logic for Non-repudiation Protocols and Attack Analysis
Matthijs Melissen · 2013
Research in security has traditionally focused on preventing all possible attacks, without focusing on the attacker and defender, and their incentives, abilities, and knowledge. However, the security of a system might depend on such aspects. Therefore, we use logic and artificial intelligence to model the attacker, the de-fender, and their interaction. We have identified three areas in which the interac-tion between attacker and defender, and thus the application of game theory and logic, is relevant. First, we study security protocols. A security protocol specifies the behavior of agents that interact with the aim of guaranteeing security properties. As secu-rity protocols are executed by interacting agents with possibly diverging interests, they are an interesting candidate for game-theoretical and logical modeling. We study in particular non-repudiation protocols, which are protocols that guaran-tee that an agent cannot deny having executed a certain event. We introduce a game-theoretical framework for analysis of security protocols. This framework is created by unifying the Cremers–Mauw protocol semantics with concurrent game