SAT-based model-checking for security protocols analysis

9 years 11 months ago
SAT-based model-checking for security protocols analysis
We present a model checking technique for security protocols based on a reduction to propositional logic. At the core of our approach is a procedure that, given a description of the protocol in a multi-set rewriting formalism and a positive integer k, builds a propositional formula whose models (if any) correspond to attacks on the protocol. Thus, finding attacks on protocols boils down to checking a propositional formula for satisfiability, problem that is usually solved very efficiently by modern SAT solvers. Experimental results indicate that the approach scales up to industrial strength security protocols with performance comparable with (and in some cases superior to) that of other state-of-the-art protocol analysers. Keywords Security Protocols
Alessandro Armando, Luca Compagna
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2008
Authors Alessandro Armando, Luca Compagna
Comments (0)