{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T15:03:22Z","timestamp":1794495802562,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466650","type":"print"},{"value":"9783662466667","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-662-46666-7_4","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:57:12Z","timestamp":1427741832000},"page":"53-72","source":"Crossref","is-referenced-by-count":58,"title":["The Foundational Cryptography Framework"],"prefix":"10.1007","author":[{"given":"Adam","family":"Petcher","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-44929-9_1","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"M. Abadi","year":"2000","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 3\u201322. Springer, Heidelberg (2000), \n                      \n                        http:\/\/dl.acm.org\/citation.cfm?id=647318.723498"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75670-5_10","volume-title":"Provable Security","author":"R. Affeldt","year":"2007","unstructured":"Affeldt, R., Tanaka, M., Marti, N.: Formal proof of provable security by game-playing in a proof assistant. In: Susilo, W., Liu, J.K., Mu, Y. (eds.) ProvSec 2007. LNCS, vol.\u00a04784, pp. 151\u2013168. Springer, Heidelberg (2007), \n                      \n                        http:\/\/dl.acm.org\/citation.cfm?id=1779394.1779408"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"1217","DOI":"10.1145\/2508859.2516652","volume-title":"Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013","author":"J.B. Almeida","year":"2013","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013, pp. 1217\u20131230. ACM, New York (2013), \n                      \n                        http:\/\/doi.acm.org\/10.1145\/2508859.2516652"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Backes, M., Unruh, D.: Computational soundness of symbolic zero-knowledge proofs against active attackers. In: 21st IEEE Computer Security Foundations Symposium, CSF 2008, pp. 255\u2013269 (June 2008), preprint on IACR ePrint 2008\/152","DOI":"10.1109\/CSF.2008.20"},{"key":"4_CR5","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.\u00a06841, pp. 71\u201390. Springer, Heidelberg (2011)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90\u2013101. ACM (2009), \n                      \n                        http:\/\/dx.doi.org\/10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"4_CR7","unstructured":"Bellare, M., Rogaway, P.: Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004\/331 (2004), \n                      \n                        http:\/\/eprint.iacr.org\/"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Maffeis, S., Gordon, A.D.: Refinement types for secure implementations. In: 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 17\u201332. IEEE (2008)","DOI":"10.1109\/CSF.2008.27"},{"key":"4_CR9","unstructured":"Berg, M.: Formal Verification of Cryptographic Security Proofs. Ph.D. thesis, Saarland University (2013), \n                      \n                        http:\/\/www.infsec.cs.uni-saarland.de\/~berg\/publications\/thesis-berg.pdf"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1109\/CSF.2007.16","volume-title":"20th IEEE Computer Security Foundations Symposium (CSF 2007)","author":"B. Blanchet","year":"2007","unstructured":"Blanchet, B.: Computationally sound mechanized proofs of correspondence assertions. In: 20th IEEE Computer Security Foundations Symposium (CSF 2007), pp. 97\u2013111. IEEE, Venice (2007)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-40041-4_20","volume-title":"Advances in Cryptology \u2013 CRYPTO 2013","author":"D. Cash","year":"2013","unstructured":"Cash, D., Jarecki, S., Jutla, C., Krawczyk, H., Ro\u015fu, M.-C., Steiner, M.: Highly-Scalable Searchable Symmetric Encryption with Support for Boolean Queries. In: Canetti, R., Garay, J.A. (eds.) CRYPTO 2013, Part I. LNCS, vol.\u00a08042, pp. 353\u2013373. Springer, Heidelberg (2013)"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/j.entcs.2007.02.012","volume":"172","author":"A. Datta","year":"2007","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (PCL). Electronic Notes in Theoretical Computer Science\u00a0172, 311\u2013358 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11523468_2","volume-title":"Automata, Languages and Programming","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 16\u201329. Springer, Heidelberg (2005)"},{"issue":"4","key":"4_CR14","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1109\/TIT.1985.1057074","volume":"31","author":"T. Elgamal","year":"1985","unstructured":"Elgamal, T.: A public key cryptosystem and a signature scheme based on discrete logarithms. IEEE Transactions on Information Theory\u00a031(4), 469\u2013472 (1985)","journal-title":"IEEE Transactions on Information Theory"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Fournet, C., Kohlweiss, M., Strub, P.Y.: Modular code-based cryptographic verification. In: Chen, Y., Danezis, G., Shmatikov, V. (eds.) ACM Conference on Computer and Communications Security, pp. 341\u2013350. ACM (2011)","DOI":"10.1145\/2046707.2046746"},{"key":"4_CR16","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (2005), \n                      \n                        http:\/\/eprint.iacr.org\/"},{"key":"4_CR17","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2004), version 8.0, \n                      \n                        http:\/\/coq.inria.fr"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Nowak, D.: A framework for game-based security proofs. Cryptology ePrint Archive, Report 2007\/199 (2007), \n                      \n                        http:\/\/eprint.iacr.org\/","DOI":"10.1007\/978-3-540-77048-0_25"},{"key":"4_CR20","first-page":"154","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002","author":"N. Ramsey","year":"2002","unstructured":"Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002, pp. 154\u2013165. ACM, New York (2002), \n                      \n                        http:\/\/doi.acm.org\/10.1145\/503272.503288"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46666-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:01:45Z","timestamp":1559138505000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46666-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466650","9783662466667"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46666-7_4","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-662-46666-7","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}