Reference : Post-collusion security and distance bounding

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Security, Reliability and Trust
	To cite this reference:	http://hdl.handle.net/10993/41607

Title :	Post-collusion security and distance bounding
Language :	English
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]
Publication date :	11-Nov-2019
Main document title :	Post-collusion security and distance bounding
Peer reviewed :	Yes
Event name :	26th ACM Conference on Computer and Communications Security
Event date :	from 11-11-2019 to 15-11-2019
Event place (city) :	London
Event country :	United Kingdom
Keywords :	[en] 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
Target :	Researchers ; Professionals
Permalink :	http://hdl.handle.net/10993/41607
FnR project :	FnR ; FNR10188265 > Jorge Luis Toro Pozo > > Symbolic verification of distance-bounding and multipartyauthentication protocols > 01/06/2015 > 31/05/2019 > 2015

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Limited access CCS19.pdf Author postprint 943.46 kB Request a copy

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map