Specifying electronic voting protocols in typed MSR

ABSTRACT

Electronic voting, as well as other privacy-preserving protocols, use special cryptographic primitives and techniques that are not widely used in other types of protocols, e.g. in authentication protocols. These include blind signatures, commitments, zero-knowledge proofs, mixes and homomorphic encryption. Furthermore, typical formalizations of the Dolev-Yao intruder's capabilities do not take into account these primitives and techniques, nor do they consider some types of attacks that e-voting as well as other types of protocols are designed to protect against, such as privacy attacks due to undesired linkability of protocol executions. This work aims to extend Typed MSR so that it is able to support the specification of privacy-preserving protocols, as well as the capabilities of a Dolev-Yao intruder designed to attack such protocols.

REFERENCES

• 1: Alessandro Acquisti. Receipt-free homomorphic elections and write-in ballots. Technical Report 2004/105, International Association for Cryptologic Research, May 2004.
• 2: David Aspinall , Adriana Compagnoni, Subtyping Dependent Types, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.86, July 27-30, 1996
• 3: Theodoros Balopoulos, Stefanos Gritzalis, and Sokratis K. Katsikas. Specifying privacy-preserving protocols in Typed MSR. Computer Standards & Interfaces, 27(5):501--512, June 2005.
• 4: Fabrice Boudot. Efficient proofs that a committed number lies in an interval. In EUROCRYPT, pages 431--444, 2000.
• 5: Iliano Cervesato. Typed Multiset Rewriting Specifications of Security Protocols. In A. Seda, editor, First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology --- MFCSIT'00, pages 1--43, Cork, Ireland, 19--21 July 2000. Elsevier ENTCS 40.
• 6: Iliano Cervesato, Typed MSR: Syntax and Examples, Proceedings of the International Workshop on Information Assurance in Computer Networks: Methods, Models, and Architectures for Network Security, p.159-177, May 21-23, 2001
• 7: David L. Chaum, Untraceable electronic mail, return addresses, and digital pseudonyms, Communications of the ACM, v.24 n.2, p.84-90, Feb. 1981 [doi>10.1145/358549.358563]
• 8: David Chaum, Security without identification: transaction systems to make big brother obsolete, Communications of the ACM, v.28 n.10, p.1030-1044, Oct. 1985 [doi>10.1145/4372.4373]
• 9: D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 2(29):198--208, 1983.
• 10: Jason E. Holt and Kent E. Seamons. Selective disclosure credential sets. Accessible as http://citeseer.nj.nec.com/541329.html, 2002.
• 11: P. Paillier. Public-key cryptosystems based on discrete logarithms residues. In Advances in Cryptology - Eurocrypt '99, pages 223--238. Springer-Verlag LNCS 1592, 1999.
• 12: Paul Syverson, Catherine Meadows, and Iliano Cervesato. Dolev- Y ao is no better than M achiavelli. In P. Degano, editor, First Workshop on Issues in the Theory of Security --- WITS'00, pages 87--92, July 2000.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Design, Security, Verification

Keywords:
Dolev-Yao intruder, electronic voting, privacy, security protocols, specification, typed MSR