{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:31:42Z","timestamp":1762522302596,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030200046"},{"type":"electronic","value":"9783030200053"}],"license":[{"start":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T00:00:00Z","timestamp":1556409600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-20005-3_3","type":"book-chapter","created":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T09:04:21Z","timestamp":1556355861000},"page":"25-35","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Efficient Verification of Security Protocols Time Properties Using SMT Solvers"],"prefix":"10.1007","author":[{"given":"Agnieszka M.","family":"Zbrzezny","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sabina","family":"Szymoniak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miros\u0142aw","family":"Kurkowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,28]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: CAV 2005, Edinburgh, Scotland, UK, 6\u201310 July 2005, pp. 281\u2013285 (2005)","DOI":"10.1007\/11513988_27"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Basin, D., Cremers, C., Meadows, C.: Model Checking Security Protocols, pp. 727\u2013762. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_22"},{"issue":"1","key":"3_CR4","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.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18\u201336 (1990)","journal-title":"ACM Trans. Comput. Syst."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed model checking of security protocols. In: Proceedings of the ACM Workshop on FMSE. ACM (2004)","DOI":"10.1145\/1029133.1029137"},{"issue":"6","key":"3_CR6","doi-asserted-by":"publisher","first-page":"619","DOI":"10.3233\/JCS-2007-15603","volume":"15","author":"R Corin","year":"2007","unstructured":"Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed analysis of security protocols. J. Comput. Secur. 15(6), 619 (2007)","journal-title":"J. Comput. Secur."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Cremers, C.J.F.: The Scyther tool: verification, falsification, and analysis of security protocols. In: CAV 2008, Princeton, NJ, USA, 7\u201314 July 2008, pp. 414\u2013418 (2008)","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: Automated Deduction - CADE-17, Pittsburgh, PA, USA, 17\u201320 June 2000, pp. 271\u2013290 (2000)","DOI":"10.1007\/10721959_21"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Hess, A., M\u00f6dersheim, S.: A typing result for stateful protocols. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, pp. 374\u2013388 (2018)","DOI":"10.1109\/CSF.2018.00034"},{"issue":"3\u20134","key":"3_CR10","first-page":"363","volume":"79","author":"G Jakubowska","year":"2007","unstructured":"Jakubowska, G., Penczek, W.: Modelling and checking timed authentication of security protocols. Fundam. Inform. 79(3\u20134), 363\u2013378 (2007)","journal-title":"Fundam. Inform."},{"issue":"4","key":"3_CR11","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Kurkowski, M., Penczek, W.: Applying timed automata to model checking of security protocols. In: Handbook of Finite State Based Models and Applications, pp. 223\u2013254 (2012)","DOI":"10.1201\/b13055-12"},{"issue":"1\u20133","key":"3_CR13","first-page":"263","volume":"72","author":"M Kurkowski","year":"2006","unstructured":"Kurkowski, M., Srebrny, M.: A quantifier-free first-order knowledge logic of authentication. Fundam. Inform. 72(1\u20133), 263\u2013282 (2006)","journal-title":"Fundam. Inform."},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Abstracting cryptographic protocols with tree automata. In: Static Analysis, SAS 1999, Venice, Italy, Proceedings, pp. 149\u2013163 (1999)","DOI":"10.1007\/3-540-48294-6_10"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of (TACAS\u20192008). LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"12","key":"3_CR16","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Penczek, W., P\u00f3lrola, A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Studies in Computational Intelligence, vol. 20. Springer (2006)","DOI":"10.1007\/978-3-540-32870-4"},{"issue":"3","key":"3_CR18","doi-asserted-by":"publisher","first-page":"127","DOI":"10.17512\/jamcm.2015.3.14","volume":"14","author":"S Szymoniak","year":"2015","unstructured":"Szymoniak, S., Kurkowski, M., Pi\u0105tkowski, J.: Timed models of security protocols including delays in the network. J. Appl. Math. Comput. Mech. 14(3), 127\u2013139 (2015)","journal-title":"J. Appl. Math. Comput. Mech."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Szymoniak, S., Siedlecka-Lamch, O., Kurkowski, M.: Timed analysis of security protocols. In: ISAT 2016 - Part II, pp. 53\u201363 (2016)","DOI":"10.1007\/978-3-319-46586-9_5"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Szymoniak, S., Siedlecka-Lamch, O., Kurkowski, M.: On some time aspects in security protocols analysis. In: CN 2018, Proceedings, pp. 344\u2013356 (2018)","DOI":"10.1007\/978-3-319-92459-5_28"},{"issue":"3","key":"3_CR21","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/182110.182113","volume":"28","author":"TYC Woo","year":"1994","unstructured":"Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. SIGOPS Oper. Syst. Rev. 28(3), 24\u201337 (1994)","journal-title":"SIGOPS Oper. Syst. Rev."},{"issue":"4","key":"3_CR22","doi-asserted-by":"publisher","first-page":"411","DOI":"10.3233\/FI-2017-1527","volume":"152","author":"B Wozna-Szczesniak","year":"2017","unstructured":"Wozna-Szczesniak, B., Zbrzezny, A.M., Zbrzezny, A.: SMT-based searching for k-quasi-optimal runs in weighted timed automata. Fundam. Inform. 152(4), 411\u2013433 (2017)","journal-title":"Fundam. Inform."},{"issue":"1\u20134","key":"3_CR23","first-page":"417","volume":"60","author":"A Zbrzezny","year":"2004","unstructured":"Zbrzezny, A.: Improvements in SAT-based reachability analysis for timed automata. Fundam. Inform. 60(1\u20134), 417\u2013434 (2004)","journal-title":"Fundam. Inform."},{"issue":"1\u20133","key":"3_CR24","first-page":"303","volume":"67","author":"A Zbrzezny","year":"2005","unstructured":"Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundam. Inform. 67(1\u20133), 303\u2013322 (2005)","journal-title":"Fundam. Inform."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Zbrzezny, A.M., Wozna-Szczesniak, B., Zbrzezny, A.: SMT-based bounded model checking for weighted epistemic ECTL. In: EPIA 2015, Coimbra, Portugal, pp. 651\u2013657 (2015)","DOI":"10.1007\/978-3-319-23485-4_65"}],"container-title":["Advances in Intelligent Systems and Computing","International Joint Conference: 12th International Conference on Computational Intelligence in Security for Information Systems (CISIS 2019) and 10th International Conference on EUropean Transnational Education (ICEUTE 2019)"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20005-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T04:08:37Z","timestamp":1558152517000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20005-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,28]]},"ISBN":["9783030200046","9783030200053"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20005-3_3","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2019,4,28]]},"assertion":[{"value":"28 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CISIS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Computational Intelligence in Security for Information Systems Conference","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Seville","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cisis2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/2019.cisisconference.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}