【摘要】 在Strand空间中引入理想的概念 ,可以简化安全协议的证明过程 .此外 ,在Strand空间中引入安全密钥的定义 ,可以作为对协议密钥设计要求的描述 .相关文献只给出了理想结构的大致轮廓 ,论文引入新的符号以给出理想结构的内部细节 .在此基础上 ,借助理想的概念重新描述了安全密钥的设计要求 .针对具有密钥分发功能的安全协议的秘密属性 ,相关文献借助理想概念给出的证明过程缺乏直观性 .论文证明 :协议实现其秘密属性的结论等价于协议对于密钥的使用符合安全密钥的设计要求的结论 .这不仅为利用理想概念证明协议秘密属性的抽象过程提供了直观解释 ,也为证明安全协议的秘密属性提供了一个新的思路更多还原

【Abstract】 Strand spaces model is a kind of formal methods which is applied to security protocol analysis. It offers a concept of ideals which makes its proof procedure of the security protocol simple and clear. In addition, the definition of safe keys is introduced by this method, which can also be viewed as the description of the design requirements of keys used in the protocol. The related literatures only give the outline of the ideals structure. In this papers, new notations are given to describe the inner details of the structure of ideals. Based on these notions, a new description of the design requirements of safe keys is presented with the help of the concept of ideals. For the secrecy of the three party security protocol with the function of the keys distribution, the proof given by the related literatures which makes use of the ideals notion lacks of intuitiveness. We prove that the conclusion that the protocol has fulfilled the property of the secrecy is equal to the conclusion that the way that protocol uses the keys has satisfied the design requirement for safe keys. This not only offers an intuitive interpretation to the abstract procedure which makes use of the ideals notion to prove the protocol secrecy, but also a new way to prove the secrecy property of the protocol.更多还原