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

An Analysis Algorithm of Key Exchange Protocol based on Correlation Semantic

安全协议的关联语义是刻画协议的核心性质,针对密钥交换协议关联特性,从分析主体认证关联语义、会话密钥关联语义、消息步骤间关联语义、消息内部关联语义和条件关联语义等方面来描述协议的内在语义,设计了基于关联语义密钥交换协议的分析模型及算法.对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.