this paper we consider the nature of machine proofs used in the CSP approach to the verification of authentication protocols. In [Sch96], a general method is presented for the analysis and verification of authentication protocols using the process algebra CSP [Hoa85]. The CSP syntax provides a natural and precise way to describe such protocols in terms of the messages accepted and transmitted by the individual protocol participants. The CSP traces model provides a formal framework for reasoning about these protocols. In the CSP method, authentication is considered to be message-oriented: