Document Open Access Logo

A Symbolic Framework to Analyse Physical Proximity in Security Protocols

Authors Alexandre Debant, Stéphanie Delaune, Cyrille Wiedling

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.29.pdf
  • Filesize: 0.54 MB
  • 20 pages

Document Identifiers

Author Details

Alexandre Debant
  • Univ Rennes, CNRS, IRISA, France
Stéphanie Delaune
  • Univ Rennes, CNRS, IRISA, France
Cyrille Wiedling
  • Univ Rennes, CNRS, IRISA, France

Funding

This work has been partially supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No 714955-POPSTAR).

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.FSTTCS.2018.29

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • cryptographic protocols
  • verification
  • formal methods
  • process algebra
  • Dolev-Yao model

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. M. Abadi and C. Fournet. Mobile Values, New Names, and Secure Communication. In Proc. 28th Symposium on Principles of Programming Languages (POPL'01), pages 104-115. ACM Press, 2001. Google Scholar
  2. A. Armando, R. Carbone, L. Compagna, J. Cuéllar, and M. L. Tobarra. Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for Google apps. In Proc. 6th ACM Workshop on Formal Methods in Security Engineering (FMSE'08), pages 1-10. ACM, 2008. Google Scholar
  3. A. Armando et al. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214, pages 267-282. Springer, 2012. Google Scholar
  4. G Avoine, MA Bingol, Ioana Boureanu, S Capkun, G Hancke, S Kardas, CH Kim, C Lauradoux, B Martin, J Munilla, et al. Security of Distance-Bounding: A Survey. ACM Computing Surveys, 2017. Google Scholar
  5. Gildas Avoine, Muhammed Ali Bingöl, Süleyman Kardaş, Cédric Lauradoux, and Benjamin Martin. A framework for analyzing RFID distance bounding protocols. Journal of Computer Security, 19(2):289-317, 2011. Google Scholar
  6. Gildas Avoine, Xavier Bultel, Sébastien Gambs, David Gerault, Pascal Lafourcade, Cristina Onete, and Jean-Marc Robert. A terrorist-fraud resistant and extractor-free anonymous distance-bounding protocol. In Proceedings of the 2017 ACM on Asia Conference on Computer and Communications Security, pages 800-814. ACM, 2017. Google Scholar
  7. David Basin, Srdjan Capkun, Patrick Schaller, and Benedikt Schmidt. Formal reasoning about physical properties of security protocols. ACM Transactions on Information and System Security (TISSEC), 14(2):16, 2011. Google Scholar
  8. B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In Proc. 14th Computer Security Foundations Workshop (CSFW'01), pages 82-96. IEEE Computer Society Press, 2001. Google Scholar
  9. Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, 2016. URL: http://dx.doi.org/10.1561/3300000004.
  10. Ioana Boureanu, Aikaterini Mitrokotsa, and Serge Vaudenay. Practical and provably secure distance-bounding. Journal of Computer Security, 23(2):229-257, 2015. Google Scholar
  11. Stefan Brands and David Chaum. Distance-bounding protocols. In Workshop on the Theory and Application of of Cryptographic Techniques, pages 344-359. Springer, 1993. Google Scholar
  12. Xavier Bultel, Sébastien Gambs, David Gerault, Pascal Lafourcade, Cristina Onete, and Jean-Marc Robert. A Prover-Anonymous and Terrorist-Fraud Resistant Distance-Bounding Protocol. In Proceedings of the 9th ACM Conference on Security & Privacy in Wireless and Mobile Networks, WISEC 2016, Darmstadt, Germany, July 18-22, 2016, pages 121-133. ACM, 2016. Google Scholar
  13. Srdjan Čapkun, Levente Buttyán, and Jean-Pierre Hubaux. SECTOR: secure tracking of node encounters in multi-hop wireless networks. In Proc. 1st ACM workshop on Security of ad hoc and sensor networks, pages 21-32. ACM, 2003. Google Scholar
  14. Tom Chothia, Flavio D. Garcia, Joeri de Ruiter, Jordi van den Breekel, and Matthew Thompson. Relay Cost Bounding for Contactless EMV Payments. In Proc. 19th International Conference on Financial Cryptography and Data Security (FC'15), volume 8975 of Lecture Notes in Computer Science, pages 189-206. Springer, 2015. Google Scholar
  15. Hubert Comon-Lundh and Véronique Cortier. Security properties: two agents are sufficient. Programming Languages and Systems, pages 99-113, 2003. Google Scholar
  16. Véronique Cortier, Jan Degrieck, and Stéphanie Delaune. Analysing routing protocols: four nodes topologies are sufficient. In International Conference on Principles of Security and Trust, pages 30-50. Springer, 2012. Google Scholar
  17. Cas Cremers, Kasper B Rasmussen, Benedikt Schmidt, and Srdjan Capkun. Distance hijacking attacks on distance bounding protocols. In Proc. IEEE Symposium on Security and Privacy (S&P'12), pages 113-127. IEEE, 2012. Google Scholar
  18. Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. http://people.irisa.fr/Alexandre.Debant/proving-physical-proximity-using-symbolic-methods.html.
  19. Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. Proving physical proximity using symbolic models. Research report, Univ Rennes, CNRS, IRISA, France, February 2018. URL: https://hal.archives-ouvertes.fr/hal-01708336.
  20. Yvo Desmedt, Claude Goutier, and Samy Bengio. Special uses and abuses of the Fiat-Shamir passport protocol. In Conference on the Theory and Application of Cryptographic Techniques, pages 21-39. Springer, 1987. Google Scholar
  21. D. Dolev and A. C. Yao. On the Security of Public Key Protocols. In Proc. 22nd Symposium on Foundations of Computer Science (FCS'81), pages 350-357. IEEE Computer Society Press, 1981. Google Scholar
  22. Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, and Ralf Sasse. Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. In CSF'2018 - 31st IEEE Computer Security Foundations Symposium, Oxford, United Kingdom, July 2018. URL: https://hal.archives-ouvertes.fr/hal-01780603.
  23. Gerhard P Hancke and Markus G Kuhn. An RFID distance bounding protocol. In Proc. 1st International Conference on Security and Privacy for Emerging Areas in Communications Networks (SECURECOMM'05), pages 67-73. IEEE, 2005. Google Scholar
  24. Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, and Carolyn Talcott. Towards timed models for cyber-physical security protocols. In Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography, 2014. Google Scholar
  25. Handan Kilinç and Serge Vaudenay. Efficient Public-Key Distance Bounding Protocol. In Advances in Cryptology - ASIACRYPT 2016 - 22nd International Conference on the Theory and Application of Cryptology and Information Security, Hanoi, Vietnam, December 4-8, 2016, Proceedings, Part II, volume 10032 of Lecture Notes in Computer Science, pages 873-901, 2016. Google Scholar
  26. Chong Hee Kim, Gildas Avoine, François Koeune, François-Xavier Standaert, and Olivier Pereira. The swiss-knife RFID distance bounding protocol. In International Conference on Information Security and Cryptology, pages 98-115. Springer, 2008. Google Scholar
  27. S. Mauw, Z. Smith, J. Toro-Pozo, and R. Trujillo-Rasua. Distance-Bounding Protocols: Verification without Time and Location. In 2018 IEEE Symposium on Security and Privacy (S&P), volume 00, pages 152-169, 2018. URL: http://dx.doi.org/10.1109/SP.2018.00001.
  28. Catherine Meadows, Radha Poovendran, Dusko Pavlovic, LiWu Chang, and Paul Syverson. Distance bounding protocols: Authentication logic analysis and collusion attacks. In Secure localization and time synchronization for wireless sensor and ad hoc networks, pages 279-298. Springer, 2007. Google Scholar
  29. S. Meier, B. Schmidt, C. Cremers, and D. Basin. The Tamarin Prover for the Symbolic Analysis of Security Protocols. In Proc. 25th International Conference on Computer Aided Verification (CAV'13), volume 8044 of LNCS, pages 696-701. Springer, 2013. Google Scholar
  30. Jorge Munilla and Alberto Peinado. Distance bounding protocols for RFID enhanced by using void-challenges and analysis in noisy channels. Wireless communications and mobile computing, 8(9):1227-1232, 2008. Google Scholar
  31. Vivek Nigam, Carolyn Talcott, and Abraão Aires Urquiza. Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders. In Proc. 21st European Symposium on Research in Computer Security (ESORICS'16), pages 450-470. Springer, 2016. Google Scholar
  32. Kasper Bonne Rasmussen and Srdjan Capkun. Realization of RF Distance Bounding. In USENIX Security Symposium, pages 389-402, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact