61672525

李梦君(1975-)男湖北云梦人博士副教授CCF专业会员主要研究领域为形式化方法与技术信息安全技术CPU验证;欧国东(1977-)男博士助理研究员主要研究领域为计算机体系结构微处理器设计形式化验证;潘国腾(1977-)男博士副研究员CCF专业会员主要研究领域为计算机体系结构微处理器设计形式化验证. 通讯作者: 国家自然科学基金（61672525）；中国科学院信息工程研究所信息安全国家重点实验室开放课题（2016-MS-21） 随着软件精化验证方法以及Isabella/HOL、VCC等验证工具不断取得进展，研究者们开始采用精化方法和验证工具设计、建模安全协议和验证安全协议源程序的正确性.在介绍Event-B方法和验证工具Isabella/HOL、VCC的基础上，综述了基于Event-B方法的安全协议形式化设计、建模与源程序验证的典型研究工作，主要包括从需求规范到消息传递形式协议的安全协议精化设计、基于TPM（trusted platform module）的安全协议应用的精化建模以及从消息传递形式协议到代码的源程序精化验证. 地址：北京市海淀区中关村南四街4号邮政编码：100190