{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T10:15:05Z","timestamp":1763201705475,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,9,1]],"date-time":"2011-09-01T00:00:00Z","timestamp":1314835200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2011,9]]},"abstract":"<jats:p>Traditional security protocols are mainly concerned with authentication and key establishment and rely on predistributed keys and properties of cryptographic operators. In contrast, new application areas are emerging that establish and rely on properties of the physical world. Examples include protocols for secure localization, distance bounding, and secure time synchronization.<\/jats:p>\n          <jats:p>We present a formal model for modeling and reasoning about such physical security protocols. Our model extends standard, inductive, trace-based, symbolic approaches with a formalization of physical properties of the environment, namely communication, location, and time. In particular, communication is subject to physical constraints, for example, message transmission takes time determined by the communication medium used and the distance between nodes. All agents, including intruders, are subject to these constraints and this results in a distributed intruder with restricted, but more realistic, communication capabilities than those of the standard Dolev-Yao intruder. We have formalized our model in Isabelle\/HOL and have used it to verify protocols for authenticated ranging, distance bounding, broadcast authentication based on delayed key disclosure, and time synchronization.<\/jats:p>","DOI":"10.1145\/2019599.2019601","type":"journal-article","created":{"date-parts":[[2011,10,4]],"date-time":"2011-10-04T13:24:18Z","timestamp":1317734658000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Formal Reasoning about Physical Properties of Security Protocols"],"prefix":"10.1145","volume":"14","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Srdjan","family":"Capkun","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Schaller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benedikt","family":"Schmidt","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,9]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1109\/TMC.2006.170"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1016\/0304-3975(94)90010-8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1023\/A:1018913028597"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.21236\/ADA464932"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/11513988_27"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1109\/CSF.2010.12"},{"key":"e_1_2_1_7_1","article-title":"A framework for analyzing RFID distance bounding protocols","author":"Avoine G.","year":"2010","journal-title":"J. Comput. Secur. (Special Issue on RFID System Security)."},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1007\/978-3-642-03359-9_1"},{"volume-title":"Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques on Advances in Cryptology (EUROCRYPT\u201993)","author":"Brands S.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/1161289.1161291"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1109\/JSAC.2005.861380"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/986858.986862"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/11964254_9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.5555\/1370677.1370679"},{"doi-asserted-by":"crossref","unstructured":"Delzanno G. and Ganty P. 2004. Automatic verification of time sensitive cryptographic protocols. In Tools and Algorithms for the Construction and Analysis of Systems. 342--356. Delzanno G. and Ganty P. 2004. Automatic verification of time sensitive cryptographic protocols. In Tools and Algorithms for the Construction and Analysis of Systems . 342--356.","key":"e_1_2_1_15_1","DOI":"10.1007\/978-3-540-24730-2_27"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1109\/TIT.1983.1056650"},{"volume-title":"Proceedings of 16th USENIX Security Symposium (Usenix\u201907)","author":"Drimer S.","key":"e_1_2_1_17_1"},{"volume-title":"Proceedings of the 6th European Symposium on Research in Computer Security (ESORICS\u201900)","author":"Evans N.","key":"e_1_2_1_18_1"},{"volume-title":"Archive: Report 2010\/332.","year":"2010","author":"Francillion A.","key":"e_1_2_1_19_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/1380564.1380571"},{"volume-title":"Proceedings of the 6th IFIP Workshop on Formal Methods for Open Object-based Distributed Systems (FMOODS\u201903)","author":"Gorrieri R.","key":"e_1_2_1_21_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1109\/SECURECOMM.2005.56"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1007\/s10207-004-0040-1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1007\/978-3-540-30114-1_17"},{"volume-title":"Proceedings of the 4th International Symposium on Information Processing in Sensor Networks (IPSN\u201905)","author":"Lazos L.","key":"e_1_2_1_25_1"},{"doi-asserted-by":"crossref","unstructured":"Meadows C. Poovendran R. Pavlovic D. Chang L. and Syverson P. 2006. Distance bounding protocols: Authentication logic analysis and collusion attacks. In Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks. 279--298. Meadows C. Poovendran R. Pavlovic D. Chang L. and Syverson P. 2006. Distance bounding protocols: Authentication logic analysis and collusion attacks. In Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks . 279--298.","key":"e_1_2_1_26_1","DOI":"10.1007\/978-0-387-46276-9_12"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1016\/j.tcs.2006.08.036"},{"doi-asserted-by":"crossref","unstructured":"Nipkow T. Paulson L. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer. Nipkow T. Paulson L. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic . Springer.","key":"e_1_2_1_28_1","DOI":"10.1007\/3-540-45949-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1109\/MCOM.2008.4473095"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.5555\/353677.353681"},{"doi-asserted-by":"crossref","unstructured":"Perrig A. and Tygar J. D. 2002. Secure Broadcast Communication in Wired and Wireless Networks. Kluwer Academic Publishers Norwell MA. Perrig A. and Tygar J. D. 2002. Secure Broadcast Communication in Wired and Wireless Networks . Kluwer Academic Publishers Norwell MA.","key":"e_1_2_1_31_1","DOI":"10.1007\/978-1-4615-0229-6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1145\/1368310.1368338"},{"volume-title":"Proceedings of the USENIX Security Symposium.","author":"Rasmussen K. B.","key":"e_1_2_1_33_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1145\/1653662.1653712"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1145\/1229285.1229314"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1145\/941311.941313"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1007\/978-3-540-72738-5_26"},{"unstructured":"Schmidt B. and Schaller P. 2010. Isabelle theory files: Formal reasoning about physical properties of security protocols. http:\/\/people.inf.ethz.ch\/benschmi\/ProtoVeriPhy\/. Schmidt B. and Schaller P. 2010. Isabelle theory files: Formal reasoning about physical properties of security protocols. http:\/\/people.inf.ethz.ch\/benschmi\/ProtoVeriPhy\/.","key":"e_1_2_1_38_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1145\/1098918.1098977"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1145\/1180405.1180439"},{"volume-title":"Proceedings of the European Symposium on Research in Computer Security (ESORICS).","author":"Tippenhauer N. O.","key":"e_1_2_1_41_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1145\/986858.986861"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2019599.2019601","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2019599.2019601","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:07:42Z","timestamp":1750273662000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2019599.2019601"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,9]]}},"alternative-id":["10.1145\/2019599.2019601"],"URL":"https:\/\/doi.org\/10.1145\/2019599.2019601","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"type":"print","value":"1094-9224"},{"type":"electronic","value":"1557-7406"}],"subject":[],"published":{"date-parts":[[2011,9]]},"assertion":[{"value":"2010-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}