|本期目录/Table of Contents|

[1]王巍,曾华朴,黄艳洋.基于模型检测的SSL协议形式化验证[J].集美大学学报(自然科学版),2014,19(5):386-392.
　WANG Wei,ZENG Hua-pu,HUANG Yan-yang.The Formal Verification of SSL Protocol Based on Model Checking[J].Journal of Jimei University,2014,19(5):386-392.
点击复制

基于模型检测的SSL协议形式化验证()
分享到：

《集美大学学报（自然科学版）》[ISSN:1007-7405/CN:35-1186/N]

卷:
第19卷
期数:
2014年第5期
页码:
386-392
栏目:
数理科学与信息工程
出版日期:
2014-09-25

文章信息/Info

Title:
The Formal Verification of SSL Protocol Based on Model Checking
作者:
王巍1; 曾华朴1; 黄艳洋2
1.集美大学计算机工程学院，福建 厦门 361021；2.集美大学信息工程学院，福建 厦门 361021
Author(s):
WANG Wei1; ZENG Hua-pu1; HUANG Yan-yang2
1.Computer Engineering College，Jimei University，Xiamen 361021,China;2.Information Engineering College，Jimei University，Xiamen 361021,China
关键词:
模型检测; SPIN; SSL协议; Promela;  LTL
Keywords:
Model checking; SPIN; SSL Protocol; Promela; LTL
分类号:
-
DOI:
-
文献标志码:
A
摘要:
针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题，提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析，然后推断目标协议存在的问题缺陷，并通过Promela语言对其构建SPIN模型，最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证，结果表明所提方法具可行性.
Abstract:
In accordance with the issues that traditional testing methods can＇t verify the logic itself for network security protocol,a set of testing methods based on formal analysis and SPIN model checking is proposed in this paper.Firstly this method formalizes analysis for target protocol by using BAN logic,then concludes the existing problems of target protocol,and makes modeling from the conclusion by using Promela language,finally proves the validity of the the inference by SPIN software.We demonstrate this methods by the SSL protocol as specific examples.The results show that the proposed method is feasible.

参考文献/References:

-

相似文献/References:

备注/Memo

备注/Memo:
-
更新日期/Last Update: 2014-12-04