基于主体关联度的安全协议形式化分析方法

摘要：

建立在协议主体参数新近一致性上的主体关联度由于能够正确反映协议安全属性与协议结构、消息组件和消息参数的逻辑关系,因此不仅能够为安全协议的正确性分析提供准确严谨的形式化判断依据,还能进一步降低协议分析的复杂度.为此,文章提出一种基于主体关联度的安全协议形式化分析方法.该方法首先在认证测试模型上,通过对消息组件的参数分类,给出协议主体关联度的量化定义;再根据认证测试规则和测试组件上的参数一致性判定条件,建立协议关联性、认证性、协商数据一致性与协议主体关联度的逻辑关联;接着在协议主体关联度上实现对安全协议设计目标的正确性分析.文章运用该方法对Neuman-Stubblebine协议进行分析,准确发现了协议中潜在的隐患及其根源,并证实了协议主体关联度在安全协议正确性分析中的应用可行性和有效性.

关键词：安全协议、认证测试、关联度、形式化分析

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金61300048,61572224;安徽省自然科学基金1608085MF143,1708085QF154;安徽省高校优秀青年人才计划项目gxyq2017154;安徽省教育厅自然科学项目KJ2014A231,KJ2016A627

在线出版日期：2018-12-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：45-51