{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:02:15Z","timestamp":1777806135608,"version":"3.51.4"},"reference-count":55,"publisher":"SAGE Publications","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCS"],"published-print":{"date-parts":[[2021,5,7]]},"abstract":"<jats:p>Protocol security verification is one of the best success stories of formal methods. However, some aspects important to protocol security, such as time and resources, are not covered by many formal models. While timing issues involve e.g., network delays and timeouts, resources such as memory, processing power, or network bandwidth are at the root of Denial of Service (DoS) attacks which have been a serious security concern. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable not only to powerful intruders, but also to resource-bounded intruders that cannot generate or intercept arbitrarily large volumes of traffic. A\u00a0refined Dolev\u2013Yao intruder model is proposed, that can only consume at most some specified amount of resources in any given time window. Timed protocol theories that specify service resource usage during protocol execution are also proposed. It is shown that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Additionally, we describe a decidable fragment in the verification of the leakage problem for resource-sensitive timed protocol theories.<\/jats:p>","DOI":"10.3233\/jcs-200012","type":"journal-article","created":{"date-parts":[[2021,2,26]],"date-time":"2021-02-26T12:31:37Z","timestamp":1614342697000},"page":"299-340","source":"Crossref","is-referenced-by-count":7,"title":["Resource and timing aspects of security protocols"],"prefix":"10.1177","volume":"29","author":[{"given":"Abra\u00e3o","family":"Aires\u00a0Urquiza","sequence":"first","affiliation":[{"name":"Federal University of Para\u00edba, Jo\u00e3o Pessoa, Brazil. E-mail:\u00a0abraauc@gmail.com"}]},{"given":"Musab\u00a0A.","family":"Alturki","sequence":"additional","affiliation":[{"name":"KFUPM, Dhahran, Saudi Arabia. E-mail:\u00a0musab@kfupm.edu.sa"},{"name":"Runtime Verification Inc., USA"}]},{"given":"Tajana","family":"Ban\u00a0Kirigin","sequence":"additional","affiliation":[{"name":"Department of Mathematics, University of Rijeka, Rijeka, Croatia. E-mail:\u00a0bank@math.uniri.hr"}]},{"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[{"name":"University College London, London, UK. E-mail:\u00a0m.kanovich@ucl.ac.uk"},{"name":"National Research University Higher School of Economics, Moscow, Russian Federation"}]},{"given":"Vivek","family":"Nigam","sequence":"additional","affiliation":[{"name":"fortiss, Germany. E-mail:\u00a0nigam@fortiss.org"},{"name":"Federal University of Para\u00edba, Jo\u00e3o Pessoa, Brazil. E-mail:\u00a0abraauc@gmail.com"}]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA. E-mail:\u00a0scedrov@math.upenn.edu"},{"name":"National Research University Higher School of Economics, Moscow, Russian Federation, until\u00a0July\u00a02020"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[{"name":"SRI International, Menlo Park, CA, USA. E-mail:\u00a0clt@csl.sri.com"}]}],"member":"179","reference":[{"key":"10.3233\/JCS-200012_ref1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.02.069","article-title":"Probabilistic modeling and analysis of DoS protection for the ASV protocol","volume":"234","author":"AlTurki","year":"2009","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10.3233\/JCS-200012_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19052-1_13"},{"key":"10.3233\/JCS-200012_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3264888.3264895"},{"issue":"2","key":"10.3233\/JCS-200012_ref4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A\u00a0theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.3233\/JCS-200012_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/948109.948140"},{"key":"10.3233\/JCS-200012_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2019599.2019601"},{"key":"10.3233\/JCS-200012_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055875"},{"issue":"4","key":"10.3233\/JCS-200012_ref8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/TDSC.2007.1005","article-title":"A\u00a0computationally sound mechanized prover for security protocols","volume":"5","author":"Blanchet","year":"2008","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"key":"10.3233\/JCS-200012_ref9","unstructured":"B.\u00a0Blanchet et al., An efficient cryptographic protocol verifier based on prolog rules, in: csfw, Vol.\u00a01, Citeseer, 2001, pp.\u00a082\u201396."},{"key":"10.3233\/JCS-200012_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/FiCloud.2014.72"},{"issue":"3\u20134","key":"10.3233\/JCS-200012_ref11","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1504\/IJTMCC.2013.056440","article-title":"Slow DoS attacks: Definition and categorisation","volume":"1","author":"Cambiaso","year":"2013","journal-title":"International Journal of Trust Management in Computing and Communications"},{"key":"10.3233\/JCS-200012_ref12","first-page":"54","article-title":"Mobile executions of slow DoS attacks","author":"Cambiaso","year":"2015","journal-title":"Logic Journal of IGPL"},{"key":"10.3233\/JCS-200012_ref13","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2001.959888"},{"key":"10.3233\/JCS-200012_ref15","unstructured":"I.\u00a0Cervesato, N.A.\u00a0Durgin, P.\u00a0Lincoln, J.C.\u00a0Mitchell and A.\u00a0Scedrov, A\u00a0meta-notation for protocol analysis, in: CSFW, 1999, pp.\u00a055\u201369."},{"key":"10.3233\/JCS-200012_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_15"},{"key":"10.3233\/JCS-200012_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14577-3_5"},{"key":"10.3233\/JCS-200012_ref18","unstructured":"M.\u00a0Clavel, F.\u00a0Dur\u00e1n, S.\u00a0Eker, P.\u00a0Lincoln, N.\u00a0Mart\u00ed-Oliet, J.\u00a0Meseguer and C.\u00a0Talcott, All About Maude: A\u00a0High-Performance Logical Framework, LNCS, Vol.\u00a04350, Springer, 2007."},{"key":"10.3233\/JCS-200012_ref19","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.17"},{"key":"10.3233\/JCS-200012_ref20","doi-asserted-by":"publisher","DOI":"10.1109\/JISIC.2014.21"},{"key":"10.3233\/JCS-200012_ref22","doi-asserted-by":"crossref","unstructured":"S.F.\u00a0Doghmi, J.D.\u00a0Guttman and F.J.\u00a0Thayer, Searching for shapes in cryptographic protocols, in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2007, pp.\u00a0523\u2013537.","DOI":"10.1007\/978-3-540-71209-1_41"},{"issue":"2","key":"10.3233\/JCS-200012_ref23","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEE Transactions on Information Theory"},{"issue":"2","key":"10.3233\/JCS-200012_ref24","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","article-title":"Multiset rewriting and the complexity of bounded security protocols","volume":"12","author":"Durgin","year":"2004","journal-title":"Journal of Computer Security"},{"key":"10.3233\/JCS-200012_ref25","doi-asserted-by":"crossref","unstructured":"J.\u00a0Eckhardt, T.\u00a0M\u00fchlbauer, M.\u00a0AlTurki, J.\u00a0Meseguer and M.\u00a0Wirsing, Stable availability under denial of service attacks through formal patterns, in: FASE, 2012, pp.\u00a078\u201393.","DOI":"10.1007\/978-3-642-28872-2_6"},{"key":"10.3233\/JCS-200012_ref26","doi-asserted-by":"crossref","unstructured":"J.\u00a0Eckhardt, T.\u00a0M\u00fchlbauer, J.\u00a0Meseguer and M.\u00a0Wirsing, Statistical model checking for composite actor systems, in: WADT, 2012, pp.\u00a0143\u2013160.","DOI":"10.1007\/978-3-642-37635-1_9"},{"key":"10.3233\/JCS-200012_ref27","isbn-type":"print","first-page":"I","volume-title":"A\u00a0Mathematical Introduction to Logic","author":"Enderton","year":"1972","ISBN":"https:\/\/id.crossref.org\/isbn\/9780122384509"},{"key":"10.3233\/JCS-200012_ref28","doi-asserted-by":"crossref","unstructured":"S.\u00a0Escobar, C.\u00a0Meadows and J.\u00a0Meseguer, Maude-NPA: Cryptographic protocol analysis modulo equational properties, in: Foundations of Security Analysis and Design, Vol.\u00a0V, Springer, 2009, pp.\u00a01\u201350.","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"10.3233\/JCS-200012_ref29","doi-asserted-by":"crossref","unstructured":"N.\u00a0Evans and S.\u00a0Schneider, Analysing time dependent security properties in CSP using PVS, in: Computer Security\u00a0\u2013 ESORICS 2000, 6th European Symposium on Research in Computer Security, Proceedings, Toulouse, France, October 4\u20136, 2000, 2000, pp.\u00a0222\u2013237.","DOI":"10.1007\/10722599_14"},{"key":"10.3233\/JCS-200012_ref30","doi-asserted-by":"crossref","unstructured":"R.\u00a0Gorrieri, E.\u00a0Locatelli and F.\u00a0Martinelli, A\u00a0simple language for real-time cryptographic protocol analysis, in: Proceedings of the 12th European Conference on Programming, ESOP\u201903, Springer-Verlag, Berlin, Heidelberg, 2003, pp.\u00a0114\u2013128, http:\/\/dl.acm.org\/citation.cfm?id=1765712.1765723. ISBN 3-540-00886-1.","DOI":"10.1007\/3-540-36575-3_9"},{"key":"10.3233\/JCS-200012_ref31","doi-asserted-by":"crossref","unstructured":"P.\u00a0Gupta and V.\u00a0Shmatikov, Security analysis of voice-over-IP protocols, in: 20th IEEE Computer Security Foundations Symposium, IEEE Computer Society, Venice, Italy, 2007, pp.\u00a049\u201363.","DOI":"10.1109\/CSF.2007.31"},{"issue":"3\u20134","key":"10.3233\/JCS-200012_ref34","first-page":"363","article-title":"Modelling and checking timed authentication of security protocols","volume":"79","author":"Jakubowska","year":"2007","journal-title":"Fundamenta Informaticae"},{"key":"10.3233\/JCS-200012_ref35","doi-asserted-by":"crossref","unstructured":"M.\u00a0Kanovich, T.\u00a0Ban Kirigin, V.\u00a0Nigam, A.\u00a0Scedrov and C.\u00a0Talcott, Discrete vs. dense times in the analysis of cyber-physical security protocols, in: Principles of Security and Trust\u00a0\u2013 4th International Conference, POST, 2015, pp.\u00a0259\u2013279.","DOI":"10.1007\/978-3-662-46666-7_14"},{"key":"10.3233\/JCS-200012_ref36","doi-asserted-by":"crossref","unstructured":"M.\u00a0Kanovich, T.\u00a0Ban Kirigin, V.\u00a0Nigam, A.\u00a0Scedrov and C.\u00a0Talcott, Timed multiset rewriting and the verification of time-sensitive distributed systems, in: 14th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2016.","DOI":"10.1007\/978-3-319-44878-7_14"},{"key":"10.3233\/JCS-200012_ref37","unstructured":"M.\u00a0Kanovich, T.\u00a0Ban Kirigin, V.\u00a0Nigam, A.\u00a0Scedrov and C.\u00a0Talcott, Can we mitigate the attacks on distance-bounding protocols by using challenge-response rounds repeatedly?, in: FCS, 2016."},{"key":"10.3233\/JCS-200012_ref39","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.19"},{"key":"10.3233\/JCS-200012_ref40","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ic.2014.07.011","article-title":"Bounded memory Dolev\u2013Yao adversaries in collaborative systems","volume":"238","author":"Kanovich","year":"2014","journal-title":"Inf. Comput."},{"issue":"6","key":"10.3233\/JCS-200012_ref41","doi-asserted-by":"publisher","first-page":"585","DOI":"10.3233\/JCS-0560","article-title":"Time, computational complexity, and probability in the analysis of distance-bounding protocols","volume":"25","author":"Kanovich","year":"2017","journal-title":"Journal of Computer Security"},{"issue":"3","key":"10.3233\/JCS-200012_ref43","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1017\/S096012951500016X","article-title":"A\u00a0rewriting framework and logic for activities subject to regulations","volume":"27","author":"Kanovich","year":"2017","journal-title":"Mathematical Structures in Computer Science"},{"issue":"3\u20134","key":"10.3233\/JCS-200012_ref44","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-010-9190-1","article-title":"Collaborative planning with confidentiality","volume":"46","author":"Kanovich","year":"2011","journal-title":"J.\u00a0Autom. Reasoning"},{"key":"10.3233\/JCS-200012_ref45","doi-asserted-by":"crossref","unstructured":"U.\u00a0Lee, J.-S.\u00a0Park, J.\u00a0Yeh, G.\u00a0Pau and M.\u00a0Gerla, Code torrent: Content distribution using network coding in VANET, in: Proceedings of the 1st International Workshop on Decentralized Resource Sharing in Mobile Computing and Networking, ACM, New York, NY, 2006, pp.\u00a01\u20135.","DOI":"10.1145\/1161252.1161254"},{"key":"10.3233\/JCS-200012_ref46","unstructured":"M.O.O.\u00a0Lemos, Y.G.\u00a0Dantas, I.\u00a0Fonseca, V.\u00a0Nigam and G.\u00a0Sampaio, A\u00a0selective defense for mitigating coordinated call attacks, in: 34th Brazilian Symposium on Computer Networks and Distributed Systems (SBRC), 2016."},{"key":"10.3233\/JCS-200012_ref47","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.jlamp.2017.09.001","article-title":"On the accuracy of formal verification of selective defenses for TDoS attacks","volume":"94","author":"Lemos","year":"2018","journal-title":"J.\u00a0Log. Algebr. Meth. Program."},{"key":"10.3233\/JCS-200012_ref48","doi-asserted-by":"crossref","unstructured":"G.\u00a0Lowe, Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR, in: TACAS, 1996, pp.\u00a0147\u2013166.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"10.3233\/JCS-200012_ref50","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00001"},{"issue":"1\/2","key":"10.3233\/JCS-200012_ref51","doi-asserted-by":"publisher","first-page":"143","DOI":"10.3233\/JCS-2001-91-206","article-title":"A\u00a0cost-based framework for analysis of denial of service networks","volume":"9","author":"Meadows","year":"2001","journal-title":"Journal of Computer Security"},{"key":"10.3233\/JCS-200012_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-46276-9_12"},{"key":"10.3233\/JCS-200012_ref53","doi-asserted-by":"publisher","DOI":"10.1016\/C2009-0-30680-7"},{"issue":"2","key":"10.3233\/JCS-200012_ref54","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/997150.997156","article-title":"A\u00a0taxonomy of DDoS attack and DDoS defense mechanisms","volume":"34","author":"Mirkovic","year":"2004","journal-title":"ACM SIGCOMM Computer Communication Review"},{"issue":"12","key":"10.3233\/JCS-200012_ref55","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","article-title":"Using encryption for authentication in large networks of computers","volume":"21","author":"Needham","year":"1978","journal-title":"Commun. ACM"},{"key":"10.3233\/JCS-200012_ref56","doi-asserted-by":"crossref","unstructured":"V.\u00a0Nigam, C.\u00a0Talcott and A.A.\u00a0Urquiza, Towards the automated verification of cyber-physical security protocols: Bounding the number of timed intruders, in: European Symposium on Research in Computer Security (ESORICS), 2016.","DOI":"10.1007\/978-3-319-45741-3_23"},{"key":"10.3233\/JCS-200012_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813680"},{"key":"10.3233\/JCS-200012_ref59","doi-asserted-by":"crossref","unstructured":"T.A.\u00a0Pascoal, Y.G.\u00a0Dantas, I.E.\u00a0Fonseca and V.\u00a0Nigam, Slow TCAM exhaustion DDoS attack, in: ICT Systems Security and Privacy Protection (IFIP SEC), 2017.","DOI":"10.1007\/978-3-319-58469-0_2"},{"key":"10.3233\/JCS-200012_ref60","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2020.107223"},{"issue":"1","key":"10.3233\/JCS-200012_ref63","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","article-title":"Rewriting modulo SMT and open system analysis","volume":"86","author":"Rocha","year":"2017","journal-title":"J.\u00a0Log. Algebr. Meth. Program."},{"key":"10.3233\/JCS-200012_ref66","doi-asserted-by":"crossref","unstructured":"R.\u00a0Shankesi, M.\u00a0AlTurki, R.\u00a0Sasse, C.A.\u00a0Gunter and J.\u00a0Meseguer, Model-checking DoS amplification for VoIP session initiation, in: ESORICS, 2009, pp.\u00a0390\u2013405.","DOI":"10.1007\/978-3-642-04444-1_24"},{"key":"10.3233\/JCS-200012_ref71","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00033"}],"container-title":["Journal of Computer Security"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JCS-200012","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:27Z","timestamp":1777495527000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/JCS-200012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,7]]},"references-count":55,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.3233\/jcs-200012","relation":{},"ISSN":["1875-8924","0926-227X"],"issn-type":[{"value":"1875-8924","type":"electronic"},{"value":"0926-227X","type":"print"}],"subject":[],"published":{"date-parts":[[2021,5,7]]}}}