文章目录
- 目前我在做网络安全协议形式化验证方法的研究，走过了一些弯路，最开始使用BAN-like的逻辑语言，后来发现这类语言有它自身的局限性，而且目前安全协议的形式化验证方法已经提出了比较新，也比较完善的模型-strand space模型，这种方法在安全协议分析中使用了很多离散数学中的形式和证明方法，通过归约为矛盾最后证明协议的安全性。最后我选择基于strand space的方法作为协议研究的基本方法，希望能在一些方面有所突破。但是国内这方面的研究比较少，只有清华和中科院的一些人做过类似的工作。所以有时做起来觉得很辛苦，特别是证明过程中的一些数学问题需要解决。
- 不知道有没有和我做类似内容的人，大家可以交流一下。
安全协议验证的研究心得- -
目前我在做网络安全协议形式化验证方法的研究，走过了一些弯路，最开始使用BAN-like的逻辑语言，后来发现这类语言有它自身的局限性，而且目前安全协议的形式化验证方法已经提出了比较新，也比较完善的模型-strand space模型，这种方法在安全协议分析中使用了很多离散数学中的形式和证明方法，通过归约为矛盾最后证明协议的安全性。最后我选择基于strand space的方法作为协议研究的基本方法，希望能在一些方面有所突破。但是国内这方面的研究比较少，只有清华和中科院的一些人做过类似的工作。所以有时做起来觉得很辛苦，特别是证明过程中的一些数学问题需要解决。
不知道有没有和我做类似内容的人，大家可以交流一下。
作者： beverly_77