Near field communication (NFC) is a standard-based wireless communication technology that allows data to be exchanged between devices (computers, TV, mobile, ...) that are a few centimeters apart. There will be a significant number of interesting applications (payment, ticketing, e-keys, mobile coupons, ...). One of these applications is mobile coupons (mCoupons), where users can get coupons from NFC mCoupon issuer (smart poster on the street or a NFC tagged newspaper) just by touching their (NFC-capable) mobiles. However, it would cause huge losses for companies if these coupons issued in uncontrolled way. Therefore, a secure protocol is needed to meet mCoupons requirements. Moreover, it must be formally verified, as all secure protocol must be, before building the system in the reality.

There is a proposed mCoupon protocol in the literature. Ali has formally analysed the protocol by using CasperFDR2. This is result in an attack founded. However, whether this attack is feasible in the really is another challenge especially with the different communication nature of NFC.