集美大学学报（自然科学版）
集美大學學報（自然科學版）
집미대학학보（자연과학판）
JOURNAL OF JIMEI UNIVERSITY(NATURAL SCIENCE)
2014年
5期
386-392
,共7页
模型检测%SPIN%SSL协议%Promela%LTL
模型檢測%SPIN%SSL協議%Promela%LTL
모형검측%SPIN%SSL협의%Promela%LTL
针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.
針對傳統的測試方法無法對網絡安全協議的邏輯本身進行驗證等問題,提齣瞭一套基于形式化分析和SPIN模型檢測的驗證方法.該方法首先以BAN邏輯對目標協議進行形式化分析,然後推斷目標協議存在的問題缺陷,併通過Promela語言對其構建SPIN模型,最後通過SPIN軟件驗證推斷的正確性.併以SSL協議作為具體實例予以論證,結果錶明所提方法具可行性.
침대전통적측시방법무법대망락안전협의적라집본신진행험증등문제,제출료일투기우형식화분석화SPIN모형검측적험증방법.해방법수선이BAN라집대목표협의진행형식화분석,연후추단목표협의존재적문제결함,병통과Promela어언대기구건SPIN모형,최후통과SPIN연건험증추단적정학성.병이SSL협의작위구체실례여이론증,결과표명소제방법구가행성.
