Post-collusion security and distance bounding

Mauw, Sjouke; Smith, Zachary Daniel; Trujillo Rasua, Rolando; Toro Pozo, Jorge Luis

Request a copy

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

Post-collusion security and distance bounding

Mauw, Sjouke; Smith, Zachary Daniel; Trujillo Rasua, Rolando et al.

2019 • In Post-collusion security and distance bounding

Peer reviewed

Permalink
https://hdl.handle.net/10993/41607

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

CCS19.pdf

Author postprint (966.1 kB)

Request a copy

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

formal security; logic and verification; mobile and wireless security

Abstract :

[en] Verification of cryptographic protocols is traditionally built upon the assumption that participants have not revealed their long-term keys. However, in some cases, participants might collude to defeat some security goals, without revealing their long-term secrets. We develop a model based on multiset rewriting to reason about collusion in security protocols. We introduce the notion of postcollusion security, which verifies security properties claimed in sessions initiated after collusion occurred. We use post-collusion security to analyse terrorist fraud on protocols for securing physical proximity, known as distance-bounding protocols. In a terrorist fraud attack, agents collude to falsely prove proximity, whilst no further false proximity proof can be issued without further collusion. Our definitions and the Tamarin prover are used to develop a modular framework for verification of distance-bounding protocols that accounts for all types of attack from literature. We perform a survey of over 25 protocols, which include industrial protocols such as Mastercard’s contactless payment PayPass and NXP’s MIFARE Plus with proximity check. For the industrial protocols we confirm attacks, propose fixes, and deliver computer-verifiable security proofs of the repaired versions

Disciplines :

Computer science

Author, co-author :

Mauw, Sjouke ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)

Smith, Zachary Daniel ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)

Trujillo Rasua, Rolando ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) ; Deakin University > School of Info Technology > Lecturer

Toro Pozo, Jorge Luis ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) ; ETH Zurich > Institute of Information Security > ISG

External co-authors :

yes

Language :

English

Title :

Post-collusion security and distance bounding

Publication date :

11 November 2019

Event name :

26th ACM Conference on Computer and Communications Security

Event place :

London, United Kingdom

Event date :

from 11-11-2019 to 15-11-2019

Main work title :

Post-collusion security and distance bounding

Peer reviewed :

Peer reviewed

Focus Area :

Security, Reliability and Trust

FnR Project :

FNR10188265 - Symbolic Verification Of Distance-bounding And Multiparty Authentication Protocols, 2015 (01/06/2015-31/05/2019) - Jorge Luis Toro Pozo

Available on ORBilu :

since 15 January 2020

Statistics

Number of views

89 (7 by Unilu)

Number of downloads

2 (2 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

Bibliography

Yonatan Aumann and Yehuda Lindell. 2010. Security Against Covert Adversaries: Efficient Protocols for Realistic Adversaries. J. Cryptology 23, 2 (2010), 281-343. https://doi.org/10.1007/s00145-009-9040-7
Gildas Avoine, Muhammed Ali Bingöl, Ioana Boureanu, Srdjan Capkun, Gerhard P. Hancke, Süleyman Kardas, Chong Hee Kim, Cédric Lauradoux, Benjamin Martin, Jorge Munilla, Alberto Peinado, Kasper Bonne Rasmussen, Dave Singelée, Aslan Tchamkerten, Rolando Trujillo-Rasua, and Serge Vaudenay. 2019. Security of Distance-Bounding: A Survey. ACM Comput. Surv. 51, 5 (2019), 94:1-94:33. https://dl.acm.org/citation.cfm?id=3264628
Gildas Avoine, Muhammed Ali Bingöl, Süleyman Kardas, Cédric Lauradoux, and Benjamin Martin. 2011. A framework for analyzing RFID distance bounding protocols. Journal of Computer Security 19, 2 (2011), 289-317. https://doi.org/10.3233/JCS-2010-0408
Gildas Avoine, Xavier Bultel, Sébastien Gambs, David Gérault, Pascal Lafourcade, Cristina Onete, and Jean-Marc Robert. 2017. 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, AsiaCCS 2017, Abu Dhabi, United Arab Emirates, April 2-6, 2017. 800-814. https://doi.org/10.1145/3052973.3053000
Gildas Avoine, Cédric Lauradoux, and Benjamin Martin. 2011. How secret-sharing can defeat terrorist fraud. In Proceedings of the Fourth ACM Conference on Wireless Network Security, WISEC 2011, Hamburg, Germany, June 14-17, 2011. 145-156. https://doi.org/10.1145/1998412.1998437
Gildas Avoine, Sjouke Mauw, and Rolando Trujillo-Rasua. 2015. Comparing distance bounding protocols: A critical mission supported by decision theory. Computer Communications 67 (2015), 92-102. https://doi.org/10.1016/j.comcom.2015.06.007
Gildas Avoine and Aslan Tchamkerten. 2009. An Efficient Distance Bounding RFID Authentication Protocol: Balancing False-Acceptance Rate and Memory Requirement. In Information Security, 12th International Conference, ISC 2009, Pisa, Italy, September 7-9, 2009. Proceedings. 250-261. https://doi.org/10.1007/ 978-3-642-04474-8_21
David A. Basin, Srdjan Capkun, Patrick Schaller, and Benedikt Schmidt. 2009. Let's Get Physical: Models and Methods for Real-World Security Protocols. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. 1-22. https://doi.org/10.1007/978-3-642-03359-9_1
David A. Basin and Cas Cremers. 2014. Know Your Enemy: Compromising Adversaries in Protocol Analysis. ACM Trans. Inf. Syst. Secur. 17, 2 (2014), 7:1-7:31. https://doi.org/10.1145/2658996
David A. Basin and Cas J. F. Cremers. 2010. Modeling and Analyzing Security in the Presence of Compromising Adversaries. In Computer Security - ESORICS 2010, 15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010. Proceedings. 340-356. https://doi.org/10.1007/ 978-3-642-15497-3_21
David A. Basin, Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, Ralf Sasse, and Vincent Stettler. 2018. A Formal Analysis of 5G Authentication. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018. 1383-1396. https://doi.org/10.1145/3243734.3243846
David A. Basin, Sasa Radomirovic, and Lara Schmid. 2016. Modeling Human Errors in Security Protocols. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016. 325-340. https://doi.org/10.1109/CSF.2016.30
Thomas Beth and Yvo Desmedt. 1990. Identification Tokens - or: Solving the Chess Grandmaster Problem. In Advances in Cryptology - CRYPTO'90, 10th Annual International Cryptology Conference, Santa Barbara, California, USA, August 11-15, 1990, Proceedings. 169-177. https://doi.org/10.1007/3-540-38424-3_12
Ioana Boureanu, Aikaterini Mitrokotsa, and Serge Vaudenay. 2013. Towards Secure Distance Bounding. In Fast Software Encryption - 20th International Workshop, FSE 2013, Singapore, March 11-13, 2013. Revised Selected Papers. 55-67. https://doi.org/10.1007/978-3-662-43933-3_4
Stefan Brands and David Chaum. 1993. Distance-Bounding Protocols (Extended Abstract). In Advances in Cryptology - EUROCRYPT'93, Workshop on the Theory and Application of of Cryptographic Techniques, Lofthus, Norway, May 23-27, 1993, Proceedings. 344-359. https://doi.org/10.1007/3- 540- 48285- 7_30
Agnès Brelurut, David Gerault, and Pascal Lafourcade. 2015. Survey of Distance Bounding Protocols and Threats. In Foundations and Practice of Security - 8th International Symposium, FPS 2015, Clermont-Ferrand, France, October 26-28, 2015, Revised Selected Papers. 29-49. https://doi.org/10.1007/978-3-319-30303-1_3
Laurent Bussard and Walid Bagga. 2005. Distance-Bounding Proof of Knowledge to Avoid Real-Time Attacks. In Security and Privacy in the Age of Ubiquitous Computing, IFIP TC11 20th International Conference on Information Security (SEC 2005), May 30 - June 1, 2005, Chiba, Japan. 223-238.
Ran Canetti and Rafail Ostrovsky. 1999. Secure Computation with Honest-Looking Parties: What If Nobody Is Truly Honest? (Extended Abstract). In Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, May 1-4, 1999, Atlanta, Georgia, USA. 255-264. https://doi.org/10.1145/301250.301313
Srdjan Capkun, Levente Buttyán, and Jean-Pierre Hubaux. 2003. SECTOR: secure tracking of node encounters in multi-hop wireless networks. In Proceedings of the 1st ACM Workshop on Security of ad hoc and Sensor Networks, SASN 2003, Fairfax, Virginia, USA, 2003. 21-32. https://doi.org/10.1145/986858.986862
Tom Chothia, Joeri de Ruiter, and Ben Smyth. 2018. Modelling and Analysis of a Hierarchy of Distance Bounding Attacks. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018. 1563-1580. https://www.usenix.org/conference/usenixsecurity18/presentation/chothia
Tom Chothia, Flavio D. Garcia, Joeri de Ruiter, Jordi van den Breekel, and Matthew Thompson. 2015. Relay Cost Bounding for Contactless EMV Payments. In Financial Cryptography and Data Security - 19th International Conference, FC 2015, San Juan, Puerto Rico, January 26-30, 2015, Revised Selected Papers. 189-206. https://doi.org/10.1007/978-3-662-47854-7_11
Katriel Cohn-Gordon, Cas Cremers, Luke Garratt, Jon Millican, and Kevin Milner. 2018. On Ends-to-Ends Encryption: Asynchronous Group Messaging with Strong Security Guarantees. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018. 1802-1819. https://doi.org/10.1145/3243734.3243747
Katriel Cohn-Gordon, Cas J. F. Cremers, and Luke Garratt. 2016. On Post-compromise Security. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016. 164-178. https://doi.org/10.1109/CSF.2016.19
Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A Comprehensive Symbolic Analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017. 1773-1788. https://doi.org/10.1145/3133956.3134063
Cas Cremers and Sjouke Mauw. 2012. Operational Semantics and Verification of Security Protocols. Springer. https://doi.org/10.1007/978-3-540-78636-8
Cas J. F. Cremers, Kasper Bonne Rasmussen, Benedikt Schmidt, and Srdjan Capkun. 2012. Distance Hijacking Attacks on Distance Bounding Protocols. In IEEE Symposium on Security and Privacy, S&P 2012, 21-23 May 2012, San Francisco, California, USA. 113-127. https://doi.org/10.1109/SP.2012.17
Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. 2018. 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, December 11-13, 2018, Ahmedabad, India. 29:1-29:20. https://doi.org/10.4230/LIPIcs.FSTTCS.2018.29
Yvo Desmedt. 1988. Major Security Problems with the “Unforgeable" (Feige)Fiat-Shamir Proofs of Identity and How to Overcome them. In SECURICOM'88. 15-17.
Yvo Desmedt, Claude Goutier, and Samy Bengio. 1987. Special Uses and Abuses of the Fiat-Shamir Passport Protocol. In Advances in Cryptology - CRYPTO'87, A Conference on the Theory and Applications of Cryptographic Techniques, Santa Barbara, California, USA, August 16-20, 1987, Proceedings. 21-39. https://doi.org/10.1007/3-540-48184-2_3
Danny Dolev and Andrew Chi-Chih Yao. 1983. On the security of public key protocols. IEEE Trans. Information Theory 29, 2 (1983), 198-207. https://doi.org/10.1109/TIT.1983.1056650
EMVCo. 2018. EMV Contactless Specifications for Payment Systems, Book C-2, Kernel 2 Specification, Version 2.7.
EMVCo. 2018. EMV Contactless Specifications for Payment Systems, Book C-3, Kernel 3 Specification, Version 2.7.
Matthew K. Franklin and Moti Yung. 1992. Communication Complexity of Secure Computation (Extended Abstract). In Proceedings of the 24th Annual ACM Symposium on Theory of Computing, May 4-6, 1992, Victoria, British Columbia, Canada. 699-710. https://doi.org/10.1145/129712.129780
Gerhard P. Hancke and Markus G. Kuhn. 2005. An RFID Distance Bounding Protocol. In First International Conference on Security and Privacy for Emerging Areas in Communications Networks, SecureComm 2005, Athens, Greece, 5-9 September, 2005. 67-73. https://doi.org/10.1109/SECURECOMM.2005.56
Martin Hirt and Ueli M. Maurer. 1997. Complete Characterization of Adversaries Tolerable in Secure Multi-Party Computation (Extended Abstract). In Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, Santa Barbara, California, USA, August 21-24, 1997. 25-34. https://doi.org/10.1145/259380.259412
Chong Hee Kim and Gildas Avoine. 2009. RFID Distance Bounding Protocol with Mixed Challenges to Prevent Relay Attacks. In Cryptology and Network Security, 8th International Conference, CANS 2009, Kanazawa, Japan, December 12-14, 2009. Proceedings. 119-133. https://doi.org/10.1007/978-3-642-10433-6_9
Chong Hee Kim, Gildas Avoine, François Koeune, François-Xavier Standaert, and Olivier Pereira. 2008. The Swiss-Knife RFID Distance Bounding Protocol. In Information Security and Cryptology - ICISC 2008, 11th International Conference, Seoul, Korea, December 3-5, 2008, Revised Selected Papers. 98-115. https://doi.org/10.1007/978-3-642-00730-9_7
Hugo Krawczyk. 2005. HMQV: A High-Performance Secure Diffie-Hellman Protocol. In Advances in Cryptology - CRYPTO 2005: 25th Annual International Cryptology Conference, Santa Barbara, California, USA, August 14-18, 2005, Proceedings. 546-566. https://doi.org/10.1007/11535218_33
Marc Kuhn, Heinrich Luecken, and Nils Ole Tippenhauer. 2010. UWB impulse radio based distance bounding. In 7th Workshop on Positioning Navigation and Communication, WPNC 2010, Dresden Germany, 11-12 March 2010, Proceedings. 28-37. https://doi.org/10.1109/WPNC.2010.5653801
Brian A. LaMacchia, Kristin E. Lauter, and Anton Mityagin. 2007. Stronger Security of Authenticated Key Exchange. In Provable Security, First International Conference, ProvSec 2007, Wollongong, Australia, November 1-2, 2007, Proceedings. 1-16. https://doi.org/10.1007/978-3-540-75670-5_1
Kristin E. Lauter and Anton Mityagin. 2006. Security Analysis of KEA Authenticated Key Exchange Protocol. In Public Key Cryptography - PKC 2006, 9th International Conference on Theory and Practice of Public-Key Cryptography, New York, NY, USA, April 24-26, 2006, Proceedings. 378-394. https://doi.org/10.1007/11745853_25
Gavin Lowe. 1995. An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Inf. Process. Lett. 56, 3 (1995), 131-133. https://doi.org/10.1016/ 0020-0190(95)00144-2
Gavin Lowe. 1997. A Hierarchy of Authentication Specifications. In 10th Computer Security Foundations Workshop (CSFW'97), June 10-12, 1997, Rockport, Massachusetts, USA. 31-44. https://doi.org/10.1109/CSFW.1997.596782
Sjouke Mauw, Zach Smith, Jorge Toro-Pozo, and Rolando Trujillo-Rasua. 2018. Distance-Bounding Protocols: Verification without Time and Location. In 2018 IEEE Symposium on Security and Privacy, S&P 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. 549-566. https://doi.org/10.1109/SP.2018.00001
Sjouke Mauw, Jorge Toro-Pozo, and Rolando Trujillo-Rasua. 2016. A Class of Precomputation-Based Distance-Bounding Protocols. In IEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016. 97-111. https://doi.org/10.1109/EuroSP.2016.19
Catherine A. Meadows, Radha Poovendran, Dusko Pavlovic, LiWu Chang, and Paul F. Syverson. 2007. Distance Bounding Protocols: Authentication Logic Analysis and Collusion Attacks. In Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks. 279-298. https://doi.org/10.1007/ 978-0-387-46276-9_12
Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Peters-burg, Russia, July 13-19, 2013. Proceedings. 696-701. https://doi.org/10.1007/ 978-3-642-39799-8_48
Jorge Munilla and Alberto Peinado. 2008. Distance bounding protocols for RFID enhanced by using void-challenges and analysis in noisy channels. Wireless Communications and Mobile Computing 8, 9 (2008), 1227-1232. https://doi.org/ 10.1002/wcm.590
Roger M. Needham and Michael D. Schroeder. 1978. Using Encryption for Authentication in Large Networks of Computers. Commun. ACM 21, 12 (1978), 993-999. https://doi.org/10.1145/359657.359659
Pedro Peris-Lopez, Julio César Hernández-Castro, Juan M. Estévez-Tapiador, Esther Palomar, and Jan C. A. van der Lubbe. 2010. Cryptographic puzzles and distance-bounding protocols: Practical tools for RFID security. In 2010 IEEE International Conference on RFID (IEEE RFID 2010). 45-52. https://doi.org/10.1109/RFID.2010.5467258
Pedro Peris-Lopez, Julio César Hernández-Castro, Juan M. Estévez-Tapiador, and Jan C. A. van der Lubbe. 2009. Shedding Some Light on RFID Distance Bounding Protocols and Terrorist Attacks. CoRR abs/0906.4618 (2009). arXiv:0906.4618 http://arxiv.org/abs/0906.4618
Kasper Bonne Rasmussen and Srdjan Capkun. 2010. Realization of RF Distance Bounding. In 19th USENIX Security Symposium, Washington, DC, USA, August 11-13, 2010, Proceedings. 389-402. http://www.usenix.org/events/sec10/tech/full_papers/Rasmussen.pdf
Jason Reid, Juan Manuel González Nieto, Tee Tang, and Bouchra Senadji. 2007. Detecting relay attacks with timing-based protocols. In Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2007, Singapore, March 20-22, 2007. 204-213. https://doi.org/10.1145/1229285. 1229314
Patrick Schaller, Benedikt Schmidt, David A. Basin, and Srdjan Capkun. 2009. Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, 2009. 109-123. https://doi.org/10.1109/CSF.2009.6
Benedikt Schmidt, Simon Meier, Cas J. F. Cremers, and David A. Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012. 78-94. https://doi.org/10.1109/CSF.2012.25
Adi Shamir. 1979. How to Share a Secret. Commun. ACM 22, 11 (1979), 612-613. https://doi.org/10.1145/359168.359176
Paul Syverson, Catherine Meadows, and Iliano Cervesato. 2000. Dolev-Yao is no better than Machiavelli. In First Workshop on Issues in the Theory of Security, WITS'00, Geneva, Switzerland, July 7-8, 2000. 87-92. https://www.nrl.navy.mil/itd/chacs/syverson-dolev-yao-no-better-machiavelli
Peter Thueringer, Hans De Jong, Bruce Murray, Heike Neumann, Paul Hubmer, and Susanne Stern. 2011. Decoupling of measuring the response time of a transponder and its authentication. US Patent No. US12994541.
Martin Tompa and Heather Woll. 1986. How to Share a Secret with Cheaters. In Advances in Cryptology - CRYPTO'86, Santa Barbara, California, USA, 1986, Proceedings. 261-265. https://doi.org/10.1007/3-540-47721-7_20
Rolando Trujillo-Rasua, Benjamin Martin, and Gildas Avoine. 2010. The Poulidor Distance-Bounding Protocol. In Radio Frequency Identification: Security and Privacy Issues - 6th International Workshop, RFIDSec 2010, Istanbul, Turkey, June 8-9, 2010, Revised Selected Papers. 239-257. https://doi.org/10.1007/ 978-3-642-16822-2_19