专访贵州大学汪学明
人物简介：
汪学明（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、进程演算和知识推理的形式方法及其应用研究方面都开展了大量工作。
网友评论