{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:36Z","timestamp":1759638936569},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642311123"},{"type":"electronic","value":"9783642311130"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31113-0_1","type":"book-chapter","created":{"date-parts":[[2012,6,20]],"date-time":"2012-06-20T01:04:11Z","timestamp":1340154251000},"page":"1-6","source":"Crossref","is-referenced-by-count":13,"title":["Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Zanella B\u00e9guelin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"1_CR2","first-page":"90","volume-title":"36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"G. Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90\u2013101. ACM, New York (2009)"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., B\u00e9guelin, S.Z.: Probabilistic reasoning for differential privacy. In: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012. ACM (2012)","DOI":"10.1145\/2103656.2103670"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/168588.168596","volume-title":"1st ACM Conference on Computer and Communications Security, CCS 1993","author":"M. Bellare","year":"1993","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: 1st ACM Conference on Computer and Communications Security, CCS 1993, pp. 62\u201373. ACM, New York (1993)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/11761679_25","volume-title":"Advances in Cryptology - EUROCRYPT 2006","author":"M. Bellare","year":"2006","unstructured":"Bellare, M., Rogaway, P.: The Security of Triple Encryption and a Framework\u00a0for\u00a0Code-Based\u00a0Game-Playing\u00a0Proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol.\u00a04004, pp. 409\u2013426. Springer, Heidelberg (2006)"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/964001.964003","volume-title":"31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004","author":"N. Benton","year":"2004","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 14\u201325. ACM, New York (2004)"},{"key":"1_CR7","unstructured":"Deng, Y., Du, W.: Logical, metric, and algorithmic characterisations of probabilistic bisimulation. Technical Report CMU-CS-11-110, Carnegie Mellon University (March 2011)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: Logic, simulation and games. In: 5th International Conference on Quantitative Evaluation of Systems, QEST 2008, pp. 264\u2013273. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.42"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11787006_1","volume-title":"Automata, Languages and Programming","author":"C. Dwork","year":"2006","unstructured":"Dwork, C.: Differential Privacy. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 1\u201312. Springer, Heidelberg (2006)"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1016\/0022-0000(84)90070-9","volume":"28","author":"S. Goldwasser","year":"1984","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci.\u00a028(2), 270\u2013299 (1984)","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR11","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (2005)"},{"key":"1_CR12","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1016\/B978-044482830-9\/50029-1","volume-title":"Handbook of Process Algebra","author":"B. Jonsson","year":"2001","unstructured":"Jonsson, B., Yi, W., Larsen, K.G.: Probabilistic extensions of process algebras. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 685\u2013710. Elsevier, Amsterdam (2001)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Segala, R., Turrini, A.: Approximated computationally bounded simulation relations for probabilistic automata. In: 20th IEEE Computer Security Foundations Symposium, CSF 2007, pp. 140\u2013156 (2007)","DOI":"10.1109\/CSF.2007.8"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31113-0_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:45:27Z","timestamp":1620114327000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31113-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642311123","9783642311130"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31113-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}