安全协议与形式化方法
课程编码：0839X5M04001H
英文名称：Security Protocols and Formal Methods
课时：60
学分：3.00
课程属性：专业核心课
主讲教师：王竹等
教学目的要求
本课程是网络空间安全学科的专业核心课。形式化方法是计算机科学的基础之一,在模型与系统的规约与验证方面有着广泛的应用。随着当今软硬件产品(程序、通信协议和电路等)日趋复杂,形式化方法已经成为越来越多设计开发人员的日常工具。安全协议是构建安全网络环境的基石,它的正确性对于网络安全极其关键. 本课程就安全协议与形式化方法的理论与技术展开讨论和介绍,主要包括：典型网络安全协议；网络安全协议的漏洞与可能存在的攻击；形式化方法基础；形式规约语言；形式化分析与验证方法；形式化测试；形式化验证工具; 应用实例分析等。本课程将注重理论联系实际,要求学生通过学习该课程初步掌握安全协议与形式化方法的基础理论与实现技术,为今后的科研和实际工作打下良好基础。
预修课程
无
大纲内容
第一章 第一章 典型网络安全协议 10学时 王竹
第1节 IPSec 协议
第2节 TLS/SSL 协议
第3节 安全电子支付协议
第4节 5G移动通信网络安全协议
第5节 比特币协议
第6节 区块链协议与智能合约
第二章 网络安全协议的漏洞与可能存在的攻击 5学时 王竹
第1节 中间人攻击
第2节 反射攻击
第3节 并发攻击
第4节 假冒攻击
第5节 跨站点请求伪造(CSRF)攻击
第6节 类型错误攻击
第7节 运行模式攻击
第8节 数据包注入攻击
第三章 形式化方法基础 9学时 姬东耀
第1节 程序正确性证明思想的提出(Floyd-Hoare逻辑,归纳断言方法,最弱前置谓词方法).
第2节 类型和类型系统
第四章 形式规约语言 6学时 姬东耀
第1节 Z语言及应用
第2节 Event-B方法及应用
第五章 形式化模型与建模 9学时 姬东耀
第1节 扩展有限状态机模型(EFSM)
第2节 性质描述逻辑(计算树逻辑CTL, 线性时序逻辑 LTL, 行为时序逻辑TLA）
第3节 通信顺序进程(CSP)
第4节 通信系统演算(CCS)
第5节 pi-演算
第六章 形式化分析与验证方法 9学时 姬东耀
第1节 模态逻辑分析
第2节 不变性分析
第3节 可达性分析
第4节 符号执行
第5节 测试等价与互模拟等价
第6节 符号模型检验
第七章 形式化测试 3学时 姬东耀
第1节 形式化测试语言
第2节 测试序列设计
第3节 测试用例自动生成
第八章 形式化验证工具 6学时 姬东耀
第1节 SPIN工具及应用
第2节 SMV工具及应用
第3节 Alloy工具及应用
第4节 ProVerif工具及应用
第九章 实例分析 3学时 姬东耀
第1节 学生根据自己的研究方向,以安全协议及安全系统作为分析对象,在教师的帮助下,以上述方法与工具为基础学生单独或分组完成一个实例分析
参考书
课程教师信息
2001年10月在西安电子科技大学通信工程学院获得博士学位,2003年10月中国科学院大学博士后流动站出站,之后一直在信息安全国家重点实验室从事网络安全协议与形式化方法应用方面的科研工作。