{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,7]],"date-time":"2026-04-07T16:32:25Z","timestamp":1775579545561,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319651262","type":"print"},{"value":"9783319651279","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-65127-9_22","type":"book-chapter","created":{"date-parts":[[2017,8,5]],"date-time":"2017-08-05T07:35:53Z","timestamp":1501918553000},"page":"275-287","source":"Crossref","is-referenced-by-count":24,"title":["Automated Cryptographic Analysis of the Pedersen Commitment Scheme"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Metere","sequence":"first","affiliation":[]},{"given":"Changyu","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,6]]},"reference":[{"key":"22_CR1","unstructured":"EasyCrypt Reference Manual. https:\/\/www.easycrypt.info\/documentation\/refman.pdf . Accessed Feb 2017"},{"issue":"3","key":"22_CR2","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1109\/32.585505","volume":"23","author":"M Abadi","year":"1997","unstructured":"Abadi, M.: Explicit communication revisited: two new attacks on authentication protocols. IEEE Trans. Software Eng. 23(3), 185\u2013186 (1997)","journal-title":"IEEE Trans. Software Eng."},{"issue":"1\u20132","key":"22_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2005.02.002","volume":"58","author":"M Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Sci. Comput. Program. 58(1\u20132), 3\u201327 (2005)","journal-title":"Sci. Comput. Program."},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"822","DOI":"10.1007\/978-3-662-49896-5_29","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2016","author":"M Ambrona","year":"2016","unstructured":"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\u2013851. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49896-5_29"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267\u2013282. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_19"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1007\/978-3-540-30227-8_68","volume-title":"Logics in Artificial Intelligence","author":"A Armando","year":"2004","unstructured":"Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS, vol. 3229, pp. 730\u2013733. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30227-8_68"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"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\u2013230. ACM (2003)","DOI":"10.1145\/948109.948140"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"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\u2013620. ACM (2014)","DOI":"10.1145\/2660267.2660276"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Barthe, G., Danezis, G., Gr\u00e9goire, 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\u2013301. IEEE (2013)","DOI":"10.1109\/CSF.2013.26"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, 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\u2013166. Springer, Cham (2014). doi: 10.1007\/978-3-319-10082-1_6"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22792-9_5"},{"issue":"1","key":"22_CR12","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/1594834.1480894","volume":"44","author":"G Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. ACM SIGPLAN Not. 44(1), 90\u2013101 (2009)","journal-title":"ACM SIGPLAN Not."},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hedin, D., B\u00e9guelin, S.Z., Gr\u00e9goire, B., Heraud, S.: A machine-checked formalization of Sigma-protocols. In: 2010 23rd IEEE Computer Security Foundations Symposium (CSF), pp. 246\u2013260. IEEE (2010)","DOI":"10.1109\/CSF.2010.24"},{"issue":"4","key":"22_CR14","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1109\/TDSC.2007.1005","volume":"5","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5(4), 193\u2013207 (2008)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, vol. 1, pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-22792-9_10","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"C Bouillaguet","year":"2011","unstructured":"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\u2013187. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22792-9_10"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-45789-5_24","volume-title":"Static Analysis","author":"R Corin","year":"2002","unstructured":"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\u2013341. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45789-5_24"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"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\u2013485. IEEE (2016)","DOI":"10.1109\/SP.2016.35"},{"issue":"2","key":"22_CR19","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proceeding of SecRet 2007 (2007)","DOI":"10.1016\/j.entcs.2007.02.053"},{"issue":"1","key":"22_CR21","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1137\/S0097539791220688","volume":"25","author":"O Goldreich","year":"1996","unstructured":"Goldreich, O., Krawczyk, H.: On the composition of zero-knowledge proof systems. SIAM J. Comput. 25(1), 169\u2013192 (1996)","journal-title":"SIAM J. Comput."},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"977","DOI":"10.1007\/3-540-45591-4_134","volume-title":"Parallel and Distributed Processing","author":"J Goubault-Larrecq","year":"2000","unstructured":"Goubault-Larrecq, J.: A method for automatic cryptographic protocol verification. In: Rolim, J. (ed.) IPDPS 2000. LNCS, vol. 1800, pp. 977\u2013984. Springer, Heidelberg (2000). doi: 10.1007\/3-540-45591-4_134"},{"key":"22_CR23","doi-asserted-by":"crossref","DOI":"10.1201\/b17668","volume-title":"Introduction to Modern Cryptography","author":"J Katz","year":"2014","unstructured":"Katz, J., Lindell, Y.: Introduction to Modern Cryptography. CRC Press, Boca Raton (2014)"},{"issue":"4","key":"22_CR24","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/49.17707","volume":"7","author":"RA Kemmerer","year":"1989","unstructured":"Kemmerer, R.A.: Analyzing encryption protocols using formal verification techniques. IEEE J. Sel. Areas Commun. 7(4), 448\u2013457 (1989)","journal-title":"IEEE J. Sel. Areas Commun."},{"issue":"3","key":"22_CR25","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inform. Process. Lett. 56(3), 131\u2013133 (1995)","journal-title":"Inform. Process. Lett."},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Lowe","year":"1996","unstructured":"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\u2013166. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61042-1_43"},{"issue":"2","key":"22_CR27","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Programm. 26(2), 113\u2013131 (1996)","journal-title":"J. Logic Programm."},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"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\u2013245. IEEE (2010)","DOI":"10.1109\/CSF.2010.23"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"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\u2013151. IEEE (1997)","DOI":"10.1109\/SECPRI.1997.601329"},{"issue":"2","key":"22_CR30","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF00196774","volume":"4","author":"M Naor","year":"1991","unstructured":"Naor, M.: Bit commitment using pseudorandomness. J. Cryptology 4(2), 151\u2013158 (1991)","journal-title":"J. Cryptology"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-46766-1_9","volume-title":"Advances in Cryptology \u2014 CRYPTO 1991","author":"TP Pedersen","year":"1992","unstructured":"Pedersen, T.P.: Non-interactive and information-theoretic secure verifiable secret sharing. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 129\u2013140. Springer, Heidelberg (1992). doi: 10.1007\/3-540-46766-1_9"},{"key":"22_CR32","unstructured":"Ramsdell, J.D., Guttman, J.D.: CPSA: A cryptographic protocol shapes analyzer. In: Hackage. The MITRE Corporation, vol. 2(009) (2009)"},{"key":"22_CR33","volume-title":"The Modelling and Analysis of Security Protocols: The CSP Approach","author":"P Ryan","year":"2001","unstructured":"Ryan, P., Schneider, S.A.: The Modelling and Analysis of Security Protocols: The CSP Approach. Addison-Wesley Professional, Reading (2001)"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"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\u201394. IEEE (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"22_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-48405-1_10","volume-title":"Advances in Cryptology \u2014 CRYPTO 1999","author":"B Schoenmakers","year":"1999","unstructured":"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\u2013164. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48405-1_10"},{"issue":"1\u20132","key":"22_CR36","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"DX Song","year":"2001","unstructured":"Song, D.X., Berezin, S., Perrig, A.: Athena: a novel approach to efficient automatic security protocol analysis. J. Comput. Secur. 9(1\u20132), 47\u201374 (2001)","journal-title":"J. Comput. Secur."},{"key":"22_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M Turuani","year":"2006","unstructured":"Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277\u2013286. Springer, Heidelberg (2006). doi: 10.1007\/11805618_21"}],"container-title":["Lecture Notes in Computer Science","Computer Network Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-65127-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,14]],"date-time":"2020-10-14T08:01:48Z","timestamp":1602662508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-65127-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319651262","9783319651279"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-65127-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}