Analysis of a security protocol in ?CRL

Needham-Schroeder public-key protocol; With the growth and commercialization of the Internet, the security of communication between computers becomes a crucial point. A variety of security protocols based on cryptographic primitives are used to establish secure communication over insecure open networks and distributed systems. Unfortunately, security protocols often contain serious errors. Formal verification can be used to obtain assurance that a protocol cannot be attacked by an intruder. In this paper, we present how the process-algebraic language ?CRL can be used to specify and analyze security protocols. To illustrate the feasibility of our approach, we analyze the Needham-Schroeder public-key protocol and reproduce the error found by Gavin Lowe [Low96a]. Two more definitions of authentication are studied. We give some remarks on our approach and discuss some possible directions for future work.