{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:40:11Z","timestamp":1750308011172,"version":"3.41.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>In this paper, we report on our effort in enhancing our model-checker for cryptographic protocols with the ability to automatically generate a deductive proof that the protocol meets its specification. More specifically, we discuss a technique that allows to transform an abstract proof extracted from the model-checker to a proof that can be checked independently of the abstracting and model-checking process.<\/jats:p>","DOI":"10.1145\/1183088.1183094","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"37-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Certifying cryptographic protocols by abstract model-checking and proof concretization"],"prefix":"10.1145","volume":"3","author":[{"given":"R.","family":"Janvier","sequence":"first","affiliation":[{"name":"VERIMAG, Gi\u00e8res, France"}]},{"given":"Y.","family":"Lakhnech","sequence":"additional","affiliation":[{"name":"VERIMAG, Gi\u00e8res, France"}]},{"given":"M.","family":"P\u00e9rin","sequence":"additional","affiliation":[{"name":"VERIMAG, Gi\u00e8res, France"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"1\n  . \n      Tamarah\n      Arons Amir\n      Pnueli Sitvanit\n      Ruah Jiazhao\n      Xu and \n      Lenore D.\n      Zuck\n  . \n  Parameterized verification with automatically computed inductive assertions\n  . In G\u00e9rard Berry Hubert Comon and Alain Finkel editors CAV volume \n  2102\n   of \n  Lecture Notes in Computer Science pages \n  221\n  -\n  234\n  . \n  Springer 2001\n  .]]   1. Tamarah Arons Amir Pnueli Sitvanit Ruah Jiazhao Xu and Lenore D. Zuck. Parameterized verification with automatically computed inductive assertions. In G\u00e9rard Berry Hubert Comon and Alain Finkel editors CAV volume 2102 of Lecture Notes in Computer Science pages 221-234. Springer 2001.]]","DOI":"10.1007\/3-540-44585-4_19"},{"key":"e_1_2_1_2_1","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2004","unstructured":"2 . Yves Bertot and Pierre Cast\u00e9ran . Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions , volume XXV of Texts in Theoretical Computer Science . An EATCS Series. Springer , 2004 . 469 p., Hard-cover. ISBN: 3-540-20854-2.]] 2. Yves Bertot and Pierre Cast\u00e9ran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, volume XXV of Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. 469 p., Hard-cover. ISBN: 3-540-20854-2.]]"},{"key":"e_1_2_1_3_1","series-title":"LNCS","volume-title":"TACAS'03","author":"Bozga L.","year":"2003","unstructured":"3 . L. Bozga , Y. Lakhnech , and M. P\u00e9rin . Abstract interpretation for secrecy using patterns . In TACAS'03 , volume 2619 of LNCS , 2003 .]] 3. L. Bozga, Y. Lakhnech, and M. P\u00e9rin. Abstract interpretation for secrecy using patterns. In TACAS'03, volume 2619 of LNCS, 2003.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_23"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0189-6"},{"key":"e_1_2_1_6_1","first-page":"154","volume-title":"LNCS","author":"Clarke E.","year":"2000","unstructured":"6 . E. Clarke , O. Grumberg , S. Jha , Y. Lu , and H. Veith . Counterexample-guided abstraction refinement. In Computer Aided Verification , LNCS , pages 154 - 169 . Springer-Verlag , 2000 .]] 6. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, LNCS, pages 154-169. Springer-Verlag, 2000.]]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734280"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694461"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_2_1_13_1","series-title":"LNCS","volume-title":"Proceedings of TACAS'96 - Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"Lowe G.","year":"1996","unstructured":"13 . G. Lowe . Breaking and fixing the needham-schroeder public-key protocol using FDR . In T. Margaria and B. Steffen, editors, Proceedings of TACAS'96 - Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems , Passau, Germany , volume 1055 of LNCS . Springer , March 1996 .]] 13. G. Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR. In T. Margaria and B. Steffen, editors, Proceedings of TACAS'96 - Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, volume 1055 of LNCS. Springer, March 1996.]]"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science, 2102: 2-??","volume-title":"Certifying model checkers","author":"Namjoshi Kedar S.","year":"2001","unstructured":"15 . Kedar S. Namjoshi . Certifying model checkers . Lecture Notes in Computer Science, 2102: 2-?? , 2001 .]] 15. Kedar S. Namjoshi. Certifying model checkers. Lecture Notes in Computer Science, 2102:2-??, 2001.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646542.696199"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"17\n  . \n      Doron\n      Peled Amir\n      Pnueli and \n      Lenore D.\n      Zuck\n  . \n  From falsification to verification\n  . In Ramesh Hariharan Madhavan Mukund and V. Vinay editors FSTTCS volume \n  2245\n   of \n  Lecture Notes in Computer Science pages \n  292\n  -\n  304\n  . \n  Springer 2001\n  .]]   17. Doron Peled Amir Pnueli and Lenore D. Zuck. From falsification to verification. In Ramesh Hariharan Madhavan Mukund and V. Vinay editors FSTTCS volume 2245 of Lecture Notes in Computer Science pages 292-304. Springer 2001.]]","DOI":"10.1007\/3-540-45294-X_25"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006376231563"},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tiziana Margaria and Wang Yi","author":"Pnueli Amir","year":"2001","unstructured":"19 . Amir Pnueli , Sitvanit Ruah , and Lenore D. Zuck . Automatic deductive verification with invisible invariants . In Tiziana Margaria and Wang Yi , editors, TACAS, volume 2031 of Lecture Notes in Computer Science , pages 82 - 97 . Springer , 2001 .]] 19. Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. Automatic deductive verification with invisible invariants. In Tiziana Margaria and Wang Yi, editors, TACAS, volume 2031 of Lecture Notes in Computer Science, pages 82-97. Springer, 2001.]]"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/647325.721668"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351290"},{"key":"e_1_2_1_22_1","volume-title":"Evidence-based model checking","author":"Tan L.","year":"2002","unstructured":"22 . L. Tan and R. Cleaveland . Evidence-based model checking , 2002 .]] 22. L. Tan and R. Cleaveland. Evidence-based model checking, 2002.]]"},{"key":"e_1_2_1_23_1","volume-title":"Logical Project","author":"Development Team The Coq","year":"2005","unstructured":"23 . The Coq Development Team . The Coq Proof Assistant Reference Manual Version 8.0 . Logical Project , January 2005 .]] 23. The Coq Development Team. The Coq Proof Assistant Reference Manual Version 8.0. Logical Project, January 2005.]]"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086292"},{"key":"e_1_2_1_25_1","unstructured":"25\n  .  http:\/\/www-verimag.imag.fr\/Liana.Bozga\/eva\/hermes.php.]]  25. http:\/\/www-verimag.imag.fr\/Liana.Bozga\/eva\/hermes.php.]]"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183088.1183094","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1183088.1183094","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:36Z","timestamp":1750259196000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183088.1183094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1183088.1183094"],"URL":"https:\/\/doi.org\/10.1145\/1183088.1183094","relation":{},"ISSN":["1551-3688"],"issn-type":[{"type":"electronic","value":"1551-3688"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}