基于模型检测的SSL协议形式化验证

• 作者: 曾华朴 王巍 黄艳洋
• 来源期刊: 集美大学学报（自然科学版）
• 学科: 工学
• 关键词: 模型检测 SPIN SSL协议 Promela LTL
• 年，卷（期）: 2014,（5）
• 所属期刊栏目: 数理科学与信息工程
• 页码范围: 386-392
• 页数: 7页
• 分类号: TP393
• 字数: 3777字
• 语种: 中文

摘要

针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王巍	集美大学计算机工程学院	12	19	2.0	3.0
2	曾华朴	集美大学计算机工程学院	3	1	1.0	1.0
3	黄艳洋	集美大学信息工程学院	6	24	3.0	4.0