User Tools

Site Tools


A Dolev-Yao-based Definition of Abuse-free Protocols (BibTeX)

@INPROCEEDINGS{KaehlerKuestersWilke-ICALP-2006,
  author = {Detlef K{\"a}hler and Ralf K{\"u}sters and Thomas Wilke},
  title = {{A Dolev-Yao-based Definition of Abuse-free Protocols}},
  booktitle = {Proceedings of the 33rd International Colloqium on Automata, Languages, and Programming (ICALP 2006)},
  year = 2006,
  publisher = {Springer},
  pages = { 95--106},
  series = {Lecture Notes in Computer Science},
  volume = 4052,
  editor = {M.~Bugliesi and B.~Preneel and V.~Sassone and I.~Wegener},
  abstract = {We propose a Dolev-Yao-based definition of abuse freeness for optimistic contract-signing protocols which, unlike other definitions, incorporates a rigorous notion of what it means for an outside party to be convinced by a dishonest party that it has the ability to determine the outcome of the protocol with an honest party, i.e., to determine whether it will obtain a valid contract itself or whether it will prevent the honest party from obtaining a valid contract. Our definition involves a new notion of test (inspired by static equivalence) which the outside party can perform.  We show that an optimistic contract-signing protocol proposed by Asokan, Shoup, and Waidner is abusive and that a protocol by Garay, Jakobsson, and MacKenzie is abuse-free according to our definition. Our analysis is based on a synchronous concurrent model in which parties can receive several messages at the same time. This results in new vulnerabilities of the protocols depending on how a trusted third party reacts in case it receives abort and resolve requests at the same time.}
}