{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:11Z","timestamp":1761596891120,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2003,10,30]],"date-time":"2003-10-30T00:00:00Z","timestamp":1067472000000},"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":[[2003,10,30]]},"DOI":"10.1145\/1035429.1035432","type":"proceedings-article","created":{"date-parts":[[2005,1,30]],"date-time":"2005-01-30T17:55:16Z","timestamp":1107107716000},"page":"24-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Using interval logics for temporal analysis of security protocols"],"prefix":"10.1145","author":[{"given":"Michael R.","family":"Hansen","sequence":"first","affiliation":[{"name":"Technical University of Denmark, Denmark"}]},{"given":"Robin","family":"Sharp","sequence":"additional","affiliation":[{"name":"Technical University of Denmark, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2003,10,30]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.2.271"},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"365","volume-title":"K. Kanchanasut and J.-J","author":"Chan P.","year":"1995","unstructured":"P. Chan and D. V. Hung . Duration calculus specification of scheduling for tasks with shared resources . In K. Kanchanasut and J.-J . Levy, editors, Asian Computing Science Conference 1995 , volume 1023 of LNCS , pages 365 - 380 . Springer-Verlag , 1995.]] P. Chan and D. V. Hung. Duration calculus specification of scheduling for tasks with shared resources. In K. Kanchanasut and J.-J. Levy, editors, Asian Computing Science Conference 1995, volume 1023 of LNCS, pages 365-380. Springer-Verlag, 1995.]]"},{"key":"e_1_3_2_1_3_1","first-page":"139","volume-title":"Proceedings of the 1983 Symposium on Security and Privacy","author":"Gligor V. D.","year":"1983","unstructured":"V. D. Gligor . A note on the denial-of-service problem . In Proceedings of the 1983 Symposium on Security and Privacy , pages 139 - 149 . IEEE Computer Society Press , 1983 .]] V. D. Gligor. A note on the denial-of-service problem. In Proceedings of the 1983 Symposium on Security and Privacy, pages 139-149. IEEE Computer Society Press, 1983.]]"},{"key":"e_1_3_2_1_4_1","first-page":"79","volume-title":"Dependable Computing for Critical Applications 5","author":"Gong L.","year":"1998","unstructured":"L. Gong and P. Syverson . Fail-stop protocols: An approach to designing secure protocols . In R. K. Iyer, M. Morganti, W. K. Fuchs, and V. Gligor, editors, Dependable Computing for Critical Applications 5 , pages 79 - 100 . IEEE Computer Society , 1998 .]] L. Gong and P. Syverson. Fail-stop protocols: An approach to designing secure protocols. In R. K. Iyer, M. Morganti, W. K. Fuchs, and V. Gligor, editors, Dependable Computing for Critical Applications 5, pages 79-100. IEEE Computer Society, 1998.]]"},{"key":"e_1_3_2_1_5_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/BFb0036915","volume-title":"ICALP'83","author":"Halpern J.","year":"1983","unstructured":"J. Halpern , B. Moszkowski , and Z. Manna . A hardware semantics based on temporal intervals . In ICALP'83 , volume 154 of Lecture Notes in Computer Science , pages 278 - 291 . Springer-Verlag , 1983 .]] J. Halpern, B. Moszkowski, and Z. Manna. A hardware semantics based on temporal intervals. In ICALP'83, volume 154 of Lecture Notes in Computer Science, pages 278-291. Springer-Verlag, 1983.]]"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211086"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/374742.374757"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/RISP.1992.213265"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-0-387-35079-0_18","volume-title":"Formal Description Techniques IX: Theory, application and tools","author":"M\u00f8rk S.","year":"1996","unstructured":"S. M\u00f8rk , J. C. Godskesen , M. R. Hansen , and R. Sharp . A timed semantics for SDL . In R. Gotzhein and J. Bredereke, editors, Formal Description Techniques IX: Theory, application and tools , pages 295 - 309 . Chapman & Hall , 1996 .]] S. M\u00f8rk, J. C. Godskesen, M. R. Hansen, and R. Sharp. A timed semantics for SDL. In R. Gotzhein and J. Bredereke, editors, Formal Description Techniques IX: Theory, application and tools, pages 295-309. Chapman & Hall, 1996.]]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1985.1662795"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795079"},{"key":"e_1_3_2_1_14_1","volume-title":"Modelling properties of security protocols. Master's thesis, Informatics and Mathematical Modelling","author":"Pilegaard H.","year":"2002","unstructured":"H. Pilegaard . Modelling properties of security protocols. Master's thesis, Informatics and Mathematical Modelling , Technical University of Denmark , Oct. 2002 .]] H. Pilegaard. Modelling properties of security protocols. Master's thesis, Informatics and Mathematical Modelling, Technical University of Denmark, Oct. 2002.]]"},{"key":"e_1_3_2_1_15_1","volume-title":"Nordic Journal of Computing","author":"Pilegaard H.","year":"2003","unstructured":"H. Pilegaard , M. R. Hansen , and R. Sharp . An approach to analyzing availability properties of security protocols . Nordic Journal of Computing , 2003 . To appear.]] H. Pilegaard, M. R. Hansen, and R. Sharp. An approach to analyzing availability properties of security protocols. Nordic Journal of Computing, 2003. To appear.]]"},{"key":"e_1_3_2_1_16_1","series-title":"Lecture Notes in Computer Science","first-page":"317","volume-title":"LPAR","author":"Rasmussen T. M.","year":"2001","unstructured":"T. M. Rasmussen . Automated proof support for interval logics. In LPAR 2001 , volume 2250 of Lecture Notes in Computer Science , pages 317 - 326 . Springer-Verlag , 2001.]] T. M. Rasmussen. Automated proof support for interval logics. In LPAR 2001, volume 2250 of Lecture Notes in Computer Science, pages 317-326. Springer-Verlag, 2001.]]"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1949221.1949249"},{"key":"e_1_3_2_1_20_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"756","DOI":"10.1007\/3-540-58468-4_194","volume-title":"H. Langmack, W. -P","author":"Yuhua Zheng","year":"1994","unstructured":"Zheng Yuhua and Zhou Chaochen . A formal proof of the deadline driven scheduler . In H. Langmack, W. -P . de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science , pages 756 - 775 . Springer-Verlag , Sept. 1994 .]] Zheng Yuhua and Zhou Chaochen. A formal proof of the deadline driven scheduler. In H. Langmack, W. -P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 756-775. Springer-Verlag, Sept. 1994.]]"},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"581","volume-title":"Compositionality: The Significant Difference (COMPOS'97)","author":"Chaochen Zhou","year":"1998","unstructured":"Zhou Chaochen and M. R. Hansen . An adequate first order interval logic . In Compositionality: The Significant Difference (COMPOS'97) , volume 1536 of Lecture Notes in Computer Science , pages 581 - 608 . Springer-Verlag , 1998 .]] Zhou Chaochen and M. R. Hansen. An adequate first order interval logic. In Compositionality: The Significant Difference (COMPOS'97), volume 1536 of Lecture Notes in Computer Science, pages 581-608. Springer-Verlag, 1998.]]"},{"key":"e_1_3_2_1_22_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-55092-5_2","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"Chaochen Zhou","year":"1992","unstructured":"Zhou Chaochen , M. R. Hansen , A. P. Ravn and H. Rischel , Duration specifications for shared processors . In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems , volume 571 of Lecture Notes in Computer Science , pages 21 - 32 . Springer-Verlag , Jan. 1992 .]] Zhou Chaochen, M. R. Hansen, A. P. Ravn and H. Rischel, Duration specifications for shared processors. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science, pages 21-32. Springer-Verlag, Jan. 1992.]]"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"}],"event":{"name":"CCS03: Tenth ACM Conference on Computer and Communications Security 2003","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Washington D.C.","acronym":"CCS03"},"container-title":["Proceedings of the 2003 ACM workshop on Formal methods in security engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1035429.1035432","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1035429.1035432","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:24:29Z","timestamp":1750263869000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1035429.1035432"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,10,30]]},"references-count":22,"alternative-id":["10.1145\/1035429.1035432","10.1145\/1035429"],"URL":"https:\/\/doi.org\/10.1145\/1035429.1035432","relation":{},"subject":[],"published":{"date-parts":[[2003,10,30]]},"assertion":[{"value":"2003-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}