License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2018.29
URN: urn:nbn:de:0030-drops-99288
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9928/
Go to the corresponding LIPIcs Volume Portal

Debant, Alexandre ; Delaune, Stéphanie ; Wiedling, Cyrille

A Symbolic Framework to Analyse Physical Proximity in Security Protocols

pdf-format:
LIPIcs-FSTTCS-2018-29.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{debant_et_al:LIPIcs:2018:9928,
  author =	{Alexandre Debant and St{\'e}phanie Delaune and Cyrille Wiedling},
  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 =	{Sumit Ganguly and Paritosh Pandya},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9928},
  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}
}

Keywords: cryptographic protocols, verification, formal methods, process algebra, Dolev-Yao model
Collection: 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
Issue Date: 2018
Date of publication: 05.12.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI