Formal Analysis for Cryptographic Protocols on a Trace Semantics

The analysis and verification of security protocols is an important field in the security of computer nowadays. Formal method has been advocated as an important means of improving the safety and reliability of software systems, especial those which are safety-critical. We propose a new simple trace semantics that can be used to analyse Cryptographic Protocols. Our technique support a protocol designer to provide formal Analysis of the security properties. We illustrate the utility of our technique by exposing two attacks on the well studied protocol TMN.