Autori: Michael Backes, Catalin Hritcu, and Matteo Maffei

Editorial: IEEE Computer Society Press, 21th IEEE Symposium on Computer Security Foundations (CSF 2008), p.195-209, 2008.

Rezumat:

We present a general technique for modeling electronic voting protocols in the applied pi-calculus and for automatically verifying their security using ProVerif.
In the first part of this paper, we provide novel definitions that address several important security properties and that are suitable for automation.
In particular, we propose a new formalization of coercion-resistance in terms of observational equivalence. In contrast to previous definitions in the symbolic model, our definition of coercion-resistance is amenable to automation, captures simulation and forced-abstention attacks, and still implies vote-privacy and receipt-freeness. Additionally, we capture inalterability, eligibility, and non-reusability as a correspondence property on traces.
In the second part, we illustrate the feasibility of our technique by providing the first automated security proof of the coercion-resistant protocol proposed by Juels, Catalano, and Jakobsson.

Cuvinte cheie: alegeri electronice, metode formale, securitatea limbajelor de programare, protocoale de securitate // electronic voting, formal methods, language-based security, security protocols

URL: http://www.infsec.cs.uni-sb.de/~hritcu/publications/ev-applied-csf-final.pdf