系统仿真学报
繫統倣真學報
계통방진학보
JOURNAL OF SYSTEM SIMULATION
2003年
z1期
11-16
,共6页
密码协议%形式化分析%时间Petri网%BAN逻辑%认证协议
密碼協議%形式化分析%時間Petri網%BAN邏輯%認證協議
밀마협의%형식화분석%시간Petri망%BAN라집%인증협의
形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入.在文中首先对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点,然后用时间Petri网来表示和分析密码协议.该方法不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估.作为实例,对Aziz-Diffie无线协议作了详细的形式分析和性能评估,验证了已知的、存在的漏洞,并且给出了该协议的改进方案.
形式化分析方法由于其精煉、簡潔和無二義性逐步成為分析密碼協議的一條可靠和準確的途徑,但是密碼協議的形式化分析研究目前還不夠深入.在文中首先對四類常見的密碼協議形式化分析方法作瞭一些比較,闡述瞭各自的特點,然後用時間Petri網來錶示和分析密碼協議.該方法不但能夠反映協議的靜態和動態的特性,而且能夠對密碼協議進行時間、空間上的性能評估.作為實例,對Aziz-Diffie無線協議作瞭詳細的形式分析和性能評估,驗證瞭已知的、存在的漏洞,併且給齣瞭該協議的改進方案.
형식화분석방법유우기정련、간길화무이의성축보성위분석밀마협의적일조가고화준학적도경,단시밀마협의적형식화분석연구목전환불구심입.재문중수선대사류상견적밀마협의형식화분석방법작료일사비교,천술료각자적특점,연후용시간Petri망래표시화분석밀마협의.해방법불단능구반영협의적정태화동태적특성,이차능구대밀마협의진행시간、공간상적성능평고.작위실례,대Aziz-Diffie무선협의작료상세적형식분석화성능평고,험증료이지적、존재적루동,병차급출료해협의적개진방안.
