Abstract
Conference Title: 2013 IEEE Third International Conference on Information Science and Technology (ICIST) Conference Start Date: 2013, March 23 Conference End Date: 2013, March 25 Conference Location: Yangzhou, Jiangsu, China An NFC-based mobile coupon (M-coupon) is a cryptographically secured electronic message with some value stored at user's mobile. In the literature, a number of NFC M-coupon protocols were proposed in order to meet particular security requirements. However, formal security analysis is required to check the security of these protocols and whether they address their requirements. This paper mainly focuses on the formal definition of the NFC M-coupon requirements, which is the first, and most important, part of the formal analysis. The formal definitions can apply to a variety of protocols. Then, we illustrate the concept on a case study. [PUBLICATION ABSTRACT]