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

IEEE Access

卷:6

Meihua Xiao¹  Xizhong Wang¹  Xiaomei Zhong¹  Jia Chen¹  Ke Yang¹  Jiawen Song¹ 

[1] School of Software, East China Jiaotong University, Nanchang, China;

关键词: NFC;    mobile payment protocol;    logic of events;    mutual authentication;   

DOI  :  10.1109/ACCESS.2018.2870200

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown