A formal framework for security analysis of NFC mobile coupon protocols

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.

Keywords

NFC M-coupon CasperFDR formal verification security protocols

1. Introduction

Near Field Communication (NFC) [34] is a Radio Frequency (RF) communication link, which allows data to be exchanged between devices that are normally less than 10 cm apart [27]. NFC-based devices are an emerging technology changing the way we communicate with objects. For instance, payments, tickets and coupons can be exchanged just by waving the NFC-based devices at the points of sale. NFC has become more prevalent in mobile phones as they are owned by a majority of people. NFC in mobiles can operate in three different modes determined by the application used; it can communicate with other NFC mobiles in Peer-to-Peer mode, or communicate with a passive RFID/NFC tag in reader/writer mode, or communicate with an NFC reader in card emulation mode [18].

The fact that NFC can perform three modes of operation has inspired a significant number of possible applications [19]. The NFC mobile coupon application (M-coupon) is one of the promising and popular applications [12,15,35,47]. An M-coupon is a cryptographically secured electronic message with some value which requires secure issuing and cashing of the M-coupons. Uncontrolled copies of the M-coupons would cause losses for a company and damage its reputation [53]. The NFC M-coupon system has a typical scenario, see Fig. 1. All parties have NFC capability, in order to communicate with each other. Firstly, a user scans his NFC mobile against an NFC issuer (e.g., a smart poster or newspaper). Then, an M-coupon is issued and sent to his mobile. Later, the user goes to the shop to cash the M-coupon with the cashier. The cashier may authenticate the user before the cashier provides the promised bonus. Only the cashier needs to have online access, whereas the issuer and the user can both be offline.

The NFC mobile coupon requires the development of secure cryptographic protocols in order to meet desired security requirements. The requirement for robust security in NFC in general has been emphasised in the literature [30,41]. NFC-SEC standards [25,26] enable two NFC devices, in Peer-to-Peer mode that do not share any common secret keys, to establish a secure channel. However, NFC-SEC standards are vulnerable to the Man In The Middle attack because they do not provide entity authentication [26]. Therefore, a number of NFC M-coupon security protocols have been proposed in the literature [23,32,33].

However, formal security analysis has not been carried out on these proposed M-coupon protocols. Formal security analysis is a powerful approach to check the security of these protocols and whether they address their requirements. Such analysis is important because implementing strong cryptographic algorithms is only half of the solution. In fact, the way encryption is used between entities is the more challenging part of protocol design. It is quite difficult to establish secure cryptographic protocols even with robust cryptographic algorithms. Many attacks can be realised during the execution of the cryptographic protocols just by intercepting and replaying encrypted messages between entities, without decrypting any messages [37]. Thus, formal security analysis of NFC protocols in general, and especially the NFC M-coupon protocol, is critically important before their widespread adoption.

Fig. 1.

General NFC mobile coupon. (Colors are visible in the online version of the article; http://dx.doi.org/10.3233/JCS-150531.)

The paper is organised as follows: after a discussion on related work in Section 2, we illustrate our modelling method in Section 3, CasperFDR approach [38] which is based on Communicating Sequential Processes (CSP) [31]. Then, in Section 4 we develop a general framework that 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. Finally, in Section 5 we demonstrate the use of the framework by applying the framework on a quadratic residue theorem (QR) based NFC M-coupon protocol proposed in the literature [32].

2. Related work

2.1. Security protocol analysis

An analysis of the security protocol is categorised into the following approaches [3,42,44]:

Computational approach;

Symbolic approach.

The main difference between the two approaches is the way cryptographic primitives are modelled. In the computational approach, cryptographic primitives are modelled as functions of strings of bits where the intruder is able to try and break them i.e. cryptanalysis. In contrast, the intruder in the symbolic approach does not perform cryptanalysis, but has a full control of the communication. The only way to encrypt/decrypt is if it holds the appropriate key. This assumption in the symbolic approach is commonly known as the perfect encryption assumption. The symbolic approach is much easier to automate than the computational approach. With regard to this paper, the analysis tool falls into the symbolic approach.

The symbolic approach uses a common way to find vulnerabilities. First, a system and its specifications are modelled as formulas of logic. Then, a test is performed to check a claim that the system and its specifications are related. Finally, the result is either true (i.e. error-free) or false where a counterexample is generated to show how the claim is violated. In the security protocol context, the system is the security protocol, the specifications are the security requirements and the counterexample is the attack.

Tools based on the symbolic approach fall into three main approaches:

Belief logic [11,13,29,39] was the first attempt to automate the verification of security protocols, where beliefs of entities can be described and evaluated through inference rules. Then, based on the evaluation process, a final statement is concluded whether the protocol is correct or not.

Theorem proving [10,16,17,21,43,49,50,52] is an approach that verifies the security through a formal proof.

State exploration: Vulnerabilities are found in the state exploration approach by exploring all possible traces of a protocol to check whether a property holds. Tools based on state exploration fall into two branches: Model checking is a method that identifies vulnerability in the given model by checking if a security requirement is violated. However, the model checking approach does not establish if the protocol is really correct. This limitation motivates the second approach, the Strand Spaces approach. Nonetheless, the majority of tools are based on the state exploration approach. There are a number of tools that based on the state exploration approach such as Scyther [20], AVISPA [51], OFMC [7], Athena [48], ProVerif [9], Spi Calculus [1], SMV [40] and BMC [8].

CasperFDR [31,38,46], our modelling tool, is a formal method tool utilises the state exploration approach. The advantages of CasperFDR for the modelling of NFC protocols fall into the following aspects:

It allows modifying the intruder’s power on every channel of the protocol. Such settings are needed to capture some behaviour in the analysed protocols. This is not possible in other similar tools such as AVISPA and Scyther, while in CasperFDR it is a default setting.

Accessing the original CSP code which allows direct modification of the model when appropriate.

The ability to use the tool for more advanced analysis such as capturing various security requirements in NFC mobile coupon. This is also possible in some tools such as AVISPA and Scyther.

It features various automated and robust security specifications. This is also provided in AVISPA and Scyther but not as powerful as in CasperFDR.

2.2. M-coupon protocols analysis

The story of the NFC M-coupon protocols development began with Dominikus and Aigner when they proposed the first protocol in the literature [23]. The protocols utilized in Dominikus and Aigner study were based on encryption and signatures meeting four basic security requirements: Multiple Cash-in, Unauthorized Generation, Manipulation and Unauthorized Copying. Based on desirable M-coupon business models, they propose two protocols, the advanced and the simple M-coupon protocols. However, efficiency is an issue in these protocols because using such encryption methods might be quite heavy for NFC mobiles.

Similarly, another protocol was proposed by Hsiang and Shih [33], where light hash functions were used to meet the same requirements with two additional requirements: Confidentiality and Data Integrity. The third protocol [32] is a further development of the hash-based protocol carried out by the same authors. In particular, they used the quadratic residue theorem to enhance the secrecy of the protocol. Secrecy of Issuer’s ID is an additional requirement in this protocol. Finally, we proposed protocols that we developed in the light of lessons learned from previous protocols [5].

A formal security analysis has been done on three of the NFC M-coupon protocols: the encryption-based protocol [4], the hash-based protocol [5] and the marketing-based protocol [5]. A number of vulnerabilities were identified and addressed formally. A formal definition of NFC M-coupon requirements was developed in [6].

3. The CasperFDR approach

CSP [31], with its model checker Failures Divergence Refinement (FDR), has been proven to be an effective method in analysing the security of protocols [46]. However, modelling protocols in CSP is not a trivial task. Gavin Lowe developed CasperFDR [38] to address this problem. CasperFDR is a tool that allows the user to write an abstract description of a security protocol, then the tool produces codes in CSP language, and directly checks it with FDR2. CasperFDR has been used to analyse many protocols [24], which proves its capability of finding vulnerabilities.

CasperFDR is a formal method tool which supports symbolic protocol analysis in the Dolev–Yao model [22] which assumes that no encrypted message can be decrypted without the decryption key, thus the CasperFDR intruder model does not perform any cryptanalysis. However, the intruder does have full control of the network traffic, and tries to break the security protocol from what passes on the network.

CasperFDR performs a refinement check of the protocol against its requirements. When refinement fails, then it provides a trace which shows how the property fails, that corresponds to an attack. The best way to illustrate the CasperFDR approach is by a simple example.

3.1. Simple example

As an illustrative example, consider the two message protocol aiming for Alice to communicate a shared secret key to Bob:

Alice → Bob: ${A, N_{A}, K_{AB}} {PK}_{B}$ ;

Bob → Alice: ${N_{A}} K_{AB}$ .

Message 1 sent by Alice to Bob contains Alice’s identity, a nonce (number used once) and a session key $K_{AB}$ , encrypted with Bob’s public key. Then, Bob sends Message 2 by encrypting the nonce ( $N_{A}$ ) with the session key. At the end of the protocol the aim is that both Alice and Bob can be confident that the session key $K_{AB}$ is a secret known to no one else.

3.2. CasperFDR modelling

We will analyse the system from Bob’s point of view: in particular, to check that Bob can be sure that he was talking to Alice, and that Bob can be sure that the key $K_{AB}$ is shared only with Alice?

Fig. 2.

CasperFDR modelling of the simple example.

Figure 2 shows the CasperFDR script of the simple protocol modelling. There are eight sections which can be considered from two main perspectives, protocol definition and system definition:

The protocol definition:

The first four sections used to give a general description of the protocol:

# Protocol description

Here, we define the exchanged messages of the protocol. The first line (0. -> A:B) means A starts the protocol with B, maybe through the user of A or the environment. The other lines are the messages of the protocol.

# Free variables

Defines any variables, or functions, used in the protocol description.

# Processes

Defines every agent in the protocol description including their initial knowledge.

# Specifications

Defines the requirements of the protocol which will be checked. Having modelled the exchanged messages between entities, we check the claimed authentication and secrecy properties for Bob using the following claims (where B is Bob and A is Alice): $\begin{array}{rcl} Agreement (Bob, Alice, [N_{A}]); \\ Secret (Bob, K_{AB}, [Alice]) . \end{array}$

Note that versions of these specifications can also be expressed from Alice’s perspective: $Agreement (Alice, Bob, [N_{A}])$ , and $Secret (Alice, K_{AB}, [Bob])$ .

The Agreement specification means that if Bob as responder has completed a run of the protocol apparently with Alice as initiator, and with nonce $N_{A}$ , then Alice must have participated in a run of the protocol as initiator, apparently with Bob as responder, and with the same nonce $N_{A}$ . If this is true then the protocol enables Bob to authenticate Alice, since Bob can only complete the protocol if Alice was also participating. The Secret specification is checking whether the key $K_{AB}$ accepted by Bob is secret between Bob and Alice. Here, Bob is the one who claims the secret. We do not have to check Alice’s belief about the key $K_{AB}$ , $Secret (Alice, K_{AB}, [Bob])$ , as she is the one who generated it.

The system definition:

We operate CasperFDR in the mode where a specific system is analysed for correctness. Identifying a particular system is written within these four steps:

# Actual variables

Similar to #Free Variables above but explicitly specifying the names of the variables.

# Functions

Functions used in the protocol are defined here.

# System definition

Defines the instances of the roles acting by agents in the protocol and how many times they can engaging in the protocol.

# The intruder

Defines the initial intruder’s knowledge.

In fact, the CasperFDR analysis finds an attack on secrecy. Figure 3(b) illustrates how an intruder can create a session key that Bob believes is secret with Alice. Anyone can generate Message 1 since Bob’s public key is publicly known. The intruder impersonates Alice by including Alice’s identity. At the end of the protocol run Bob believes the session key $K_{MB}$ is a secret shared with Alice. However, it is known by the intruder.

Fig. 3.

Simple example. (a) Simple protocol and events. (b) Simple protocol attack. (Colors are visible in the online version of the article; http://dx.doi.org/10.3233/JCS-150531.)

3.3. Hierarchy of authentication and secrecy

CasperFDR provides different flavours of testing authentication and secrecy. Capturing authentication between Alice and Bob in the protocol is done by utilising new events injected in the protocol as demonstrated in Fig. 3(a). These events are Running and Commit. For secrecy, only the Claim_Secret event is used by Alice and Bob.

Aliveness. Aliveness is the weakest form of authentication specification. It guarantees to Bob aliveness of Alice. Aliveness means if Bob thinks he has successfully completed a run of the protocol with Alice, then Alice has previously been running the protocol. The meaning of “then Alice has previously been running the protocol” is that Alice has engaged in the protocol until the last message that Alice has sent. However, Alice may have thought she was running the protocol with someone other than Bob.

Weak agreement. WeakAgreement includes the definition of the Aliveness specification, and it is a stronger specification which adds the condition that Alice has agreed he was running the protocol with Bob. However, Alice and Bob may disagree on their role played in relation to the protocol.

Non-injective agreement. NonInjectiveAgreement includes the definition of the Weak agreement specification, and it is a stronger specification which adds the condition that Alice and Bob agree as to which roles each was taking, and also agree upon some of the date items used in the exchanged messages. However, there is no guarantee of one-to-one relationship between Alice and Bob i.e. Bob may believe that he has completed two runs, whereas Alice has only engaged in one of them. Each run made by one participant is matched by a run from another, albeit these can also overlap. For example, two “Commit” events may correspond to the same “Running” event.

Agreement. Agreement includes the Non-injective agreement specification, and it is the strongest specification. It adds the condition that there is a one-to-one relationship between Alice and Bob i.e. each run of Bob corresponds to a unique run of Alice.

Secret. Secret specifies that a claimed secret value should only be known by a specified set of parties following a complete run of the protocol by the honest agent.

Strong secret. StrongSecret includes the Secret specification and a testing of the claimed secret even without the honest agent completing a full run of the protocol. This specification is required in some protocols where compromising a value even in the middle of the protocol would count as an attack e.g., a credit card number.

4. Formal definition of NFC M-coupon security requirements

In the literature [4,23,32,33], there are eight common security requirements:

Confidentiality: An unauthorized third party shall not be able to obtain the M-coupon by eavesdropping.

Data Integrity: An attacker shall not be able to modify data during the communication.

Forgery Protection:

No Unauthorized Generation: An attacker shall not be able to issue his own M-coupon.

No Manipulation: An M-coupon shall not remain valid after a manipulation.

Unauthorized Copying: An attacker shall not be able to produce a valid copy of an M-coupon and cash it in. This requirement can be divided into:

Not Transferable: Whatever identity is presented at issuing phase shall not be changed during the protocol. However, other users may use the M-coupon as long as the M-coupon includes a valid identity that was presented at the issuing time.

User Authentication: in addition to Not Transferable, the identity of the user is the one who it claims to be. The user who was issued the M-coupon must be the one who is cashing it at the cashier. This requires the cashier to authenticate the user through some authentication methods.

No Multiple Cash-in: An attacker shall not be able to use the same M-coupon multiple times.

Secrecy of Issuer’s ID: The identity of the issuer shall be secret throughout the protocol between the issuer and the cashier. This provides anonymity of the issuer from the cashier.

Nevertheless, not all these requirements are promised by proposed protocols in the literature, and depending on the M-coupon system some of these requirements are optional.

The following sections show what one has to write in CasperFDR to model different protocol’s requirements and subsequently how it is captured underneath in terms of Running, Commit and Claim_Secret events. This will enable one to have formal and precise descriptions of NFC mobile coupon requirements.

These general models can be applied to any protocol trying to meet the NFC M-coupon requirements, and have the three main players (issuer, user and cashier) engaging in the two main phases (issuing phase and cashing phase). We generally define the values that engaging entities have to agree upon since these models are general. For example when we specify that the issuer and the cashier have to agree on the M-coupon, this means that they have to agree on the data that represents the M-coupon in the analysed protocol, which can be different from one protocol to another. The same is applied to other general values in the different general models (Secret, UserID, ALL DATA, credentials, IssuerID). Finally, we will consider a running example of an airline issuing M-coupons to customers. For each requirement we illustrate how an M-coupon is becoming stronger and, hence, more useful with an airline M-coupon example.

4.1. Threat model

The threat model used in the formal analysis is Dolev–Yao model [22], which assumes no encrypted message can be decrypted without the decryption key, thus the intruder does not perform any cryptanalysis. However, he or she has full control of the network traffic, i.e. block, replay, redirect, spoof and duplicate messages, and tries to break the security protocol from what has been learned.

The analysis threat model does not include proximity. Therefore, Relay attacks are not considered in our analysis since it is a general attack against NFC technology [28]. Relay attack is a well-known attack that manipulates the proximity factor between entities. Cryptographic measures are believed to be not sufficient for addressing the attack on its own. The main danger of the relay attack is the fact that the attack works even with secure protocols. Thus, it is warranted to assume that there are some non-cryptographic techniques for addressing NFC relay attacks, discussed in [28], and in which case relay attacks are not a primary concern of the formal analysis.

4.2. Confidentiality

We model confidentiality in CasperFDR as follows: $\begin{matrix} StrongSecret (Cashier, Secret, [Issuer]) . \end{matrix}$

This secrecy specification means the cashier claims that Secret is confidential with the Issuer. Secret will be the critical part of the M-coupon. StrongSecret checks whether the intruder is able to break this claim and knows the Secret during, or at the end, of the protocol. If Secret is leaked at the middle of the protocol, the intruder may use it to generate new M-coupons. For example, the issuer generates an M-coupon to the intruder who can use Secret, from the M-coupon, to generate a variety of M-coupons either to oneself or different users.

Figure 4 (number 6) illustrates this specification. When the cashier performs the Claim_Secret.C.I.Secret event where C is the Cashier and I stands for Issuer, it can expect Secret to be confidential with the issuer. If this is violated then the intruder can complete a run of the protocol with the cashier without taking the issuer role, and in the process learn the secret value Secret. The value Secret is what the issuer and the cashier believe to be confidential and is needed to redeem the M-coupon. If this holds, then the value Secret is confidential from the issuer to the cashier at a complete, or incomplete, run of the protocol.

Here, the airline can make sure that wherever a customer brought their M-coupon from, the secret keys/values remain a secret throughout the protocol. This is a fundamental requirement that many requirements are built on.

Fig. 4.

Capturing NFC M-coupon requirements in CasperFDR.

4.3. Forgery Protection (No Unauthorised Generation/No Manipulation)

We model Forgery Protection (No Unauthorised Generation and No Manipulation) in CasperFDR as follows: $\begin{matrix} NonInjectiveAgreement (Issuer, Cashier, [M-coupon]) . \end{matrix}$

First, one has to identify which part of the exchanged messages represents the M-coupon. This states that if the cashier accepts M-coupon, then the issuer must have issued them. NonInjective means that this property is not concerned with repeats i.e. the cashier can accept many times what was issued once. This property is violated if the cashier accepts an M-coupon that has not been issued by the issuer: either that the M-coupon has been created by an attacker (i.e. Unauthorised Generation) or else that the M-coupon generated by the issuer has been modified to another (i.e. No Manipulation). Hence, if this property holds then one has Forgery Protection: No Unauthorised Generation and No Manipulation.

This is illustrated in Fig. 4 (number 1). After the issuer completes its part of the protocol, it performs the Running.I.C.M-coupon event, which means the Issuer starts a run of the protocol, apparently, with the Cashier, agreeing on M-coupon. Later, the cashier will perform the Commit.C.I.M-coupon event at the end of its part of the protocol, which means the Cashier has finished the protocol with the Issuer, agreeing on the M-coupon. Each run of the issuer matches a run of the cashier but they can overlap since one is not concerned with repeats. If this holds, then a genuine M-coupon has been generated by a genuine issuer and accepted by the cashier.

Now, the airline can make sure of the fact that the M-coupon is genuine. They can use the M-coupon for increase and encourage people visiting their shops in the airport with promotions and discounts such as free coffee. The airline is not concerned with who is using the M-coupon as long as it is genuinely issued or has been transferred by a friend who had issued it genuinely.

4.4. Unauthorized Copying (Not Transferable)

We model Not Transferable in CasperFDR as follows: $\begin{matrix} NonInjectiveAgreement (Issuer, Cashier, [M-coupon, User ID]) . \end{matrix}$

This specification is similar to forgery protection specification, but also with an agreement on a user’s identity. The M-coupon must be attached to one user only, User ID. Both the issuer and the cashier agree on the user to use the coupon as many times as he/she like, as long as the coupon has been issued by a genuine issuer and is being used by the intended user.

This is shown in Fig. 4 (number 2). After the issuer completes its part of the protocol, it performs the Running.I.C.M-coupon.User ID event, which means the Issuer starts a running of the protocol, apparently, with the Cashier, agreeing on M-coupon and User ID. Later, the cashier will perform the Commit.C.I.M-coupon.User ID event at the end of its part of the protocol, which means the Cashier has finished the protocol with the Issuer and agreed on the M-coupon and User ID.

Observe that this property is stronger than forgery protection. If it holds then not only must the M-coupon be genuine, as for forgery protection, but it must also have the same user. This is violated if the cashier accepts a M-coupon that was issued for another user.

The airline can use the M-coupon as a frequent flyer coupon where one coupon can be used multiple times for the same user without authenticating the user every time as the cashier trusts the issuing phase procedure. Another use of the M-coupon is that the airline is able to encourage the original user to pass the M-coupon to friends with promising the original user to get some credit for this.

4.5. Unauthorized Copying (User Authentication)

We model User Authentication in CasperFDR as follows: $\begin{matrix} Agreement (User, Cashier, [credential]) . \end{matrix}$

This specification is a stronger definition of Unauthorized Copying since it emphasises authenticating the user who is carrying the M-coupon. The user who issued the M-coupon must be the one who is cashing it at the cashier. This requires the cashier to authenticate the user through some authentication methods, credential. Agreement is used because even though the M-coupon might be used many times, the user must be authenticated each time.

This is illustrated in Fig. 4 (number 4). Normally, Message 2 would include some proof of user authentication to the cashier. Before the user sends Message 2 of the protocol, it performs the Running.U.C.credential event, which means the user U starts a run of the protocol, apparently, with the cashier, agreeing on credential. Later, the cashier will perform the Commit.C.U.credential event at the end of its part of the protocol, which means the cashier has finished the protocol with the user, agreeing on the credential. If this holds, then the cashing user is the one who issued the M-coupon. This is violated if the intruder was able to crack the authentication measure between the user and the cashier.

Here, the airline wants a stronger layer of user authentication. Maybe because it suspects the user or the M-coupon has a very high value. The airline is happy to delay the protocol slightly as long as it has more assurance about the user. The M-coupon in this case may include other sensitive procedure like payment.

4.6. Data Integrity

We can check the integrity of the whole data of the protocol by examining the following specification in CasperFDR: $\begin{matrix} NonInjectiveAgreement (Issuer, Cashier, [ALL DATA]) . \end{matrix}$

This will check the integrity of the protocol. Both the cashier and the issuer must agree on ALL DATA in the protocol. Figure 4 (number 3) shows how it is captured. This is violated if any data in the protocol was modified. If this holds, then the integrity of data between the issuer and the cashier is confirmed.

The airline is assured of the integrity of data included in the M-coupon. In addition, this is a higher level of meeting Forgery Protection and Not Transferable.

4.7. No Multiple Cash-in

We model No Multiple Cash-in in CasperFDR as follows: $\begin{matrix} Agreement (Issuer, Cashier, [M-coupon]) . \end{matrix}$

This specification states that every time the cashier accepts M-coupon, there must be a separate occasion where the issuer must have issued them. Hence, cashier cannot accept M-coupon more times than the issuer sent them.

Figure 4 (numbers 1 and 7) illustrates a scenario where the cashier is engaging in the protocol twice, with one issuer run. The first time, the cashier runs the protocol with the user’s mobile, and the second time with Mallory who might be an intruder or the user. The second time, Commit should not occur if there was not a separate Running. If this is violated, then there is a vulnerability in which the M-coupon was cashed twice.

The airline wants to issue special targeted offers for some potential customers to access their VIP lounge, but the access is only valid once.

4.8. Secrecy of Issuer’s ID

We model the Secrecy of Issuer’s ID in CasperFDR as follows: $\begin{matrix} StrongSecret (Cashier, Issuer’s ID, [Issuer]) . \end{matrix}$

Throughout the protocol, the identity of the issuer must remain secret between the issuer and the cashier. This is illustrated in Fig. 4 (number 5). The cashier claims the secrecy of the issuer’s identity at the end of the protocol. This is violated if the intruder, or the user, can eavesdrop the issuer’s identity.

Issuer’s ID is assumed to be a different identity from the normal identity of the issuer (Issuer) for two reasons. First, random identities is common in RFID/NFC protocols [2]. Second, it is the only way to test this specification without limiting the power of the intruder. If we test the secrecy of the normal identity (Issuer), then we need to remove the normal issuer’s ID from the intruder’s knowledge in order to make this specification hold. However, this would mean that the intruder would not be able to generate his own coupon, which would become a major limitation in the specification.

Here, the airline is assured with the secrecy of their issuers, which are distributed at different paces.

5. Modelling and analysis of QR-based NFC M-coupon protocol

In this section we demonstrates an application of the framework by analysing a quadratic residue theorem (QR) based NFC M-coupon protocol presented in [32]. The QR-based protocol is an enhanced version of a previous NFC hash-based protocol in the literature [33], and intends to meet all eight NFC M-coupon security requirements.

5.1. Protocol description

The Hsiang et al. (QR-based) protocol utilises quadratic residue [14,45] to securely hide some values. The main idea of QR is that assuming one has $n = p * q$ where p and q are two large primes, and given $a = x^{2} (mod n)$ , it is computationally infeasible to find x. The only parties who can extract x are those who know p and q.

Fig. 5.

Quadratic Residue-based M-coupon protocol.

Figure 5 shows the messages of the protocols and notations used in Table 1. The three main participants are: the issuer, the user and the cashier.

Before the beginning of the protocol, there are some initial steps. The user downloads a coupon application where the cashier and the user share a secret password pin and an identity is assigned to the user User. In addition, the cashier computes $V_i = h_{x} [Issuer, offer]$ and then writes $Issuer$ , $h [Issuer]$ and $V_i$ into issuer’s memory where $Issuer$ , x and $offer$ remain secret through the protocol. The cashier computes $n = p * q$ as well provide the issuer with n.

There are four messages in this protocol:

$U \to I$ : User;

$I \to U$ : $M = Y, R, h (y), h (r), V_m$ ;

$U \to C$ : User, E, P and M;

$C \to U$ : BONUS.

Message 1: the user sends their identity User to the issuer. The issuer replies in Message 2 with the M-coupon $M = Y, R, h (y), h (r), V_m$ : $\begin{array}{rcl} y = h [Issuer] \oplus r \oplus User, \\ Y = y^{2} (mod n), \\ R = r^{2} (mod n), \\ V_m = h_{V_i} [r, y] . \end{array}$

The value y contains a hash of the following: an Xor of the identity of the issuer (Issuer), issuer’s random number r and the identity of the user (User). The values y and r are secret between the issuer and the cashier by using QR, and can be computed from Y and R. The cashier can compute y and r from p and q. V_m is for the integrity of y and r, where V_m contains a keyed hash of y and r with $V_i$ as a key.

Table 1

Hsiang et al. (QR-based) protocol notation

$Issuer$	Issuer ID
$User$	User ID
$Cashier$	Cashier ID
$offer$	Data about the Offer
x	A secret key shared between the issuer and the cashier
$pin$	A secret password shared between the user and the cashier
⊕	Exclusive or (XOR)
r	Issuer’s random number
$r_c$	User’s random number
$h [. .]$	Hash function
$h_{s} [. .]$	Keyed hash function with secret s

Message 3, the user’s mobile sends the M-coupon M with the authentication credential: User, E and P: $\begin{array}{rcl} E = r_c \oplus pin, \\ P = h_{pin} [User, r_c] . \end{array}$

In E, a random number r_c is used to make a random password PIN. The cashier knows the pin from the identity of the user User. In order to link the password pin to the user identity User, P is a keyed hash of User and r_c, with pin as a key.

The cashier verifies the authenticity of the user’s credentials, and the validation of the M-coupon. If both are accepted and share the same user’s identity, then the cashier sends BONUS to the user, Message 4.

5.2. Modelling

5.2.1. The protocol: Messages and system

This section shows the protocol modelling, Fig. 6 (#Protocol description). In addition to the general modelling of the protocol, we explain how to solve two technical problems with CasperFDR:

First, we could not directly model an initial step of placing x and offer into the issuer’s memory at the manufacturing stage. We solve this by making the issuer know x and offer, whereas in reality the issuer does not know it explicitly but rather implicitly from the value $V_i$ (where $V_i = h_{x} [Issuer, offer]$ ) which is placed by the cashier inside the issuer’s memory during the manufacturing stage. However, if this model holds, then it guarantees more security because our modelling is more vulnerable than the original protocol.

Second, modelling the quadratic residue theorem, where we propose two ways of abstracting QR in the model with the pros and cons of both methods, which can be applied to any protocol use QR (not only this protocol). The QR used in this protocol is assumed to be indeed computationally infeasible since this is the basis for the protocol. Any claimed secret values utilising QR are assumed to be secret in this analysis. The model does not concern with any mathematical attacks against the QR (cryptanalysis) and, in that way, deals with it as if it is a secure and robust encryption algorithm.

A way to abstract QR might be by modelling QR as a shared secret key between the issuer and the cashier. Any value utilising the QR to be secret is encrypted with a normal encryption algorithm and a key named as QR. The shared secret key method is equivalent to QR from a secrecy perspective and both of them need some initial secret values. The advantage of modelling through the shared secret key is that it is as secure as QR (secrecy of hidden values), and as vulnerable as the QR (e.g. replay attack), where any attack against the QR can be detected. With that in mind, we model the QR as a shared secret key between the issuer and the cashier QR(I,C), see #Protocol description Messages 2QR and 3QR. Note that we split Messages 2 and 3 into sub-messages for efficiency reason.

In #System all participants engage in the protocol only once, except on the occasion where the cashier engages twice to examine No Multiple Cash-in property.

Fig. 6.

CasperFDR modelling of the Hsiang et al. (QR-based) protocol.

5.2.2. The protocol’s requirements

This section illustrates modelling and capturing properties of the protocol.

Fig. 7.

Capturing Hsiang et al. (QR-based) NFC M-coupon requirements.

Confidentiality and Secrecy of Issuer’s ID. Secrecy of Issuer’s ID is not captured in this model because the protocol does not assume a random ID for the issuer.

Confidentiality is modelled in CasperFDR as follows: $\begin{array}{rcl} Confidentiality – QR Based : StrongSecret(C,x,offer,r,[I]); \\ Confidentiality – QR Based : StrongSecret(C,rc,[U]) . \end{array}$

Cashier C claims that x, offer and r are confidential between them and issuer I. StrongSecret checks whether the intruder is able to break the claims without completing the protocol.

Figure 7 illustrates the secrecy specification between the issuer and the cashier. When cashier C performs the Claim_Secret.C.I.x.offer.r event, it can expect x, offer and r to be secret with issuer I. If this is violated, the intruder can complete a run of the protocol with the cashier without taking the issuer’s role, and learn some of the secret values.

Forgery Protection. Forgery Protection is modelled in CasperFDR as follows: $\begin{array}{rcl} Forgery Protection – QR Based : \\ NonInjectiveAgreement(I,C,[x,offer,Issuer]) . \end{array}$

The M-coupon is identified with x, offer and Issuer. This states that if a cashier accepts x, offer and Issuer, then the issuer must have issued them. NonInjective means that it is not concerned with repeats, i.e. the cashier can accept a number of times what has been issued only once. This is violated if the cashier accepts x, offer and Issuer that have not been issued by the issuer. This implies either that x, offer or Issuer have been created by an intruder (i.e. Unauthorised Generation) or that an M-coupon generated by the issuer has been modified to another (i.e. No Manipulation). Hence, if this property holds then there is Forgery Protection: No Unauthorised Generation and No Manipulation.

This is illustrated in Fig. 7. After the issuer completes its part of the protocol, it performs the Running.I.C.x.offer.Issuer event, which means issuer I starts a running of the protocol, apparently, with cashier C, agreeing on x, offer and Issuer. Later, the cashier will perform the Commit.C.I.x.offer.Issuer event at the end of its part of the protocol, which means that cashier C has finished the protocol with issuer I, agreeing on the x, offer and Issuer.

Unauthorized Copying (Not Transferable). Not Transferable is modelled in CasperFDR as follows: $\begin{array}{rcl} Not Transferable – QR Based : \\ NonInjectiveAgreement(I,C,[x,offer,Issuer,User]) . \end{array}$

A stronger specification than forgery protection is Not Transferable. The Not Transferable requires also an agreement on user identity. The coupon, $[x, offer, Issuer]$ , must be attached to one user only User. Both the issuer and cashier agree on the user to use the coupon as many times as they like, as long as the coupon has been issued by a genuine issuer, and is being used by the intended user.

This is shown in Fig. 7. After the issuer completes its part of the protocol, it performs the Running.I.C.x.offer.Issuer.User event, which means issuer I starts a running of the protocol, apparently, with cashier C, agreeing on x, offer, Issuer and User. Later, the cashier will perform the Commit.C.I.x.offer.Zssuer.User event at the end of its part of the protocol, which means that cashier C has finished the protocol with issuer I, agreeing on the x, offer, Issuer and User.

If it holds, not only then must the M-coupon be genuine, as for forgery protection, but it also must have the same user.

Data Integrity. Data Integrity is modelled in CasperFDR as follows: $\begin{array}{rcl} Data Integrity – QR Based : \\ NonInjectiveAgreement(I,C,[x,offer,Issuer,User,r]) . \end{array}$

This will check the integrity of the protocol between the issuer and the cashier. Both the cashier and issuer must agree on all the information in the protocol. This is shown in Fig. 7, the Running.I.C.x.offer.Issuer.User.r event and the Commit.C.I.x.offer.Issuer.User.r.

Unauthorized Copying (User Authentication). This is a stronger specification of Unauthorized Copying. It is an authentication between the user and the cashier that the user is the one who he/she claims to be. We model User Authentication in CasperFDR as follows: $\begin{matrix} User Authentication – QR Based : Agreement(U,C,[User,pin]) . \end{matrix}$ The user is authenticated with a password pin shared between the user and the cashier. If this is violated, then the authentication measure fails and the user is not properly authenticated. If this holds, then this means that the use of the password pin has been uniquely used, for only this run of the protocol, by the associated user User.

This is illustrated in Fig. 7. Just before Message 3, the user performs the Running.U.C.pin event, which means that user U declares they are running the protocol, apparently, with the cashier C, agreeing on pin. Later, the cashier will perform the Commit.C.U.pin event at the end of its part of the protocol, which means that cashier C has finished the protocol with user U, agreeing on pin. Agreement will make sure that every Running event by the user corresponds to one Commit by the cashier, which is required in such an authentication.

No Multiple Cash-in. No Multiple Cash-in is modelled in CasperFDR as follows: $\begin{matrix} Agreement(I,C,[x,offer,Issuer]) . \end{matrix}$

This specification states that every time the cashier accepts x, offer and Issuer, there must be a separate occasion where the issuer must have issued them. Hence, a cashier cannot accept x, offer and Issuer more times than an issuer sent them.

Figure 7 illustrates a scenario where the cashier is engaging in the protocol twice, with one issuer run. The first time the cashier runs the protocol with the user’s mobile, and the second – illegal – time with Mallory who might be an intruder or the user himself. The second Commit should not occur if there was not a separate Running.

Intruder knowledge. In order for the intruder to be able to communicate with all of all engaging parties, the intruder knows the identities of them (User, Issuer and Cashier). The hash function h is assumed to be known by the intruder. We extend the intruder knowledge with a new nonce (Rm), a different password with the cashier PinM, a previous secret value x (Xm) and a different offer (OfferM).

5.3. Analysis

Table 2
QR based protocol against requirements

QR based protocol

Confidentiality √

Secrecy of Issuer’s ID √

Forgery Protection √

Data Integrity √

No Multiple Cash-in √

Not Transferable √

User Authentication x

	QR based protocol
Confidentiality	√
Secrecy of Issuer’s ID	√
Forgery Protection	√
Data Integrity	√
No Multiple Cash-in	√
Not Transferable	√
User Authentication	x

Fig. 8.

The QR-based protocol attack trace.

In Table 2, the analysis shows no attack against all properties except for User Authentication. Figure 8 shows the attack trace found by CasperFDR. After the user sends their identity to a dishonest issuer (the intruder), the intruder passes the identity to the issuer in order to get a coupon issued with the user ID. Then, the issuer generates an M-coupon containing QR and M (as described in Fig. 8). As the user is waiting for an M-coupon, the intruder sends the QR, which cannot be modified, and a manipulated M ( $M^{'}$ ). At the cashing phase, the only part the intruder needs to cash the M-coupon is the user authentication credential part (Auth). The intruder combines an Auth with the QR and M to get a valid M-coupon. In fact, this attack suggests that a user authentication credential Auth can be attached to any M-coupon generated for the same user, and then can be cashed by any dishonest user. There is no relationship between the M-coupon and the authentication credential (the password PIN) except the user’s ID. If the user has issued other M-coupons, then the intruder is able to combine different M-coupons with different passwords. At the end of the protocol, the cashier will conclude with a false belief about the relationship between an M-coupon and a user authentication.

We check the attack against a weaker intruder who does not know the different values of x an offer, Xm and OfferM respectively, and found that the attack is still valid. The tested systems are as follows:

1 User, 1 Issuer and 1 Cashier, with a powerful Intruder.

1 User, 1 Issuer and 2 Cashiers, with a powerful Intruder.

1 User, 1 Issuer and 1 Cashier, with a weaker Intruder (i.e. does not know Xm and OfferM).

1 User, 1 Issuer and 2 Cashiers, with a weaker Intruder.

1 User, 2 Issuers and 1 Cashiers, with a powerful Intruder.

In order to succeed, the attack would need the attacker to impersonate the cashier and the User’s mobile would need to initiate the protocol to the fake NFC terminal. Impersonation of the cashier need not be so difficult, for example the attacker could carry the necessary equipment hidden in a backpack to perform the necessary man-in-the-middle manipulations. However, tricking the victim to initiate the coupon cashing part of the protocol might be more difficult, depending on how this is triggered. In practice this does appear feasible but would require careful exploitation of the relative proximities of the parties.

This attack can be addressed by requiring the user to include a hash all M-coupon parts (Auth, QR and M) and include this hash in order to enhance the integrity once the cashier checks.

The analysis included removing some parts of the protocol and checking the result. We removed $h (y)$ and $h (r)$ from Messages 2 and 3. We found no attack, which means they are unnecessary parts of the protocols for the properties under consideration. The reason is that the integrity of values y and r are already established in the hash in $V_m = h_{V_{i}} [r, y]$ at the same message.

5.4. Dividing messages in CasperFDR

During the process of analysis, an interesting observation was made regarding attacks found in divided messages. Once we divided long messages into different parts which is fine according to the CasperFDR manual [38], finding an attack can be affected by the sequence arrangement of these messages. As illustrated in Fig. 9, this is related to how CasperFDR places the authentication events (Running/Commit) in the protocol. The user normally performs the Running event at the last sent message. As we divide the last message into three parts, Alice considers them as three different messages and only declares the running event at the last message sent (Message 1 (part C)). The Intruder may be able to only use parts 1 or 2 of Message 1 to launch an attack, without part 3, satisfying the definition of CasperFDR attack (completing a run of the protocol, with bob, without a Running event from Alice). However, the intruder would not be able to do this if all data of Message 1 were sent in a complete session as assumed by the protocol.

In the QR-based protocol, we divide the last message sent from the user to the cashier to three parts (Auth, QR and M) because it is a large message and we want to enhance the analysis performance. The attack should be detected with any sequence arrangement of these parts but if one places the Auth part at the end, no attack is found. As we explained above, this is related to Running event performed by the user. When the intruder gets the Auth part before running event by the user, the different parts of the M-coupon can be combined successfully. Then, the intruder is able to complete the protocol with the cashier when the cashier performs Commit event.

Fig. 9.

Placing authentication events. (a) Data sent in a single message. (b) Data sent in a divided message.

So, dividing messages into different parts can result to false attacks. Of course, the best way to avoid such behaviour is by sending the message in one part, however this is quite difficult and sometimes even impossible as the message is too large and CasperFDR cannot handle it. Therefore, we advice with divided message to rearrange the order of these sub messages. If there is an attack in the protocol, it should be detected in all orders. If there is not any attack in the protocol, then it should not be any attack with any order as well. However, if an attack is detected because of the order of sub messages, this needs more consideration and justification to the analysed protocol to decide whether it is a true attack.

6. Conclusion

The journey of securing the NFC M-coupon has already started since 2007. Three NFC M-coupon protocols have been proposed in the literature, and all of which tried to meet some NFC M-coupon security requirements by designing secure cryptographic protocols. Likewise, all of them have “informally” analysed the security of their protocols and how their protocols meet the claimed security requirements.

We introduced a security framework for modelling and analysis of NFC mobile coupon. The framework captures eight security requirements of NFC M-coupon protocols. In previous publications, three NFC M-coupon protocols in the literature were formally analysed, and solutions were suggested when attacks are found in these protocols.

In this paper, we illustrate the use of the framework by analysing the QR-based protocol. We solved the challenge of modelling the quadratic residue theorem by proposing two ways of abstracting QR in the model with the pros and cons of both methods. The alternative solutions can be applied to any protocol with QR either in NFC or other domain such as the Internet. CasperFDR found that the protocol is vulnerable to a user authentication attack. This result to a possibility for an intruder to combine different M-coupons with different passwords as long as it is not known by the cashier. However, if all parts of the M-coupon are sent by the user in one message, then this is a difficult attack to do. In addition, we made an important observation regarding dividing long messages in CasperFDR and how this might affect the validity of an attack.

There are a number of possible future work directions:

The formal security approach provided in this paper can be used to create new NFC protocols for different applications. The requirements of other application might overlap with the NFC M-coupon, which will make the modelling process much easier. In fact, the approach can be implemented for any other existing technologies, such as the Internet and wireless, or new similar emerging technologies such as iBeacon which was introduced by Apple.1

https://developer.apple.com/ibeacon/.

Designing a formal general architecture for NFC protocols that normally include three parties: a user, initiator and receiver. For example, in M-coupon: a user, an issuer and a cashier, in M-payment: a user, a bank and a merchant and in M-ticketing: a user, an issuer and the gate. It would be very useful for NFC community to have a general secure architecture that deals with such protocols. Required modification for each application should be allowed within the main architecture itself.

Capturing the anonymity aspect of NFC M-coupon protocols either in native CSP or by other tools such as the ProVerif tool [36].

Footnotes

Acknowledgments

We are grateful to the anonymous reviewers for their careful and thorough consideration of the paper and their suggestions for improvements.

References

[1]

Abadi and

A.D.

Gordon, A calculus for cryptographic protocols: The spi calculus, in: Proceedings of the 4th ACM Conference on Computer and Communications Security, ACM, 1997, pp. 36–47.

[2]

Abughazalah,

Markantonakis and

Mayes, A mutual authentication protocol for low-cost RFID tags formally verified using casper/FDR and AVISPA, in: 2013 8th International Conference for Internet Technology and Secured Transactions (ICITST), 2013, pp. 44–51.

[3]

Al-Shadly, Verification of security properties using formal techniques, PhD thesis, Niedersächsische Staats- und Universitätsbibliothek Göttingen, 2013.

[4]

Alshehri,

J.A.

Briffa,

Schneider and

Wesemeyer, Formal security analysis of NFC m-coupon protocols using casper/FDR, in: 2013 5th International Workshop on Near Field Communication (NFC), 2013, pp. 1–6.

[5]

Alshehri and

Schneider, Formal security analysis and improvement of a hash-based NFC m-coupon protocol, in: 12th Smart Card Research and Advanced Application Conference (CARDIS 2013), 2013.

[6]

Alshehri and

Schneider, Formally defining NFC m-coupon requirements, with a case study, in: 2013 8th International Conference for Internet Technology and Secured Transactions (ICITST), 2013, pp. 52–58.

[7]

Basin,

Mödersheim and

Vigano, OFMC: A symbolic model checker for security protocols, International Journal of Information Security 4(3) (2005), 181–208.

[8]

Biere,

Cimatti,

E.M.

Clarke,

Fujita and

Zhu, Symbolic model checking using SAT procedures instead of BDDs, in: Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, ACM, 1999, pp. 317–320.

[9]

Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: Proceedings of the 14th IEEE Computer Security Foundations Workshop, IEEE Computer Society, 2001, pp. 82–96.

10.

[10]

Bournelle,

Laurent-Maknavicius,

Tschofenig and

El Mghazli, Handover-aware access control mechanism: CTP for PANA, in: Universal Multiservice Networks, Springer, 2004, pp. 430–439.

11.

[11]

S.H.

Brackin, A HOL extension of GNY for automatically analyzing cryptographic protocols, in: Proceedings of the 9th IEEE Computer Security Foundations Workshop, 1996, IEEE, 1996, pp. 62–76.

12.

[12]

Brown, The future is NFC says coupons.com exec, 2011, available at: http://www.nfcworld.com/2011/03/10/36399/the-future-is-nfc-says-coupons-com-exec/.

13.

[13]

Burrows,

Abadi and

R.M.

Needham, A logic of authentication, Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences 426(1871) (1989), 233–271.

14.

[14]

Chen,

J.-S.

Chou and

H.-M.

Sun, A novel mutual authentication scheme based on quadratic residues for RFID systems, Computer Networks 52(12) (2008), 2373–2380.

15.

[15]

Clark, Survey: Discounts and coupons will drive adoption of mobile payments, 2011, available at: http://www.nfcworld.com/2011/06/23/38289/survey-discounts-and-coupons-will-drive-adoption-of-mobile-payments.

16.

[16]

Cohen, Taps: A first-order verifier for cryptographic protocols, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW-13, IEEE, 2000, pp. 144–158.

17.

[17]

Cohen, First-order verification of cryptographic protocols, Journal of Computer Security 11(2) (2003), 189–216.

18.

[18]

Coskun,

Ok and

Ozdenizci, Near Field Communication: From Theory to Practice, 1st edn, John Wiley and Sons, Ltd, 2012.

19.

[19]

Coskun,

Ozdenizci and

Ok, A survey on near field communication (NFC) technology, Wireless Personal Communications 71(3) (2013), 2259–2294.

20.

[20]

C.J.F.

Cremers, Scyther: Semantics and verification of security protocols, 2006.

21.

[21]

Delaune,

Lin and

Lynch, Protocol verification via rigid/flexible resolution, in: Logic for Programming, Artificial Intelligence, and Reasoning, Springer, 2007, pp. 242–256.

22.

[22]

Dolev and

Yao, On the security of public-key protocols, IEEE Transactions on Information Theory 29(2) (1983), 198–208.

23.

[23]

Dominikus and

M.J.

Aigner, M-coupons: An application for near field communication (NFC), in: Advanced Information Networking and Applications Workshops, 2007, pp. 421–428.

24.

[24]

Donovan,

Norris and

Lowe, Analyzing a library of security protocols using Casper and FDR, in: Proceedings of the Workshop on Formal Methods and Security Protocols, 1999.

25.

[25]ECMA International, NFC-SEC: NFCIP-1 security services and protocol, 2010.

26.

[26]ECMA International, NFC-SEC-01: NFC-SEC cryptography standard using ECDH and AES, 2010.

27.

[27]

Finkenzeller, RFID Handbook: Fundamentals and Applications in Contactless Smart Cards, Radio Frequency Identification and Near-Field Communication, 3rd edn, John Wiley and Sons, Ltd, 2010.

28.

[28]

Francis,

G.P.

Hancke,

Mayes and

Markantonakis, Practical NFC peer-to-peer relay attack using mobile phones, in: RFIDSec, 2010, pp. 35–49.

29.

[29]

Gong,

Needham and

Yahalom, Reasoning about belief in cryptographic protocols, in: Proceedings of 1990 IEEE Computer Society Symposium on Research in Security and Privacy, IEEE, 1990, pp. 234–248.

30.

[30]

Haselsteiner and

Breitfuß, Security in near field communication (NFC), in: Proceedings of Workshop on RFID and Lightweight Crypto (RFIDSec06), 2006.

31.

[31]

C.A.R.

Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.

32.

[32]

H.-C.

Hsiang,

H.-C.

Kuo and

W.-K.

Shih, A secure m-coupon scheme using near field communication, International Journal of Innovative Computing, Information and Control 5(11) (2009), 3901–3909.

33.

[33]

H.-C.

Hsiang and

W.-K.

Shih, Secure m-coupons scheme using NFC, in: International Conference on Business and Information, 2011.

34.

[34]ISO/IEC, Information technology – Telecommunications and information exchange between systems – Near field communication – Interface and protocol (NFCIP-1), 2004.

35.

[35]Juniper Research, Mobile coupons – Ecosystem analysis and marketing channel strategy 2011–2016, Technical report, Juniper Research, 2011.

36.

[36]

Kremer and

Ryan, Analysis of an electronic voting protocol in the applied pi calculus, in: Programming Languages and Systems, Springer, 2005, pp. 186–200.

37.

[37]

Lowe, An attack on the Needham–Schroeder public-key authentication protocol, Inf. Process. Lett. 56(3) (1995), 131–133.

38.

[38]

Lowe, Casper: A compiler for the analysis of security protocols, Journal of Computer Security 6(1-2) (1998), 53–84.

39.

[39]

Mathuria,

Safavi-Naini and

Nickolas, On the automation of GNY logic, Australian Computer Science Communications 17 (1995), 370–379.

40.

[40]

K.L.

McMillan, Symbolic Model Checking, Springer, 1993.

41.

[41]

Mulliner, Vulnerability analysis and attacks on NFC-enabled mobile phones, in: ARES, 2009, pp. 695–700.

42.

[42]

Patel,

Borisaniya,

Patel,

Rajarajan and

Zisman, Comparative analysis of formal model checking tools for security protocol verification, in: Recent Trends in Network Security and Applications,

Meghanathan,

Boumerdassi,

Chaki and

Nagamalai, eds, Communications in Computer and Information Science, Vol. 89, Springer, Berlin, Heidelberg, 2010, pp. 152–163.

43.

[43]

L.C.

Paulson, The inductive approach to verifying cryptographic protocols, Journal of computer security 6(1) (1998), 85–128.

44.

[44]

J.C.L.

Pimentel and

Monroy, Formal support to security protocol development: A survey, Computación y Sistemas 12(1) (2008), 89–108.

45.

[45]

K.H.

Rosen, Elementary Number Theory and Its Applications, Reading, MA, 1993.

46.

[46]

P.Y.A.

Ryan,

S.A.

Schneider,

Goldsmith,

Lowe and

A.W.

Roscoe, Modelling and Analysis of Security Protocols, Addison-Wesley–Longman, 2001.

47.

[47]Smart Card Alliance, Proximity mobile payments business scenarios: Research report on stakeholder perspective, Technical report, Smart Card Alliance, 2008.

48.

[48]

D.X.

Song,

Berezin and

Perrig, Athena: A novel approach to efficient automatic security protocol analysis, Journal of Computer Security 9(1) (2001), 47–74.

49.

[49]

Steel and

Bundy, Attacking group protocols by refuting incorrect inductive conjectures, Journal of Automated Reasoning 36(1-2) (2006), 149–176.

50.

[50]

Steel,

Bundy and

Denney, Finding counterexamples to inductive conjectures and discovering security protocol attacks, AISB Journal 1(2) (2002), 169–182.

51.

[51]

Viganò, Automated security protocol analysis with the AVISPA tool, Electronic Notes in Theoretical Computer Science 155 (2006), 61–86.

52.

[52]

Weidenbach,

Afshordel,

Brahm,

Cohrs,

Engel,

Keen,

Theobalt and

Topić, System description: Spass version 1.0.0, in: Automated Deduction – CADE-16, Springer, 1999, pp. 378–382.

53.

[53]

Wolverton, Disney battles coupon goof, 2002, available at: http://news.cnet.com/2100-1017-964831.html.

A formal framework for security analysis of NFC mobile coupon protocols

Abstract

Keywords

1. Introduction

2.1. Security protocol analysis

2.2. M-coupon protocols analysis

3. The CasperFDR approach

3.1. Simple example

3.2. CasperFDR modelling

4. Formal definition of NFC M-coupon security requirements

4.1. Threat model

4.2. Confidentiality

4.4. Unauthorized Copying (Not Transferable)

4.5. Unauthorized Copying (User Authentication)

4.6. Data Integrity

4.7. No Multiple Cash-in

4.8. Secrecy of Issuer’s ID

5. Modelling and analysis of QR-based NFC M-coupon protocol

5.1. Protocol description

5.2.1. The protocol: Messages and system

Table 2 QR based protocol against requirements QR based protocol Confidentiality √ Secrecy of Issuer’s ID √ Forgery Protection √ Data Integrity √ No Multiple Cash-in √ Not Transferable √ User Authentication x

Footnotes

Acknowledgments

References

Table 2
QR based protocol against requirements

QR based protocol

Confidentiality √

Secrecy of Issuer’s ID √

Forgery Protection √

Data Integrity √

No Multiple Cash-in √

Not Transferable √

User Authentication x