基于Event-B方法的安全协议设计、建模与验证

来源：软件学报杂志2018年第11期北京时间：

作者：李梦君,潘国腾,欧国东

单位：李梦君，国防科技大学 计算机学院, 湖南 长沙 410073;信息安全国家重点实验室(中国科学院 信息工程研究所), 北京 10009311,潘国腾，国防科技大学 计算机学院, 湖南 长沙 41007302,欧国东，国防科技大学 计算机学院, 湖南 长沙 41007303

摘要：随着软件精化验证方法以及Isabella/HOL、VCC等验证工具不断取得进展，研究者们开始采用精化方法和验证工具设计、建模安全协议和验证安全协议源程序的正确性.在介绍Event-B方法和验证工具Isabella/HOL、VCC的基础上，综述了基于Event-B方法的安全协议形式化设计、建模与源程序验证的典型研究工作，主要包括从需求规范到消息传递形式协议的安全协议精化设计、基于TPM（trusted platform module）的安全协议应用的精化建模以及从消息传递形式协议到代码的源程序精化验证.

关键词：安全协议设计;安全协议建模与验证;精化;Event-B方法

基金资助：国家自然科学基金（61672525）；中国科学院信息工程研究所信息安全国家重点实验室开放课题（2016-MS-21）