Attacking Fair-Exchange Protocols: Parallel Models vs. Trace Models

Most approaches to formal protocol verification rely on an operational model based on traces of atomic actions. Modulo CSP, CCS, state-exploration, Higher Order Logic or strand spaces frills, authentication or secrecy are analyzed by looking at the existence or the absence of traces with a suitable property. We introduced an alternative operational approach based on parallel actions and an explicit representation of time. Our approach consists in specifying protocols within a logic language (ALSP), and associating the existence of an attack to the protocol with the existence of a model for the specifications of both the protocol and the attack. In this paper we show that, for a large class of protocols such as authentication and key exchange protocols, modeling in ALSP is equivalent - as far as authentication and secrecy attacks are considered - to modeling in trace based models. We then consider fair exchange protocols introduced by N. Asokan et al. showing that parallel attacks may l...