Abstract:

Security protocols are the foundation of modern secure networked systems. Proving the security properties of cryptographic protocols is a challenge. Logic of event  is a formal method for describing the state migration of a distributed system, which formally describes security protocols, and which is the basis of theorem proving. Using the language of event orderings, event classes, and a type of atoms representing random numbers, keys,signatures, and ciphertexts, we present a theory in which authentication protocols can be formally defined and strong authentication properties proven. The improved NeedhamSchroeder protocol with time stamp, is proved to be of good security by our theory. The thoery can also be applied to formal analysis and verification of similar security protocols.

Key words: logic of event;modified Needham-Schroeder protocol;formal method;strong authentication theory