{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T20:43:20Z","timestamp":1773348200282,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":57,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642154966","type":"print"},{"value":"9783642154973","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15497-3_10","type":"book-chapter","created":{"date-parts":[[2010,9,1]],"date-time":"2010-09-01T10:51:46Z","timestamp":1283338306000},"page":"151-167","source":"Crossref","is-referenced-by-count":24,"title":["A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on \u03a3-Protocols"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[]},{"given":"Endre","family":"Bangerter","sequence":"additional","affiliation":[]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Krenn","sequence":"additional","affiliation":[]},{"given":"Ahmad-Reza","family":"Sadeghi","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Almeida, J., Bangerter, E., Barbosa, M., Krenn, S., Sadeghi, A.R., Schneider, T.: A certifying compiler for zero-knowledge proofs of knowledge based on \u03a3-protocols. Cryptology ePrint Archive, Report 2010\/339 (2010)","DOI":"10.1007\/978-3-642-15497-3_10"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-48071-4_28","volume-title":"Advances in Cryptology - CRYPTO \u201992","author":"M. Bellare","year":"1993","unstructured":"Bellare, M., Goldreich, O.: On defining proofs of knowledge. In: Brickell, E.F. (ed.) CRYPTO 1992. LNCS, vol.\u00a0740, pp. 390\u2013420. Springer, Heidelberg (1993)"},{"key":"10_CR3","first-page":"517","volume":"25","author":"W. Han","year":"2009","unstructured":"Han, W., Chen, K., Zheng, D.: Receipt-freeness for Groth e-voting schemes. Journal of Information Science and Engineering\u00a025, 517\u2013530 (2009)","journal-title":"Journal of Information Science and Engineering"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/s00500-009-0449-6","volume":"14","author":"H. Kikuchi","year":"2010","unstructured":"Kikuchi, H., Nagai, K., Ogata, W., Nishigaki, M.: Privacy-preserving similarity evaluation and application to remote biometrics authentication. Soft Computing\u00a014, 529\u2013536 (2010)","journal-title":"Soft Computing"},{"key":"10_CR5","unstructured":"Camenisch, J.: Group Signature Schemes and Payment Systems Based on the Discrete Logarithm Problem. PhD thesis, ETH Zurich, Konstanz (1998)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-48910-X_8","volume-title":"Advances in Cryptology - EUROCRYPT \u201999","author":"J. Camenisch","year":"1999","unstructured":"Camenisch, J., Michels, M.: Proving in zero-knowledge that a number is the product of two safe primes. In: Stern, J. (ed.) EUROCRYPT 1999. LNCS, vol.\u00a01592, pp. 107\u2013122. Springer, Heidelberg (1999)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-48329-2_26","volume-title":"CRYPTO 1993","author":"S. Brands","year":"1994","unstructured":"Brands, S.: Untraceable off-line cash in wallet with observers. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol.\u00a0773, pp. 302\u2013318. Springer, Heidelberg (1994)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-85855-3_2","volume-title":"Security and Cryptography for Networks","author":"Y. Lindell","year":"2008","unstructured":"Lindell, Y., Pinkas, B., Smart, N.P.: Implementing two-party computation efficiently with security against malicious adversaries. In: Ostrovsky, R., De Prisco, R., Visconti, I. (eds.) SCN 2008. LNCS, vol.\u00a05229, pp. 2\u201320. Springer, Heidelberg (2008)"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1145\/1030083.1030103","volume-title":"ACM CCS 2004","author":"E. Brickell","year":"2004","unstructured":"Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: ACM CCS 2004, pp. 132\u2013145. ACM Press, New York (2004)"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/586110.586114","volume-title":"ACM CCS 2002","author":"J. Camenisch","year":"2002","unstructured":"Camenisch, J., Herreweghen, E.V.: Design and implementation of the idemix anonymous credential system. In: ACM CCS 2002, pp. 21\u201330. ACM Press, New York (2002)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/11745853_3","volume-title":"Public Key Cryptography - PKC 2006","author":"S. Kunz-Jacques","year":"2006","unstructured":"Kunz-Jacques, S., Martinet, G., Poupard, G., Stern, J.: Cryptanalysis of an efficient proof of knowledge of discrete logarithm. In: Yung, M., Dodis, Y., Kiayias, A., Malkin, T.G. (eds.) PKC 2006. LNCS, vol.\u00a03958, pp. 27\u201343. Springer, Heidelberg (2006)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-30580-4_11","volume-title":"Public Key Cryptography - PKC 2005","author":"E. Bangerter","year":"2005","unstructured":"Bangerter, E., Camenisch, J., Maurer, U.: Efficient proofs of knowledge of discrete logarithms and representations in groups with hidden order. In: Vaudenay, S. (ed.) PKC 2005. LNCS, vol.\u00a03386, pp. 154\u2013171. Springer, Heidelberg (2005)"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BF00196725","volume":"4","author":"C. Schnorr","year":"1991","unstructured":"Schnorr, C.: Efficient signature generation by smart cards. Journal of Cryptology\u00a04, 161\u2013174 (1991)","journal-title":"Journal of Cryptology"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/3-540-46766-1_9","volume-title":"Advances in Cryptology - CRYPTO \u201991","author":"T.P. Pedersen","year":"1992","unstructured":"Pedersen, T.P.: Non-interactive and information-theoretic secure verifiable secret sharing. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol.\u00a0576, pp. 129\u2013140. Springer, Heidelberg (1992)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-44987-6_7","volume-title":"Advances in Cryptology - EUROCRYPT 2001","author":"J. Camenisch","year":"2001","unstructured":"Camenisch, J., Lysyanskaya, A.: An efficient system for non-transferable anonymous credentials with optional anonymity revocation. In: Pfitzmann, B. (ed.) EUROCRYPT 2001. LNCS, vol.\u00a02045, pp. 93\u2013118. Springer, Heidelberg (2001)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-40061-5_26","volume-title":"Advances in Cryptology - ASIACRYPT 2003","author":"H. Lipmaa","year":"2003","unstructured":"Lipmaa, H.: On diophantine complexity and statistical zeroknowledge arguments. In: Laih, C.-S. (ed.) ASIACRYPT 2003. LNCS, vol.\u00a02894, pp. 398\u2013415. Springer, Heidelberg (2003)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle","year":"1994","unstructured":"Paulson, L.: Isabelle: a Generic Theorem Prover. Volume 828 of LNCS. Springer (1994)"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1145\/948109.948139","volume-title":"ACM CCS 2003","author":"P. MacKenzie","year":"2003","unstructured":"MacKenzie, P., Oprea, A., Reiter, M.K.: Automatic generation of two-party computations. In: ACM CCS 2003, pp. 210\u2013219. ACM, New York (2003)"},{"key":"10_CR19","unstructured":"Malkhi, D., Nisan, N., Pinkas, B., Sella, Y.: Fairplay \u2014 a secure two-party computation system. In: USENIX Security 2004 (2004)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-00468-1_10","volume-title":"Public Key Cryptography \u2013 PKC 2009","author":"I. Damg\u00e5rd","year":"2009","unstructured":"Damg\u00e5rd, I., Geisler, M., Kr\u00f8igaard, M., Nielsen, J.B.: Asynchronous multiparty computation: Theory and implementation. In: Jarecki, S., Tsudik, G. (eds.) Public Key Cryptography \u2013 PKC 2009. LNCS, vol.\u00a05443, pp. 160\u2013179. Springer, Heidelberg (2009)"},{"key":"10_CR21","unstructured":"Briner, T.: Compiler for zero-knowledge proof-of-knowledge protocols. Master\u2019s thesis, ETH Zurich (2004)"},{"key":"10_CR22","unstructured":"Camenisch, J., Rohe, M., Sadeghi, A.R.: Sokrates - a compiler framework for zero-knowledge protocols. In: WEWoRC 2005 (2005)"},{"key":"10_CR23","unstructured":"Bangerter, E., Camenisch, J., Krenn, S., Sadeghi, A.R., Schneider, T.: Automatic generation of sound zero-knowledge protocols. Cryptology ePrint Archive, Report 2008\/471, Poster Session of EUROCRYPT 2009 (2008)"},{"key":"10_CR24","unstructured":"Bangerter, E., Briner, T., Heneka, W., Krenn, S., Sadeghi, A.R., Schneider, T.: Automatic generation of \u03a3-protocols. In: EuroPKI 2009 (to appear, 2009)"},{"key":"10_CR25","unstructured":"Bangerter, E., Krenn, S., Sadeghi, A.R., Schneider, T., Tsay, J.K.: On the design and implementation of efficient zero-knowledge proofs of knowledge. In: Software Performance Enhancements for Encryption and Decryption and Cryptographic Compilers \u2013 SPEED-CC 2009, October 12-13 (2009)"},{"key":"10_CR26","unstructured":"Meiklejohn, S., Erway, C., K\u00fcp\u00e7\u00fc, A., Hinkle, T., Lysyanskaya, A.: ZKPDL: A language-based system for efficient zero-knowledge proofs and electronic cash. In: USENIX 10 (to appear, 2010)"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/359340.359342","volume":"21","author":"R. Rivest","year":"1978","unstructured":"Rivest, R., Shamir, A., Adleman, L.: A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM\u00a021, 120\u2013126 (1978)","journal-title":"Communications of the ACM"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1109\/SP.2008.23","volume-title":"IEEE Symposium on Security and Privacy \u2013 SP 2008","author":"M. Backes","year":"2008","unstructured":"Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: IEEE Symposium on Security and Privacy \u2013 SP 2008, pp. 202\u2013215. IEEE, Los Alamitos (2008)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-10622-4_11","volume-title":"Advances in Computer Science - ASIAN 2009. Information Security and Privacy","author":"A. Baskar","year":"2009","unstructured":"Baskar, A., Ramanujam, R., Suresh, S.P.: A dolev-yao model for zero knowledge. In: Datta, A. (ed.) ASIAN 2009. LNCS, vol.\u00a05913, pp. 137\u2013146. Springer, Heidelberg (2009)"},{"key":"10_CR30","unstructured":"Blanchet, B.: ProVerif: Cryptographic protocol verifier in the formal model (2010)"},{"key":"10_CR31","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/1455770.1455816","volume-title":"ACM CCS 2008","author":"M. Backes","year":"2008","unstructured":"Backes, M., Hritcu, C., Maffei, M.: Type-checking zero-knowledge. In: ACM CCS 2008, pp. 357\u2013370. ACM, New York (2008)"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Backes, M., Unruh, D.: Computational soundness of symbolic zero-knowledge proofs against active attackers. In: IEEE Computer Security Foundations Symposium - CSF 2008, 255\u2013269 Preprint on IACR ePrint 2008\/152 (2008)","DOI":"10.1109\/CSF.2008.20"},{"key":"10_CR33","volume-title":"23rd IEEE Computer Security Foundations Symposium, CSF 2010","author":"G. Barthe","year":"2010","unstructured":"Barthe, G., Hedin, D., Zanella B\u00e9guelin, S., Gr\u00e9goire, B., Heraud, S.: A machine-checked formalization of \u03a3-protocols. In: 23rd IEEE Computer Security Foundations Symposium, CSF 2010, IEEE, Los Alamitos (2010)"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: ACM SIGPLAN-SIGACT POPL 2009, pp. 90\u2013101 (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-540-30579-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C\u00a0code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 363\u2013379. Springer, Heidelberg (2005)"},{"issue":"1","key":"10_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1452044.1452049","volume":"31","author":"K. Bhargavan","year":"2008","unstructured":"Bhargavan, K., Fournet, C., Gordon, A., Tse, S.: Verified interoperable implementations of security protocols. ACM Trans. Program. Lang. Syst.\u00a031(1), 1\u201361 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR37","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/1455770.1455828","volume-title":"ACM CCS 2008","author":"K. Bhargavan","year":"2008","unstructured":"Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: ACM CCS 2008, pp. 459\u2013468. ACM, New York (2008)"},{"key":"10_CR38","first-page":"82","volume-title":"Workshop on Computer Security Foundations \u2013 CSFW 2001","author":"B. Blanchet","year":"2001","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Workshop on Computer Security Foundations \u2013 CSFW 2001, p. 82. IEEE, Los Alamitos (2001)"},{"key":"10_CR39","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1109\/SP.2006.1","volume-title":"IEEE Symposium on Security and Privacy \u2013 SP 2006","author":"B. Blanchet","year":"2006","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy \u2013 SP 2006, pp. 140\u2013154. IEEE, Los Alamitos (2006)"},{"key":"10_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/BFb0052252","volume-title":"Advances in Cryptology - CRYPTO \u201997","author":"J. Camenisch","year":"1997","unstructured":"Camenisch, J., Stadler, M.: Efficient group signature schemes for large groups (extended abstract). In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol.\u00a01294, pp. 410\u2013424. Springer, Heidelberg (1997)"},{"key":"10_CR41","unstructured":"Cramer, R.: Modular Design of Secure yet Practical Cryptographic Protocols. PhD thesis, CWI and University of Amsterdam (1997)"},{"key":"10_CR42","unstructured":"Damg\u00e5rd, I.: On \u03a3-protocols, Lecture on Cryptologic Protocol Theory, Faculty of Science, University of Aarhus (2004)"},{"key":"10_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/0-387-34799-2_16","volume-title":"Advances in Cryptology - CRYPTO \u201988","author":"L. Guillou","year":"1990","unstructured":"Guillou, L., Quisquater, J.J.: A \u201cparadoxical\u201d identity-based signature scheme resulting from zero-knowledge. In: Goldwasser, S. (ed.) CRYPTO 1988. LNCS, vol.\u00a0403, pp. 216\u2013231. Springer, Heidelberg (1990)"},{"key":"10_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/BFb0055717","volume-title":"Advances in Cryptology - CRYPTO \u201998","author":"R. Cramer","year":"1998","unstructured":"Cramer, R., Shoup, V.: A practical public key cryptosystem provably secure against adaptive chosen ciphertext attack. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol.\u00a01462, pp. 13\u201325. Springer, Heidelberg (1998)"},{"key":"10_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/BFb0052225","volume-title":"Advances in Cryptology - CRYPTO \u201997","author":"E. Fujisaki","year":"1997","unstructured":"Fujisaki, E., Okamoto, T.: Statistical zero knowledge protocols to prove modular polynomial relations. In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol.\u00a01294, pp. 16\u201330. Springer, Heidelberg (1997)"},{"key":"10_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-36178-2_8","volume-title":"Advances in Cryptology - ASIACRYPT 2002","author":"I. Damg\u00e5rd","year":"2002","unstructured":"Damg\u00e5rd, I., Fujisaki, E.: A statistically-hiding integer commitment scheme based on groups with hidden order. In: Zheng, Y. (ed.) ASIACRYPT 2002. LNCS, vol.\u00a02501, pp. 77\u201385. Springer, Heidelberg (2002)"},{"key":"10_CR47","unstructured":"Bangerter, E.: Efficient Zero-Knowledge Proofs of Knowledge for Homomorphisms. PhD thesis, Ruhr-University Bochum (2005)"},{"key":"10_CR48","unstructured":"Smart, N.P. (ed.): Final Report on Unified Theoretical Framework of Efficient Zero-Knowledge Proofs of Knowledge. CACE project deliverable (2009)"},{"key":"10_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/3-540-48658-5_19","volume-title":"Advances in Cryptology - CRYPTO \u201994","author":"R. Cramer","year":"1994","unstructured":"Cramer, R., Damg\u00e5rd, I., Schoenmakers, B.: Proofs of partial knowledge and simplified design of witness hiding protocols. In: Desmedt, Y.G. (ed.) CRYPTO 1994. LNCS, vol.\u00a0839, pp. 174\u2013187. Springer, Heidelberg (1994)"},{"key":"10_CR50","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1145\/359168.359176","volume":"22","author":"A. Shamir","year":"1979","unstructured":"Shamir, A.: How to share a secret. Communications of the ACM\u00a022, 612\u2013613 (1979)","journal-title":"Communications of the ACM"},{"key":"10_CR51","series-title":"Lecture Notes in Computer Science","first-page":"186","volume-title":"Advances in Cryptology - CRYPTO \u201986","author":"A. Fiat","year":"1987","unstructured":"Fiat, A., Shamir, A.: How to prove yourself: practical solutions to identification and signature problems. In: Odlyzko, A.M. (ed.) CRYPTO 1986. LNCS, vol.\u00a0263, pp. 186\u2013194. Springer, Heidelberg (1987)"},{"key":"10_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-69053-0_22","volume-title":"Advances in Cryptology - EUROCRYPT \u201997","author":"S. Brands","year":"1997","unstructured":"Brands, S.: Rapid demonstration of linear relations connected by boolean operators. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol.\u00a01233, pp. 318\u2013333. Springer, Heidelberg (1997)"},{"key":"10_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-45811-5_21","volume-title":"Information Security","author":"E. Bresson","year":"2002","unstructured":"Bresson, E., Stern, J.: Proofs of knowledge for non-monotone discrete-log formulae and applications. In: Chan, A.H., Gligor, V.D. (eds.) ISC 2002. LNCS, vol.\u00a02433, pp. 272\u2013288. Springer, Heidelberg (2002)"},{"key":"10_CR54","unstructured":"Granlund, T.: The GNU MP Bignum Library (2010), \n                    \n                      http:\/\/gmplib.org\/"},{"key":"10_CR55","unstructured":"Nipkow, T., Paulson, L.: Isabelle (2010), \n                    \n                      http:\/\/isabelle.in.tun.de"},{"key":"10_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"10_CR57","unstructured":"Ballarin, C., Kamm\u00fcller, F., Paulson, L.: The Isabelle\/HOL Algebra Library (2008), \n                    \n                      http:\/\/isabelle.in.tum.de\/library\/HOL\/HOL-Algebra\/document.pdf"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2010"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15497-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T20:29:45Z","timestamp":1559507385000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15497-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642154966","9783642154973"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15497-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}