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
Published in:
Meeting Requirements Imposed by Secure Software Development Standards and Still Remaining Agile Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Automated Cryptographic Analysis of the Pedersen Commitment Scheme

Authors : Roberto Metere, Changyu Dong

Published in: Computer Network Security

Publisher: Springer International Publishing

Log in

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

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.

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

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
previous chapter HEPPA: Highly Efficient Privacy Preserving Authentication for ITS
next chapter Steganalysis Based on Statistical Properties of the Encrypted Messages
Literature
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.
Metadata
Title
Automated Cryptographic Analysis of the Pedersen Commitment Scheme
Authors
Roberto Metere
Changyu Dong
Copyright Year
2017
Book
Computer Network Security

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

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

Copyright Year: 2017

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

Premium Partner

    Image Credits