Formal Analysis for Network Security Properties on a Trace Semantics

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 specify security properties. 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.