DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2018.29

A Symbolic Framework to Analyse Physical Proximity in Security Protocols

Authors: Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract

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.

Cite as

Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. A Symbolic Framework to Analyse Physical Proximity in Security Protocols. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{debant_et_al:LIPIcs.FSTTCS.2018.29,
  author =	{Debant, Alexandre and Delaune, St\'{e}phanie and Wiedling, Cyrille},
  title =	{{A Symbolic Framework to Analyse Physical Proximity in Security Protocols}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.29},
  URN =		{urn:nbn:de:0030-drops-99288},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.29},
  annote =	{Keywords: cryptographic protocols, verification, formal methods, process algebra, Dolev-Yao model}
}

Search Results

Documents authored by Debant, Alexandre

A Symbolic Framework to Analyse Physical Proximity in Security Protocols

Abstract

Cite as

Thanks for your feedback!

Could not send message