Symbolic analysis of terrorist fraud resistance

Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. Symbolic analysis of terrorist fraud resistance. In Proceedings of the 24th European Symposium on Research in Computer Security (ESORICS'19), Lecture Notes in Computer Science, Springer, Luxembourg, 2019.

Download

[PDF] 

Abstract

Distance-bounding protocols aim at preventing several kinds ofattacks, amongst which terrorist fraud, where a far away maliciousprover colludes with an attacker to authenticate once, without giving him any advantage for future authentication. In this paper, we consider a symbolic setting and propose a formaldefinition of terrorist fraud, as well as two reduction results.When looking for an attack, we can first restrict ourselves to consider a particular (and quite simple) topology. Moreover, under some mildhypotheses, the far away malicious prover has a best strategy on which we canfocus on when looking for an attack.These two reduction results make possiblethe analysis of terrorist fraud resistance using an existingverification tool. As an application, we analyse several distance-bounding protocols, as well as some contactless payment protocolsusing the ProVerif tool.

BibTeX

@inproceedings{DDW-esorics19,
  address =       {Luxembourg},
  abstract = {Distance-bounding protocols aim at preventing several kinds of
attacks, amongst which terrorist fraud, where a far away malicious
prover colludes with an attacker to authenticate once, without giving him any advantage 
for future authentication. In this paper, we consider a symbolic 
setting and propose a formal
definition of terrorist fraud, as well as two reduction results.
When looking for an attack, we can first restrict ourselves to consider a particular (and quite simple) topology. Moreover, under some mild
hypotheses, the far away malicious prover has a best strategy on which we can
focus on when looking for an attack.
These two reduction results make possible
the analysis of terrorist fraud resistance using an existing
verification tool. As an application, we analyse several distance-bounding protocols, as well as some contactless payment protocols
using the ProVerif tool.
},
  author    = {Alexandre Debant and
               St{\'{e}}phanie Delaune and
               Cyrille Wiedling},
  title =        {Symbolic analysis of terrorist fraud resistance},
  booktitle = {{P}roceedings of the 24th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity (ESORICS'19)},
  year =         {2019},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  acronym =       {{ESORICS}'19},
}