{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T10:17:14Z","timestamp":1774261034096,"version":"3.50.1"},"reference-count":39,"publisher":"SAGE Publications","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCS"],"published-print":{"date-parts":[[2017,8,24]]},"DOI":"10.3233\/jcs-0560","type":"journal-article","created":{"date-parts":[[2017,8,1]],"date-time":"2017-08-01T16:29:17Z","timestamp":1501604957000},"page":"585-630","source":"Crossref","is-referenced-by-count":14,"title":["Time, computational complexity, and\u00a0probability in the analysis of\u00a0distance-bounding protocols"],"prefix":"10.1177","volume":"25","author":[{"given":"Max","family":"Kanovich","sequence":"first","affiliation":[{"name":"Department of Computer Science (UCL-CS), University College London, London, UK. E-mail:\u00a0m.kanovich@ucl.ac.uk"},{"name":"Faculty of Computer Science, National Research University Higher School of Economics, Moscow, Russian Federation"}]},{"given":"Tajana","family":"Ban Kirigin","sequence":"additional","affiliation":[{"name":"Department of Mathematics, University of Rijeka, Rijeka, Croatia. E-mail:\u00a0bank@math.uniri.hr"}]},{"given":"Vivek","family":"Nigam","sequence":"additional","affiliation":[{"name":"Computer Science Department, Federal University of Para\u00edba, Jo\u00e3o Pessoa, Brazil. E-mail:\u00a0vivek@ci.ufpb.br"},{"name":"fortiss, Munich, Germany"}]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[{"name":"Faculty of Computer Science, National Research University Higher School of Economics, Moscow, Russian Federation"},{"name":"Department of Mathematics, University of Pennsylvania, Philadelphia, PA, USA. E-mail:\u00a0scedrov@math.upenn.edu"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[{"name":"Computer Science Laboratory, SRI International, Menlo Park, CA, USA. E-mail:\u00a0clt@csl.sri.com"}]}],"member":"179","reference":[{"key":"10.3233\/JCS-0560_ref1","unstructured":"R.\u00a0Alur, Principles of Cyber-Physical Systems, MIT Press, 2015."},{"key":"10.3233\/JCS-0560_ref2","doi-asserted-by":"crossref","unstructured":"R.\u00a0Alur and P.\u00a0Madhusudan, Decision problems for timed automata: A survey, in: SFM, 2004, pp.\u00a01\u201324.","DOI":"10.1007\/978-3-540-30080-9_1"},{"key":"10.3233\/JCS-0560_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2019599.2019601"},{"key":"10.3233\/JCS-0560_ref5","doi-asserted-by":"crossref","unstructured":"S.\u00a0Brands and D.\u00a0Chaum, Distance-bounding protocols (extended abstract), in: EUROCRYPT, 1993, pp.\u00a0344\u2013359.","DOI":"10.1007\/3-540-48285-7_30"},{"issue":"2","key":"10.3233\/JCS-0560_ref6","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/JSAC.2005.861380","article-title":"Secure positioning in wireless networks","volume":"24","author":"Capkun","year":"2006","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"10.3233\/JCS-0560_ref7","unstructured":"I.\u00a0Cervesato, N.A.\u00a0Durgin, P.\u00a0Lincoln, J.C.\u00a0Mitchell and A.\u00a0Scedrov, A meta-notation for protocol analysis, in: CSFW, 1999, pp.\u00a055\u201369."},{"key":"10.3233\/JCS-0560_ref8","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cheval and V.\u00a0Cortier, Timing attacks in security protocols: Symbolic framework and proof techniques, in: Principles of Security and Trust \u2013 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings, London, UK, April 11\u201318, 2015, pp.\u00a0280\u2013299.","DOI":"10.1007\/978-3-662-46666-7_15"},{"key":"10.3233\/JCS-0560_ref9","doi-asserted-by":"crossref","unstructured":"T.\u00a0Chothia, F.D.\u00a0Garcia, J.\u00a0de\u00a0Ruiter, J.\u00a0van den Breekel and M.\u00a0Thompson, Relay cost bounding for contactless EMV payments, in: Financial Cryptography and Data Security, 2015.","DOI":"10.1007\/978-3-662-47854-7_11"},{"key":"10.3233\/JCS-0560_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14577-3_5"},{"key":"10.3233\/JCS-0560_ref11","unstructured":"M.\u00a0Clavel, F.\u00a0Dur\u00e1n, S.\u00a0Eker, P.\u00a0Lincoln, N.\u00a0Mart\u00ed-Oliet, J.\u00a0Meseguer and C.\u00a0Talcott, All About Maude: A High-Performance Logical Framework, LNCS, Vol.\u00a04350, 2007."},{"issue":"6","key":"10.3233\/JCS-0560_ref12","doi-asserted-by":"publisher","first-page":"619","DOI":"10.3233\/JCS-2007-15603","article-title":"Timed analysis of security protocols","volume":"15","author":"Corin","year":"2007","journal-title":"J. Comput. Secur."},{"key":"10.3233\/JCS-0560_ref13","doi-asserted-by":"crossref","unstructured":"C.J.F.\u00a0Cremers, K.B.\u00a0Rasmussen, B.\u00a0Schmidt and S.\u00a0Capkun, Distance hijacking attacks on distance bounding protocols, in: SP, 2012.","DOI":"10.1109\/SP.2012.17"},{"issue":"2","key":"10.3233\/JCS-0560_ref14","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-0560_ref15","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":"J. Comput. Secur."},{"key":"10.3233\/JCS-0560_ref16","unstructured":"H.B.\u00a0Enderton, A Mathematical Introduction to Logic, Academic Press, 1972."},{"key":"10.3233\/JCS-0560_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1380564.1380571"},{"key":"10.3233\/JCS-0560_ref18","doi-asserted-by":"crossref","unstructured":"G.\u00a0Hancke and M.\u00a0Kuhn, An RFID distance bounding protocol, in: First International Conference on Security and Privacy for Emerging Areas in Communications Networks (SECURECOMM\u201905), 2005, pp.\u00a067\u201373.","DOI":"10.1109\/SECURECOMM.2005.56"},{"key":"10.3233\/JCS-0560_ref19","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":"Information and Computation"},{"key":"10.3233\/JCS-0560_ref20","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: 4th Conference on Principles of Security and Trust (POST), London, UK, April, LNCS, Vol.\u00a09036, Springer-Verlag, 2015, pp.\u00a0259\u2013279.","DOI":"10.1007\/978-3-662-46666-7_14"},{"issue":"3","key":"10.3233\/JCS-0560_ref21","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1017\/S096012951500016X","article-title":"A rewriting framework and logic for activities subject to regulations","volume":"27","author":"Kanovich","year":"2017","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.3233\/JCS-0560_ref22","doi-asserted-by":"crossref","unstructured":"M.I.\u00a0Kanovich, T.\u00a0Ban Kirigin, V.\u00a0Nigam and A.\u00a0Scedrov, Bounded memory protocols and progressing collaborative systems, in: ESORICS, 2013, pp.\u00a0309\u2013326.","DOI":"10.1007\/978-3-642-40203-6_18"},{"issue":"3\u20134","key":"10.3233\/JCS-0560_ref23","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/j.cl.2014.05.003","article-title":"Bounded memory protocols","volume":"40","author":"Kanovich","year":"2014","journal-title":"Computer Languages, Systems & Structures"},{"key":"10.3233\/JCS-0560_ref25","unstructured":"M.I.\u00a0Kanovich, T.\u00a0Ban Kirigin, V.\u00a0Nigam, A.\u00a0Scedrov, C.L.\u00a0Talcott and R.\u00a0Perovic, A rewriting framework for activities subject to regulations, in: RTA, 2012, pp.\u00a0305\u2013322."},{"key":"10.3233\/JCS-0560_ref26","doi-asserted-by":"crossref","unstructured":"M.I.\u00a0Kanovich, P.\u00a0Rowe and A.\u00a0Scedrov, Policy compliance in collaborative systems, in: CSF \u201909: Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, 2009, pp.\u00a0218\u2013233.","DOI":"10.1109\/CSF.2009.19"},{"issue":"3\u20134","key":"10.3233\/JCS-0560_ref27","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. Autom. Reasoning"},{"issue":"5\u20136","key":"10.3233\/JCS-0560_ref28","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00236-010-0121-8","article-title":"Reachability results for timed automata with unbounded data structures","volume":"47","author":"Lanotte","year":"2010","journal-title":"Acta Inf."},{"key":"10.3233\/JCS-0560_ref29","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-0560_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-46276-9_12"},{"issue":"12","key":"10.3233\/JCS-0560_ref32","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-0560_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45741-3_23"},{"issue":"1\u20132","key":"10.3233\/JCS-0560_ref34","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","article-title":"Semantics and pragmatics of real-time Maude","volume":"20","author":"\u00d6lveczky","year":"2007","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"4","key":"10.3233\/JCS-0560_ref35","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2007.06.005","article-title":"Abstraction and completeness for real-time Maude","volume":"176","author":"\u00d6lveczky","year":"2007","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10.3233\/JCS-0560_ref36","doi-asserted-by":"crossref","unstructured":"D.\u00a0Pavlovic and C.\u00a0Meadows, Deriving ephemeral authentication using channel axioms, in: Security Protocols Workshop, 2009, pp.\u00a0240\u2013261.","DOI":"10.1007\/978-3-642-36213-2_27"},{"key":"10.3233\/JCS-0560_ref37","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.entcs.2010.08.007","article-title":"Bayesian authentication: Quantifying security of the Hancke\u2013Kuhn protocol","volume":"265","author":"Pavlovic","year":"2010","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10.3233\/JCS-0560_ref38","doi-asserted-by":"crossref","unstructured":"R.\u00a0Ramanujam and S.P.\u00a0Suresh, Tagging makes secrecy decidable with unbounded nonces as well, in: FST TCS, 2003.","DOI":"10.1007\/978-3-540-24597-1_31"},{"issue":"5","key":"10.3233\/JCS-0560_ref39","first-page":"132","article-title":"RFID based security system","volume":"2","author":"Ravi","year":"2013","journal-title":"International Journal of Innovative Technology and Exploring Engineering"},{"key":"10.3233\/JCS-0560_ref40","doi-asserted-by":"crossref","unstructured":"V.\u00a0Shmatikov and M.-H.\u00a0Wang, Secure verification of location claims with simultaneous distance modification, in: ASIAN, 2007, pp.\u00a0181\u2013195.","DOI":"10.1007\/978-3-540-76929-3_17"},{"key":"10.3233\/JCS-0560_ref41","doi-asserted-by":"crossref","unstructured":"K.\u00a0Sun, P.\u00a0Ning and C.\u00a0Wang, Tinysersync: Secure and resilient time synchronization in wireless sensor networks, in: CCS, 2006, pp.\u00a0264\u2013277.","DOI":"10.1145\/1180405.1180439"},{"key":"10.3233\/JCS-0560_ref42","doi-asserted-by":"crossref","unstructured":"N.O.\u00a0Tippenhauer and S.\u00a0Capkun, ID-based secure distance bounding and localization, in: ESORICS, 2009, pp.\u00a0621\u2013636.","DOI":"10.1007\/978-3-642-04444-1_38"}],"container-title":["Journal of Computer Security"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JCS-0560","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T19:46:29Z","timestamp":1750794389000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/JCS-0560"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,24]]},"references-count":39,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.3233\/jcs-0560","relation":{},"ISSN":["1875-8924","0926-227X"],"issn-type":[{"value":"1875-8924","type":"electronic"},{"value":"0926-227X","type":"print"}],"subject":[],"published":{"date-parts":[[2017,8,24]]}}}