Attacking Fair-Exchange Protocols
Electronic Notes in Theoretical Computer Science, pp. 51-68, 2003.
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.
Full Text (Upload PDF)
PPT (Upload PPT)