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