聊城大学学报（自然科学版）
聊城大學學報（自然科學版）
료성대학학보（자연과학판）
JOURNAL OF LIAOCHENG TEACHERS UNIVERSITY（NATURAL SCIENCE EDITION）
2015年
1期
79-82
,共4页
安全协议%串空间模型%N-S公钥协议
安全協議%串空間模型%N-S公鑰協議
안전협의%천공간모형%N-S공약협의
security protocol%the strand space model%N-S public key protocol
串空间模型认证测试方法是定理证明安全协议分析法中最具有代表性的一类。利用串空间模型理论对Needham‐Schroeder（N‐S）公钥协议中中间人攻击问题进行形式化分析与设计，并对其进行证明。与原有技术相比，该方法更为形式化，协议分析人员可以很方便地进行手动分析，并且更有利于协议分析自动化工具的实现。
串空間模型認證測試方法是定理證明安全協議分析法中最具有代錶性的一類。利用串空間模型理論對Needham‐Schroeder（N‐S）公鑰協議中中間人攻擊問題進行形式化分析與設計，併對其進行證明。與原有技術相比，該方法更為形式化，協議分析人員可以很方便地進行手動分析，併且更有利于協議分析自動化工具的實現。
천공간모형인증측시방법시정리증명안전협의분석법중최구유대표성적일류。이용천공간모형이론대Needham‐Schroeder（N‐S）공약협의중중간인공격문제진행형식화분석여설계，병대기진행증명。여원유기술상비，해방법경위형식화，협의분석인원가이흔방편지진행수동분석，병차경유리우협의분석자동화공구적실현。
The certification testing of method Strand space model is the most representative in the methods of theorem provingsecurity protocol analysis .Using the strand space model theory Analysis and design Formalization to the problem of intermediator attacks in n‐s public key protocol ,and prove it . Compared with the original technique ,The approach is more formal .Protocol analysis personnel can be very convenient formanual analysis ,and more conducive to the realization of protocol analysisautomation tools .
