计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2010年
7期
38-41
,共4页
安全协议%模型检测%TLA%TLA+%TLC
安全協議%模型檢測%TLA%TLA+%TLC
안전협의%모형검측%TLA%TLA+%TLC
行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑,在描述并发转移系统中,行为时序逻辑通过引入行动和行为的概念,使得系统和属性可用同一种行为时序逻辑来表示.本文首先介绍行为时序逻辑的语法、语义及简单推理规则;然后以典型的NS公开密钥协议为例,对其进行形式化分析,建立了入侵者参加的简化模型.通过对模型进行FSM建模,转化为TLA+描述的规约系统,然后对其进行TLC检测,发现其存在中间人的重放攻击.
行為時序邏輯是一種組閤瞭時序邏輯與行為邏輯來對併髮繫統進行描述與驗證的邏輯,在描述併髮轉移繫統中,行為時序邏輯通過引入行動和行為的概唸,使得繫統和屬性可用同一種行為時序邏輯來錶示.本文首先介紹行為時序邏輯的語法、語義及簡單推理規則;然後以典型的NS公開密鑰協議為例,對其進行形式化分析,建立瞭入侵者參加的簡化模型.通過對模型進行FSM建模,轉化為TLA+描述的規約繫統,然後對其進行TLC檢測,髮現其存在中間人的重放攻擊.
행위시서라집시일충조합료시서라집여행위라집래대병발계통진행묘술여험증적라집,재묘술병발전이계통중,행위시서라집통과인입행동화행위적개념,사득계통화속성가용동일충행위시서라집래표시.본문수선개소행위시서라집적어법、어의급간단추리규칙;연후이전형적NS공개밀약협의위례,대기진행형식화분석,건립료입침자삼가적간화모형.통과대모형진행FSM건모,전화위TLA+묘술적규약계통,연후대기진행TLC검측,발현기존재중간인적중방공격.
