基于串空间的Kao Chow加密协议形式化验证

Formal verification of Kao Chow cryptographic protocol based on strand space model

Kao Chow加密协议是由Kao和Chow提出的,他们利用BAN逻辑证明了该协议的认证性,但没有证明该协议的保密性,而且没有说明协议参与实体间得到的新会话密钥是否一致.事实上,由于BAN逻辑自身的缺陷,它无法用于证明加密协议的保密性.基于此,给出了Kao Chow加密协议的串空间模型,这个模型不仅验证了该协议的认证性,还验证了它的保密性及新会话密钥的一致性.

Kao and Chow proposed an efficient and secure cryptographic protocol called Kao Chow protocol. They used BAN to prove its authenticity property. However, they didn＇t prove its secrecy and agreement on new session keys. Due to BAN＇s limitations, it can not be used to analyze cryptographic protocol＇s secrecy property. Thus a strand space model is given on the basis of which, a rigorous proof of its secrecy and agreement on new session keys as well as its authenticity property is obtained.