{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T22:28:01Z","timestamp":1780352881285,"version":"3.54.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030916305","type":"print"},{"value":"9783030916312","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91631-2_2","type":"book-chapter","created":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T21:02:24Z","timestamp":1637269344000},"page":"22-49","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Protocol Analysis with Time and Space"],"prefix":"10.1007","author":[{"given":"Dami\u00e1n","family":"Aparicio-S\u00e1nchez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julia","family":"Sapi\u00f1a","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,11,19]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-030-65277-7_7","volume-title":"Progress in Cryptology \u2013 INDOCRYPT 2020","author":"D Aparicio-S\u00e1nchez","year":"2020","unstructured":"Aparicio-S\u00e1nchez, D., Escobar, S., Meadows, C., Meseguer, J., Sapi\u00f1a, J.: Protocol analysis with time. In: Bhargavan, K., Oswald, E., Prabhakaran, M. (eds.) INDOCRYPT 2020. LNCS, vol. 12578, pp. 128\u2013150. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-65277-7_7"},{"issue":"2","key":"2_CR2","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2019599.2019601","volume":"14","author":"DA Basin","year":"2011","unstructured":"Basin, D.A., Capkun, S., Schaller, P., Schmidt, B.: Formal reasoning about physical properties of security protocols. ACM Trans. Inf. Syst. Secur. 14(2), 16:1-16:28 (2011)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03359-9_1","volume-title":"Theorem Proving in Higher Order Logics","author":"D Basin","year":"2009","unstructured":"Basin, D., Capkun, S., Schaller, P., Schmidt, B.: Let\u2019s get physical: models and methods for real-world security protocols. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 1\u201322. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_1"},{"key":"2_CR4","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 \u201993","author":"S Brands","year":"1994","unstructured":"Brands, S., Chaum, D.: Distance-bounding protocols (Extended abstracts). In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 344\u2013359. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-48285-7_30"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Srdjan Capkun. Secure positioning and location-based security for IoT and beyond. In: Chang, C.-H., R\u00fchrmair, U., Holcomb, D.E., Guajardo, J., (eds.) Proceedings of the 2018 Workshop on Attacks and Solutions in Hardware Security, ASHES@CCS 2018, Toronto, ON, Canada, October 19, 2018, p. 81. ACM (2018)","DOI":"10.1145\/3266444.3266455"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Srdjan Capkun and Jean-Pierre Hubaux. Secure positioning of wireless devices with application to sensor networks. In INFOCOM 2005. 24th Annual Joint Conference of the IEEE Computer and Communications Societies, 13\u201317 March 2005, Miami, FL, USA, pages 1917\u20131928. IEEE, 2005","DOI":"10.1109\/INFCOM.2005.1498470"},{"issue":"2","key":"2_CR7","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/JSAC.2005.861380","volume":"24","author":"S Capkun","year":"2006","unstructured":"Capkun, S., Hubaux, J.-P.: Secure positioning in wireless networks. IEEE J. Sel. Areas Commun. 24(2), 221\u2013232 (2006)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-030-17138-4_7","volume-title":"Principles of Security and Trust","author":"A Debant","year":"2019","unstructured":"Debant, A., Delaune, S.: Symbolic verification of distance bounding protocols. In: Nielson, F., Sands, D. (eds.) POST 2019. LNCS, vol. 11426, pp. 149\u2013174. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17138-4_7"},{"issue":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoret. Comput. Sci. 367(1), 162\u2013202 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.ic.2014.07.007","volume":"238","author":"S Escobar","year":"2014","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the maude-NRL protocol analyzer. Inf. Comput. 238, 157\u2013186 (2014)","journal-title":"Inf. Comput."},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-319-25527-9_16","volume-title":"Programming Languages with Applications to Biology and Security","author":"S Escobar","year":"2015","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Symbolic protocol analysis with disequality constraints modulo equational theories. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 238\u2013261. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25527-9_16"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Leu, P., Singh, M., Roeschlin, M., Paterson, K.G., Capkun, S.: Message time of arrival codes: a fundamental primitive for secure distance measurement. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 500\u2013516 (2020)","DOI":"10.1109\/SP40000.2020.00010"},{"key":"2_CR13","unstructured":"Mathematica (2021). https:\/\/www.wolfram.com\/mathematica"},{"key":"2_CR14","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"2_CR15","first-page":"1","volume":"4120","author":"C Neumann","year":"2005","unstructured":"Neumann, C., Yu, T., Hartman, S., Raeburn, K.: The kerberos network authentication service (V5). Request Comments 4120, 1\u201337 (2005)","journal-title":"Request Comments"},{"key":"2_CR16","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). https:\/\/doi.org\/10.1007\/978-3-319-45741-3_23"},{"issue":"1\u20132","key":"2_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1\u20132), 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"2_CR18","first-page":"1","volume":"4082","author":"A Perrig","year":"2005","unstructured":"Perrig, A., Song, D., Canetti, R., Tygar, J.D., Briscoe, B.: Timed Efficient Stream Loss-Tolerant Authentication (TESLA): multicast source authentication transform introduction. Request Comments 4082, 1\u201322 (2005)","journal-title":"Request Comments"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Schaller, P., Schmidt, B., Basin, D.A., Capkun, S.: Modeling and verifying physical properties of security protocols for wireless networks. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, New York, USA, 8\u201310 July, pp. 109\u2013123. IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.6"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-76929-3_17","volume-title":"Advances in Computer Science \u2013 ASIAN 2007. Computer and Network Security","author":"V Shmatikov","year":"2007","unstructured":"Shmatikov, V., Wang, M.-H.: Secure verification of location claims with simultaneous distance modification. In: Cervesato, I. (ed.) ASIAN 2007. LNCS, vol. 4846, pp. 181\u2013195. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76929-3_17"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJ Thayer","year":"1999","unstructured":"Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"2_CR22","unstructured":"Yang, F., Escobar, S., Meadows, C., Meseguer, J.: Strand spaces with choice via a process algebra semantics. Computing Research Repository (2019)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Yang, F., Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), pp. 76\u201389. ACM Press (2016)","DOI":"10.1145\/2967973.2968609"},{"key":"2_CR24","unstructured":"The Yices SMT Solver (2021). https:\/\/yices.csl.sri.com"},{"key":"2_CR25","unstructured":"The Z3 SMT Solver (2021). https:\/\/github.com\/Z3Prover\/z3"}],"container-title":["Lecture Notes in Computer Science","Protocols, Strands, and Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91631-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T16:08:30Z","timestamp":1726157310000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91631-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030916305","9783030916312"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91631-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}