Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events

The near field communication (NFC) is widely used on mobile devices and make it possible to take advantage of NFC system to complete mobile payment. But with the development of NFC, its problem are increasingly exposed, especially the security and privacy of authentication. The logic of events is a...

Full description

Bibliographic Details
Main Authors:	Ke Yang, Meihua Xiao, Jiawen Song, Jia Chen, Xiaomei Zhong, Xizhong Wang
Format:	Article
Language:	English
Published:	IEEE 2018-01-01
Series:	IEEE Access
Subjects:	NFC mobile payment protocol logic of events mutual authentication
Online Access:	https://ieeexplore.ieee.org/document/8466579/

id	doaj-3fce8d550bec41a98b86b06c8120b5b1
record_format	Article
spelling	doaj-3fce8d550bec41a98b86b06c8120b5b12021-03-29T21:02:57ZengIEEEIEEE Access2169-35362018-01-016518535186310.1109/ACCESS.2018.28702008466579Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of EventsKe Yang0https://orcid.org/0000-0002-6441-2309Meihua Xiao1Jiawen Song2Jia Chen3Xiaomei Zhong4Xizhong Wang5School of Software, East China Jiaotong University, Nanchang, ChinaSchool of Software, East China Jiaotong University, Nanchang, ChinaSchool of Software, East China Jiaotong University, Nanchang, ChinaSchool of Software, East China Jiaotong University, Nanchang, ChinaSchool of Software, East China Jiaotong University, Nanchang, ChinaSchool of Software, East China Jiaotong University, Nanchang, ChinaThe near field communication (NFC) is widely used on mobile devices and make it possible to take advantage of NFC system to complete mobile payment. But with the development of NFC, its problem are increasingly exposed, especially the security and privacy of authentication. The logic of events is a formal method to describe the protocol state transition and algorithm in concurrent and distributed systems, which can be used to prove the security of network protocols. Based on logic of events, we propose migration rule and derive inheritability to reduce redundancy and complexity of protocol analysis procedure and improve efficiency of protocol analysis. We study the KerNeeS protocol which providing mutual authentication between POS and NFC phone, and conclude that the protocol can guarantee mutual authentication property between entities involved in the payment for secure payment transactions. The logic of events can be applied to the formal analysis of similar mobile payment protocols.https://ieeexplore.ieee.org/document/8466579/NFCmobile payment protocollogic of eventsmutual authentication
collection	DOAJ
language	English
format	Article
sources	DOAJ
author	Ke Yang Meihua Xiao Jiawen Song Jia Chen Xiaomei Zhong Xizhong Wang
spellingShingle	Ke Yang Meihua Xiao Jiawen Song Jia Chen Xiaomei Zhong Xizhong Wang Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events IEEE Access NFC mobile payment protocol logic of events mutual authentication
author_facet	Ke Yang Meihua Xiao Jiawen Song Jia Chen Xiaomei Zhong Xizhong Wang
author_sort	Ke Yang
title	Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events
title_short	Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events
title_full	Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events
title_fullStr	Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events
title_full_unstemmed	Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events
title_sort	proving mutual authentication property of kernees protocol based on logic of events
publisher	IEEE
series	IEEE Access
issn	2169-3536
publishDate	2018-01-01
description	The near field communication (NFC) is widely used on mobile devices and make it possible to take advantage of NFC system to complete mobile payment. But with the development of NFC, its problem are increasingly exposed, especially the security and privacy of authentication. The logic of events is a formal method to describe the protocol state transition and algorithm in concurrent and distributed systems, which can be used to prove the security of network protocols. Based on logic of events, we propose migration rule and derive inheritability to reduce redundancy and complexity of protocol analysis procedure and improve efficiency of protocol analysis. We study the KerNeeS protocol which providing mutual authentication between POS and NFC phone, and conclude that the protocol can guarantee mutual authentication property between entities involved in the payment for secure payment transactions. The logic of events can be applied to the formal analysis of similar mobile payment protocols.
topic	NFC mobile payment protocol logic of events mutual authentication
url	https://ieeexplore.ieee.org/document/8466579/
work_keys_str_mv	AT keyang provingmutualauthenticationpropertyofkerneesprotocolbasedonlogicofevents AT meihuaxiao provingmutualauthenticationpropertyofkerneesprotocolbasedonlogicofevents AT jiawensong provingmutualauthenticationpropertyofkerneesprotocolbasedonlogicofevents AT jiachen provingmutualauthenticationpropertyofkerneesprotocolbasedonlogicofevents AT xiaomeizhong provingmutualauthenticationpropertyofkerneesprotocolbasedonlogicofevents AT xizhongwang provingmutualauthenticationpropertyofkerneesprotocolbasedonlogicofevents
_version_	1724193605200904192

Proving Mutual Authentication Property of KerNeeS Protocol Based on Logic of Events

Similar Items