Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks
Authors: Graham Steel ; Alan Bundy ; Ewen Denney
Date:Jul 2002
Publication Title:Proceedings of 2002 Workshop on Foundations of Computer Security
Publication Type:Conference Paper
We present an implementation of a method for finding counterexamples to universally quantified conjectures in first-order logic. Our method uses the proof by consistency strategy to guide a search for a counterexample and a standard first-order theorem prover to perform a concurrent check for inconsistency. We explain briefly the theory behind the method, describe our implementation, and evaluate results achieved on a variety of incorrect conjectures from various sources. Some work in progress is also presented: we are applying the method to the verification of cryptographic security protocols. In this context, a counterexample to a security property can indicate an attack on the protocol, and our method extracts the trace of messages exchanged in order to effect this attack. This application demonstrates the advantages of the method, in that quite complex side conditions decide whether a particular sequence of messages is possible. Using a theorem prover provides a natural way of dealing with this. Some early results are presented and we discuss future work.
2002 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Graham Steel and Alan Bundy and Ewen Denney },
title = {Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks},
book title = {Proceedings of 2002 Workshop on Foundations of Computer Security},
year = 2002,
month = {Jul},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh