{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:13Z","timestamp":1750221253378,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,15]],"date-time":"2018-01-15T00:00:00Z","timestamp":1515974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"King Fahd University of Petroleum and Minerals","award":["SL161003"],"award-info":[{"award-number":["SL161003"]}]},{"name":"Croatian Science Foundation","award":["UIP-05-2017-9219"],"award-info":[{"award-number":["UIP-05-2017-9219"]}]},{"name":"Office of Naval Research","award":["N00014-15-1-2202"],"award-info":[{"award-number":["N00014-15-1-2202"]}]},{"name":"Naval Research Laboratory","award":["N0017317-1-G002"],"award-info":[{"award-number":["N0017317-1-G002"]}]},{"name":"National Research University Higher School of Economics","award":["Russian Academic Excellence Project 5-100"],"award-info":[{"award-number":["Russian Academic Excellence Project 5-100"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,15]]},"DOI":"10.1145\/3264888.3264895","type":"proceedings-article","created":{"date-parts":[[2018,10,16]],"date-time":"2018-10-16T13:23:10Z","timestamp":1539696190000},"page":"60-71","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols"],"prefix":"10.1145","author":[{"given":"Musab A.","family":"Alturki","sequence":"first","affiliation":[{"name":"King Fahd University of Petroleum and Minerals & Runtime Verification Inc., Dhahran, Saudi Arabia"}]},{"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[{"name":"University College London & NRU HSE, London, United Kingdom"}]},{"given":"Tajana","family":"Ban Kirigin","sequence":"additional","affiliation":[{"name":"University of Rijeka, Rijeka, Croatia"}]},{"given":"Vivek","family":"Nigam","sequence":"additional","affiliation":[{"name":"Federal University of Para\u00edba & fortiss, Paraiba, Brazil"}]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[{"name":"University of Pennsylvania & NRU HSE, Philadelphia, PA, USA"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[{"name":"SRI International, Menlo Park, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,1,15]]},"reference":[{"volume-title":"Actors: a model of concurrent computation in distributed systems","author":"Agha Gul","key":"e_1_3_2_1_1_1","unstructured":"Gul Agha . 1986. Actors: a model of concurrent computation in distributed systems . MIT Press , Cambridge, MA, USA . Gul Agha. 1986. Actors: a model of concurrent computation in distributed systems .MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_1_2_1","volume-title":"Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories. In International Workshop on Foundations of Computer Security (FCS'05)","author":"Agha Gul","year":"2005","unstructured":"Gul Agha , Carl A. Gunter , Michael Greenwald , Sanjeev Khanna , Jos\u00e9 Meseguer , Koushik Sen , and Prasanna Thati . 2005 . Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories. In International Workshop on Foundations of Computer Security (FCS'05) . IEEE, Chicago, IL. Gul Agha, Carl A. Gunter, Michael Greenwald, Sanjeev Khanna, Jos\u00e9 Meseguer, Koushik Sen, and Prasanna Thati. 2005. Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories. In International Workshop on Foundations of Computer Security (FCS'05). IEEE, Chicago, IL."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"Alturki and Jos\u00e9 Meseguer","author":"Musab","year":"2011","unstructured":"Musab A. Alturki and Jos\u00e9 Meseguer . 2011 . PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. In Algebra and Coalgebra in Computer Science, Lecture Notes in Computer Science , Vol. 6859 . Springer Berlin \/ Heidelberg , 386--392. Musab A. Alturki and Jos\u00e9 Meseguer. 2011. PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. In Algebra and Coalgebra in Computer Science, Lecture Notes in Computer Science, Vol. 6859. Springer Berlin \/ Heidelberg, 386--392."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.069"},{"key":"e_1_3_2_1_6_1","first-page":"2","article-title":"A Framework for Analyzing RFID Distance Bounding Protocols","volume":"19","author":"Avoine Gildas","year":"2011","unstructured":"Gildas Avoine , Muhammed Ali Bing\u00f6l , S\u00fcleyman Kardacs , C\u00e9dric Lauradoux , and Benjamin Martin . 2011 . A Framework for Analyzing RFID Distance Bounding Protocols . J. Comput. Secur. , Vol. 19 , 2 (April 2011), 289--317. http:\/\/dl.acm.org\/citation.cfm?id=1971859.1971864 Gildas Avoine, Muhammed Ali Bing\u00f6l, S\u00fcleyman Kardacs, C\u00e9dric Lauradoux, and Benjamin Martin. 2011. A Framework for Analyzing RFID Distance Bounding Protocols. J. Comput. Secur. , Vol. 19, 2 (April 2011), 289--317. http:\/\/dl.acm.org\/citation.cfm?id=1971859.1971864","journal-title":"J. Comput. Secur."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3052973.3053000"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_1"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2019599.2019601"},{"volume-title":"Lightweight Cryptography for Security and Privacy","author":"Boureanu Ioana","key":"e_1_3_2_1_10_1","unstructured":"Ioana Boureanu , Aikaterini Mitrokotsa , and Serge Vaudenay . 2013. Secure and Lightweight Distance-Bounding . In Lightweight Cryptography for Security and Privacy , Springer Berlin Heidelberg , Berlin, Heidelberg , 97--113. Ioana Boureanu, Aikaterini Mitrokotsa, and Serge Vaudenay. 2013. Secure and Lightweight Distance-Bounding. In Lightweight Cryptography for Security and Privacy, Springer Berlin Heidelberg, Berlin, Heidelberg, 97--113."},{"key":"e_1_3_2_1_11_1","volume-title":"Advances in Cryptology -- EUROCRYPT '93: Workshop on the Theory and Application of Cryptographic Techniques Lofthus, Norway, May 23--27","author":"Brands Stefan","year":"1993","unstructured":"Stefan Brands and David Chaum . 1994. Distance-Bounding Protocols . In Advances in Cryptology -- EUROCRYPT '93: Workshop on the Theory and Application of Cryptographic Techniques Lofthus, Norway, May 23--27 , 1993 Proceedings, Tor Helleseth (Ed.). Springer , Berlin, Heidelberg, 344--359. Stefan Brands and David Chaum. 1994. Distance-Bounding Protocols. In Advances in Cryptology -- EUROCRYPT '93: Workshop on the Theory and Application of Cryptographic Techniques Lofthus, Norway, May 23--27, 1993 Proceedings, Tor Helleseth (Ed.). Springer, Berlin, Heidelberg, 344--359."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.04.012"},{"key":"e_1_3_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"Clavel Manuel","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Patrick Lincoln , Narciso Mart'i-Oliet , Jos\u00e9 Meseguer , and Carolyn Talcott . 2007. All About Maude - A High-Performance Logical Framework . Lecture Notes in Computer Science , Vol. 4350 . Springer-Verlag , Secaucus, NJ, USA . Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart'i-Oliet, Jos\u00e9 Meseguer, and Carolyn Talcott. 2007. All About Maude - A High-Performance Logical Framework. Lecture Notes in Computer Science, Vol. 4350. Springer-Verlag, Secaucus, NJ, USA."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.17"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/JISIC.2014.21"},{"key":"e_1_3_2_1_16_1","unstructured":"EasyCrypt. (last accessed: 2018-08--15). https:\/\/www.easycrypt.info\/trac\/.  EasyCrypt. (last accessed: 2018-08--15). https:\/\/www.easycrypt.info\/trac\/."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECURECOMM.2005.56"},{"key":"e_1_3_2_1_18_1","volume-title":"Workshop on Foundations of Computer Security .","author":"Kanovich Max","year":"2016","unstructured":"Max Kanovich , Tajana Ban Kirigin , Vivek Nigam , Andre Scedrov , and Carolyn Talcott . 2016 . Can we mitigate the attacks on Distance-Bounding Protocols by using challenge-response rounds repeatedly? . In Workshop on Foundations of Computer Security . Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, and Carolyn Talcott. 2016. Can we mitigate the attacks on Distance-Bounding Protocols by using challenge-response rounds repeatedly?. In Workshop on Foundations of Computer Security ."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-0560"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_10"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10433-6_9"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39958-2_3"},{"key":"e_1_3_2_1_23_1","volume-title":"Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM","author":"Liu Si","year":"2017","unstructured":"Si Liu , Peter Csaba \u00d6lveczky , Jatin Ganhotra , Indranil Gupta , and Jos\u00e9 Meseguer . 2017. Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking . In Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017 , Xi'an, China, November 13--17, 2017, Proceedings , Springer International Publishing , Cham, 298--314. Si Liu, Peter Csaba \u00d6lveczky, Jatin Ganhotra, Indranil Gupta, and Jos\u00e9 Meseguer. 2017. Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking. In Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13--17, 2017, Proceedings , Springer International Publishing, Cham, 298--314."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"volume-title":"Proc. WADT'97 (Lecture Notes in Computer Science)","author":"Meseguer Jos\u00e9","key":"e_1_3_2_1_25_1","unstructured":"Jos\u00e9 Meseguer . 1998. Membership algebra as a logical framework for equational specification . In Proc. WADT'97 (Lecture Notes in Computer Science) , , F. Parisi-Presicce (Ed.), Vol. 1376 . Springer , 18--61. Jos\u00e9 Meseguer. 1998. Membership algebra as a logical framework for equational specification. In Proc. WADT'97 (Lecture Notes in Computer Science), , F. Parisi-Presicce (Ed.), Vol. 1376. Springer, 18--61."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1455665.1455675"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.007"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.14"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.6"}],"event":{"name":"CCS '18: 2018 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Toronto Canada","acronym":"CCS '18"},"container-title":["Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and PrivaCy"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3264888.3264895","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3264888.3264895","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3264888.3264895","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:58Z","timestamp":1750212478000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3264888.3264895"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,15]]},"references-count":29,"alternative-id":["10.1145\/3264888.3264895","10.1145\/3264888"],"URL":"https:\/\/doi.org\/10.1145\/3264888.3264895","relation":{},"subject":[],"published":{"date-parts":[[2018,1,15]]},"assertion":[{"value":"2018-01-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}