A User Interface for a Game-Based Protocol Verification Tool

We present a platform that allows a protocol researcher to specify the sequence of games from an initial protocol to a protocol where the security property under consideration can be shown to hold using "conventional" means. Our tool represents the protocol in the form of a program dependency graph. A step in the sequence corresponds to replacing a local fragment in the current graph. The researcher interacts with the tool by pointing out the location of this fragment and choosing the applied transformation from a list. The tool guarantees the errorfreeness of the sequence. By our knowledge, this is the first time where the aspects of user interaction have been seriously considered for a sequenceof-games-based protocol analyzer.

• Type: Journal
• Year: 2009
• Where: IFIP
• Authors: Peeter Laud, Ilja Tsahhirov
• Keywords: IFIP 2009, Program Dependency Graph, Programming Languages, Sequenceof-games-based Protocol Analyzer, Tool