Improvement of SAT-Based Model Checking of Security Protocols
Yuanyuan Yang, Wenping Ma · 2009
In SAT-based model checking, some abilities of the intruder are not mentioned. In this paper, these abilities are added and all the power of the intruder is included. Moreover, type-change ability is endowed with the intruder, which can check type-flaw attack. Finally, a message-match algorithm, which can significantly improve the efficiency of the SAT-based model checking, is proposed. Experiment shows that the algorithm can greatly reduce the production of useless message.