An approach to finding the attacks on the cryptographic protocols

摘要

It is necessary to development the formal tools for verifying cryptographic protocols because of the subtlety of cryptographic protocols flaws; In terms of the notions of the restrictive channel and the equivalent message, this paper presents an approach that utilizes the substitution rules of messages and the deduction rules to prove whether the insecure states of the cryptographic protocols are reachable or not, and the analysis of several famous protocols shows the validity of the method.