软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2011年
3期
509-521
,共13页
陈明%吴开贵%吴长泽%徐洁%吴中福
陳明%吳開貴%吳長澤%徐潔%吳中福
진명%오개귀%오장택%서길%오중복
异步通信%公平交换%形式化分析%推理逻辑%模型检查
異步通信%公平交換%形式化分析%推理邏輯%模型檢查
이보통신%공평교환%형식화분석%추리라집%모형검사
在深入分析公平交换协议现有研究和各项安全属性的基础上,由于信任逻辑方法难以分析乐观公平交换协议的公平性和时限性,提出一种公平交换协议形式化模型和推理逻辑.新模型将信道错误转化为攻击行为,将参与者分为诚实与不诚实两类,并将这些威胁归结为两类入侵者.基于模型检查思想,新逻辑将协议定义为Kripke结构的演化系统,将参与者看作异步环境中的通信进程,定义了时间算子控制实体行为的转换.同时,新逻辑继承了信任逻辑简单、实用的优点.以一个典型协议为例,采用逻辑结合模型检查的方法,演示了分析协议的过程.发现并改进了协议实例的安全缺陷.案例分析表明,新逻辑能够分析公平交换协议的公平性和时限性.
在深入分析公平交換協議現有研究和各項安全屬性的基礎上,由于信任邏輯方法難以分析樂觀公平交換協議的公平性和時限性,提齣一種公平交換協議形式化模型和推理邏輯.新模型將信道錯誤轉化為攻擊行為,將參與者分為誠實與不誠實兩類,併將這些威脅歸結為兩類入侵者.基于模型檢查思想,新邏輯將協議定義為Kripke結構的縯化繫統,將參與者看作異步環境中的通信進程,定義瞭時間算子控製實體行為的轉換.同時,新邏輯繼承瞭信任邏輯簡單、實用的優點.以一箇典型協議為例,採用邏輯結閤模型檢查的方法,縯示瞭分析協議的過程.髮現併改進瞭協議實例的安全缺陷.案例分析錶明,新邏輯能夠分析公平交換協議的公平性和時限性.
재심입분석공평교환협의현유연구화각항안전속성적기출상,유우신임라집방법난이분석악관공평교환협의적공평성화시한성,제출일충공평교환협의형식화모형화추리라집.신모형장신도착오전화위공격행위,장삼여자분위성실여불성실량류,병장저사위협귀결위량류입침자.기우모형검사사상,신라집장협의정의위Kripke결구적연화계통,장삼여자간작이보배경중적통신진정,정의료시간산자공제실체행위적전환.동시,신라집계승료신임라집간단、실용적우점.이일개전형협의위례,채용라집결합모형검사적방법,연시료분석협의적과정.발현병개진료협의실례적안전결함.안례분석표명,신라집능구분석공평교환협의적공평성화시한성.
