贵州大学学报（自然科学版）
貴州大學學報（自然科學版）
귀주대학학보（자연과학판）
JOURNAL OF GUIZHOU UNIVERSITY(NATURAL SCIENCE)
2012年
5期
53-57
,共5页
EKE协议%TLA%TLA+%模型检测
EKE協議%TLA%TLA+%模型檢測
EKE협의%TLA%TLA+%모형검측
行为时序逻辑(TLA)是Leslie Lamport于20世纪90年代提出的一种新的逻辑,运用这种逻辑对软件或协议系统进行建模,在一定程度上减少了由于状态空间爆炸带来的压力,它能在一种语言中同时表达模型程序与系统属性.文中首先介绍了行为时序逻辑的语法和语义,然后以EKE协议为例,用基于行为时序逻辑语言TLA+对EKE协议进行了建模分析,用TLA建模并用行为时序逻辑语言TLA+进行协议的描述,最后用TLC检测工具进行分析,发现存在中间人的重放攻击漏洞.
行為時序邏輯(TLA)是Leslie Lamport于20世紀90年代提齣的一種新的邏輯,運用這種邏輯對軟件或協議繫統進行建模,在一定程度上減少瞭由于狀態空間爆炸帶來的壓力,它能在一種語言中同時錶達模型程序與繫統屬性.文中首先介紹瞭行為時序邏輯的語法和語義,然後以EKE協議為例,用基于行為時序邏輯語言TLA+對EKE協議進行瞭建模分析,用TLA建模併用行為時序邏輯語言TLA+進行協議的描述,最後用TLC檢測工具進行分析,髮現存在中間人的重放攻擊漏洞.
행위시서라집(TLA)시Leslie Lamport우20세기90년대제출적일충신적라집,운용저충라집대연건혹협의계통진행건모,재일정정도상감소료유우상태공간폭작대래적압력,타능재일충어언중동시표체모형정서여계통속성.문중수선개소료행위시서라집적어법화어의,연후이EKE협의위례,용기우행위시서라집어언TLA+대EKE협의진행료건모분석,용TLA건모병용행위시서라집어언TLA+진행협의적묘술,최후용TLC검측공구진행분석,발현존재중간인적중방공격루동.
