An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols

In previous work we showed that automatic SAT-based model-checking techniques based on a reduction of protocol (in)security problems to a sequence of propositional satisfiability problems can be used to effectively find attacks on protocols. In this paper we present an optimized intruder model that...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2005-03, Vol.125 (1), p.91-108
Main Authors: Armando, Alessandro, Compagna, Luca
Format: Article
Language:English
Subjects:
Bounded Model Checking
Rewriting
SAT
Security Protocols
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In previous work we showed that automatic SAT-based model-checking techniques based on a reduction of protocol (in)security problems to a sequence of propositional satisfiability problems can be used to effectively find attacks on protocols. In this paper we present an optimized intruder model that may lead in many cases to shorter attacks which can be detected in our framework by generating smaller propositional formulae. The key idea is to assume that some of the abilities of the intruder have instantaneous effect, whereas in the previously adopted approach all the abilities of the intruder were modeled as state transitions. This required non trivial extensions to the SAT-reduction techniques which are formally described in the paper. Experimental results indicate the advantages of the proposed optimization.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2004.05.021