串空间中数据机密性与起源性的新证明

串空间中理想及其推论大大简化了安全协议的分析,但现有的定理只适用于基于对称密钥的安全协议,不适用于基于非对称密钥的安全协议,因此使用原始串空间理论对基于非对称密钥的协议安全性分析会非常繁琐.为了使理想的概念也可同时应用于基于非对称密钥安全协议的分析过程,提出并证明了可同时应用于基于对称密钥和非对称密钥安全协议的数据机密性和机密数据起源性定理.首先,对原始的串空间理论进行了扩展,定义了子串和一组正则串机密数据子串,对数据机密性定理进行了重新定义,在数据机密性定理的定义中,考虑到对非对称密钥安全协议的分析,加入了私钥的机密性条件,并从正则串和攻击者串两个角度重新对数据的机密性进行了严格完整的证明.然后,又从数据的机密性定理出发,首次提出了机密数据的起源性定理.该定理证明了安全协议中的机密性数据具有唯一起源性.由于两个新定理同时考虑了对称密钥和非对称密钥安全协议的情况,因此可以同时应用于基于对称密钥和非对称密钥的协议的安全性分析.与原始的串空间理论相比,数据机密性和机密数据起源性定理的提出可以大大简化安全协议的分析步骤,提高分析的效率.最后,应用数据机密性和机密数据起源性定理,重新分析了NSPK协议,说明了其存在攻击的原因.

New proof of confidentiality and originality of data in strand space

The ideal and its corollaries in strand space model greatly simplify the analysis of security protocols.But the existing theorems are only adaptive to the security protocols based on symmetric key,they,however,can't be used to analyze the security protocols based on asymmetric key,so it is very tedious to analyze security protocols based on asymmetric key with the original strand space theorems.To analyze the security protocols based on symmetric as well as asymmetric key,the theorems of data confidentialit...