{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:33Z","timestamp":1750308213459,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,10,29]],"date-time":"2004-10-29T00:00:00Z","timestamp":1099008000000},"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":[],"published-print":{"date-parts":[[2004,10,29]]},"DOI":"10.1145\/1029133.1029137","type":"proceedings-article","created":{"date-parts":[[2005,1,30]],"date-time":"2005-01-30T17:58:48Z","timestamp":1107107928000},"page":"23-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Timed model checking of security protocols"],"prefix":"10.1145","author":[{"given":"R.","family":"Corin","sequence":"first","affiliation":[{"name":"University of Twente, The Netherlands"}]},{"given":"S.","family":"Etalle","sequence":"additional","affiliation":[{"name":"University of Twente, The Netherlands"}]},{"given":"P. H.","family":"Hartel","sequence":"additional","affiliation":[{"name":"University of Twente, The Netherlands"}]},{"given":"A.","family":"Mader","sequence":"additional","affiliation":[{"name":"University of Twente, The Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2004,10,29]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/3-540-36467-6_3","volume-title":"Int. Workshop on Privacy Enhancing Technologies (PET)","volume":"2482","author":"Abadi M.","year":"2002","unstructured":"M. Abadi . Private authentication. In R. Dingledine and P. F. Syverson, editors, 2nd . Int. Workshop on Privacy Enhancing Technologies (PET) , volume LNCS 2482 , pages 27 -- 40 , San Francisco, California , Apr 2002 . Springer-Verlag, Berlin.]] M. Abadi. Private authentication. In R. Dingledine and P. F. Syverson, editors, 2nd. Int. Workshop on Privacy Enhancing Technologies (PET), volume LNCS 2482, pages 27--40, San Francisco, California, Apr 2002. Springer-Verlag, Berlin.]]"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_3_1","first-page":"99","volume-title":"UPPAAL - Now, Next, and Future","author":"Amnell T.","year":"2000","unstructured":"T. Amnell , G. Behrmann , J. Bengtsson , P. R. D'Argenio , A. David , A. Fehnker , T. Hune , B. Jeannet , K. G. Larsen , M. O. M\u00f6ller , P. Pettersson , C. Weise , and W. Yi . UPPAAL - Now, Next, and Future . In F. Cassez, C. Jard, B. Rozoy, and M. D. Ryand, editors, 4th Summer School on Modeling and Verification of Parallel Processes (MOVEP), volume LNCS 2067 , pages 99 -- 124 , Nantes, France, Jun 2000 . Springer-Verlag , Berlin.]] T. Amnell, G. Behrmann, J. Bengtsson, P. R. D'Argenio, A. David, A. Fehnker, T. Hune, B. Jeannet, K. G. Larsen, M. O. M\u00f6ller, P. Pettersson, C. Weise, and W. Yi. UPPAAL - Now, Next, and Future. In F. Cassez, C. Jard, B. Rozoy, and M. D. Ryand, editors, 4th Summer School on Modeling and Verification of Parallel Processes (MOVEP), volume LNCS 2067, pages 99--124, Nantes, France, Jun 2000. Springer-Verlag, Berlin.]]"},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","first-page":"361","volume-title":"J.-J","author":"Bella G.","year":"1998","unstructured":"G. Bella and L. C. Paulson . Kerberos version IV: Inductive analysis of the secrecy goals . In J.-J . Quisquater, editor, Proc. 5th European Symposium on Research in Computer Security, volume 1485 of LNCS , pages 361 -- 375 , Louvain-la-Neuve, Belgium, 1998 . Springer-Verlag .]] G. Bella and L. C. Paulson. Kerberos version IV: Inductive analysis of the secrecy goals. In J.-J. Quisquater, editor, Proc. 5th European Symposium on Research in Computer Security, volume 1485 of LNCS, pages 361--375, Louvain-la-Neuve, Belgium, 1998. Springer-Verlag.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/381906.381946"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77649"},{"key":"e_1_3_2_1_7_1","unstructured":"J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. http:\/\/www.cs.york.ac.uk\/ jac\/papers\/drareview.ps.gz 1997.]]  J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. http:\/\/www.cs.york.ac.uk\/ jac\/papers\/drareview.ps.gz 1997.]]"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.718316"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-44804-7_6","volume-title":"Joint Int. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV)","author":"D'Argenio P. R.","year":"2001","unstructured":"P. R. D'Argenio , H. Hermanns , J.-P. Katoen , and J. Klaren . MODEST : A modelling language for stochastic timed systems . In L. de Alfaro and S. Gilmore, editors, Joint Int. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV) , volume LNCS 2165 , pages 87 -- 104 , Aachen, Germany, Sep 2001 . Springer-Verlag , Berlin.]] P. R. D'Argenio, H. Hermanns, J.-P. Katoen, and J. Klaren. MODEST : A modelling language for stochastic timed systems. In L. de Alfaro and S. Gilmore, editors, Joint Int. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV), volume LNCS 2165, pages 87--104, Aachen, Germany, Sep 2001. Springer-Verlag, Berlin.]]"},{"key":"e_1_3_2_1_10_1","first-page":"76","volume-title":"Proof theory, transformations, and logic programming for debugging security protocols","author":"Delzanno G.","year":"2001","unstructured":"G. Delzanno and S. Etalle . Proof theory, transformations, and logic programming for debugging security protocols . In A. Pettorossi, editor, 11th Int. Logic Based Program Synthesis and Transformation (LOPSTR), volume LNCS 2372 , pages 76 -- 90 , Paphos, Greece, Nov 2001 . Springer-Verlag , Berlin.]] G. Delzanno and S. Etalle. Proof theory, transformations, and logic programming for debugging security protocols. In A. Pettorossi, editor, 11th Int. Logic Based Program Synthesis and Transformation (LOPSTR), volume LNCS 2372, pages 76--90, Paphos, Greece, Nov 2001. Springer-Verlag, Berlin.]]"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_27"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.485898"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"N.\n      Evans\n     and \n      S.\n      Schneider\n  . \n  Analysing time dependent security properties in CSP using PVS\n  . In Fr\u00e9d\u00e9ric Cuppens Yves Deswarte Dieter Gollmann and Michael Waidner editors ESORICS volume \n  1895\n   of \n  LNCS pages \n  222\n  --\n  237\n  . \n  Springer 2000\n  .]]   N. Evans and S. Schneider. Analysing time dependent security properties in CSP using PVS. In Fr\u00e9d\u00e9ric Cuppens Yves Deswarte Dieter Gollmann and Michael Waidner editors ESORICS volume 1895 of LNCS pages 222--237. Springer 2000.]]","DOI":"10.1007\/10722599_14"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/352600.352606"},{"key":"e_1_3_2_1_16_1","volume-title":"Formal models of timing attacks on web privacy","author":"Focardi R.","year":"2002","unstructured":"R. Focardi , R. Gorrieri , R. Lanotte , A. Maggiolo-Schettini , F. Martinelli , S. Tini , and E. Tronci . Formal models of timing attacks on web privacy . In Marina Lenisa and Marino Miculan, editors, ENTCS, volume 62 . Elsevier , 2002 .]] R. Focardi, R. Gorrieri, R. Lanotte, A. Maggiolo-Schettini, F. Martinelli, S. Tini, and E. Tronci. Formal models of timing attacks on web privacy. In Marina Lenisa and Marino Miculan, editors, ENTCS, volume 62. Elsevier, 2002.]]"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765533.1765562"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"R.\n      Gorrieri E.\n      Locatelli and \n      F.\n      Martinelli\n  . \n  A simple language for real-time cryptographic protocol analysis\n  . In Pierpaolo Degano editor 12th European Symposium on Programming ESOP \n  2003 volume \n  2618\n   of \n  LNCS pages \n  114\n  --\n  128 Heidelberg 2003. \n  Springer-Verlag\n  .]]   R. Gorrieri E. Locatelli and F. Martinelli. A simple language for real-time cryptographic protocol analysis. In Pierpaolo Degano editor 12th European Symposium on Programming ESOP 2003 volume 2618 of LNCS pages 114--128 Heidelberg 2003. Springer-Verlag.]]","DOI":"10.1007\/3-540-36575-3_9"},{"key":"e_1_3_2_1_19_1","series-title":"LNCS","first-page":"52","volume-title":"J.-P","author":"Kwiatkowska M.","year":"2002","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . Probabilistic symbolic model checking with PRISM: A hybrid approach . In J.-P . Katoen and P. Stevens, editors, (TACAS'02), volume 2280 of LNCS , pages 52 -- 66 . Springer , 2002 .]] M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In J.-P. Katoen and P. Stevens, editors, (TACAS'02), volume 2280 of LNCS, pages 52--66. Springer, 2002.]]"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993.2994"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795076"},{"key":"e_1_3_2_1_23_1","first-page":"3143","volume-title":"In 10th IEEE Computer Security Foundations Workshop","author":"Lowe G.","unstructured":"G. Lowe . A hierarchy of authentication specifications . In In 10th IEEE Computer Security Foundations Workshop , page 3143 . IEEE Computer Society Press, 1997.]] G. Lowe. A hierarchy of authentication specifications. In In 10th IEEE Computer Security Foundations Workshop, page 3143. IEEE Computer Society Press, 1997.]]"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"D. Mills. Cryptographic authentication for real-time network protocols. 45:135--144 1999.]]  D. Mills. Cryptographic authentication for real-time network protocols. 45:135--144 1999.]]","DOI":"10.1090\/dimacs\/045\/08"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1994.315935"}],"event":{"name":"CCS04: 11th ACM Conference on Computer and Communications Security 2004","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","ACM Association for Computing Machinery"],"location":"Washington DC USA","acronym":"CCS04"},"container-title":["Proceedings of the 2004 ACM workshop on Formal methods in security engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1029133.1029137","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1029133.1029137","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:07Z","timestamp":1750264267000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1029133.1029137"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10,29]]},"references-count":25,"alternative-id":["10.1145\/1029133.1029137","10.1145\/1029133"],"URL":"https:\/\/doi.org\/10.1145\/1029133.1029137","relation":{},"subject":[],"published":{"date-parts":[[2004,10,29]]},"assertion":[{"value":"2004-10-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}