This paper proposes a new simple trace semantics that can be used to specify security properties, this technique supports a protocol designer to provide formal analysis of the security properties.

To define the semantics of Communicating Sequential Processes, the notions of trace, assertion trace set, kernel of assertion trace set and process trace aet are introduced in this paper.