A generic model for symbolic analyzing security protocols

Formal methods have proved useful in the analysis of security protocols. In this paper, we propose a generic model for symbolic analyzing security protocols (GSPM for short) that supports message passing semantics and constructs for modelling the behavior of protocol participants. GSPM is simple, but it is expressive enough to express security protocols and properties in a precise and faithful manner. In order to address that the execution of a protocol generates infinitely many paths, we use symbolic method. Based on GSPM, it is shown how security properties such as confidentiality, authentication, non-repudiation, fairness and anonymity can be described.