基于高阶逻辑系统HOL的数字硬件形式化验证
| 绪论 | 第1-7页 |
| 第一章 数字硬件形式化验证概述 | 第7-13页 |
| 1．1 形式化 | 第7页 |
| 1．2 形式化的方法 | 第7页 |
| 1．3 形式化的发展 | 第7-9页 |
| 1．4 硬件形式化描述 | 第9-10页 |
| 1．5 硬件形式化验证的过程 | 第10-11页 |
| 1．6 定理证明器 | 第11-13页 |
| 第二章 HOL系统 | 第13-27页 |
| 2．1 ML语言的介绍 | 第13-17页 |
| 2．2 HOL系统 | 第17-27页 |
| 第三章 RSA加密算法的形式化证明 | 第27-39页 |
| 3．1 RSA算法 | 第27-28页 |
| 3．2 RSA的安全性 | 第28页 |
| 3．3 RSA的现状和前景 | 第28-29页 |
| 3．4 RSA算法正确性的形式化验证 | 第29-39页 |
| 第四章 RSA数字硬件的形式化验证 | 第39-61页 |
| 4．1 VHDL语言简介 | 第39-43页 |
| 4．2 RSA数字硬件的实现 | 第43-44页 |
| 4．3 模和同余的转换的形式化证明 | 第44-46页 |
| 4．4 模乘运算模块的形式化验证 | 第46-52页 |
| 4．5 加密模块的形式化验证 | 第52-57页 |
| 4．6 证明思路的总结 | 第57-58页 |
| 4．7 验证的结果 | 第58-61页 |
| 结论 | 第61-62页 |
| 致谢 | 第62-63页 |
| 参考文献 | 第63-64页 |
| 作者在读期间的研究成果 | 第64-65页 |
| 附录A 重要定理证明对策清单 | 第65-67页 |
| 附录B RSA数字硬件VHDL程序清单 | 第67-69页 |
