安全协议验证的研究体会---目前我正在进行网络安全协议形式化验证方法的研究。 我绕了一些弯路。 最初使用的是BAN-like的逻辑语言，但后来发现这种语言有自己的局限性。 此外，目前安全协议形式化验证方法比较新，提出了比较完善的模型-strand space模型。 该方法在安全协议分析中使用了许多离散数学中的形式和证明方法。 最后，我选择了基于strand space的方法作为协议研究的基本方法，希望能在几个方面取得突破。 但国内这方面的研究比较少，只有清华和中科院的部分人做过类似的工作。 所以，有时我觉得做起来很辛苦。 特别是证明过程中的一些数学问题需要解决。 不知道有没有和我有类似内容的人，请大家交流一下。
作者： beverly_77