Stéphanie Delaune: Bounding the number of agents, for equivalence too

Bounding the number of agents, for equivalence too

Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Bounding the number of agents, for equivalence too. In Proceedings of the 5th International Conference on Principles of Security and Trust (POST'16), pp. 211–232, Lecture Notes in Computer Science 9635, Springer, Eindhoven, The Netherlands, April 2016.

Download

[PDF]

Abstract

Bounding the number of agents is a current practice when modeling a protocol. In 2003, it has been shown that one honest agent and one dishonest agent are indeed sufficient to find all possible attacks, for secrecy properties. This is no longer the case for equivalence properties, crucial to express many properties such as vote privacy or untraceability.
In this paper, we show that it is sufficient to consider two honest agents and two dishonest agents for equivalence properties, for deterministic processes with standard primitives and without else branches. More generally, we show how to bound the number of agents for arbitrary constructor theories and for protocols with simple else branches. We show that our hypotheses are tight, providing counter-examples for non actiondeterministic processes, non constructor theories, or protocols with complex else branches.

BibTeX

@inproceedings{CDD-post16,
  abstract =      {Bounding the number of agents is a current practice
                   when modeling a protocol. In~2003, it has been shown
                   that one honest agent and one dishonest agent are
                   indeed sufficient to find all possible attacks, for
                   secrecy properties. This is no longer the case for
                   equivalence properties, crucial to express many
                   properties such as vote privacy or
                   untraceability.\par In this paper, we show that it is
                   sufficient to consider two honest agents and two
                   dishonest agents for equivalence properties, for
                   deterministic processes with standard primitives and
                   without else branches. More generally, we show how to
                   bound the number of agents for arbitrary constructor
                   theories and for protocols with simple else branches.
                   We show that our hypotheses are tight, providing
                   counter-examples for non actiondeterministic
                   processes, non constructor theories, or protocols
                   with complex else branches.},
  address =       {Eindhoven, The~Netherlands},
  author =        {Cortier, V{\'e}ronique and Dallon, Antoine and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 5th {I}nternational {C}onference
                   on {P}rinciples of {S}ecurity and {T}rust
                   ({POST}'16)},
  OPTDOI =           {10.1007/978-3-662-49635-0_11},
  editor =        {Piessens, Frank and Vigan{\'o}, Luca},
  month =         apr,
  pages =         {211-232},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Bounding the number of agents, for equivalence~too},
  volume =        {9635},
  year =          {2016},
  acceptrate =    {13/},
  acronym =       {{POST}'16},
  nmonth =        {4},
  OPTLONGPDF =       {https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
                  rr-lsv-2016-01.pdf},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}