Generalizes the approach defined by the author in Proc. 3rd ACM Conf. on Comput. & Commun. Security (1996) so as to be able to formally verify electronic payment protocols. The original approach is based on the use of general-purpose formal methods. It is complementary with modal logic-based approaches as it allows for a description of protocols, hypotheses and authentication properties at a finer level of precision and with more freedom. The proposed generalization mainly requires being able to express and verify payment properties. Such properties are indeed much more elaborate than authentication ones and require a significant generalization in the way properties are expressed. The modelling of the protocol and of the potential knowledge held by intruders, on the other hand, is left unchanged. The approach is currently being applied to the C-SET and SET (secure electronic transactions) protocols, and has already led to significant results.

We present an approach to the verification of authentication protocols.The approach is based on the use of general purpose formal methods.It is complementary with modal logic based-approach{~S as it allows for a description of protocol, hypotheses and authentication properties at a finer level of precision and with more freedom.It differs from formal methods based approaches and in particular from Meadows' approach in that it focuses more on proof conciseness and readability than on proof automatization.To achieve this we use a clear separation between the modeling of reliable agents and that of unreliable agents or more generally of intruders.We also show how to express authentication properties using basic and precise temporal notions.The approach is presented by the mean of an application example based on a public key version of the Needham-Schroeder protocol.