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. 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. EASST best paper award of the ETAPS conference.

Download

[PDF] [HTML]

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 trace 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 action-deterministic processes, non constructor theories, or protocols with complex else branches.

BibTeX

@inproceedings{CDD-post16,
  	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)},
  	editor =	{Piessens, Frank and Vigan{\'o}, Luca},
  	month =	apr,
  	OPTnote =	{},
  	publisher =	{Springer},
  	series =	{Lecture Notes in Computer Science},
  	title =	{Bounding the number of agents, for equivalence~too},
  	year =	{2016},
	pages = {211-232},
volume    = {9635},
  	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 trace 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 action-deterministic processes, non constructor theories, or protocols with
complex else branches.},
  doi       = {10.1007/978-3-662-49635-0_11},
note = {{\bf EASST best paper award of the ETAPS conference}}
}