一种基于关联语义的密钥交换协议分析算法设计  

An Analysis Algorithm of Key Exchange Protocol based on Correlation Semantic

作　　者：胡声洲 曾志朋[2] 康小强 

机构地区：[1]江西省数值模拟与仿真技术重点实验室 [2]赣南师范大学数学与计算机科学学院,江西赣州341000

出　　处：《赣南师范大学学报》2017年第6期80-86,共7页Journal of Gannan Normal University

基　　金：国家自然科学基金项目(61562003;31660321);江西省科技厅重点研发计划项目(20151BBF60071;20171BBE50065);江西省自然科学基金项目(20151BAB207029)

摘　　要：安全协议的关联语义是刻画协议的核心性质,针对密钥交换协议关联特性,从分析主体认证关联语义、会话密钥关联语义、消息步骤间关联语义、消息内部关联语义和条件关联语义等方面来描述协议的内在语义,设计了基于关联语义密钥交换协议的分析模型及算法.对Ban-Yahalom Protocol协议进行了分析,指出该协议存在冒充第三方S生成会话密钥的安全隐患,但却未泄漏协议会话密钥.从实验结果来看,该分析方法对密钥交换协议进行关联语义验证分析是行之有效的.These mantic of correlation insecurity protocols is core nature of key exchange protocols. From the analysis of correlation semantics about the principals＇authentication, session key, relationship between message steps, internal structure in message and additional condition aspects, wedescribed these mantic of key exchange protocol and designed the corresponding analysis algorithm. After analyzing Ban-Yahalom protocol, we pointed out that the protocol existed a hidden security danger of being deceived to the third party S by creating a session key, but not disclosing the session key. The experimental results show it is effective to verifythe correlation semantic in the key exchange protocol.

关 键 词：关联语义 密钥交换协议 表示式 验证分析 

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