University of Surrey

Test tubes in the lab Research in the ATI Dance Research

A Formal Framework for Security Analysis of NFC Mobile Coupon Protocols

Alshehri, A and Schneider, SA (2015) A Formal Framework for Security Analysis of NFC Mobile Coupon Protocols Journal of Computer Security.

[img] Text
A_Formal_Framework_for_Security_Analysis_of_NFC_Mobile_Coupon_Protocols.pdf - ["content_typename_Accepted version (post-print)" not defined]
Restricted to Repository staff only
Available under License : See the attached licence file.

Download (1MB)
[img] PDF (licence)
SRI_deposit_agreement.pdf
Restricted to Repository staff only
Available under License : See the attached licence file.

Download (33kB)

Abstract

Near Field Communication (NFC) is a Radio Frequency (RF) technology that allows data to be exchanged between devices that are in close proximity. An NFC-based mobile coupon (M-coupon) is a coupon that is retrieved by the user from a source such as a newspaper or a smart poster and redeemed afterwards. The M-coupon is a cryptographically secured electronic message with some value stored on user’s mobile.We develop a formal framework for security analysis of NFC mobile coupons protocols using formal methods (CasperFDR). The framework aims to check whether NFC M-coupon protocols address their security requirements. The paper starts with a formal definition of the NFC M-coupon requirements in which can be applied to a variety of protocols. Then, we apply the framework to a quadratic residue-based NFC M-coupon protocol proposed in the literature. The analysis shows an attack against User Authentication property. An additional contribution is that we model the protocol with a challenge of modelling the quadratic residue theorem (QR). We propose two ways of abstracting QR in the model with the pros and cons of both methods. We show how to overcome some limitations of CasperFDR, the protocol analysis tool used, that prevent us from modelling the protocol in a natural way. Moreover, we discuss an interesting observation regarding how found attacks can be affected by a divided long message in CasperFDR

Item Type: Article
Authors :
AuthorsEmailORCID
Alshehri, AUNSPECIFIEDUNSPECIFIED
Schneider, SAUNSPECIFIEDUNSPECIFIED
Date : 31 December 2015
Uncontrolled Keywords : NFC, M-coupon, Casper-FDR, Formal Verification, Security protocols
Depositing User : Symplectic Elements
Date Deposited : 28 Mar 2017 10:55
Last Modified : 28 Mar 2017 10:55
URI: http://epubs.surrey.ac.uk/id/eprint/808494

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800