Edinburgh Research Explorer

Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks

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

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

Conference

ConferenceProceedings of 2002 Workshop on Foundations of Computer Security
CountryDenmark
CityCopenhagen
Period25/07/0226/07/02

Abstract

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.

Event

Proceedings of 2002 Workshop on Foundations of Computer Security

25/07/0226/07/02

Copenhagen, Denmark

Event: Conference

ID: 25317116