Abstract: The security protocol model-checking based on classcial logic is introduced in this paper, using the model- checker SATMC and the model-checker ProVerif as examples, and a security protocol model-checker JLU-PV exploited by us based on SAT is also introdu

Key words: Security protocol,Model-checking,Propositional satisfiability, Resolution