Cryptology ePrint Archive: Report 2009/543

A Formal Framework for Cryptanalyzing RFID Distance Bounding Protocols

Gildas Avoine and Muhammed Ali Bingol and Suleyman Kardas and Cedric Lauradoux and Benjamin Martin

Abstract: Many distance bounding protocols appropriate for RFID technology have been proposed recently. However, the design and the analysis of these protocols are not based on a formal perspective. Motivated by this need, a formal framework is presented that helps the future attempts to cryptanalyze and design new distance bounding protocols. We first formalize the adversary scenarios, the protocol means, and the adversary goals in general. Then, we focus on the formalism for RFID systems by describing and extending the adversary strategies and the prover model. Two recently published distance bounding protocols are cryptanalyzed using our formal framework to demonstrate its relevancy and efficiency. Our formalism thus allows to prove that the adversary success probabilities are higher than the originally claimed ones.

Category / Keywords: Authentication, Relay Attacks, Distance Bounding, RFID

Date: received 5 Nov 2009, withdrawn 16 Feb 2010

Contact author: gildas avoine at uclouvain be

Available format(s): (-- withdrawn --)

Version: 20100216:134440 (All versions of this report)

Discussion forum: Show discussion | Start new discussion

[ Cryptology ePrint archive ]