Abstract
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.