桂林电子科技大学学报
桂林電子科技大學學報
계림전자과기대학학보
JOURNAL OF GUILIN UNIVERSITY OF ELECTRONIC TECHNOLOGY
2007年
5期
378-382
,共5页
组合协议%协议分析%操作语义模型%Scyther
組閤協議%協議分析%操作語義模型%Scyther
조합협의%협의분석%조작어의모형%Scyther
协议的可组合性问题是安全协议形式化分析及验证领域的一个公开问题,通过提出采用安全协议的操作语义模型对组合协议进行形式分析和验证,建立了Yahalom和Denning-Sacco组合协议的操作语义模型,并用基于操作语义模型的自动化验证工具Scyther验证了其安全性,发现了一个针对Yahalom协议机密性的组合攻击.结果表明,操作语义模型是分析与验证组合协议的一种可行方法.
協議的可組閤性問題是安全協議形式化分析及驗證領域的一箇公開問題,通過提齣採用安全協議的操作語義模型對組閤協議進行形式分析和驗證,建立瞭Yahalom和Denning-Sacco組閤協議的操作語義模型,併用基于操作語義模型的自動化驗證工具Scyther驗證瞭其安全性,髮現瞭一箇針對Yahalom協議機密性的組閤攻擊.結果錶明,操作語義模型是分析與驗證組閤協議的一種可行方法.
협의적가조합성문제시안전협의형식화분석급험증영역적일개공개문제,통과제출채용안전협의적조작어의모형대조합협의진행형식분석화험증,건립료Yahalom화Denning-Sacco조합협의적조작어의모형,병용기우조작어의모형적자동화험증공구Scyther험증료기안전성,발현료일개침대Yahalom협의궤밀성적조합공격.결과표명,조작어의모형시분석여험증조합협의적일충가행방법.
