Scyther

An Online Security Protocol for NFC Payment Formally Analyzed by The Scyther Tool

Nour El Madhoun∗, Fouad Guenane†, Guy Pujolle∗

∗Sorbonne Universités, UPMC Univ Paris 06, CNRS, LIP6 UMR 7606, 4 place Jussieu 75005 Paris, France †Devoteam Group, 1 Rue Galvani 91300 Massy, France

Email: {nour.el-madhoun, guy.pujolle}@lip6.fr; [email protected]

Abstract—Nowadays, NFC technology is integrated into bank cards, smartphones and sales point terminals in order to immedi- ately execute payment transactions without any physical contact. EMV is the standard intended to secure both contact (traditional) and contactless-NFC payment operations. In fact, researchers in recent years have detected some security vulnerabilities in this protocol (EMV). Therefore, in this paper, we introduce the risks entailed by the vulnerabilities of EMV and particularly those at stake in the case of NFC payment. Hence, in order to overcome EMV weaknesses, we propose a new security protocol based on an online communication with a trusted entity. The proposal is destined to secure contactless-NFC payment transactions using NFC bank cards that are unconnected client payment devices (without Wi-Fi or 4G). A security verification tool called Scyther is used to analyze the correctness of the proposal.

Index Terms—NFC, EMV, mutual authentication, confidential- ity, NFC bank card, NFC payment terminal.

I. INTRODUCTION

Near Field Communication (NFC) is a wireless proximity

technology operating at 13.56 MHz. It enables interaction

between two electronic devices without contact and within

a short distance (maximum 10 centimeters) [1]. Today, it is

widely used in contactless payment systems: VISA payWave

[2] and MasterCard PayPass [3]. A contactless-NFC payment

operation is executed simply by approaching an NFC bank

card (or an NFC phone) near to an NFC point of sale ter-

minal. In addition, NFC payment applications can be divided

into micro and macro payments. Micro-payment is for small

amounts (maximum limit, 20 Euro in France) with no need to

compose a PIN code or a signature. If the amount is higher

than the authorized limit, the transaction is termed a macro-

payment. In this case, the client must confirm the transaction

by entering a PIN code or a signature [4].

Europay Mastercard Visa (EMV) is the security protocol

implemented for: (1) the classical payment system (inserting

the card into the terminal), (2) the contactless payment system

based on NFC technology. However, researchers have found

security vulnerabilities in this protocol by studying EMV

specifications [5]. Consequently, the work [6] and [7] show

that EMV vulnerabilities represent a big risk in the case of

NFC payment compared to the traditional payment: because

an attacker can, by remotely using NFC radio waves, retrieve

sensitive banking data stored on a victim’s NFC bank card.

In this paper, we propose a new security protocol allowing

to overcome weaknesses that have been emerged in EMV

standard. The proposal is based on an online communication

with an authentication server that is considered a representative

of the confidence and security of issuing and acquiring banks,

and it is connected to them in real time. We suggest that

the proposal is intended primarily to secure contactless-NFC

payment operations using unconnected (without Wi-Fi or 4G)

NFC client payment devices such as NFC bank cards.

Thanks to the asymmetric cryptography, the proposed proto-

col ensures: (1) mutual authentication and (2) non-repudiation

between an NFC bank and an NFC payment terminal, (3) the

integrity of banking data, (4) the validity of the bank card (not

revoked). (5) The encryption of banking data (confidentiality)

is well guaranteed using a symmetric session key calculated

during the authentication steps. We verify formally the cor-

rectness of the proposal by the Scyther tool which provides

formal evidence for security protocols.

This paper is organized as follows. Section II details EMV

protocol and EMV weaknesses whereas section III introduces

the related literature. In section IV, we describe the proposed

security protocol and in section V we discuss some possible

attacks. In section VI, we present Scyther verification results.

The last section provides a brief conclusion.

II. EMV PROTOCOL

EMV Consortium (EMVCo) has initiated EMV as the

international security protocol for contact and contactless-NFC

payment systems. It is a set of security rules for performing a

payment transaction between participants: client’s payment de-

vice, payment terminal, terminal’s acquiring bank and client’s

issuing bank [5].

A. EMV Procedure

To execute a purchase transaction (contact or contactless-

NFC), three EMV security steps are required [8] [9]:

• Card authentication: ensures the payment terminal of the

authenticity of the client’s payment device and integrity

of sensitive banking data. It allows protection against

counterfeit client payment devices.

• Cardholder verification: ensures customer authenticity to

the payment terminal with the verification of a PIN code

or a signature. It allows protection against lost and stolen

client payment devices. This phase is not guaranteed in

the case of NFC micro-payments.

• Transaction authorization: ensures the payment terminal

that the client’s issuing bank authorizes the transaction.

1

In fact, EMV phases can be executed either online or offline

[10] [11]. The mode of execution depends on the connec-

tion availability in payment terminals, for example payment

transactions in a supermarket require an online mode whereas

transactions on an airplane require an offline mode.

• Online mode: first of all requires a connection between

the payment terminal and its acquiring bank, and then

between the latter and the client’s issuing bank. In this

mode, security procedures will be performed by issuing

and acquiring banks.

• Offline mode: means that security procedures will be

made in the payment terminal.

B. EMV weaknesses

In the online mode, the revocation of a client’s payment

device is well checked by the payment terminal thanks to the

connection to banks. However, during an offline transaction,

the payment terminal cannot verify if the client’s payment

device has been revoked. So, a malicious person can use

for example a revoked bank card to perform unauthorized

transactions [12]. This vulnerability will not be processed in

this work. It will be the objective for a future contribution.

Thus, in this paper, we deal with two security vulnerabilities

that have been detected by researchers in the first phase "Card

authentication" of EMV procedure (in both modes) [6] [7]:

• The authenticity of the payment terminal is not ensured

to the client’s payment device.

• The banking data exchanged between the client’s pay-

ment device and the point of sale terminal are not

encrypted and are transferred in clear. In fact, according

to EMV specifications [5], the Primary Account Number

(PAN) is the banking information which must be sent in

clear because it identifies the client’s payment device in

the issuing bank, but we note that the PAN is a sensitive

information and therefore must be protected.

C. Risks

In the case of NFC payment, the communication takes

place in an open environment using NFC radio waves which

represents a major risk, but EMVCo has assumed that within

a maximum reading distance of 10 centimeters, it is difficult

for an attacker to steal private banking data from an NFC bank

card with an unauthenticated NFC reader [5]. The studies [6]

and [7] confirm that the previous assumption is very weak and

show that EMV protocol is not suited to security needs of NFC

payment systems: an attacker who has radio-electronics skills,

is able to use an NFC reader (or an NFC smartphone) equipped

with a special antenna, to remotely steal (from a distance of a

few meters) sensitive banking data from a victim’s NFC bank

card even if the latter is in the bag.

The information that can be retrieved by an attacker are: the

PAN and expiration date. The visual cryptogram (CVV: Card

Verification Value) and the cardholder’s name are not recov-

erable. Hence, the attacker can harm the victim by making

for example fraudulent purchase transactions on the Internet.

Today, there are e-commerce websites that apply the CVV and

other websites do not apply it such as "www.amazon.com",

which leaves a breach for fraudulent transactions (exploitation

of data). As Fig-1 illustrates, we were able to buy sev-

eral items on "www.amazon.com" using banking information:

PAN, expiration date, the good cardholder’s name and without

providing a CVV. In addition, the cardholder’s name is not

verified in many websites where we can add a random name

and confirm transactions. We have also tried to add the same

banking data to "www.amazon.com" but with a random name

and we have succeeded again in buying several items.

Fig. 1. Adding banking data (amazon)

III. RELATED LITERATURE

NFC technology allows to store and manage personal and

monetary data, so it must be able to provide a safe and

secure environment for users. In fact, on the NFC wireless

communication, there are several possible attacks, such as:

data insertion, data modification, eavesdropping, replay at-

tacks, etc. An attacker can insert falsified data during the

NFC communication into the data transmitted, he can also

replace the original data with other information. Therefore,

many research studies have proposed solutions to these attacks:

an approach consists in using a secure communication channel

is introduced in [13] and [14].

For the eavesdropping, an attacker can use a good and

large antenna to intercept data transmitted between two NFC

devices. Hence, the NFC-SEC protocol (NFCIP-1 Security

Services and Protocol) is introduced to enable a symmetric

encryption between NFC devices by exchanging a symmetric

secret key [14]. Thus, Elbagoury et al. [15] have proposed a

solution allowing to prevent eavesdropping by operating the

noisy wireless channel to get a provable key and then distribute

it among participants of the NFC communication. In addition,

a replay attack can be prevented using random numbers

(nonce) [16] or using physical proximity based information

(temperature data) [17].

Recently, the security of contactless-NFC payment systems

has become an interesting topic in scientific research to

provide new security solutions. Urien and Piramuthu [18] have

proposed a framework and new authentication protocols based

on Elliptic Curve Cryptography (ECC) and intended to secure

NFC payment systems using NFC smartphones in a retail store

environment. Thanks to ECC, the proposed protocols allow a

low-complexity (minimal messages, lower storage, etc.) for

NFC smartphone’s resources (memory, space, etc.). However,

when the attacks on bank data can be made in a very simple

and fast way thanks to the NFC radio waves (as presented

2

in the section II-C), the risks are increasing and consequently

they are becoming more dangerous.

Ceipidor et al. [19] have proposed a mutual authentication

protocol between NFC phones and point of sale terminals

allowing to secure NFC payment operations. This protocol

is based on an online communication with an authentication

server that shares symmetric keys with phones and terminals.

It ensures mutual authentication and confidentiality of private

banking data. Therefore, it solves EMV weaknesses but it

lacks ensuring origin non-repudiation, banking data integrity

and the validity of the phone (banking data are not revoked).

In addition, the idea of using a single server that shares secret

symmetric keys with NFC phones and terminals, remains a

little difficult to implement in a real environment.

In our previous work [20], we have proposed a security

protocol that allows to overcome EMV vulnerabilities and is

based on a Cloud infrastructure using asymmetric cryptogra-

phy. It is designed especially for NFC payment transactions

between an NFC payment terminal and an NFC smartphone,

which is a connected object (Wi-Fi or 4G) communicating

through a secure channel with the Cloud. The latter offers

security services for NFC phones. Hence, this protocol enables

a very efficient use of the smartphone’s resources, because its

purpose is to offload the authenticity verification procedure of

the terminal from the NFC phone to the Cloud. It ensures:

mutual authentication and non-repudiation between the NFC

terminal and the NFC smartphone, confidentiality and integrity

of banking data. It lacks ensuring the validity of banking data

that they are not revoked because it is executed in the offline

mode (the payment terminal is not connected to banks).

IV. PROPOSED PROTOCOL

A. Principal

We propose in this study a security protocol that treats EMV

weaknesses founded in the EMV card authentication phase

(see section II-B). Tab-I shows the abbreviations allowing to

simplify future descriptions. The proposal includes three actors

illustrated in Fig-2: Authentication Server (AS), NFC Point

of Sale (POS), NFC Bank Card (C). Each actor represents a

specific role detailed in the next section IV-B. Tab-II details

the security elements we assume each actor has in this work.

We specify several assumptions:

• The proposal is based on an online communication with

an authentication server AS using the asymmetric cryp-

tography (not sharing symmetric keys as [19]) which is

more rapid for authentication purposes compared to the

symmetric cryptography.

• AS is able to execute security functions. The acquiring

banks and the issuing banks trust and rely on this server

for NFC transactions.

• The proposal is mainly destined to secure NFC payment

transactions in the case of using unconnected NFC bank

cards (without Wi-Fi or 4G), that are able to communicate

with other devices only via NFC radio waves.

• The NFC payment terminals and NFC bank cards trust

the server AS.

• We suggest to use an identifier IdC which is different

from PAN (keep PAN secret) to identify an NFC bank

card C in AS and its issuing bank. IdC cannot be used

for purchases on the Internet

• POS can communicate directly with AS, but C can

communicate with AS only through POS.

• AS must register identifiers of all NFC bank cards assum-

ing that the issuing banks have already agreed to this.

TABLE I ABBREVIATIONS

Abbreviation Description

POS NFC Point Of Sale

C NFC Bank Card

AS Authentication Server

CAi Certification Authority (i=1,2,3)

IssBank Card’s Issuing Bank

AcqBank Terminal’s Acquiring Bank

Hash(M) One way hashing function of M = m1,m2..

BankData Banking data stored on the Card

TD Transaction Data generated by POS (Unique)

Certificate(X) Certificate of X

pubKey(X) Public Key of X

secKey(X) Secret Key of X

K(POS,C) Symmetric session Key generated by AS to exchange information between POS and Card

K(AS,POS) Session Key allows to protect information exchange between AS and POS

B. Actors

1) Authentication Server (AS): it is a trusted entity not

only able to authenticate NFC bank cards to NFC payment

terminals, but also to authenticate the latter to NFC bank cards.

It is considered as a representative of confidence and security

of issuing and acquiring banks where it is connected to them

in real time. We assume that this server:

• Is available at any time and from any location.

• Stores a list of trusted certification authorities.

• Contains a security application that allows the verification

of certificates and digital signatures.

2) NFC Payment Terminal (POS): it is used to perform

NFC payment operations in shops for example. It is a con-

nected device and can communicate directly with AS for

security purposes, instead of communicating with its acquiring

bank and then the latter contacts the issuing bank. It connects

to AS through a secure channel TLS (Transport Layer Security)

[21]. At each connection, they (POS and AS) authenticate each

other and exchange a new session key K(AS,POS).

3) NFC Bank Card (C): to make purchases with an NFC

bank card C, the user needs only to approach it to POS. In fact,

C stores the server’s certificate and to communicate (through

the terminal POS) for security purposes with the server (AS),

it uses the server’s public key.

C. Details of the Protocol

This section describes all the steps of exchanged messages

of the proposed protocol illustrated in Fig-2.

3

Fig. 2. The proposed NFC security protocol

1) C Authentication request (POS->C):

• In the first step, POS sends to C in cleartext: transaction

data TD (date, hour, random values, etc.) that is unique for

each transaction and serves to prevent replay attacks, an

authentication request for C RequestC, Certificate(POS),

Certificate(AcqBank) and SignaturePOS.

– SignaturePOS is a signature generated by

secKey(POS) of ’POS, C, TD, RequestC’ message

after its hash.

• Certificate(POS), Certificate(AcqBank) and Signature-

POS allow to authenticate POS, guarantee the integrity

of ’POS, C, TD, RequestC’ message and ensure that

POS cannot deny having sent SignaturePOS in the future

(non-repudiation of origin).

• C does not have an application allowing the verification of

the authenticity of POS, but in the next step, it will send

the received message (1) to AS through POS to execute

an authentication verification procedure for POS.

2) POS Authentication and session requests (C->POS):

• (1) is the received message from POS requesting C au-

thentication and providing evidence authenticating POS:

Certificate(POS), Certificate(AcqBank), SignaturePOS.

• To prevent replay attacks, C generates a random num-

ber RandomC by hashing its identifier IdC and TD:

Hash(IdC,TD). Thus, C sends to AS through POS:

TABLE II WHAT HAS EACH ACTOR

Actor Owns

AS - pubKey(AS)/secKey(AS)

- Certificate(AS) signed by secKey(CA1) of CA1

POS - Certificate(AS)

- pubKey(POS)/secKey(POS)

- Certificate(POS) signed by secKey(AcqBank)

- Certificate(AcqBank) signed by secKey(CA2) of CA2

C - BankData: IdC, PAN, name, expiration date, etc.

- Certificate(AS)

- pubKey(C)/secKey(C)

- Certificate(C) signed by secKey(IssBank)

- Certificate(IssBank) signed by secKey(CA3) of CA3

- An electronic signature of BankData generated by secKey(IssBank): {Hash(BankData)}secKey(IssBank)

– Its identifier IdC in AS in cleartext.

– Information encrypted with pubKey(AS): the received

message (1), RandomC, an authentication request

for POS RequestPOS and a payment session request

4

RequestS. The latter asks AS to generate a session

key to begin a payment transaction. It also sends

Certificate(C), Certificate(IssBank) and SignatureC

encrypted with pubKey(AS).

– SignatureC is a signature generated by secKey(C)

of ’C, POS, AS, RandomC, RequestPOS, Request-

Session’ message after its hash.

• Certificate(C), Certificate(IssBank) and SignatureC al-

low to authenticate C, guarantee the integrity of ’C, POS,

AS, RandomC, RequestPOS, RequestSession’ message

and ensure that C cannot deny having sent SignatureC

in the future (non-repudiation of origin).

3) POS and C Authentication requests (POS->AS):

• POS cannot decipher the received message (2) because it

does not have the secret key of AS. Then, it sends to AS

in an encrypted text with the session key K(AS,POS) of

the current connection TLS: TD and the message (2).

• AS deciphers (3) with K(AS,POS), obtains TD and (2). It

checks TD validity and if it is not valid, then it will not

respond to POS. Otherwise, it deciphers the message (2)

with its secret key secKey(AS) and obtains the content.

• In fact, AS and POS have already authenticated each other

during the TLS session and they communicate securely

using K(AS,POS) session key, so AS will proceed to

authenticate the NFC bank card C to POS, and if it leads

to successful results, then it executes another verification

procedure (different from TLS procedure) authenticating

POS to C because:

– It has received an POS authentication request Re-

questPOS from C (message (2)).

– C has received evidence authenticating POS (mes-

sage (1)) but it could not verify POS authenticity

and it trusts in fact AS to execute security functions.

• Therefore, AS proceeds classically in order to authenticate

the card C to POS. It checks that:

– Certificate(C) and Certificate(IssBank) are valid to-

day (validity period) and not revoked.

– The issuing CA3 of Certificate(IssBank) is a trusted

certification authority.

– pubKey(CA3) validates the signature contained in

Certificate(IssBank).

– pubKey(IssBank) validates the signature contained in

Certificate(C).

– pubKey(C) validates SignatureC.

• If AS can successfully authenticate C, then it proceeds to

authenticate POS to C. It checks that:

– Certificate(POS) and Certificate(AcqBank) are valid

today (validity period) and not revoked.

– The issuing CA2 of Certificate(AcqBank) is a trusted

certification authority.

– pubKey(CA2) validates the signature contained in

Certificate(AcqBank).

– pubKey(AcqBank) validates the signature contained

in Certificate(POS).

– pubKey(POS) validates SignaturePOS.

4) C Authenticity and session confirmations (AS->POS):

• If AS leads to successful results of POS authenticity, then

it generates a session key K(POS,C) that serves to start

a new secure payment transaction between POS and C.

• Thus, it sends to POS in an encrypted text with

K(AS,POS) Conf1 and Conf2 respectively confirming the

authenticity of C and POS, and mainly containing the

session key K(POS,C) (see Fig-2).

• POS deciphers the received message, checks TD and

RandomC, authenticates C with AuthC message, obtains

K(POS,C), Conf2 and Certificate(IssBank). The latter is

verified and confirmed by AS, and serves for POS to

verify the signature of banking data in step (6) (see

section IV-C6). Conf2 cannot be deciphered by POS

because it is encrypted with pubKey(C) and it is destined

in reality from AS to C passing by POS. It mainly

contains a confirmation message of the POS authenticity

AuthPOS, K(POS,C) session key and SignatureAS.

– SignatureAS is a signature generated by secKey(AS)

of ’POS, C, AS, K(POS,C), TD, RandomC, AuthPOS’

message after its hash.

5) POS Authenticity and session confirmations(POS->C):

• In this step, POS sends to C Conf2 received from AS, and

confirms to C that it starts a payment transaction session

by sending a new random value RandomPOS (serves to

prevent replay attacks) in a ciphertext with the session

key K(POS,C).

• C also receives (5), deciphers Conf2 with its secret

key secKey(C), checks TD and RandomC and obtains

K(POS,C), AuthPOS, SignatureAS.

• In fact, C trusts AS and stores Certificate(AS) containing

pubKey(AS), it verifies SignatureAS using pubKey(AS)

in order to authenticate AS, guarantee the integrity of

’POS, C, AS, K(POS,C), TD, RandomC, AuthPOS’ and

ensure that AS cannot deny having sent SignatureAS in

the future (non-repudiation of origin).

• C also confirms the authenticity of POS with AuthPOS,

deciphers {RandomC, TD, RandomPOS}K(POS,C) using

K(POS,C) session key and obtains RandomPOS.

6) Exchange of the banking data and Confirmation to POS

(C->POS):

• C starts with POS a secured payment session using the

session key K(POS,C) by sending: RandomPOS-1 (calcu-

lated from RandomPOS), the banking data BankData and

their electronic signature. The latter is the electronic sig-

nature of BankData by secKey(IssBank) ensuring banking

data integrity for POS.

• Therefore, POS decrypts (6), checks RandomPOS-1 and

obtains BankData and their signature. POS also checks

the signature using pubKey(IssBank) obtained in step (4).

D. Results

During an NFC payment transaction, if C and POS execute

all steps of the proposed protocol, then we ensure that:

5

• They are mutually authenticated. In step (4), POS con-

firms the authenticity of C. In step (5), C confirms the

authenticity of POS.

• They cannot deny (non-repudiation of origin) having sent

the electronic signatures (SignaturePOS and SignatureC)

in the future.

• The integrity of private banking data BankData stored on

C is ensured (step (6)) using the electronic signature.

• The confidentiality of private banking data BankData is

ensured using a symmetric session key (step (6)).

• The validity of C that the banking data are not revoked

is well ensured to POS by verifying the revocation of

certificates in step (3).

V. DISCUSSIONS

In this section, we discuss some possible attacks:

1) Malicious reader MalPOS: which wants to pose as POS

to communicate with C. Possible attacks:

• In step (1), MalPOS sends to C: its TDmalpos, Certifi-

cate(POS), Certificate(AcqBank), RequestC and its sig-

nature SignatureMalPOS generated by its secret key

secKey(MalPOS). In step (3), AS rejects POS authentic-

ity because it could not verify SignatureMalPOS with

pubKey(POS) (obtained from Certificate(POS)).

• If MalPOS replays the message (1), then this is can be

detected by TD validity in step (3).

2) Malicious card MalC: which wants to pose as C to

communicate with POS. Possible attacks:

• In step (2), MalC sends to AS mainly through POS:

Certificate(C), Certificate(IssBank) and its signature Sig-

natureMalC generated by its secret key secKey(MalC).

POS receives MalC message believing that it is from C,

sends it to AS but the latter rejects C authenticity be-

cause it could not verify SignatureMalC with pubKey(C)

(obtained from Certificate(C)).

• If MalC replays the message (2), then this is can be

detected by TD validity in step (3).

3) Bank data integrity: is satisfied using the electronic

signature of banking data generated by the issuing bank’s

secret key secKey(IssBank) and stored on the NFC bank card C

during its construction. It is verified by POS using the issuing

bank’s public key pubKey(IssBank) in step (6).

4) Bank data confidentiality: is satisfied using the symmet-

ric session key K(POS,C) after authentication steps.

VI. SCYTHER VERIFICATION

A. Overview

We have chosen the Scyther tool in order to verify the

correctness of the security protocol proposed in this paper.

Scyther is an effective tool for verification, falsification, and

analysis of security protocols to identify potential attacks and

vulnerabilities. It can be freely downloaded at [22]. Studies in

[23] have extensively investigated the performance of Scyther

compared to other verification tools. Scyther is based on a

development model algorithm providing infinite representa-

tions of traces. It can verify protocols using specific Scyther

claims with an unbounded number of sessions and guaranteed

termination. Also, it is able to detect several possible attacks

and generates a graph for each attack found corresponding to

the mentioned claim [24].

TABLE III VARIABLE SYMBOLS SPDL

Symbol Signification Symbol Signification

P POS C Card

AS Authentication Server

IB IssBank

AB AcqBank H(M) Hash(M)

TD Transaction Data X BankData

pk(X) pubKey(X) sk(X) secKey(X)

kpc K(POS,C) k(AS,P) K(AS,POS)

Fig. 3. The proposed protocol written in SPDL (step (1) to (3))

B. Implementation

The language used to write protocols in Scyther is Security

Protocol Description Language (SPDL) which is based on

the operational semantics found in [25]. Hence, we wrote

the proposed protocol in SPDL language to verify authentica-

tion (with non-repudiation) and confidentiality Scyther claims

whether hold or not. Tab-III presents the correspondence

between the variables declared in the program SPDL and

abbreviations presented in Tab-I. Fig-3 illustrates the proto-

col implementation in SPDL language, it shows a part of

exchanged messages (step (1) to (3)).

6

C. Scyther claims

As illustrated in Fig-4, the protocol successfully guaran-

tees all Scyther claims for P, C, AS and no attacks are

found. Authentication claims: Alive, Weakagree, Niagree and

Nisynch are used to detect replay, reflection and man in the

middle attacks. Secret and SKR (Session Key Reveal) are

confidentiality claims. Formal definitions for all Scyther claims

can be found in [25] and [26].

Fig. 4. Verification results

VII. CONCLUSION

In this paper, we introduced a new security protocol for

NFC payment transactions allowing to solve EMV security

weaknesses. We have based this solution on an online com-

munication with an authentication server that is considered as

a trusted security center for terminals, cards and banks. The

protocol ensures: mutual authentication and non-repudiation

(compared to [19]) between an NFC bank card and an NFC

point of sale, integrity (compared to [19]) and confidentiality

of private banking informaion, the validity of banking data that

they are not revoked (compared to [20]). We have successfully

analyzed the protocol correctness using the Scyther tool.

In fact, the proposal of this paper and the protocol that we

have proposed in [20] use the authentication with certificates

and signatures whereas they are different in: objective, pay-

ment environment (online/offline), payment actors, the content

of the messages exchanged and results. Thus, we note that our

proposal can be implemented with a connected object such as

an NFC smartphone instead of an NFC bank card, but in this

case, the advantage of the connection interface (Wi-Fi or 4G)

available in the mobile will not be considered. It can also be

implemented to secure contact payment communications.

REFERENCES

[1] NFC Forum, http://nfc-forum.org/, last connection (07/05/2015). [2] VISA payWave, http://www.visa.ca/fr/personal/visa-paywave/index.jsp,

last connection (07/05/2015). [3] MasterCard PayPass, http://www.mastercard.com/contactless/index.html,

last connection (07/05/2015). [4] M. Pasquet, J. Reynaud, and C. Rosenberger, “Secure payment with nfc

mobile phone in the smarttouch project,” IEEE International Symposium on Collaborative Technologies and Systems (CTS), pp. 121–126, 2008.

[5] EMV Books - Integrated Circuit Card Specifications for Payment Systems, Book 1: Application Independent ICC to Terminal Interface Requirements, Book 2: Security and Key Management, Book 3: Ap- plication Specification, Book 4: Cardholder Attendant and Acquirer Interface Requirements, Version 4.3, EMVCo, http://www.emvco.com/, November 2011.

[6] M. Emms and A. van Moorsel, “Practical attack on contactless payment cards,” HCI2011 Workshop Heath, Wealth and Identity Theft, 2011.

[7] R. Lifchitz, “Hacking the nfc credit cards for fun and debit,” Hackito Ergo Sum conference, April 2012.

[8] O. Ogundele, P. Zavarsky, R. Ruhl, and D. Lindskog, “Fraud reduction on emv payment cards by the implementation of stringent security fea- tures,” International Journal of Intelligent Computing Research (IJICR), 2012.

[9] S. J. Murdoch, S. Drimer, R. Anderson, and M. Bond, “Chip and pin is broken,” IEEE Symposium on Security and Privacy (SP), pp. 433–446, 2010.

[10] M. Ward, “Emv card payments–an update,” Elsevier Information Secu- rity Technical Report, pp. 89–92, 2006.

[11] J. De Ruiter and E. Poll, “Formal analysis of the emv protocol suite,” Springer Theory of Security and Applications, pp. 113–129, 2012.

[12] M. Levi, P. Bissell, T. Richardson, and C. P. Unit, “The prevention of cheque and credit card fraud,” Citeseer, 1991.

[13] N. A. Chattha, “Nfc-vulnerabilities and defense,” IEEE Conference on Information Assurance and Cyber Security (CIACS), pp. 35–38, 2014.

[14] H. Eun, H. Lee, and H. Oh, “Conditional privacy preserving security protocol for nfc applications,” IEEE Transactions on Consumer Elec- tronics, pp. 153–160, 2013.

[15] A. Elbagoury, A. Mohsen, M. Ramadan, and M. Youssef, “Practical provably secure key sharing for near field communication devices,” IEEE International Conference on Computing, Networking and Communica-

tions (ICNC), pp. 750–755, 2013. [16] M. S. Jung, “A study on electronic-money technology using near field

communication,” Multidisciplinary Digital Publishing Institute Symme- try, pp. 1–14, 2014.

[17] P. Urien and S. Piramuthu, “Elliptic curve-based rfid/nfc authentication with temperature sensor input for relay attacks,” Elsevier Decision Support Systems, pp. 28–36, 2014.

[18] ——, “Framework and authentication protocols for smartphone, nfc, and rfid in retail transactions,” IEEE Eighth International Conference on Intelligent Sensors, Sensor Networks and Information Processing, pp. 77–82, 2013.

[19] U. B. Ceipidor, C. M. Medaglia, A. Marino, S. Sposato, and A. Moroni, “Kernees: A protocol for mutual authentication between nfc phones and pos terminals for secure payment transactions,” IEEE 9th International ISC Conference on Information Security and Cryptology (ISCISC), pp. 115–120, 2012.

[20] N. El Madhoun, F. Guenane, and G. Pujolle, “A cloud-based secure authentication protocol for contactless-nfc payment,” IEEE 4th Interna- tional Conference on Cloud Networking (CloudNet), pp. 328–330, 2015.

[21] T. Dierks, “The transport layer security (tls) protocol version 1.2,” 2008. [22] Scyther Website, http://www.cs.ox.ac.uk/people/cas.cremers/scyther/,

last connection (07/05/2015). [23] C. Cremers and P. Lafourcade, “Comparing state spaces in automatic

protocol verification,” International Workshop on Automated Verification of Critical Systems (AVoCS), 2007.

[24] C. J. Cremers, “The scyther tool: Verification, falsification, and analysis of security protocols,” Springer Computer Aided Verification, 2008.

[25] C. Cremers and S. Mauw, “Operational semantics and verification of security protocols,” Springer Science & Business Media, 2012.

[26] G. Lowe, “A hierarchy of authentication specifications,” IEEE 10th Computer Security Foundations Workshop, pp. 31–43, 1997.

7