nach oben

Software and Systems Modeling

Erschienen in:

17.06.2015 | Theme Section Paper

Constructing and verifying a robust Mix Net using CSP

verfasst von: Efstathios Stathakidis, David M. Williams, James Heather

Erschienen in: Software and Systems Modeling | Ausgabe 4/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Automated anonymity verification of the ThreeBallot and VAV voting systems

Nächster Artikel The Unit-B method: refinement guided by progress concerns

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

The complete script can be found at http://www.tvsproject.org/csp/SoSyM_sec4.csp.

The complete script can be found at http://www.tvsproject.org/csp/SoSyM_sec5.csp.

Adida, B.: Helios: Web-based open-audit voting. In: Proceedings of the 17th USENIX Security Symposium (Security ’08) (2008)

Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, Schmidt (eds.) POPL, pp. 104–115. ACM (2001)

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)

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)

Canetti, R.: Universally Composable security: a new paradigm for cryptographic protocols. In: FOCS, pp. 136–145. IEEE Computer Society (2001)

Chaum, D., Crépeau, C., Damgård, I.: Multiparty unconditionally secure protocols (extended abstract). In: Simon (ed.) STOC, pp. 11–19. ACM (1988)

Chaum, D.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24(2), 84–88 (1981)CrossRef

Chaum, D., Pedersen, T.P.: Wallet databases with observers. In: Advances in Cryptology, CRYPTO ’92, pp. 89–105. Springer (1992)

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.

Dolev, D., Yao, A.C.-C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983)MathSciNetCrossRefMATH

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.

Roscoe, A.: Understanding Concurrent Systems, 1st edn. Springer, New York (2010)CrossRefMATH

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.

Wikström, D.: Verificatum. (2014). http://www.verificatum.org

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)

Titel: Constructing and verifying a robust Mix Net using CSP
verfasst von: Efstathios Stathakidis
David M. Williams
James Heather
Publikationsdatum: 17.06.2015
Verlag: Springer Berlin Heidelberg
Erschienen in: Software and Systems Modeling / Ausgabe 4/2016
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI: https://doi.org/10.1007/s10270-015-0474-0

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2016

Model-checking software library API usage rules

How to write a successful SoSyM submission

Contract-based verification of discrete-time multi-rate Simulink models

Supporting different process views through a Shared Process Model

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Theme issue on Integrated Formal Methods