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

• 作者: 李梦君 欧国东 潘国腾
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 安全协议设计 安全协议建模与验证 精化 Event-B方法
• 年，卷（期）: 2018,（11）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 3400-3411
• 页数: 12页
• 分类号: TP311
• 字数: 14916字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005622

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	潘国腾	国防科技大学计算机学院	7	20	2.0	4.0
2	欧国东	国防科技大学计算机学院	7	19	2.0	4.0