计算机应用
計算機應用
계산궤응용
Journal of Computer Applications
2015年
7期
1870-1876
,共7页
串空间%认证测试%安全协议%自动化验证%认证属性%BAN-Yahalom协议%安全传输层握手协议
串空間%認證測試%安全協議%自動化驗證%認證屬性%BAN-Yahalom協議%安全傳輸層握手協議
천공간%인증측시%안전협의%자동화험증%인증속성%BAN-Yahalom협의%안전전수층악수협의
strand space%authentication test%security protocol%automatic verification%authentication property%BAN-Yahalom protocol%Transport Layer Security (TLS) handshake protocol
针对目前串空间理论依赖分析人员主观判断、无法使用自动化工具进行验证的问题,提出了基于串空间理论的协议认证属性标准化验证过程.首先为协议消息项定义类型标签,对串空间及认证测试理论进行扩展;然后通过判断测试元素出现位置、检验测试元素参数一致性、确认变换进行边唯一存在性和检验目标串参数一致性,将基于串空间理论的协议验证过程标准化为可程序实现的步骤.该算法的时间复杂度为O(n2),避免了模型检测方法的状态空间爆炸问题,并在此基础上实现了安全协议认证属性的自动化验证工具.以BAN-Yahalom协议和TLS 1.0握手协议为例进行了标准化的分析验证,找到了对BAN-Yahalom协议的一种新攻击形式.该攻击无需限制服务器对随机数的检查,比Syverson发现的攻击更具普遍性.
針對目前串空間理論依賴分析人員主觀判斷、無法使用自動化工具進行驗證的問題,提齣瞭基于串空間理論的協議認證屬性標準化驗證過程.首先為協議消息項定義類型標籤,對串空間及認證測試理論進行擴展;然後通過判斷測試元素齣現位置、檢驗測試元素參數一緻性、確認變換進行邊唯一存在性和檢驗目標串參數一緻性,將基于串空間理論的協議驗證過程標準化為可程序實現的步驟.該算法的時間複雜度為O(n2),避免瞭模型檢測方法的狀態空間爆炸問題,併在此基礎上實現瞭安全協議認證屬性的自動化驗證工具.以BAN-Yahalom協議和TLS 1.0握手協議為例進行瞭標準化的分析驗證,找到瞭對BAN-Yahalom協議的一種新攻擊形式.該攻擊無需限製服務器對隨機數的檢查,比Syverson髮現的攻擊更具普遍性.
침대목전천공간이론의뢰분석인원주관판단、무법사용자동화공구진행험증적문제,제출료기우천공간이론적협의인증속성표준화험증과정.수선위협의소식항정의류형표첨,대천공간급인증측시이론진행확전;연후통과판단측시원소출현위치、검험측시원소삼수일치성、학인변환진행변유일존재성화검험목표천삼수일치성,장기우천공간이론적협의험증과정표준화위가정서실현적보취.해산법적시간복잡도위O(n2),피면료모형검측방법적상태공간폭작문제,병재차기출상실현료안전협의인증속성적자동화험증공구.이BAN-Yahalom협의화TLS 1.0악수협의위례진행료표준화적분석험증,조도료대BAN-Yahalom협의적일충신공격형식.해공격무수한제복무기대수궤수적검사,비Syverson발현적공격경구보편성.
