An improved SAT model for detection of type flaw attacks
Abstract：For the problem that the current SAT model checker can not detect type flaw attacks, a new improved model SAT#was proposed. Through introducing non-type variables under the match mode and defining the concept of non-type messages, the new model relieves the type restriction of SAT model checker to unknown messages. Moreover, it replaces the original strong type restriction messages with the non-type messages in the rewrite rules of veracity agent. Through adding the message match algorithm, the veracity agent can accept the type flaw messages to realize the detection of type flaw attacks. The detection results on Otway-Rees protocol demonstrate that not only the existing type flaw attack to the initiator A but also a new type flaw attack to the responder B are found. The experimental results show that the SAT# model has a certain reliability.
Keywords：security protocolformal analysismodel checkingrewrite rulestype flaw attackmatchmodegraphplan-based encodingSAT problem
Publication Date：2011-01-01
Online Publishing Date：2025-08-15(First online date of this platform, not the publication date of the document)