SATMC: A SAT-Based Model Checker for Security Protocols

摘要

We present SATMC (SAT-based Model Checker), an open and flexible platform for SAT-based bounded model checking of security protocols. Under the standard assumptions of perfect cryptography and of strong typing, SATMC performs a bounded analysis of the problem by considering scenarios with a finite number of sessions whereby messages are exchanged on a channel controlled by the most general intruder based on the Dolev-Yao model. Given a positive integer k and a protocol description written in a rewrite-based formalism, SATMC automatically generates a propositional formula by using sophisticated encoding techniques developed for planning (see for a survey); state-of-the-art SAT-solvers taken off-the-shelf are then used to check the propositional formula for satisfiability and any model found by the solver is turned into a partially ordered set of transitions of depth k whose linearizations correspond to attacks on the protocol. If the formula is found to be unsatisfi-able, then k is incremented and the whole procedure is iterated until either a termination condition is met or a given upper bound for k is reached. Experimental results indicate that the approach is very effective: SATMC takes a few seconds to analyze and detect flaws on 22 protocols of the Clark&Jacob library.