Verification of strategic properties for the Prêt-À-Voter protocol using Tamarin (joint work with Wojtek Jamroga and Damian Kurpiewski)

Speaker:  Catalin Dima (Université Paris-Est Créteil)

Abstract:

We report on the verification of anonymity and coercion-freeness properties of the Prêt-À-Voter electronic voting protocol using the Tamarin tool for symbolic verification of security properties. Our approach is to generate many models corresponding with each choice of attacker actions (i.e. attacker strategies) and check, on each model, a “trace equivalence” lemma modeling the fact that the attacker does not distinguish between a trace in which the coerced voter has obeyed the orders, from a trace in which the voter has ignored the coercion. This seems to be the only approach available in Tamarin for modeling epistemic knowledge, a notion necessary for encoding anonymity. The results are far from encouraging since many false negatives or positives are obtained, necessitating model adaptations which cannot be done automatically, and when correct results are obtained the running times are prohibitive. Our conclusions point the need for theory and tool improvement in which equational and rewriting logics be combined with strategy logics.