2000, 22(3): 505-508.
刊出日期：2000-05-19
关键词:
模态逻辑; BAN逻辑; 新鲜子
本文从BAN逻辑的基本结构和基本规则出发,对BAN逻辑中的新鲜子进行了分析研究,指出BAN逻辑在实际应用中不稳固的某些本质原因并不是理想化问题,而是原基本规则中存在的某些问题所致,并进一步对此进行了相应的改进,使得BAN逻辑更趋于稳固和完善。
2000, 22(4): 579-584.
刊出日期：2000-07-19
关键词:
认证协议; BAN-逻辑
本文指出了BAN-逻辑推理中存在的逻辑错误，提出了一种改进的BAN-逻辑，它具有精确的语义定义和正确的推理规则，当协议的初始条件正确时，逻辑推理的结论是正确的。
2002, 24(8): 1131-1133.
刊出日期：2002-08-19
关键词:
密码协议; BAN逻辑; 新鲜子
该文通过一个反例说明,宋荣功等对BAN逻辑中新鲜子的研究中关于BAN逻辑新鲜子规则条件过于严格,可能把一个安全的协议分析成不安全的协议。
2000, 22(1): 73-77.
刊出日期：2000-01-19
关键词:
认证协议; BAN逻辑
本文指出了W.Mao(1995)对其协议(1)的证明中存在的错误,并对其在协议理想化过程中提出的N-u规则作了探讨,指出其扩展N-u的三条规则的缺陷,并作了改进,最后,给出一个例子说明N-u规则的应用。
2016, 38(2): 361-366.
doi: 10.11999/JEIT150653
刊出日期：2016-02-19
针对资源受限的RFID标签，结合伪随机数和共享秘密机制，该文提出一种基于散列函数的轻量级双向认证协议，实现了后端数据库、阅读器和标签之间的双向认证。详细分析了双向认证协议的抗攻击性能和效率性能，并基于BAN逻辑分析方法对协议模型进行了形式化证明。理论分析表明，该文提出的认证协议能够实现预期安全目标，抗攻击性能好，认证执行效率高且标签开销小，适用于大数量的RFID应用。
1999, 21(4): 494-499.
刊出日期：1999-07-19
关键词:
个人通信系统; 认证协议; BAN逻辑
假冒和窃听攻击是无线通信面临的主要威胁。在个人通信系统中,为了对无线链路提供安全保护,必须对链路上所传送的数据/话音进行加密,而且在用户与服务网络之间必须进行相互认证。近年来,人们在不同的移动通信网络(如GSM,IS-41,CDPD,Wireless LAN等)中提出了许多安全协议。然而,这些协议在个人通信环境中应用时存在不同的弱点。本文基于个人通信系统的双钥保密与认证模型,设计了用户位置登记认证协议;并采用BAN认证逻辑对协议的安全性进行了形式化证明,也对协议的计算复杂性进行了定性分析。分析表明,所提出的协议与现有的协议相比具有许多新的安全特性。
2022, 44(12): 4294-4303.
doi: 10.11999/JEIT211137
刊出日期：2022-12-16
目前，网络安全及隐私受到广泛关注。前向安全性是Günther在1989年提出的一种认证密钥协商协议( AKA)的安全属性(doi: 10.1007/3-540-46885-4_5)，该性质经过30年的蓬勃发展已经成为研究领域的热点之一。该文主要分析了MZK20和VSR20两个AKA协议。首先在启发式分析的基础上，利用BAN逻辑分析了MZK20协议不具有弱前向安全性；其次利用启发式分析和Scyther工具证明了VSR20协议不具备前向安全性。最后，在分析VSR20协议设计缺陷的基础上，提出了改进方案，并在eCK模型下证明了改进后协议的安全性；并且，结合Scyther软件证明了改进VSR20协议与VSR20协议相比明显提高了安全性。
