Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Software and Systems Modeling
Published in: Software and Systems Modeling 4/2016

17-06-2015 | Theme Section Paper

Constructing and verifying a robust Mix Net using CSP

Authors: Efstathios Stathakidis, David M. Williams, James Heather

Published in: Software and Systems Modeling | Issue 4/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

A Mix Net is a cryptographic protocol that unlinks the correspondence between its inputs and its outputs. In this paper, we formally analyse a Mix Net using the process algebra CSP and its associated model checker FDR. The protocol that we verify removes the reliance on a Web Bulletin Board: rather than communicating via a Web Bulletin Board, the protocol allows the mix servers to communicate directly, exchanging signed messages and maintaining their own records of the messages they have received. Mix Net analyses in the literature are invariably focused on safety properties; important liveness properties, such as deadlock freedom, are wholly neglected. This is an unhappy omission, however, since a Mix Net that produces no results is of little use. In contrast, we verify here that the Mix Net is guaranteed to terminate, with each honest mix server outputting the decrypted vector of plaintexts alongside a chain proving that each re-encryption/permutation and partial decryption operation was performed correctly, under the assumption that there is an honest majority of them acting according to the protocol.
previous article Automated anonymity verification of the ThreeBallot and VAV voting systems
next article The Unit-B method: refinement guided by progress concerns

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
Literature
1.
Adida, B.: Helios: Web-based open-audit voting. In: Proceedings of the 17th USENIX Security Symposium (Security ’08) (2008)
2.
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, Schmidt (eds.) POPL, pp. 104–115. ACM (2001)
3.
Burton, C., Culnane, C., Heather, J., Peacock, T., Ryan, P.Y.A., Schneider, S., Srinivasan, S., Teague, V., Wen, R., Xia, Z.: A supervised verifiable voting protocol for the Victorian Electoral Commission. In: Kripp et al. (eds.) Electronic Voting. LNI 205, pp. 81–94. GI (2012)
4.
Boneh, D.: The decision Diffie–Hellman problem. In: Buhler (ed.) Algorithmic Number Theory, Third International Symposium, ANTS-III, Portland, OR, USA, 21–25 June 1998, Proceedings. LNCS 1423, pp. 48–63. Springer (1998)
5.
Canetti, R.: Universally Composable security: a new paradigm for cryptographic protocols. In: FOCS, pp. 136–145. IEEE Computer Society (2001)
6.
Chaum, D., Crépeau, C., Damgård, I.: Multiparty unconditionally secure protocols (extended abstract). In: Simon (ed.) STOC, pp. 11–19. ACM (1988)
7.
Chaum, D.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24(2), 84–88 (1981)CrossRef
8.
Chaum, D., Pedersen, T.P.: Wallet databases with observers. In: Advances in Cryptology, CRYPTO ’92, pp. 89–105. Springer (1992)
9.
Desmedt, Y., Kurosawa, K.: How to break a practical MIX and design a new one. In: Preneel (ed.) EUROCRYPT. LNCS 1807, pp. 557–572. Springer (2000)
10.
Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)CrossRefMATH
11.
12.
Fiat, A., Shamir, A.: How to prove yourself: practical solutions to identification and signature problems. In: Odlyzko (ed.) CRYPTO. Lecture Notes in Computer Science 263, pp. 186–194. Springer (1986)
13.
Gamal, T.E.: A public key cryptosystem and a signature scheme based on discrete logarithms. IEEE Trans. Inf. Theory 31(4), 469–472 (1985)MathSciNetCrossRef
14.
Golle, P., Jakobsson, M., Juels, A., Syverson, P.F.: Universal re-encryption for mixnets. In: Okamoto (ed.) CT-RSA. LNCS 2964, pp. 163–178. Springer (2004)
15.
Heather, J., Lundin, D.: The append-only Web Bulletin Board. In: Degano et al. (eds.) Formal Aspects in Security and Trust. LNCS 5491, pp. 242–256. Springer (2008)
16.
Jakobsson, M.: A practical mix. In: Advances in Cryptology—EuroCrypt ’98, pp. 448–461. Springer, London (1998)
17.
Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis et al. (eds.) ESORICS. LNCS 6345, pp. 389–404. Springer (2010)
18.
Lowe, G.: An attack on the Needham–Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–133 (1995)CrossRefMATH
19.
Lowe, G.: Breaking and fixing the Needham–Schroeder public-key protocol using FDR. In: Margaria, Steffen (eds.) TACAS. LNCS 1055, pp. 147–166. Springer (1996)
20.
Lamport, L., Shostak, R.E., Pease, M.C.: The Byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982)CrossRefMATH
21.
Meadows, C.: Analyzing the Needham–Schroeder public-key protocol: a comparison of two approaches. In: Bertino et al. (eds.) ESORICS. LNCS 1146, pp. 351–364. Springer (1996)
22.
Neff, A.C.: A verifiable secret shuffle and its application to e-voting. In: ACM Conference on Computer and Communications Security, pp. 116–125 (2001)
23.
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)CrossRefMATH
24.
Nguyen, L., Safavi-Naini, R., Kurosawa, K.: Verifiable shuffles: a formal model and a Paillier-based efficient construction with provable security. In: Jakobsson et al. (eds.) ACNS. LNCS 3089, pp. 61–75. Springer (2004)
25.
Paillier, P.: Public-key cryptosystems based on composite degree residuosity classes. In: Stern (ed.) EUROCRYPT. LNCS 1592, pp. 223–238. Springer (1999)
26.
Rabin, T., Ben-Or, M.: Verifiable secret sharing and multiparty protocols with honest majority (extended abstract). In: Johnson (ed.) STOC, pp. 73–85. ACM (1989)
27.
Ryan, P.Y.A., Bismark, D., Heather, J., Schneider, S., Xia, Z.: Prêt à voter: a voter-verifiable voting system. IEEE Trans. Inf. Forensics Secur. 4(4), 662–673 (2009)CrossRef
28.
Roscoe, A.W., Goldsmith, M.: The perfect spy for model-checking crypto-protocols. In: Proceedings of DIMACS workshop on the design and formal verification of crypto-protocols (1997)
29.
Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: CSFW, pp. 98–107. IEEE Computer Society (1995)
30.
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1998)
31.
32.
Roscoe, A.W., Ryan, P., Schneider, S., Goldsmith, M., Lowe, G.: The Modelling and Analysis of Security Protocols. Addison-Wesley, Reading (2001)
33.
Schneider, S.: Concurrent and Real Time Systems: The CSP Approach, 1st edn. Wiley, New York (1999)
34.
Sako, K., Kilian, J.: Receipt-free mix-type voting scheme—a practical solution to the implementation of a voting booth. In: Guillou, Quisquater (eds.) EUROCRYPT. LNCS 921, pp. 393–403. Springer (1995)
35.
Stathakidis, E., Williams, D.M., Heather, J.: Verifying a mix net in CSP. In: Proceedings of the 13th International Workshop on Automated Verification of Critical Systems (AVoCS 2013). Electronic Communications of the EASST 66. European Association of Software Science and Technology (2013)
36.
Wikström, D., Groth, J.: An adaptively secure mix-net without erasures. In: Bugliesi et al. (eds.) ICALP (2). LNCS 4052, pp. 276–287. Springer (2006)
37.
Wikström, D.: A universally composable mix-net. In: Naor (ed.) TCC. LNCS 2951, pp. 317–335. Springer (2004)
38.
Wikström, D.: On the security of mix-nets and hierarchical group signatures. PhD thesis, KTH, Sweden (2005)
39.
Wikström, D.: A commitment-consistent proof of a huffle. In: Boyd, Nieto (eds.) Information Security and Privacy, 14th Australasian Conference, ACISP 2009, Brisbane, Australia, 1–3 July 2009, Proceedings. LNCS 5594, pp. 407–421. Springer (2009)
40.
41.
Williams, D.M., de Ruiter, J., Fokkink, W.: Model checking under fairness in ProB and its application to fair exchange protocols. In: Roychoudhury. D’Souza (eds.) ICTAC. LNCS 7521, pp. 168–182. Springer (2012)
42.
Yao, A.C.-C.: Protocols for secure computations (extended abstract). In: FOCS, pp. 160–164. IEEE Computer Society (1982)
Metadata
Title
Constructing and verifying a robust Mix Net using CSP
Authors
Efstathios Stathakidis
David M. Williams
James Heather
Publication date
17-06-2015
Publisher
Springer Berlin Heidelberg
Published in
Software and Systems Modeling / Issue 4/2016
Print ISSN: 1619-1366
Electronic ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-015-0474-0

Other articles of this Issue 4/2016

Software and Systems Modeling 4/2016 Go to the issue

Theme Section Paper

Knowledge-based construction of distributed constrained systems

Theme Section Paper

Automated anonymity verification of the ThreeBallot and VAV voting systems

Regular Paper

Supporting different process views through a Shared Process Model

Guest Editorial

Theme issue on Integrated Formal Methods

Theme Section Paper

Model-checking software library API usage rules

Theme Section Paper

A formal verification framework for static analysis

Premium Partner

    Image Credits