通信学报
通信學報
통신학보
JOURNAL OF CHINA INSTITUTE OF COMMUNICATIONS
2012年
z1期
250-254
,共5页
安全协议%形式化方法%协议组合逻辑%Otway-Rees协议
安全協議%形式化方法%協議組閤邏輯%Otway-Rees協議
안전협의%형식화방법%협의조합라집%Otway-Rees협의
选取认证密钥分配协议Otway-Rees协议作为研究对象,利用协议组合逻辑(PCL)作为协议证明工具,对安全协议形式化分析及证明进行了研究.首先给出了 Otway-Rees 协议常见的攻击形式,分析了存在的缺陷,提出了改进方案(AOR协议);然后,为了更好地形式化描述 AOR协议,对传统的 PCL进行一定的扩展;紧接着,用扩展后的PCL对改进的协议中各个实体的行为和协议的安全属性进行形式化描述,将改进后的协议进行模块化划分,并利用PCL进行组合证明;最后,得出改进后的AOR协议具有密钥保密属性.
選取認證密鑰分配協議Otway-Rees協議作為研究對象,利用協議組閤邏輯(PCL)作為協議證明工具,對安全協議形式化分析及證明進行瞭研究.首先給齣瞭 Otway-Rees 協議常見的攻擊形式,分析瞭存在的缺陷,提齣瞭改進方案(AOR協議);然後,為瞭更好地形式化描述 AOR協議,對傳統的 PCL進行一定的擴展;緊接著,用擴展後的PCL對改進的協議中各箇實體的行為和協議的安全屬性進行形式化描述,將改進後的協議進行模塊化劃分,併利用PCL進行組閤證明;最後,得齣改進後的AOR協議具有密鑰保密屬性.
선취인증밀약분배협의Otway-Rees협의작위연구대상,이용협의조합라집(PCL)작위협의증명공구,대안전협의형식화분석급증명진행료연구.수선급출료 Otway-Rees 협의상견적공격형식,분석료존재적결함,제출료개진방안(AOR협의);연후,위료경호지형식화묘술 AOR협의,대전통적 PCL진행일정적확전;긴접착,용확전후적PCL대개진적협의중각개실체적행위화협의적안전속성진행형식화묘술,장개진후적협의진행모괴화화분,병이용PCL진행조합증명;최후,득출개진후적AOR협의구유밀약보밀속성.