| 基于模型检测的SSL协议形式化验证 |
| |
| 引用本文： | 王巍,曾华朴,黄艳洋.基于模型检测的SSL协议形式化验证[J].集美大学学报(自然科学版),2014,19(5). |
| |
| 作者姓名： | 王巍 曾华朴 黄艳洋 |
| |
| 作者单位： | 1. 集美大学计算机工程学院,福建厦门,361021
2. 集美大学信息工程学院,福建厦门,361021 |
| |
| 基金项目： | 福建省自然科学基金资助项目 |
| |
| 摘 要： | 针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.
|
| 关 键 词： | 模型检测 SPIN SSL协议 Promela LTL |
The Formal Verification of SSL Protocol Based on Model Checking |
| |
| WANG Wei,ZENG Hua-pu,HUANG Yan-yang.The Formal Verification of SSL Protocol Based on Model Checking[J].the Editorial Board of Jimei University(Natural Science),2014,19(5). |
| |
| Authors: | WANG Wei ZENG Hua-pu HUANG Yan-yang |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
