汪教授指点信息安全迷津
主持人：对于有志于从事信息安全形式化技术研究的学生，请汪教授指点下如何起步？
汪教授：安全协议（密码协议）比一般的网络协议复杂，因为它涉及加密、认证和密钥交换等密码学知识。所以安全协议的分析与设计实际上是密码学的一个非常重要的应用领域，也是信息安全的研究重点之一。
对于有志于从事信息安全形式化技术研究的学生，首先应该具有稳固的数学和计算机网络基础、扎实的密码学与信息安全原理知识。然后从现有的比较成熟且简单易学的模态逻辑方法入手，阅读大量相关文献资料，理解模型逻辑的公理或推理规则并运用它分析简单的安全协议。在熟练运用后可以对形式化逻辑方法中的逻辑推理规则进行扩展，进而结合协议的应用环境分析更为复杂的安全协议。在模型检测技术方面，可以从熟悉模型检测工具的运用入手，着重研究模型检测工具基于的形式化逻辑体系和使用的建模语法，研究如何更加有效地采用建模语法描述协议和用形式化的逻辑方法描述协议所应具备的安全属性。进一步的工作，可以自己设计一套建模流程、改进建模工具、提出安全属性新的逻辑描述等。对于数学基础牢固的同学可以适时开展基于定理证明的安全协议形式化分析。
主持人：安全协议的形式化分析可以使用许多模型检测工具，他们分别基于不同的逻辑，请汪教授介绍下他们各自的特点。
汪教授：目前安全协议的形式化分析可以使用的模型检测工具很多，其中著名的有Spin 、SMV、Mocha，他们分别基于线性时序逻辑LTL、计算时序逻辑CTL和交换时序逻辑ATL。
基于线性时序逻辑的模型检测工具Spin具有很强的描述能力，可以对协议系统进行形式化建模分析，并且在系统不满足某一安全属性时自动给出图形化的反例，易于分析，因此得到了广泛应用。基于计算时序逻辑的模型检测工具SMV能够对协议的并发性进行更为准确的描述。但是Spin和SMV都存在以封闭系统方式分析安全协议的缺点。基于ATL逻辑的模型检测工具Mocha克服了这个缺点，它可以更好地描述协议主体之间合作和竞争的关系，以及协议内部和外部环境的联系，更适用于分析复杂的多方安全协议。
主持人：形式化技术在信息安全领域中的推广应用还需要我们做哪些工作？
汪教授：形式化方法是一种用于描述系统性质的数学方法，主要用于发现一个系统中的歧义性、不一致性与不完备性。但是，现有的形式化分析方法都不很完善。为了促进形式化技术在信息安全领域中的推广应用，首先应该增强信息安全工作者自觉运用形式化技术分析和解决信息安全问题的意识。然后通过对现有的形式化分析理论和技术进行深入研究，扩展或提出新的形式化方法，完善或开发新的模型检测工具，并把这些新方法、新工具运用于信息安全领域。
主持人：在信息安全研究中，从事信息安全形式化技术相关方面研究的学生数量比较少，研究过程中会遇到重重困难，那么请汪教授对已经从事信息安全形式化技术以及有志于从事信息安全形式化技术方面研究的学生给些建议。
汪教授：形式化方法及其在信息安全领域的应用研究方兴未艾。对于已经从事信息安全形式化技术研究的同学，我希望他们不怕困难，勇于创新，相信通过他们的不懈努力，一定会取得圆满成功。对于有志于从事信息安全形式化技术方面研究的同学，请现在就抓紧时间认真学习形式化方法及相关知识，同时对自己即将从事的研究工作有一个全面了解，不要急功近利，坚持到底就是胜利。预祝同学们为我国的信息安全形式化技术的发展做出自己应有的贡献。
主持人：感谢汪教授做客中国信息安全博士网——高端访谈栏目，我是润洁，下期再见。
网友评论