{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:29Z","timestamp":1771024229764,"version":"3.50.1"},"reference-count":31,"publisher":"Oxford University Press (OUP)","issue":"2","license":[{"start":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T00:00:00Z","timestamp":1604275200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"Polish Minister of Science and Higher Education","award":["020\/RID\/2018\/19"],"award-info":[{"award-number":["020\/RID\/2018\/19"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,3,25]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>The paper presents a novel method for the verification of security protocols\u2019 (SPs)time properties. The new method uses a translation to satisfiability modulo theories (SMT) problem. In our approach, we model protocol users\u2019 behaviours using networks of synchronized timed automata. Suitably specified correctness properties are defined as a reachability property of some chosen states in an automata network. Then, the network of timed automata and the property are translated to an SMT problem and checked using an SMT-solver and a BMC algorithm. We consider the most important time properties of protocol executions using specially constructed time conditions. The new method was also implemented and experimentally evaluated for six well-known SPs. We also compared our new SMT-based technique with the corresponding SAT-based approach.<\/jats:p>","DOI":"10.1093\/jigpal\/jzaa062","type":"journal-article","created":{"date-parts":[[2020,9,29]],"date-time":"2020-09-29T21:01:32Z","timestamp":1601413292000},"page":"289-300","source":"Crossref","is-referenced-by-count":5,"title":["Practical Approach in Verification of Security Systems Using Satisfiability Modulo Theories"],"prefix":"10.1093","volume":"30","author":[{"given":"Agnieszka M","family":"Zbrzezny","sequence":"first","affiliation":[{"name":"Faculty of Mathematics and Computer Science, University of Warmia and Mazury in Olsztyn, 10-719 Olsztyn, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sabina","family":"Szymoniak","sequence":"additional","affiliation":[{"name":"Faculty of Mechanical Engineering and Computer Science, Czestochowa University of Technology, 42-201 Czestochowa, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miroslaw","family":"Kurkowski","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, Cardinal St. Wyszynski University, 07-938 Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2020,11,2]]},"reference":[{"key":"2022032112132590000_ref1","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","article-title":"A logic of authentication","volume":"8","author":"Burrows","year":"1990","journal-title":"ACM Transactions on Computer Systems"},{"key":"2022032112132590000_ref2","first-page":"234","article-title":"Reasoning about belief in cryptographic protocols","volume-title":"Proceedings of the IEEE Comp. Soc. Symp. on Research in Security and Privacy","author":"Gong","year":"1990"},{"key":"2022032112132590000_ref3","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/112600.112618","article-title":"A semantics for a logic of authentication (extended abstract)","volume-title":"Proceedings of PODC \u201891","author":"Abadi","year":"1991"},{"key":"2022032112132590000_ref4","first-page":"147","article-title":"Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR","volume-title":"Proceedings of the 2nd TACAS \u201896","author":"Lowe","year":"1996"},{"key":"2022032112132590000_ref5","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","article-title":"An attack on the Needham\u2013Schroeder public-key authentication protocol","volume":"56","author":"Lowe","year":"1995","journal-title":"Information Processing Letters"},{"key":"2022032112132590000_ref6","first-page":"281","article-title":"The AVISPA tool for the automated validation of internet security protocols and applications","volume-title":"CAV, 2005","author":"Armando","year":"2005"},{"key":"2022032112132590000_ref7","first-page":"414","article-title":"The Scyther tool: Verification, falsification, and analysis of security protocols","volume-title":"CAV, 2008","author":"Cremers","year":"2008"},{"key":"2022032112132590000_ref8","first-page":"223","article-title":"Applying timed automata to model checking of security protocols","volume-title":"Handbook of Finite State Based Models and Applications","author":"Kurkowski","year":"2012"},{"key":"2022032112132590000_ref9","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-662-49635-0_12","article-title":"AIF-$\\omega $: Set-based protocol abstraction with countable families","volume-title":"Principles of Security and Trust\u2014Proc. of 5th Int. Conf. POST","author":"M\u00f6dersheim","year":"2016"},{"key":"2022032112132590000_ref10","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1007\/978-3-319-10575-8_22","article-title":"Model checking security protocols","volume-title":"Handbook of Model Checking","author":"Basin","year":"2018"},{"key":"2022032112132590000_ref11","first-page":"451","article-title":"Formalizing and proving a typing result for security protocols in Isabelle\/HOL","volume-title":"Proceedings of the 30th IEEE Computer Security Foundations Symposium, CSF","author":"Hess","year":"2017"},{"key":"2022032112132590000_ref12","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1109\/CSF.2018.00034","article-title":"A typing result for stateful protocols","volume-title":"31st IEEE Computer Security Foundations Symposium, CSF 2018","author":"Hess","year":"2018"},{"key":"2022032112132590000_ref13","doi-asserted-by":"crossref","first-page":"157185","DOI":"10.1109\/ACCESS.2019.2948922","article-title":"Multifactor authentication protocol in a mobile environment","volume":"7","author":"Bart\u0142omiejczyk","year":"2019","journal-title":"IEEE Access"},{"key":"2022032112132590000_ref14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.3233\/JCS-181139","article-title":"Secure authentication in the grid: A formal analysis of DNP3 sav5","volume":"27","author":"Cremers","year":"2019","journal-title":"Journal of Computer Security"},{"key":"2022032112132590000_ref15","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"2022032112132590000_ref16","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying real-time properties with metric temporal logic","volume":"2","author":"Koymans","year":"1990","journal-title":"Real-Time Systems"},{"key":"2022032112132590000_ref17","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-32870-4","article-title":"Studies in Computational Intelligence","volume-title":"Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach","author":"Penczek","year":"2006"},{"key":"2022032112132590000_ref18","first-page":"53","article-title":"Timed analysis of security protocols","volume-title":"ISAT 2016\u2014Part II","author":"Szymoniak","year":"2016"},{"key":"2022032112132590000_ref19","first-page":"417","article-title":"Improvements in SAT-based reachability analysis for timed automata","volume":"60","author":"Zbrzezny","year":"2004","journal-title":"Fundamenta Informaticae"},{"key":"2022032112132590000_ref20","first-page":"363","article-title":"Modelling and checking timed authentication of security protocols","volume":"79","author":"Jakubowska","year":"2007","journal-title":"Fundamenta Informaticae"},{"key":"2022032112132590000_ref21","first-page":"344","article-title":"On some time aspects in security protocols analysis","volume-title":"CN 2018","author":"Szymoniak","year":"2018"},{"key":"2022032112132590000_ref22","doi-asserted-by":"crossref","first-page":"411","DOI":"10.3233\/FI-2017-1527","article-title":"SMT-based searching for k-quasi-optimal runs in weighted timed automata","volume":"152","author":"Wozna-Szczesniak","year":"2017","journal-title":"Fundamenta Informaticae"},{"key":"2022032112132590000_ref23","first-page":"337","article-title":"Z3: An efficient SMT solver","volume-title":"Proceedings of (TACAS\u20192008)","author":"De Moura","year":"2008"},{"key":"2022032112132590000_ref24","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/10721959_21","article-title":"Rewriting for cryptographic protocol verification","volume-title":"Automated Deduction\u2014CADE-17","author":"Genet","year":"2000"},{"key":"2022032112132590000_ref25","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/3-540-48294-6_10","article-title":"Abstracting cryptographic protocols with tree automata","volume-title":"Static Analysis, SAS \u201899","author":"Monniaux","year":"1999"},{"key":"2022032112132590000_ref26","doi-asserted-by":"crossref","DOI":"10.1145\/1029133.1029137","article-title":"Timed model checking of security protocols","volume-title":"Proceedings of the ACM Workshop on FMSE","author":"Corin","year":"2004"},{"key":"2022032112132590000_ref27","doi-asserted-by":"crossref","first-page":"619","DOI":"10.3233\/JCS-2007-15603","article-title":"Timed analysis of security protocols","volume":"15","author":"Corin","year":"2007","journal-title":"Journal of Computer Security"},{"key":"2022032112132590000_ref28","first-page":"127","article-title":"Timed models of security protocols including delays in the network","volume":"14","author":"Szymoniak","year":"2015","journal-title":"JAMCM Journal"},{"key":"2022032112132590000_ref29","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"2022032112132590000_ref30","first-page":"303","article-title":"SAT-based reachability checking for timed automata with diagonal constraints","volume":"67","author":"Zbrzezny","year":"2005","journal-title":"Fundamenta Informaticae"},{"key":"2022032112132590000_ref31","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1145\/358722.358740","article-title":"Timestamps in key distribution protocols","volume":"24","author":"Denning","year":"1981","journal-title":"Communications of the ACM"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/2\/289\/42901481\/jzaa062.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/2\/289\/42901481\/jzaa062.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,21]],"date-time":"2022-03-21T12:18:55Z","timestamp":1647865135000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/30\/2\/289\/5943717"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,2]]},"references-count":31,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2020,11,2]]},"published-print":{"date-parts":[[2022,3,25]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzaa062","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,4]]},"published":{"date-parts":[[2020,11,2]]}}}