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 language | English |
---|---|
Pages (from-to) | 51-68 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 55 |
Issue number | 1 |
DOIs | |
Publication status | Published - Jan 2003 |
Externally published | Yes |
Event | LACPV'2001, Logical Aspects of Cryptographic Protocol Verification (in Connection with CAV '01) - , France Duration: 23 Jul 2001 → 23 Jul 2001 |