{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:52:16Z","timestamp":1725749536029},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642409240"},{"type":"electronic","value":"9783642409257"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40925-7_25","type":"book-chapter","created":{"date-parts":[[2013,9,19]],"date-time":"2013-09-19T11:54:58Z","timestamp":1379591698000},"page":"265-276","source":"Crossref","is-referenced-by-count":2,"title":["Using Backward Induction Techniques in (Timed) Security Protocols Verification"],"prefix":"10.1007","author":[{"given":"Miros\u0142aw","family":"Kurkowski","sequence":"first","affiliation":[]},{"given":"Olga","family":"Siedlecka-Lamch","sequence":"additional","affiliation":[]},{"given":"Pawe\u0142","family":"Dudek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45510-8_4","volume-title":"Modeling and Verification of Parallel Processes","author":"T. Amnell","year":"2001","unstructured":"Amnell, T., et al.: UPPAAL - Now, Next, and Future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, pp. 99\u2013124. Springer, Heidelberg (2001)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"issue":"1","key":"25_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10207-007-0041-y","volume":"7","author":"A. Armando","year":"2008","unstructured":"Armando, A., Compagna, L.: Sat-based model-checking for security protocols analysis. International Journal of Information Security\u00a07(1), 3\u201332 (2008)","journal-title":"International Journal of Information Security"},{"issue":"1","key":"25_CR4","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1109\/JSAC.2002.806133","volume":"20","author":"G. Bella","year":"2003","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: Verifying the set registration protocols. IEEE Journal on Selected Areas in Communications\u00a020(1), 77\u201387 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"25_CR5","unstructured":"Bella, G., Paulson, L.C.: Using Isabelle to prove properties of the kerberos authentication system. In: Orman, H., Meadows, C. (eds.) Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)"},{"issue":"1","key":"25_CR6","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst.\u00a08(1), 18\u201336 (1990)","journal-title":"ACM Trans. Comput. Syst."},{"key":"25_CR7","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1109\/CSFW.2000.856933","volume-title":"CSFW 2000: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000)","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: TAPS: A first-order verifier for cryptographic protocols. In: CSFW 2000: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000), p. 144. IEEE Computer Society, Washington, DC (2000)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed model checking of security protocols. In: Proc. of the 2004 ACM Workshop FMSE, pp. 23\u201332. ACM (2004)","DOI":"10.1145\/1029133.1029137"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-540-24730-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"2004","unstructured":"Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 342\u2013356. Springer, Heidelberg (2004)"},{"issue":"2","key":"25_CR10","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a029(2), 198\u2013207 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"25_CR11","first-page":"241","volume":"41","author":"I. Fray El","year":"2012","unstructured":"El Fray, I., Kurkowski, M., Peja\u015b, J., Ma\u0107k\u00f3w, W.: A New Mathematical Model for the Analytical Risk Assessment and Prediction in IT Systems. Control & Cybernetics\u00a041, 241\u2013268 (2012); Systems Research Institute PAS, Warsaw","journal-title":"Control & Cybernetics"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722599_14","volume-title":"Computer Security - ESORICS 2000","author":"N. Evans","year":"2000","unstructured":"Evans, N., Schneider, S.: Analysing time dependent security properties in CSP using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol.\u00a01895. Springer, Heidelberg (2000)"},{"key":"25_CR13","unstructured":"Jakubowska, G., Penczek, W., Srebrny, M.: Verifying security protocols with timestamps via translation to timed automata. In: Proc. of the International Workshop on Concurrency, Specification and Programming (CS&P 2005), pp. 100\u2013115. Warsaw University (2005)"},{"issue":"1-4","key":"25_CR14","first-page":"313","volume":"85","author":"M. Kacprzak","year":"2008","unstructured":"Kacprzak, M., et al.: Verics 2007 - a model checker for knowledge and real-time. Fundam. Inform.\u00a085(1-4), 313\u2013328 (2008)","journal-title":"Fundam. Inform."},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-1-4419-9226-0_24","volume-title":"Artificial Intelligence and Security in Computing Systems","author":"M. Kurkowski","year":"2003","unstructured":"Kurkowski, M., Ma\u0107k\u00f3w, W.: Using Backward Strategy to the Needham-Schroeder Public Key Protocol Verification. In: Artificial Intelligence and Security in Computing Systems, pp. 249\u2013260. Kluwer Academic Publishers, Boston (2003)"},{"key":"25_CR16","first-page":"157","volume-title":"Artificial Intelligence and Security in Computing Systems","author":"M. Kurkowski","year":"2003","unstructured":"Kurkowski, M., Peja\u015b, J.: A Propositional Logic for Access Control Policy in Distributed Systems. In: Artificial Intelligence and Security in Computing Systems, pp. 157\u2013191. Kluwer Academic Publishers, Boston (2003)"},{"issue":"3-4","key":"25_CR17","first-page":"453","volume":"79","author":"M. Kurkowski","year":"2007","unstructured":"Kurkowski, M., Penczek, W.: Verifying Security Protocols Modeled by Networks of Automata. Fund. Inform.\u00a079(3-4), 453\u2013471 (2007)","journal-title":"Fund. Inform."},{"issue":"1-3","key":"25_CR18","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/FI-2009-0100","volume":"93","author":"M. Kurkowski","year":"2009","unstructured":"Kurkowski, M., Penczek, W.: Verifying Timed Security Protocols via Translation to Timed Automata. Fund. Inform.\u00a093(1-3), 245\u2013259 (2009)","journal-title":"Fund. Inform."},{"key":"25_CR19","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1201\/b13055-12","volume-title":"Handbook of Finite State Based Models and Applications","author":"M. Kurkowski","year":"2012","unstructured":"Kurkowski, M., Penczek, W.: Applying Timed Automata to Model Checking of Security Protocols. In: Wang, J. (ed.) Handbook of Finite State Based Models and Applications, pp. 223\u2013254. Chapman&Hall\/CRC Press, Boca Raton (2012)"},{"key":"25_CR20","first-page":"263","volume":"72","author":"M. Kurkowski","year":"2006","unstructured":"Kurkowski, M., Srebrny, M.: A Quantifier-free First-order Knowledge Logic of Authentication. Fund. Inform.\u00a072, 263\u2013282 (2006)","journal-title":"Fund. Inform."},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-key Protocol Using fdr. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"25_CR22","unstructured":"Lowe, G.: Some new attacks upon security protocols. In: Proceedings of the Computer Security Foundations Workshop VIII. IEEE Computer Society Press (1996)"},{"issue":"2","key":"25_CR23","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming\u00a026(2), 13\u2013131 (1996)","journal-title":"Journal of Logic Programming"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Moore, J.H.: Protocol failures in cryptosystems. Proceedings of the IEEE\u00a076(5) (1988)","DOI":"10.1109\/5.4444"},{"issue":"12","key":"25_CR25","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. Commun. ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"issue":"3","key":"25_CR26","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: Inductive analysis of the internet protocol tls. ACM Trans. Inf. Syst. Secur.\u00a02(3), 332\u2013351 (1999)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"25_CR27","first-page":"191","volume-title":"Proceedings of 21st International Workshop on Concurrency, Specification and Programming (CS&P 2012)","author":"O. Siedlecka-Lamch","year":"2012","unstructured":"Siedlecka-Lamch, O., Kurkowski, M., Piech, H.: A New Effective Approach for Modeling and Verification of Security Protocols. In: Proceedings of 21st International Workshop on Concurrency, Specification and Programming (CS&P 2012), pp. 191\u2013202. Humboldt University Press, Berlin (2012)"}],"container-title":["Lecture Notes in Computer Science","Computer Information Systems and Industrial Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40925-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,4]],"date-time":"2020-08-04T06:27:21Z","timestamp":1596522441000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40925-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642409240","9783642409257"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40925-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}