论文部分内容阅读
安全协议的本质是协议主体采用密码学方法通过挑战—响应来对协议其他方的存在做出判断,同时完成一些数据如会话密钥的协商．大部分国内外现有的分析方法或者采用状态检测等定理证明技术,或者采用认证逻辑等推理技术,存在着分析能力与可操作性之间的矛盾．为了解决这个问题,文中提出一种新的安全协议保密性和关联性的分析方法,该方法基于线空间模型理论给出了协议保密目标和认证目标的形式化定义,采用认证逻辑作为基础分析手段．保密性分析被分解为显式泄密和隐性泄密两种情况,其中隐性泄密分析依赖于关联性的判断,而关联性的分析被总结为Strand的存在关系和参数一致性分析的问题．新的分析方法既具有线空间模型的分析能力,又具有认证逻辑的易用性．
The essence of the security protocol is that the main body of the protocol adopts the method of cryptography to judge the existence of the other parties through the challenge-response and complete some data such as the session key negotiation. Most of the existing analytical methods at home and abroad either adopt the theorem proving techniques such as state detection, or use reasoning techniques such as authentication logic, so there is a contradiction between analytical ability and operability. In order to solve this problem, a new security protocol confidentiality and correlation analysis method is proposed in this paper. The method is based on the linear space model theory and gives the formal definition of the protocol confidentiality target and the authentication target. The authentication logic is used as the basic analysis method . Confidentiality analysis is decomposed into two cases: explicit disclosure and implicit disclosure. The analysis of implicit disclosure depends on the judgment of relevance, while the analysis of relevance is summarized as the existence of Strand and the consistency analysis of parameters. The new analysis method not only has the analytical ability of the line space model, but also has the ease of use of the authentication logic.