A formal framework for security analysis of NFC mobile coupon protocols
A formal framework for security analysis of NFC mobile coupon protocols
复制标题
DOI：
10.3233/jcs-150531
复制
发表时间：
2015-01-01
影响因子：
1.2
通讯作者：
Schneider, Steve
中科院分区：
文献类型：
--
作者：
Alshehri, Ali;Schneider, Steve
近场通信(NFC)是一种射频(RF)技术，允许在距离很近的设备之间交换数据。基于NFC的移动优惠券(M-Coupon)是用户从报纸或智能海报等来源检索并在之后兑换的优惠券。M-优惠券是一种加密的安全电子消息，用户的手机上存储着一定的价值。提出了一种使用形式化方法分析NFC移动优惠券协议安全性的形式化框架(CasperFDR)。该框架旨在检查NFC M-Coupon协议是否满足了他们的安全需求。本文首先对NFC M-优惠券要求进行了形式化定义，该定义可以适用于各种协议。然后，我们将该框架应用于文献中提出的一个基于二次剩余的NFC M-Coupon协议。分析显示了对用户身份验证属性的攻击。另一个贡献是，我们用二次剩余定理(QR)建模的挑战来建模协议。我们提出了两种抽象模型中QR的方法，并比较了这两种方法的优缺点。我们展示了如何克服所使用的协议分析工具CasperFDR的一些限制，这些限制阻碍了我们以自然的方式对协议进行建模。此外，我们还讨论了一个有趣的观察，即CasperFDR中分裂的长消息如何影响已发现的攻击。
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.