本课程是网络空间安全学科的专业核心课。形式化方法是计算机科学的基础之一，在模型与系统的规约与验证方面有着广泛的应用。随着当今软硬件产品(程序、通信协议和电路等)日趋复杂，形式化方法已经成为越来越多设计开发人员的日常工具。安全协议是构建安全网络环境的基石，它的正确性对于网络安全极其关键. 本课程就安全协议与形式化方法的理论与技术展开讨论和介绍，主要包括：典型网络安全协议；网络安全协议的漏洞与可能存在的攻击；形式化方法基础；形式规约语言；形式化分析与验证方法；形式化测试；形式化验证工具; 应用实例分析等。本课程将注重理论联系实际，要求学生通过学习该课程初步掌握安全协议与形式化方法的基础理论与实现技术，为今后的科研和实际工作打下良好基础。

第一章	典型网络安全协议
1.1 IPSec 协议.  
1.2  TLS/SSL 协议.  
1.3 安全电子支付协议. 
1.4 4G移动通信网络安全协议. 
1.5 比特币协议.
第二章 网络安全协议的漏洞与可能存在的攻击
     2.1中间人攻击. 
2.2 反射攻击. 
2.3 并发攻击. 
2.4假冒攻击. 
 2.5跨站点请求伪造(CSRF)攻击.  
2.6 类型错误攻击. 
2.7 运行模式攻击.  
2.8 数据包注入攻击.

第三章 形式化方法基础
3.1 程序正确性证明思想的提出(Floyd-Hoare逻辑，归纳断言方法，最弱前置谓词方法).  
3.2 类型和类型系统。
第四章 形式规约语言 
    4.1  Z语言及应用. 
 4.2  Event-B方法及应用.
第五章：形式化模型与建模
5.1 扩展有限状态机模型(EFSM). 
5.2 性质描述逻辑(计算树逻辑CTL, 线性时序逻辑 LTL, 行为时序逻辑TLA).
 5.3 通信顺序进程(CSP). 
5.4 通信系统演算(CCS).    
5.5 pi-演算.
第六章：形式化分析与验证方法
6.1 模态逻辑分析.
 6.2 不变性分析. 
6.3可达性分析. 
6.4符号执行. 
6.5 测试等价与互模拟等价. 
6.6 符号模型检验.
第七章：形式化测试 
7.1形式化测试语言TTCN.  
7.2 测试序列设计. 
7.3 测试用例自动生成.
第八章：形式化验证工具
8.1 SPIN工具及应用.  
8.2  SMV工具及应用.  
8.3 Alloy工具及应用.  
8.4  ProVerif工具及应用.
第九章：实例分析
    9.1 学生根据自己的研究方向，以安全协议及安全系统作为分析对象，在教师的帮助下，以上述方法与工具为基础学生单独或分组完成一个实例分析.

1 古天龙，蔡国永，《软件开发中的形式化方法》，高等教育出版社，2005.
2.古天龙，蔡国永，《网络协议的形式化分析与设计》，电子工业出版社，2003. 
3.李建华主编，《网络安全协议的形式化分析与验证》，机械工业出版社，2010.
4.韩俊刚，杜慧敏，《数字硬件的形式验证》，北京大学出版社，2001.
5.Dines Bjorner著，《软件工程》卷一：抽象与建模；卷二：系统与语言规约. 清华大学出版社， 2012.
6. Jean-Francois Monin, 《Understanding Formal methods》，Springer,  2003.
7. 冯登国，《安全协议-理论与实践》，清华大学出版社，2011.
8. Doron A.Peled 著, 王林章 译， 《软件可靠性方法》，机械工业出版社，2012.
9. 寇晓蕤，王清贤，《网络安全协议-原理、结构和应用》，高等教育出版社，2011.