{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:49Z","timestamp":1725490249655},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745099"},{"type":"electronic","value":"9783540745105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74510-5_38","type":"book-chapter","created":{"date-parts":[[2007,8,21]],"date-time":"2007-08-21T11:11:35Z","timestamp":1187694695000},"page":"373-386","source":"Crossref","is-referenced-by-count":1,"title":["Timed Traces and Strand Spaces"],"prefix":"10.1007","author":[{"given":"Robin","family":"Sharp","sequence":"first","affiliation":[]},{"given":"Michael R.","family":"Hansen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"38_CR1","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1093\/logcom\/10.2.271","volume":"10","author":"R. Barua","year":"2000","unstructured":"Barua, R., Roy, S., Chaochen, Z.: Completeness of neighbourhood logic. Journal of Logic and Computation\u00a010(2), 271\u2013295 (2000)","journal-title":"Journal of Logic and Computation"},{"key":"38_CR2","unstructured":"Bellovin, S.M., Merritt, M.: Limitations of the Kerberos authentication system. In: Proc. of the USENIX Conference, pp. 253\u2013267. USENIX Assoc. (1991)"},{"key":"38_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-60688-2_56","volume-title":"Algorithms, Concurrency and Knowledge","author":"P. Chan","year":"1995","unstructured":"Chan, P., Hung, D.V.: Duration calculus specification of scheduling for tasks with shared resources. In: Kanchanasut, K., Levy, J.-J. (eds.) Algorithms, Concurrency and Knowledge. LNCS, vol.\u00a01023, pp. 365\u2013380. Springer, Heidelberg (1995)"},{"key":"38_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0036915","volume-title":"Automata, Languages and Programming","author":"J. Halpern","year":"1983","unstructured":"Halpern, J., Moszkowski, B., Manna, Z.: A hardware semantics based on temporal intervals. In: D\u00edaz, J. (ed.) Automata, Languages and Programming. LNCS, vol.\u00a0154, pp. 278\u2013291. Springer, Heidelberg (1983)"},{"issue":"3","key":"38_CR5","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BF01211086","volume":"9","author":"M.R. Hansen","year":"1997","unstructured":"Hansen, M.R., Chaochen, Z.: Duration Calculus: Logical foundations. Formal Aspects of Computing\u00a09(3), 283\u2013330 (1997)","journal-title":"Formal Aspects of Computing"},{"key":"38_CR6","doi-asserted-by":"crossref","unstructured":"Kohl, J., Neuman, C.: RFC1510: The Kerberos network authentication service (V5). IETF (September 1993)","DOI":"10.17487\/rfc1510"},{"key":"38_CR7","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1109\/CSFW.1996.503701","volume-title":"Proc. of the 9th IEEE Security Foundations Workshop","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Some new attacks upon security protocols. In: Proc. of the 9th IEEE Security Foundations Workshop, pp. 162\u2013169. IEEE Computer Society Press, Los Alamitos (1996)"},{"issue":"1\/2","key":"38_CR8","doi-asserted-by":"crossref","first-page":"143","DOI":"10.3233\/JCS-2001-91-206","volume":"9","author":"C. Meadows","year":"2001","unstructured":"Meadows, C.: A cost-based framework for analysis of denial-of-service in networks. Journal of Computer Security\u00a09(1\/2), 143\u2013164 (2001)","journal-title":"Journal of Computer Security"},{"key":"38_CR9","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":"S. M\u00f8rk","year":"1996","unstructured":"M\u00f8rk, S., Godskesen, J.C., Hansen, M.R., Sharp, R.: A timed semantics for SDL. In: Formal Description Techniques IX: Theory, application and tools, pp. 295\u2013309. Chapman & Hall, Sydney, Australia (1996)"},{"issue":"2","key":"38_CR10","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B. Moszkowski","year":"1985","unstructured":"Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Computer\u00a018(2), 10\u201319 (1985)","journal-title":"IEEE Computer"},{"issue":"12","key":"38_CR11","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Communications of the ACM"},{"key":"38_CR12","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"38_CR13","unstructured":"Pilegaard, H.: Modelling properties of security protocols. Master\u2019s thesis, Informatics and Mathematical Modelling, Technical University of Denmark (October 2002)"},{"issue":"4","key":"38_CR14","first-page":"337","volume":"10","author":"H. Pilegaard","year":"2003","unstructured":"Pilegaard, H., Hansen, M.R., Sharp, R.: An approach to analyzing availability properties of security protocols. Nordic Journal of Computing\u00a010(4), 337\u2013373 (2003)","journal-title":"Nordic Journal of Computing"},{"key":"38_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-45653-8_22","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T.M. Rasmussen","year":"2001","unstructured":"Rasmussen, T.M.: Automated proof support for interval logics. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 317\u2013326. Springer, Heidelberg (2001)"},{"key":"38_CR16","unstructured":"Rasmussen, T.M.: Interval Logic \u2013 Proof Theory and Theorem Proving. PhD thesis, Informatics and Mathematical Modelling, Technical University of Denmark (2002)"},{"issue":"1","key":"38_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/32.210306","volume":"19","author":"A.P. Ravn","year":"1993","unstructured":"Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Trans. on Software Engineering\u00a019(1), 41\u201355 (1993)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"38_CR18","volume-title":"Proc. of the 8th IEEE Security Foundations Workshop","author":"A.W. Roscoe","year":"1995","unstructured":"Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: Proc. of the 8th IEEE Security Foundations Workshop, IEEE Comp. Soc. Press, Los Alamitos (1995)"},{"key":"38_CR19","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J. Thayer F\u00e1brega","year":"1999","unstructured":"Thayer F\u00e1brega, F.J., Herzog, J.C., Guttman, J.D.: Strand Spaces: Proving security protocols correct. Journal of Computer Security\u00a07, 191\u2013230 (1999)","journal-title":"Journal of Computer Security"},{"key":"38_CR20","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1109\/SECPRI.1988.8111","volume-title":"1988 IEEE Symposium on Security and Privacy","author":"C.-F. Yu","year":"1988","unstructured":"Yu, C.-F., Gligor, V.D.: A formal specification and verification method for the prevention of denial of service. In: 1988 IEEE Symposium on Security and Privacy, pp. 187\u2013202. IEEE Comp. Soc. Press, Los Alamitos (1988)"},{"key":"38_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"756","DOI":"10.1007\/3-540-58468-4_194","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"Z. Yuhua","year":"1994","unstructured":"Yuhua, Z., Chaochen, Z.: A formal proof of the deadline driven scheduler. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol.\u00a0863, pp. 756\u2013775. Springer, Heidelberg (1994)"},{"key":"38_CR22","series-title":"Monographs in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-06784-0","volume-title":"Duration Calculus: A Formal Approach to Real-Time Systems","author":"Z. Chaochen","year":"2004","unstructured":"Chaochen, Z., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"38_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/3-540-49213-5_23","volume-title":"Compositionality: The Significant Difference","author":"Z. Chaochen","year":"1998","unstructured":"Chaochen, Z., Hansen, M.R.: An adequate first order interval logic. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 581\u2013608. Springer, Heidelberg (1998)"},{"key":"38_CR24","series-title":"Lecture Notes in Computer Science","first-page":"21","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"Z. Chaochen","year":"1991","unstructured":"Chaochen, Z., Hansen, M.R., Ravn, A.P., Rischel, H.: Duration specifications for shared processors. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol.\u00a0571, pp. 21\u201332. Springer, Heidelberg (1991)"},{"issue":"5","key":"38_CR25","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters\u00a040(5), 269\u2013276 (1991)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Computer Science \u2013 Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74510-5_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:21:57Z","timestamp":1619504517000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74510-5_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745099","9783540745105"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74510-5_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}