Heuristic Methods for Security Protocols

Qurat ul Ain Nizamani
(Department of Computer Science, University of Leicester, UK)
Emilio Tuosto
(Department of Computer Science, University of Leicester, UK)

Model checking is an automatic verification technique to verify hardware and software systems. However it suffers from state-space explosion problem. In this paper we address this problem in the context of cryptographic protocols by proposing a security property-dependent heuristic. The heuristic weights the state space by exploiting the security formulae; the weights may then be used to explore the state space when searching for attacks.

In Michele Boreale and Steve Kremer: Proceedings 7th International Workshop on Security Issues in Concurrency (SECCO 2009), Bologna, Italy, 5th September 2009, Electronic Proceedings in Theoretical Computer Science 7, pp. 61–75.
Published: 23rd October 2009.

ArXived at: http://dx.doi.org/10.4204/EPTCS.7.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org