一种含时间因素的安全协议形式化分析方法

提出一种针对包含时间因素的安全协议的有色Petri(CPN)形式化分析方法,利用CPN Tools中的内置全局自动时钟标记,时间相关性质可通过仿真和生成状态图进行分析验证。基于这一方法,对著名的NS协议(简化版)建模,来分析验证与时间相关的安全属性。然后利用CPN Tools,采用CPN ML语言编写查询函数验证协议的AUT性质,从而发现协议的漏洞。应用分析结果表明方法有效,且操作简单容易理解。

抗去同步化的轻量级RFID双向认证协议

针对低成本RFID应用中轻量级认证协议的安全性进行研究,提出一种组合型去同步化攻击方法,该类攻击不用篡改任何协议消息,仅通过拦截、窃听、重放等攻击手段的顺序组合就能导致后台数据库/标签的共享密钥失去同步;设计一种轻量级抗去同步化的RFID双向认证协议,并利用形式化工具CPN Tools模拟运行该协议,该协议可以达到预期状态空间;与同类RFID协议相比,该协议在满足一般隐私安全属性的同时,还能有效抵抗来自恶意阅读器的组合型去同步化攻击,同时能有效减少RFID系统的计算开销,弥补原始协议的不足,更适合低成本RFID系统应用的隐私安全需求。