Research on Relationship between Safe Keys and Secrecy Property
Shu Qing Lv · 2004
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.