Title :
Verifying Security Properties of Cryptoprotocols: A Novel Approach
Author :
Saleh, Mohamed ; Debbabi, Mourad
Author_Institution :
Concordia Univ., Montreal
Abstract :
We model security protocols as a game tree using concepts of game semantics. Using this model we ascribe semantics to protocols written in the standard simple arrow notation. According to the semantics, a protocol is interpreted as a set of strategies over a game tree that represents the type of the protocol. Moreover, in order to specify properties of the model, a logic that deals with games and strategies is developed. A tableau-based proof system is given for the logic, which can serve as a basis for a model checking algorithm. This approach allows us to model a wide range of security protocol types and verify different properties instead of using a variety of methods as is currently the practice. Furthermore, the analyzed protocols are specified using only the simple arrow notation heavily used by protocol designers and by practitioners.
Keywords :
cryptographic protocols; formal verification; game theory; trees (mathematics); cryptoprotocols; game semantics; game tree; model checking algorithm; security protocols; tableau-based proof system; Algebra; Authentication; Computational modeling; Cryptography; Equations; Information security; Information systems; Logic; Protocols; Software engineering;
Conference_Titel :
Software Engineering and Formal Methods, 2007. SEFM 2007. Fifth IEEE International Conference on
Conference_Location :
London
Print_ISBN :
978-0-7695-2884-7
DOI :
10.1109/SEFM.2007.46