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

Formal Analysis Method of Security Protocol Based on Correlation Degree of Principals

作　　者：余磊[1] 魏仕民[1] 江明明 YU Lei;WEI Shimin;JIANG Mingming(School of Computer Science and Technology,Huaibei Normal University,Huaibei Anhui 235000,China)

机构地区：[1]淮北师范大学计算机科学与技术学院,安徽淮北235000

出　　处：《信息网络安全》2018年第6期45-51,共7页Netinfo Security

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

摘　　要：建立在协议主体参数新近一致性上的主体关联度由于能够正确反映协议安全属性与协议结构、消息组件和消息参数的逻辑关系,因此不仅能够为安全协议的正确性分析提供准确严谨的形式化判断依据,还能进一步降低协议分析的复杂度。为此,文章提出一种基于主体关联度的安全协议形式化分析方法。该方法首先在认证测试模型上,通过对消息组件的参数分类,给出协议主体关联度的量化定义;再根据认证测试规则和测试组件上的参数一致性判定条件,建立协议关联性、认证性、协商数据一致性与协议主体关联度的逻辑关联;接着在协议主体关联度上实现对安全协议设计目标的正确性分析。文章运用该方法对Neuman-Stubblebine协议进行分析,准确发现了协议中潜在的隐患及其根源,并证实了协议主体关联度在安全协议正确性分析中的应用可行性和有效性。The correlation degree of principals established on recent consistency of protocol principals parameters can correctly reflect the logical relationship between protocol security properties and protocol structure, message components and message parameters, which not only can provide accurate and rigorous formal judgment basis for the analysis of the correctness of the security protocol, but can further reduce the complexity of protocol analysis. Therefore, this paper proposes a formal analysis method for security protocols based on correlation degree of principals. Firstly, on the authentication test model, the parameters of message components are classified, and the quantitative definition of the correlation degree of the protocol principals is given. Then according to the rules of authentication test and the criteria for determining the consistency of the parameters on the components, the logical association between the correlation, authentication and the consistency of the negotiation data of the protocol and correlation degree of protocol principals is established. Next, the correctness of the design goals of security protocol is analyzed on the correlation degree of protocol principals. This paper analyzes the Neuman-Stubblebine protocol using the method, which accurately finds the potential defects and its roots in the protocol, and confirms the application feasibility and efficiency of the correlation degree of protocol principals in the correctness analysis of the security protocol.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]