Abstract:
Abstract〖WT〗:This article mainly aims at security protocol automation analysis and verification of the attacker problems.It is discussed the attacker model in the communication Communicating Sequential order process (CSP) Processes firstly.Further,the model is an open,extensible,concern with synchronous and construction principles,uses formalism method to descript it.At last,the model uses this specific construction principle to attack a security protocol to test the model,and lay a basis on application of automation analysis and design security protocol.