首页    期刊浏览 2024年11月08日 星期五
登录注册

文章基本信息

  • 标题:A Symbolic Framework to Analyse Physical Proximity in Security Protocols
  • 本地全文:下载
  • 作者:Alexandre Debant ; St{\'e}phanie Delaune ; Cyrille Wiedling
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2018
  • 卷号:122
  • 页码:1-20
  • DOI:10.4230/LIPIcs.FSTTCS.2018.29
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:For many modern applications like e.g., contactless payment, and keyless systems, ensuring physical proximity is a security goal of paramount importance. Formal methods have proved their usefulness when analysing standard security protocols. However, existing results and tools do not apply to e.g., distance bounding protocols that aims to ensure physical proximity between two entities. This is due in particular to the fact that existing models do not represent in a faithful way the locations of the participants, and the fact that transmission of messages takes time. In this paper, we propose several reduction results: when looking for an attack, it is actually sufficient to consider a simple scenario involving at most four participants located at some specific locations. These reduction results allow one to use verification tools (e.g. ProVerif, Tamarin) developed for analysing more classical security properties. As an application, we analyse several distance bounding protocols, as well as a contactless payment protocol.
  • 关键词:cryptographic protocols; verification; formal methods; process algebra; Dolev-Yao model
国家哲学社会科学文献中心版权所有