Edinburgh Research Explorer

Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions


Original languageEnglish
Title of host publicationProceedings of 2002 Workshop on Foundations of Computer Security
Number of pages10
Publication statusPublished - Jun 2002
EventProceedings of 2002 Workshop on Foundations of Computer Security - Copenhagen, Denmark
Duration: 25 Jul 200226 Jul 2002


ConferenceProceedings of 2002 Workshop on Foundations of Computer Security


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 concur- rent 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.


Proceedings of 2002 Workshop on Foundations of Computer Security


Copenhagen, Denmark

Event: Conference

Download statistics

No data available

ID: 25317116