一种改进SVO逻辑的新方法

安全协议的形式化验证能有效检验安全协议的安全性,BAN类逻辑的发展极大的促进了这一领域的研究,而SVO逻辑是BAN类逻辑的佼佼者.本文通过增加和改进SVO逻辑的推理规则以及公理,提出了一种改进SVO逻辑的新方法,使其可以更好的分析认证协议.本文运用改进SVO逻辑对Needham-Schroeder认证协议进行形式化分析,发现改进的SVO逻辑能证明Needham-Schroeder认证协议能够达到预期目标.     

一种改进的Woo-Lam协议

串空间是一种基于定理证明的,新兴的安全协议形式化分析模型.认证协议使用密码技术实现网络环境下的身份认证和信息保密.本文针对Woo-Lam协议的不足,对其进行改进,提出了一种新的Woo-Lam协议,使其成为双向认证协议,并基于串空间模型,然后对改进的Woo-Lam协议进行分析证明,结果证明了改进的Woo-Lam协议为双向认证协议.最后通过比较了改进前后的Woo-Lam协议,得出了结论.