engleski

Specifying and verifying timing aspects of security protocols

Protocol Security Verification is one of the greatest success stories of formal methods. Indeed, a number of attacks on security protocols have been found using formal methods. Tools are used in the automated discovery of new attacks and the shaping of new protocols. However, some aspects relevant to protocol security are not covered by many formal models. Time is one of such important aspects. We describe the use of Multiset Rewriting for the specification and verification of timing aspects of protocols, such as network delays, processing time, timeouts, timed intruder models and distance bounding properties. We investigate such timed features and specify these timing aspects of security protocols using multiset rewriting with real time. We formalize timed Dolev-Yao intruder theories, as well as network and protocol theories that take into account physical laws related to time. We also investigate related verification problems, such as the secrecy problem and the false acceptance and the false rejection problems related to DistanceBounding Protocols. We describe decidable fragments of our framework for the specification and verification of timing properties of security protocols and provide PSPACE complexity results.

Multiset Rewriting, Security Protocols, Dolev-Yao Intruder, DistanceBounding Protocols, Computational Complexity

nije evidentirano