Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Meeting Requirements Imposed by Secure Software Development Standards and Still Remaining Agile Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Automated Cryptographic Analysis of the Pedersen Commitment Scheme

verfasst von : Roberto Metere, Changyu Dong

Erschienen in: Computer Network Security

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Aiming for strong security assurance, recently there has been an increasing interest in formal verification of cryptographic constructions. This paper presents a mechanised formal verification of the popular Pedersen commitment protocol, proving its security properties of correctness, perfect hiding, and computational binding. To formally verify the protocol, we extended the theory of EasyCrypt, a framework which allows for reasoning in the computational model, to support the discrete logarithm and an abstraction of commitment protocols. Commitments are building blocks of many cryptographic constructions, for example, verifiable secret sharing, zero-knowledge proofs, and e-voting. Our work paves the way for the verification of those more complex constructions.

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 "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

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
Vorheriges Kapitel HEPPA: Highly Efficient Privacy Preserving Authentication for ITS
Nächstes Kapitel Steganalysis Based on Statistical Properties of the Encrypted Messages
Literatur
1.
2.
Abadi, M.: Explicit communication revisited: two new attacks on authentication protocols. IEEE Trans. Software Eng. 23(3), 185–186 (1997)CrossRef
3.
Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Sci. Comput. Program. 58(1–2), 3–27 (2005)MathSciNetCrossRefMATH
4.
Ambrona, M., Barthe, G., Schmidt, B.: Automated unbounded analysis of cryptographic constructions in the generic group model. In: Fischlin, M., Coron, J.-S. (eds.) EUROCRYPT 2016. LNCS, vol. 9666, pp. 822–851. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49896-5_​29 CrossRef
5.
Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28756-5_​19 CrossRef
6.
7.
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proceedings of the 10th ACM Conference on Computer and Communications Security (CCS), pp. 220–230. ACM (2003)
8.
Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: Proceedings of the 21st ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 609–620. ACM (2014)
9.
Barthe, G., Danezis, G., Grégoire, B., Kunz, C., Zanella-Beguelin, S.: Verified computational differential privacy with applications to smart metering. In: 2013 IEEE 26th Computer Security Foundations Symposium, pp. 287–301. IEEE (2013)
10.
Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146–166. Springer, Cham (2014). doi:10.​1007/​978-3-319-10082-1_​6 CrossRef
11.
Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22792-9_​5 CrossRef
12.
Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. ACM SIGPLAN Not. 44(1), 90–101 (2009)CrossRefMATH
13.
Barthe, G., Hedin, D., Béguelin, S.Z., Grégoire, B., Heraud, S.: A machine-checked formalization of Sigma-protocols. In: 2010 23rd IEEE Computer Security Foundations Symposium (CSF), pp. 246–260. IEEE (2010)
14.
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5(4), 193–207 (2008)CrossRef
15.
Blanchet, B., et al.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, vol. 1, pp. 82–96 (2001)
16.
Bouillaguet, C., Derbez, P., Fouque, P.-A.: Automatic search of attacks on round-reduced AES and applications. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 169–187. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22792-9_​10 CrossRef
17.
Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 326–341. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45789-5_​24 CrossRef
18.
Cremers, C., Horvat, M., Scott, S., van der Merwe, T.: Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication. In: 2016 IEEE Symposium on Security and Privacy (SP), pp. 470–485. IEEE (2016)
19.
20.
Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proceeding of SecRet 2007 (2007)
21.
22.
23.
Katz, J., Lindell, Y.: Introduction to Modern Cryptography. CRC Press, Boca Raton (2014)MATH
24.
Kemmerer, R.A.: Analyzing encryption protocols using formal verification techniques. IEEE J. Sel. Areas Commun. 7(4), 448–457 (1989)CrossRef
25.
Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inform. Process. Lett. 56(3), 131–133 (1995)CrossRefMATH
26.
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996). doi:10.​1007/​3-540-61042-1_​43 CrossRef
27.
Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Programm. 26(2), 113–131 (1996)CrossRefMATH
28.
Meier, S., Cremers, C., Basin, D.: Strong invariants for the efficient construction of machine-checked protocol security proofs. In: 2010 23rd IEEE Computer Security Foundations Symposium (CSF), pp. 231–245. IEEE (2010)
29.
Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Mur\(\varphi \). In: 1997 IEEE Symposium on Security and Privacy, Proceedings, pp. 141–151. IEEE (1997)
30.
31.
Pedersen, T.P.: Non-interactive and information-theoretic secure verifiable secret sharing. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 129–140. Springer, Heidelberg (1992). doi:10.​1007/​3-540-46766-1_​9
32.
Ramsdell, J.D., Guttman, J.D.: CPSA: A cryptographic protocol shapes analyzer. In: Hackage. The MITRE Corporation, vol. 2(009) (2009)
33.
Ryan, P., Schneider, S.A.: The Modelling and Analysis of Security Protocols: The CSP Approach. Addison-Wesley Professional, Reading (2001)
34.
Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), pp. 78–94. IEEE (2012)
35.
Schoenmakers, B.: A simple publicly verifiable secret sharing scheme and its application to electronic voting. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 148–164. Springer, Heidelberg (1999). doi:10.​1007/​3-540-48405-1_​10
36.
Song, D.X., Berezin, S., Perrig, A.: Athena: a novel approach to efficient automatic security protocol analysis. J. Comput. Secur. 9(1–2), 47–74 (2001)CrossRef
37.
Metadaten
Titel
Automated Cryptographic Analysis of the Pedersen Commitment Scheme
verfasst von
Roberto Metere
Changyu Dong
Copyright-Jahr
2017
Buch
Computer Network Security

Print ISBN: 978-3-319-65126-2

Electronic ISBN: 978-3-319-65127-9

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-65127-9_22