Formal security analysis of NFC M-coupon protocols using Casper/FDR
Ali A. Alshehri, Johann A. Briffa, Steve A. Schneider, Stephan Wesemeyer⋆ · 2013
Near field communication (NFC) is a standard-based, radio frequency (RF), wireless communication technology that allows data to be exchanged between devices that are less than 10 cm apart. NFC security protocols require formal security analysis before massive adoptions, in order to check whether these protocols meet its requirements and goals. In this paper we formally analyse NFC-based mobile coupon protocols using formal methods (Casper/FDR). We find an attack against the advanced protocol, and then we provide a solution that addresses the vulnerability formally.