Attacking fair-exchange protocols: Parallel models vs. Trace models

L.C. Aiello, F. Massacci

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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 lead the trusted third party of the protocol into an inconsistent state. We show that the trace based model does not allow for the representation of this kind of attacks, whereas our approach can represent them. © 2001 Published by Elsevier Science B.V.
Original languageEnglish
Pages (from-to)51-68
JournalElectronic Notes in Theoretical Computer Science
Volume55
Issue number1
DOIs
Publication statusPublished - Jan 2003
Externally publishedYes
EventLACPV'2001, Logical Aspects of Cryptographic Protocol Verification (in Connection with CAV '01) - , France
Duration: 23 Jul 200123 Jul 2001

Fingerprint

Dive into the research topics of 'Attacking fair-exchange protocols: Parallel models vs. Trace models'. Together they form a unique fingerprint.

Cite this