论文部分内容阅读
形式化分析是密码协议安全性证明的一个有效途径.串空间模型是在Dolev-Yao代数模型的基础上,结合Woo-Lam模型、CSP、Schneider秩函数和Paulson归纳法等方法的优点所提出的一种新的密码协议形式化模型,它可为密码协议安全性的证明提供新的方法.文章介绍了串空间模型的研究背景,分析它的架构和特点,综述有关研究工作,并分析其进一步的研究趋势.