{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T13:01:15Z","timestamp":1772283675415,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":65,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,10,15]],"date-time":"2018-10-15T00:00:00Z","timestamp":1539561600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N000141512750"],"award-info":[{"award-number":["N000141512750"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,10,15]]},"DOI":"10.1145\/3243734.3243825","type":"proceedings-article","created":{"date-parts":[[2018,10,16]],"date-time":"2018-10-16T12:56:36Z","timestamp":1539694596000},"page":"538-555","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Symbolic Proofs for Lattice-Based Cryptography"],"prefix":"10.1145","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"given":"Xiong","family":"Fan","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]},{"given":"Joshua","family":"Gancher","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"INRIA, Sophia-Antipolis, France"}]},{"given":"Charlie","family":"Jacomme","sequence":"additional","affiliation":[{"name":"LSV & CNRS & ENS Paris-Saclay & INRIA & Universit\u00e9 Paris-Saclay, Paris, France"}]},{"given":"Elaine","family":"Shi","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,10,15]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13190-5_28"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25385-0_2"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44371-2_17"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53644-5_12"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516663"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866350"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939145"},{"key":"e_1_3_2_2_9_1","volume-title":"Benjamin Gr\u00e9 goire, C\u00e9 sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub.","author":"Barthe Gilles","year":"2013","unstructured":"Gilles Barthe , Francc ois Dupressoir , Benjamin Gr\u00e9 goire, C\u00e9 sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013 . EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier Lopez, and Fabio Martinelli (Eds.), Vol. 8604 . Springer , 146--166. Gilles Barthe, Francc ois Dupressoir, Benjamin Gr\u00e9 goire, C\u00e9 sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier Lopez, and Fabio Martinelli (Eds.), Vol. 8604. Springer, 146--166."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_2_11_1","volume-title":"Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO 2011 (LNCS ), Phillip Rogaway (Ed.)","volume":"6841","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , Sylvain Heraud , and Santiago Zanella B\u00e9guelin . 2011 . Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO 2011 (LNCS ), Phillip Rogaway (Ed.) , Vol. 6841 . Springer, Heidelberg, 71--90. Gilles Barthe, Benjamin Gr\u00e9goire, Sylvain Heraud, and Santiago Zanella B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO 2011 (LNCS ), Phillip Rogaway (Ed.), Vol. 6841. Springer, Heidelberg, 71--90."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813697"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_2_2_14_1","volume-title":"An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001","author":"Blanchet Bruno","year":"2001","unstructured":"Bruno Blanchet . 2001 . An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001 ), 11--13 June 2001, Cape Breton, Nova Scotia, Canada. IEEE Computer Society, 82--96. Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11--13 June 2001, Cape Breton, Nova Scotia, Canada. IEEE Computer Society, 82--96."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24676-3_14"},{"key":"e_1_3_2_2_17_1","volume-title":"Arithmetic Circuit ABE and Compact Garbled Circuits. In EUROCRYPT 2014 (LNCS ), Phong Q. Nguyen and Elisabeth Oswald (Eds.)","volume":"8441","author":"Boneh Dan","year":"2014","unstructured":"Dan Boneh , Craig Gentry , Sergey Gorbunov , Shai Halevi , Valeria Nikolaenko , Gil Segev , Vinod Vaikuntanathan , and Dhinakaran Vinayagamurthy . 2014 . Fully Key-Homomorphic Encryption , Arithmetic Circuit ABE and Compact Garbled Circuits. In EUROCRYPT 2014 (LNCS ), Phong Q. Nguyen and Elisabeth Oswald (Eds.) , Vol. 8441 . Springer, Heidelberg, 533--556. Dan Boneh, Craig Gentry, Sergey Gorbunov, Shai Halevi, Valeria Nikolaenko, Gil Segev, Vinod Vaikuntanathan, and Dhinakaran Vinayagamurthy. 2014. Fully Key-Homomorphic Encryption, Arithmetic Circuit ABE and Compact Garbled Circuits. In EUROCRYPT 2014 (LNCS ), Phong Q. Nguyen and Elisabeth Oswald (Eds.), Vol. 8441. Springer, Heidelberg, 533--556."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978425"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488680"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088216.1088219"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24597-1_11"},{"key":"e_1_3_2_2_22_1","volume-title":"18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. 271--280","author":"Comon-Lundh H.","unstructured":"H. Comon-Lundh and V. Shmatikov . 2003. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or . In 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. 271--280 . H. Comon-Lundh and V. Shmatikov. 2003. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. 271--280."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_27"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_22"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455817"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.23"},{"key":"e_1_3_2_2_30_1","volume-title":"Commutative Algebra: with a view toward algebraic geometry","author":"Eisenbud David","unstructured":"David Eisenbud . 2013. Commutative Algebra: with a view toward algebraic geometry . Vol. 150 . Springer Science & Business Media . David Eisenbud. 2013. Commutative Algebra: with a view toward algebraic geometry. Vol. 150. Springer Science & Business Media."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40203-6_17"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_4"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1374376.1374407"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48000-7_25"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813636"},{"key":"e_1_3_2_2_36_1","volume-title":"44th Symposium on Foundations of Computer Science (FOCS 2003), 11--14 October 2003, Cambridge, MA, USA, Proceedings. IEEE Computer Society, 372--383","author":"Impagliazzo Russell","unstructured":"Russell Impagliazzo and Bruce M. Kapron . 2003. Logics for Reasoning about Cryptographic Constructions . In 44th Symposium on Foundations of Computer Science (FOCS 2003), 11--14 October 2003, Cambridge, MA, USA, Proceedings. IEEE Computer Society, 372--383 . Russell Impagliazzo and Bruce M. Kapron. 2003. Logics for Reasoning about Cryptographic Constructions. In 44th Symposium on Foundations of Computer Science (FOCS 2003), 11--14 October 2003, Cambridge, MA, USA, Proceedings. IEEE Computer Society, 372--383."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/73007.73009"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00197942"},{"key":"e_1_3_2_2_39_1","volume-title":"Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. In 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017","author":"Kobeissi Nadim","year":"2017","unstructured":"Nadim Kobeissi , Karthikeyan Bhargavan , and Bruno Blanchet . 2017 . Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. In 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017 , Paris, France, April 26--28 , 2017. IEEE, 435--450. Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. In 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26--28, 2017. IEEE, 435--450."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9203-0"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90016-9"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_20"},{"key":"e_1_3_2_2_43_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Lowe Gavin","unstructured":"Gavin Lowe . 1996. Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR . In Tools and Algorithms for the Construction and Analysis of Systems , Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg , 147--166. Gavin Lowe. 1996. Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 147--166."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.18"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29011-4_41"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/501983.502007"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90283-6"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/281508.281595"},{"key":"e_1_3_2_2_49_1","article-title":"The Inductive Approach to Verifying Cryptographic Protocols","volume":"6","author":"Paulson Lawrence","year":"2000","unstructured":"Lawrence Paulson . 2000 . The Inductive Approach to Verifying Cryptographic Protocols . Journal of Computer Security , Vol. 6 (12 2000). Lawrence Paulson. 2000. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, Vol. 6 (12 2000).","journal-title":"Journal of Computer Security"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536461"},{"key":"e_1_3_2_2_51_1","volume-title":"Proceedings (Lecture Notes in Computer Science), Michele Mosca (Ed.)","volume":"8772","author":"Peikert Chris","year":"2014","unstructured":"Chris Peikert . 2014 . Lattice Cryptography for the Internet. In Post-Quantum Cryptography - 6th International Workshop, PQCrypto 2014, Waterloo, ON, Canada, October 1--3, 2014 . Proceedings (Lecture Notes in Computer Science), Michele Mosca (Ed.) , Vol. 8772 . Springer, 197--219. Chris Peikert. 2014. Lattice Cryptography for the Internet. In Post-Quantum Cryptography - 6th International Workshop, PQCrypto 2014, Waterloo, ON, Canada, October 1--3, 2014. Proceedings (Lecture Notes in Computer Science), Michele Mosca (Ed.), Vol. 8772. Springer, 197--219."},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000074"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060590.1060603"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060590.1060603"},{"key":"e_1_3_2_2_56_1","volume-title":"Subalgebra bases","author":"Robbiano Lorenzo","unstructured":"Lorenzo Robbiano and Moss Sweedler . 1990. Subalgebra bases . In Commutative Algebra, Winfried Bruns and Aron Simis (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 61--87. Lorenzo Robbiano and Moss Sweedler. 1990. Subalgebra bases. In Commutative Algebra, Winfried Bruns and Aron Simis (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 61--87."},{"key":"e_1_3_2_2_57_1","volume-title":"Symposium on(LICS)","volume":"00","author":"Rusinowitch M.","unstructured":"M. Rusinowitch , R. K\u00fcsters , M. Turuani , and Y. Chevalier . 2003. An NP Decision Procedure for Protocol Insecurity with XOR. In Logic in Computer Science , Symposium on(LICS) , Vol. 00 . 261. M. Rusinowitch, R. K\u00fcsters, M. Turuani, and Y. Chevalier. 2003. An NP Decision Procedure for Protocol Insecurity with XOR. In Logic in Computer Science, Symposium on(LICS), Vol. 00. 261."},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/2780696.2781023"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.25"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.5555\/1947337.1947362"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80047-6"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000142"},{"key":"e_1_3_2_2_63_1","first-page":"51","article-title":"Semantic Security Invariance under Variant Computational Assumptions","volume":"2018","author":"Theodorakis Eftychios","year":"2018","unstructured":"Eftychios Theodorakis and John C. Mitchell . 2018 . Semantic Security Invariance under Variant Computational Assumptions . IACR Cryptology ePrint Archive , Vol. 2018 (2018), 51 . http:\/\/eprint.iacr.org\/2018\/051 Eftychios Theodorakis and John C. Mitchell. 2018. Semantic Security Invariance under Variant Computational Assumptions. IACR Cryptology ePrint Archive, Vol. 2018 (2018), 51. http:\/\/eprint.iacr.org\/2018\/051","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_64_1","volume-title":"Proceedings (Lecture Notes in Computer Science), Amy P. Felty and Aart Middeldorp (Eds.)","volume":"9195","author":"Tiwari Ashish","year":"2015","unstructured":"Ashish Tiwari , Adri\u00e0 Gasc\u00f3 n, and Bruno Dutertre . 2015 . Program Synthesis Using Dual Interpretation. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1--7, 2015 , Proceedings (Lecture Notes in Computer Science), Amy P. Felty and Aart Middeldorp (Eds.) , Vol. 9195 . Springer, 482--497. Ashish Tiwari, Adri\u00e0 Gasc\u00f3 n, and Bruno Dutertre. 2015. Program Synthesis Using Dual Interpretation. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1--7, 2015, Proceedings (Lecture Notes in Computer Science), Amy P. Felty and Aart Middeldorp (Eds.), Vol. 9195. Springer, 482--497."},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03356-8_36"}],"event":{"name":"CCS '18: 2018 ACM SIGSAC Conference on Computer and Communications Security","location":"Toronto Canada","acronym":"CCS '18","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243734.3243825","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3243734.3243825","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3243734.3243825","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:08:19Z","timestamp":1750212499000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243734.3243825"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,15]]},"references-count":65,"alternative-id":["10.1145\/3243734.3243825","10.1145\/3243734"],"URL":"https:\/\/doi.org\/10.1145\/3243734.3243825","relation":{},"subject":[],"published":{"date-parts":[[2018,10,15]]},"assertion":[{"value":"2018-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}