受邀嘉宾：汪学明    本期记者：润洁   视频处理：     发布时间：2011-04-02

视频地址：

http://www.secdoctor.com/html/yingxiangtianxia/shipincaifang/2011/0402/12492.html

      视频说明：

汪学明（1965.1）男，教授，博士。贵州大学计算机学院学术委员会委员、信息安全实验室主任，贵州省计算机学会理事、贵州省逻辑教学研究会副会长、贵州制约逻辑学会常务副理事长，中国密码学会高级会员。

主要研究方向：无线与移动网络、密码学与信息安全、协议分析与模型检测、逻辑学及其应用。主持参加国家自然科学基金项目1项、省自然基金项目3项、省教育厅自然基金项目3项、贵阳市科技攻关项目2项、校级项目6项。参加国际学术会议12次（担任Session Chair 6次）、国内学术会议16次，主办“全国性逻辑系统、智能科学与信息科学学术会议”4届。发表论文60余篇 (其中核心16篇、SCI收录1篇、EI收录4篇、ISTP收录5篇)。主编出版《Java语言及应用》、《Java程序设计指导》、《逻辑学及其应用研究》等著作3部。

主持人：各位网友大家好！

欢迎来到本期的中国信息安全博士网高端访谈栏目。我是润洁，今天做客嘉宾是：贵州大学计算机学院学术委员会委员、信息安全实验室主任——汪学明教授。

我们知道汪教授在逻辑学领域有着深厚的积累，可是逻辑学对于很多人来说很陌生，大家对信息安全的理解主要为攻防技术，但是以逻辑为基础的形式化技术同样在信息安全领域中有着重要的地位，那么请汪教授首先介绍一下形式化技术在信息安全领域中的应用。

汪教授： 形式化技术在信息安全领域中的应用目前主要集中在安全协议的形式化分析和设计。

长期以来，密码学专家一直依赖经验性的指导原则来设计安全协议(又称密码协议)，这种非形式化的设计方法很容易忽略掉一些微妙的直觉难以发现的漏洞。由于安全协议运行的复杂性，对安全协议进行分析以及设计都是非常困难的。因此，将形式化方法用于安全协议的分析与设计过程成为必然。

主持人：用于信息安全领域的形式化技术有哪些？

汪教授： 安全的密码协议是网络通信和应用必不可少的组件之一，是构筑信息安全体系的基础。设计安全和有效的密码协议是协议工程领域中的主要研究内容。在设计、描述(建模)、验证、性能分析、实现、测试和维护等协议工程的各个环节中，协议验证是最为关键的一个环节。协议分析和协议综合是实现协议验证的两种有效途径，前者更为有效和实用。自上个世纪七十年代末以来，人们提出多种安全协议分析的形式化理论，包括Dolev-Yao模型、模态逻辑、Paulson归纳法、串空间模型以及Spi演算理论等，并从这些理论中归纳出基于模态逻辑推理、基于模型状态检验、基于定理证明和基于类型检测等安全目标验证方法。前两类方法只能推理密码协议的不安全性，不能给出其安全目标的可信证明，而后一类方法又不具有完备性，唯有基于定理证明的安全目标验证方法试图给出密码协议的安全性证明。

主持人：当前，国内外采用形式化技术在信息安全领域中的研究有哪些进展？

汪教授： 国内外采用形式化技术在信息安全领域中的最新研究有：
（1）基于ATL博弈逻辑形式化方法及其在多方安全协议分析中的应用研究
（2）基于TLA（行为时序逻辑）形式化方法及其应用研究面
（3）基于进程演算和知识推理的安全协议形式化分析
（4）基于逻辑的复合协议形式化分析方法研
（5）量子密码协议的形式化分析方法研究

值得一提的是，贵州大学计算机软件与理论研究所、博士点、博士后工作站的研究团队在基于ATL、TLA、进程演算和知识推理的形式方法及其应用研究方面都开展了大量工作。

主持人：对于有志于从事信息安全形式化技术研究的学生，请汪教授指点下如何起步？

汪教授：安全协议（密码协议）比一般的网络协议复杂，因为它涉及加密、认证和密钥交换等密码学知识。所以安全协议的分析与设计实际上是密码学的一个非常重要的应用领域，也是信息安全的研究重点之一。

对于有志于从事信息安全形式化技术研究的学生，首先应该具有稳固的数学和计算机网络基础、扎实的密码学与信息安全原理知识。然后从现有的比较成熟且简单易学的模态逻辑方法入手，阅读大量相关文献资料，理解模型逻辑的公理或推理规则并运用它分析简单的安全协议。在熟练运用后可以对形式化逻辑方法中的逻辑推理规则进行扩展，进而结合协议的应用环境分析更为复杂的安全协议。在模型检测技术方面，可以从熟悉模型检测工具的运用入手，着重研究模型检测工具基于的形式化逻辑体系和使用的建模语法，研究如何更加有效地采用建模语法描述协议和用形式化的逻辑方法描述协议所应具备的安全属性。进一步的工作，可以自己设计一套建模流程、改进建模工具、提出安全属性新的逻辑描述等。对于数学基础牢固的同学可以适时开展基于定理证明的安全协议形式化分析。

主持人：安全协议的形式化分析可以使用许多模型检测工具，他们分别基于不同的逻辑，请汪教授介绍下他们各自的特点。

汪教授：目前安全协议的形式化分析可以使用的模型检测工具很多，其中著名的有Spin 、SMV、Mocha，他们分别基于线性时序逻辑LTL、计算时序逻辑CTL和交换时序逻辑ATL。

基于线性时序逻辑的模型检测工具Spin具有很强的描述能力，可以对协议系统进行形式化建模分析，并且在系统不满足某一安全属性时自动给出图形化的反例，易于分析，因此得到了广泛应用。基于计算时序逻辑的模型检测工具SMV能够对协议的并发性进行更为准确的描述。但是Spin和SMV都存在以封闭系统方式分析安全协议的缺点。基于ATL逻辑的模型检测工具Mocha克服了这个缺点，它可以更好地描述协议主体之间合作和竞争的关系，以及协议内部和外部环境的联系，更适用于分析复杂的多方安全协议。

主持人：形式化技术在信息安全领域中的推广应用还需要我们做哪些工作？

汪教授：形式化方法是一种用于描述系统性质的数学方法，主要用于发现一个系统中的歧义性、不一致性与不完备性。但是，现有的形式化分析方法都不很完善。为了促进形式化技术在信息安全领域中的推广应用，首先应该增强信息安全工作者自觉运用形式化技术分析和解决信息安全问题的意识。然后通过对现有的形式化分析理论和技术进行深入研究，扩展或提出新的形式化方法，完善或开发新的模型检测工具，并把这些新方法、新工具运用于信息安全领域。

主持人：在信息安全研究中，从事信息安全形式化技术相关方面研究的学生数量比较少，研究过程中会遇到重重困难，那么请汪教授对已经从事信息安全形式化技术以及有志于从事信息安全形式化技术方面研究的学生给些建议。

汪教授：形式化方法及其在信息安全领域的应用研究方兴未艾。对于已经从事信息安全形式化技术研究的同学，我希望他们不怕困难，勇于创新，相信通过他们的不懈努力，一定会取得圆满成功。对于有志于从事信息安全形式化技术方面研究的同学，请现在就抓紧时间认真学习形式化方法及相关知识，同时对自己即将从事的研究工作有一个全面了解，不要急功近利，坚持到底就是胜利。预祝同学们为我国的信息安全形式化技术的发展做出自己应有的贡献。

主持人：感谢汪教授做客中国信息安全博士网——高端访谈栏目，我是润洁，下期再见。