{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:04:52Z","timestamp":1743026692858,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171377"},{"type":"electronic","value":"9783030171384"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17138-4_7","type":"book-chapter","created":{"date-parts":[[2019,4,2]],"date-time":"2019-04-02T14:04:43Z","timestamp":1554213883000},"page":"149-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Symbolic Verification of Distance Bounding Protocols"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Debant","sequence":"first","affiliation":[]},{"given":"St\u00e9phanie","family":"Delaune","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 104\u2013115. ACM Press (2001)","DOI":"10.1145\/373243.360213"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Avoine, G., et al.: A terrorist-fraud resistant and extractor-free anonymous distance-bounding protocol. In: Proceedings of the 12th ACM Asia Conference on Computer and Communications Security (AsiaCCS 2017), pp. 800\u2013814. ACM (2017)","DOI":"10.1145\/3052973.3053000"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Baelde, D., Delaune, S., Gazeau, I., Kremer, S.: Symbolic verification of privacy-type properties for security protocols with XOR. In: 2017 IEEE 30th Computer Security Foundations Symposium (CSF), pp. 234\u2013248. IEEE (2017)","DOI":"10.1109\/CSF.2017.22"},{"issue":"2","key":"7_CR4","first-page":"1","volume":"13","author":"D Baelde","year":"2017","unstructured":"Baelde, D., Delaune, S., Hirschi, L.: A reduced semantics for deciding trace equivalence. Log. Methods Comput. Sci. 13(2), 1\u201348 (2017)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2","key":"7_CR5","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/2019599.2019601","volume":"14","author":"D Basin","year":"2011","unstructured":"Basin, D., Capkun, S., Schaller, P., Schmidt, B.: Formal reasoning about physical properties of security protocols. ACM Trans. Inf. Syst. Secur. (TISSEC) 14(2), 16 (2011)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"issue":"3","key":"7_CR6","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"DA Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181\u2013208 (2005)","journal-title":"Int. J. Inf. Secur."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: Proceedings of the 38th IEEE Symposium on Security and Privacy (S&P 2017), pp. 483\u2013502 (2017)","DOI":"10.1109\/SP.2017.26"},{"issue":"1\u20132","key":"7_CR8","first-page":"1","volume":"1","author":"B Blanchet","year":"2016","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. Found. Trends Priv. Secur. 1(1\u20132), 1\u2013135 (2016)","journal-title":"Found. Trends Priv. Secur."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Symbolic and computational mechanized verification of the ARINC823 avionic protocols. In: Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF 2017), pp. 68\u201382. IEEE (2017)","DOI":"10.1109\/CSF.2017.7"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-48285-7_30","volume-title":"Advances in Cryptology \u2014 EUROCRYPT 1993","author":"S Brands","year":"1994","unstructured":"Brands, S., Chaum, D.: Distance-bounding protocols. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 344\u2013359. Springer, Heidelberg (1994). \n                    https:\/\/doi.org\/10.1007\/3-540-48285-7_30"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Bultel, X., Gambs, S., Gerault, D., Lafourcade, P., Onete, C., Robert, J.: A prover-anonymous and terrorist-fraud resistant distance-bounding protocol. In: Proceedings of the 9th ACM Conference on Security & Privacy in Wireless and Mobile Networks, WISEC 2016, Darmstadt, Germany, 18\u201322 July 2016, pp. 121\u2013133. ACM (2016)","DOI":"10.1145\/2939918.2939919"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocol. ACM Trans. Comput. Logic 23(4), 23:1\u201323:32 (2016)","DOI":"10.1145\/2926715"},{"key":"7_CR13","unstructured":"Chothia, T., de Ruiter, J., Smyth, B.: Modelling and analysis of a hierarchy of distance bounding attacks. In: Proceedings of the 27th USENIX Security Symposium (USENIX 2018), pp. 1563\u20131580. USENIX Association (2018)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-662-47854-7_11","volume-title":"Financial Cryptography and Data Security","author":"T Chothia","year":"2015","unstructured":"Chothia, T., Garcia, F.D., de Ruiter, J., van den Breekel, J., Thompson, M.: Relay cost bounding for contactless EMV payments. In: B\u00f6hme, R., Okamoto, T. (eds.) FC 2015. LNCS, vol. 8975, pp. 189\u2013206. Springer, Heidelberg (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-662-47854-7_11"},{"issue":"2","key":"7_CR15","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/1656242.1656244","volume":"11","author":"H Comon-Lundh","year":"2010","unstructured":"Comon-Lundh, H., Cortier, V., Z\u0103linescu, E.: Deciding security properties for cryptographic protocols. Application to key cycles. ACM Trans. Comput. Logic 11(2), 9 (2010)","journal-title":"ACM Trans. Comput. Logic"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: Proceedings of the 24th ACM Conference on Computer and Communications Security (CCS 2017), pp. 1773\u20131788 (2017)","DOI":"10.1145\/3133956.3134063"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Debant, A., Delaune, S.: Symbolic verification of distance bounding protocols. Research report, Univ Rennes, CNRS, IRISA, France, February 2019","DOI":"10.1007\/978-3-030-17138-4_7"},{"key":"7_CR19","unstructured":"Debant, A., Delaune, S., Wiedling, C.: A symbolic framework to analyse physical proximity in security protocols. In: Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). LIPICS (2018)"},{"issue":"2","key":"7_CR20","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 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. theory"},{"key":"7_CR21","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Proceedings of the Workshop on Formal Methods and Security Protocols (FMSP 1999), Trento, Italy (1999)"},{"key":"7_CR22","unstructured":"EMVCo: EMV contactless specifications for payment systems, version 2.6 (2016)"},{"key":"7_CR23","unstructured":"Hancke, G.P., Kuhn, M.G.: An RFID distance bounding protocol. In: Proceedings of the 1st International Conference on Security and Privacy for Emerging Areas in Communications Networks (SECURECOMM 2005), pp. 67\u201373. IEEE (2005)"},{"key":"7_CR24","unstructured":"Janssens, P.: Proximity check for communication devices. US Patent 9,805,228, 31 October 2017"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-00730-9_7","volume-title":"Information Security and Cryptology \u2013 ICISC 2008","author":"CH Kim","year":"2009","unstructured":"Kim, C.H., Avoine, G., Koeune, F., Standaert, F.-X., Pereira, O.: The Swiss-Knife RFID distance bounding protocol. In: Lee, P.J., Cheon, J.H. (eds.) ICISC 2008. LNCS, vol. 5461, pp. 98\u2013115. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-00730-9_7"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Mauw, S., Smith, Z., Toro-Pozo, J., Trujillo-Rasua, R.: Distance-bounding protocols: verification without time and location. In: Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P 2018), pp. 152\u2013169 (2018)","DOI":"10.1109\/SP.2018.00001"},{"key":"7_CR27","series-title":"Advances in Information Security","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-0-387-46276-9_12","volume-title":"Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks","author":"C Meadows","year":"2007","unstructured":"Meadows, C., Poovendran, R., Pavlovic, D., Chang, L., Syverson, P.: Distance bounding protocols: authentication logic analysis and collusion attacks. In: Poovendran, R., Roy, S., Wang, C. (eds.) Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks. ADIS, vol. 30, pp. 279\u2013298. Springer, Boston (2007). \n                    https:\/\/doi.org\/10.1007\/978-0-387-46276-9_12"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM Conference on Computer and Communications Security (CCS 2001). ACM Press (2001)","DOI":"10.1145\/501983.502007"},{"issue":"4","key":"7_CR30","doi-asserted-by":"publisher","first-page":"575","DOI":"10.3233\/JCS-2009-0351","volume":"18","author":"S M\u00f6dersheim","year":"2010","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L., Basin, D.A.: Constraint differentiation: search-space reduction for the constraint-based analysis of security protocols. J. Comput. Secur. 18(4), 575\u2013618 (2010)","journal-title":"J. Comput. Secur."},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-319-45741-3_23","volume-title":"Computer Security \u2013 ESORICS 2016","author":"V Nigam","year":"2016","unstructured":"Nigam, V., Talcott, C., Aires Urquiza, A.: Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 450\u2013470. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-45741-3_23"},{"issue":"1\u20133","key":"7_CR32","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/S0304-3975(02)00490-5","volume":"299","author":"M Rusinowitch","year":"2003","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. Theoret. Comput. Sci. 299(1\u20133), 451\u2013475 (2003)","journal-title":"Theoret. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17138-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:17:57Z","timestamp":1558343877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17138-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171377","9783030171384"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17138-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"POST","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Principles of Security and Trust","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"post2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/post","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}