{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:45:47Z","timestamp":1740181547179,"version":"3.37.3"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T00:00:00Z","timestamp":1656720000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T00:00:00Z","timestamp":1656720000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004488","name":"Croatian Science Foundation","doi-asserted-by":"crossref","award":["UIP-05-2017-9219"],"award-info":[{"award-number":["UIP-05-2017-9219"]}],"id":[{"id":"10.13039\/501100004488","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["R006865\/1"],"award-info":[{"award-number":["R006865\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009917","name":"U.S. Naval Research Laboratory","doi-asserted-by":"publisher","award":["N0017317-1-G002"],"award-info":[{"award-number":["N0017317-1-G002"]}],"id":[{"id":"10.13039\/100009917","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003593","name":"National Council for Scientific and Technological Development","doi-asserted-by":"crossref","award":["303909\/2018-8"],"award-info":[{"award-number":["303909\/2018-8"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000006","name":"U. S. Office of Naval Research","doi-asserted-by":"crossref","award":["N00014-20-1-2635","N00014-15-1-2202"],"award-info":[{"award-number":["N00014-20-1-2635","N00014-15-1-2202"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000006","name":"U. S. Office of Naval Research","doi-asserted-by":"crossref","award":["N00014-20-1-2644"],"award-info":[{"award-number":["N00014-20-1-2644"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100009917","name":"U.S. Naval Research Laboratory","doi-asserted-by":"publisher","award":["N0017317-1-G002"],"award-info":[{"award-number":["N0017317-1-G002"]}],"id":[{"id":"10.13039\/100009917","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["SN COMPUT. SCI."],"DOI":"10.1007\/s42979-022-01223-9","type":"journal-article","created":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T15:02:24Z","timestamp":1656774144000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Security and Complexity of Periodic Systems"],"prefix":"10.1007","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7957-1081","authenticated-orcid":false,"given":"Musab A.","family":"Alturki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tajana","family":"Ban Kirigin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vivek","family":"Nigam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,7,2]]},"reference":[{"key":"1223_CR1","unstructured":"Ademaj et\u00a0al. Time sensitive networks for flexible manufacturing testbed\u2014description of converged traffic types, IIC white paper 2019."},{"key":"1223_CR2","doi-asserted-by":"crossref","unstructured":"AlTurki MA, Kanovich M, Ban\u00a0Kirigin T, Nigam V, Scedrov A, Talcott C. Statistical model checking of distance fraud attacks on the Hancke-Kuhn family of protocols. In: Proceedings of the 2018\u00a0workshop on cyber-physical systems security and privacy, 60\u201371. ACM 2018.\u00a0https:\/\/dl.acm.org\/doi\/10.1145\/3264888.3264895","DOI":"10.1145\/3264888.3264895"},{"key":"1223_CR3","doi-asserted-by":"crossref","unstructured":"AlTurki MA, Ban\u00a0Kirigin T, Kanovich M, Nigam V, Scedrov A, Talcott C. On security analysis of periodic systems: expressiveness and complexity. In: ICISSP 2021-Proceedings of the 7th International Conference on information systems security and privacy. 2021;1:43\u201354.","DOI":"10.5220\/0010195100430054"},{"key":"1223_CR4","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y. Bounded model checking. Adv Comput. 2003;58:117\u201348.","journal-title":"Adv Comput"},{"key":"1223_CR5","unstructured":"Cyberattack has caused confirmed physical damage for the second time ever. 2015. https:\/\/www.wired.com\/2015\/01\/german-steel-mill-hack-destruction\/. Accessed 30 Sep 2021"},{"key":"1223_CR6","volume-title":"All about Maude: a high-performance logical framework, volume 4350 of LNCS","author":"M Clavel","year":"2007","unstructured":"Clavel M, Dur\u00e1n F, Eker S, Lincoln P, Mart\u00ed-Oliet N, Meseguer J, Talcott C. All about Maude: a high-performance logical framework, volume 4350 of LNCS. Berlin: Springer; 2007."},{"issue":"2","key":"1223_CR7","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 Trans Inf Theory. 1983;29(2):198\u2013208.","journal-title":"IEEE Trans Inf Theory"},{"issue":"2","key":"1223_CR8","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"NA Durgin","year":"2004","unstructured":"Durgin NA, Lincoln P, Mitchell JC, Scedrov A. Multiset rewriting and the complexity of bounded security protocols. J Comput Secur. 2004;12(2):247\u2013311.","journal-title":"J Comput Secur"},{"key":"1223_CR9","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"1972","unstructured":"Enderton HB. A mathematical introduction to logic. Cambridge: Academic Press; 1972."},{"key":"1223_CR10","unstructured":"ENISA. Good practices for security of internet of things in the context of smart manufacturing 2018. https:\/\/www.enisa.europa.eu\/publications\/good-practices-for-security-of-iot. Accessed 30 Sep 2021"},{"key":"1223_CR11","unstructured":"Fiat M, et al. OPC UA security analysis 2017. https:\/\/opcfoundation.org\/wp-content\/uploads\/2017\/04\/OPC_UA_security_analysis-OPC-F-Responses-2017_04_21.pdf. Accessed 30 Sep 2021"},{"key":"1223_CR12","doi-asserted-by":"crossref","unstructured":"Kanovich M, Ban Kirigin T, Nigam V, Scedrov A. Bounded memory protocols and progressing collaborative systems. In: Crampton J, Jajodia S, Mayes K, editors. Computer Security\u2014ESORICS. 2013;2013:309\u201326.","DOI":"10.1007\/978-3-642-40203-6_18"},{"key":"1223_CR13","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ic.2014.07.011","volume":"238","author":"MI Kanovich","year":"2014","unstructured":"Kanovich MI, Ban Kirigin T, Nigam V, Scedrov A. Bounded memory Dolev-Yao adversaries in collaborative systems. Inf Comput. 2014;238:233\u201361.","journal-title":"Inf Comput"},{"issue":"3","key":"1223_CR14","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1017\/S096012951500016X","volume":"27","author":"MI Kanovich","year":"2017","unstructured":"Kanovich MI, Ban Kirigin T, Nigam V, Scedrov A, Talcott CL, Perovic R. A rewriting framework and logic for activities subject to regulations. Math Struct Comput Sci. 2017;27(3):332\u201375.","journal-title":"Math Struct Comput Sci"},{"issue":"6","key":"1223_CR15","doi-asserted-by":"publisher","first-page":"585","DOI":"10.3233\/JCS-0560","volume":"25","author":"MI Kanovich","year":"2017","unstructured":"Kanovich MI, Ban Kirigin T, Nigam V, Scedrov A, Talcott CL. Time, computational complexity, and probability in the analysis of distance-bounding protocols. J Comput Secur. 2017;25(6):585\u2013630.","journal-title":"J Comput Secur"},{"issue":"3\u20134","key":"1223_CR16","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-010-9190-1","volume":"46","author":"MI Kanovich","year":"2011","unstructured":"Kanovich MI, Rowe P, Scedrov A. Collaborative planning with confidentiality. J Autom Reason. 2011;46(3\u20134):389\u2013421.","journal-title":"J Autom Reason"},{"issue":"1","key":"1223_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3373270","volume":"23","author":"R Lanotte","year":"2020","unstructured":"Lanotte R, Merro M, Munteanu A, Vigan\u00f2 L. A formal approach to physics-based attacks in cyber-physical systems. ACM Trans Priv Secur. 2020;23(1):1\u201341. https:\/\/dl.acm.org\/doi\/10.1145\/3373270","journal-title":"ACM Trans Priv Secur"},{"key":"1223_CR18","unstructured":"Leveson NG, Thomas JP. STPA handbook. 2018. https:\/\/psas.scripts.mit.edu\/home\/get_file.php?name=STPA_handbook.pdf. Accessed 30 Sep 2021"},{"key":"1223_CR19","doi-asserted-by":"crossref","unstructured":"Nigam V, Talcott C. Formal security verification of industry 4.0 applications. In: The 24th IEEE International Conference on emerging technologies and factory automation (ETFA), special track on cybersecurity in industrial control systems, 2019;1043\u20131050.\u00a0https:\/\/ieeexplore.ieee.org\/document\/8869428","DOI":"10.1109\/ETFA.2019.8869428"},{"key":"1223_CR20","doi-asserted-by":"crossref","unstructured":"Nigam V, Talcott C. Automated construction of security integrity wrappers for Industry 4.0 applications. In: The 13th International Workshop on rewriting logic and its applications, volume 12328 of LNCS, 2020; p. 197\u2013215.","DOI":"10.1007\/978-3-030-63595-4_11"},{"key":"1223_CR21","volume-title":"Models of computation","author":"JE Savage","year":"1998","unstructured":"Savage JE. Models of computation. Reading: Addison-Wesley; 1998."},{"issue":"3","key":"1223_CR22","doi-asserted-by":"publisher","first-page":"299","DOI":"10.3233\/JCS-200012","volume":"29","author":"AA Urquiza","year":"2021","unstructured":"Urquiza AA, AlTurki MA, Kanovich M, Ban Kirigin T, Nigam V, Scedrov A, Talcott C. Resource and timing aspects of security protocols. J Comput Secur. 2021;29(3):299\u2013340.","journal-title":"J Comput Secur"},{"key":"1223_CR23","doi-asserted-by":"crossref","unstructured":"Urquiza AA, AlTurki MA, Kanovich M, Ban Kirigin T, Nigam V, Scedrov A, Talcott C . Resource-bounded intruders in denial of service attacks. In: 32nd Computer Security Foundations Symposium (CSF), 2019; p. 382\u201396. IEEE.","DOI":"10.1109\/CSF.2019.00033"},{"key":"1223_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10521-5","volume-title":"Model-driven design using IEC 61499: a synchronous approach for embedded automation systems","author":"LH Yoong","year":"2015","unstructured":"Yoong LH, Roop PS, Bhatti ZE, Kupz MMY. Model-driven design using IEC 61499: a synchronous approach for embedded automation systems. Berlin: Springer; 2015."},{"key":"1223_CR25","doi-asserted-by":"crossref","unstructured":"Zoitl A, Lewis R. Modelling control systems using IEC 61499. In: Control Engineering Series 95. London: The Institution of Electrical Engineers; 2014. \u00a0 \u00a0 \u00a0 \u00a0 https:\/\/www.amazon.com\/Modelling-Control-Systems-Robotics-Sensors\/dp\/1849197601","DOI":"10.1049\/PBCE095E"}],"container-title":["SN Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-022-01223-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42979-022-01223-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-022-01223-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,28]],"date-time":"2024-09-28T09:53:54Z","timestamp":1727517234000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42979-022-01223-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,2]]},"references-count":25,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2022,9]]}},"alternative-id":["1223"],"URL":"https:\/\/doi.org\/10.1007\/s42979-022-01223-9","relation":{},"ISSN":["2661-8907"],"issn-type":[{"type":"electronic","value":"2661-8907"}],"subject":[],"published":{"date-parts":[[2022,7,2]]},"assertion":[{"value":"30 September 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 May 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 July 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declaration"}},{"value":"The authors declare that they have no conflicting or competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Code developed for this work is available at.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Code availibility"}}],"article-number":"356"}}