Game semantics model for security protocols

Our aim is to present a game semantics model for the specification of security protocols. Game semantics has been used to give an operational flavor to denotational semantics, thereby combining the best of both worlds by having an elegant mathematical structure and at the same time describing steps of execution. Game semantics was successfully used to prove full abstraction of PCF and has since been used to describe the semantics of a variety of programming languages. It fits naturally in the framework of security protocols as the interactions between communicating parties can be described as moves in a game, where honest agents are the players and the intruder is the opponent. We propose a game-based calculus for the specification of security protocols. First, we define games that represent interactions in security protocols, these games are then used to ascribe denotational semantics to security protocols.