软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2006年
7期
1510-1516
,共7页
不可否认%时限性%SVO逻辑%形式化分析
不可否認%時限性%SVO邏輯%形式化分析
불가부인%시한성%SVO라집%형식화분석
虽然SVO逻辑由于其简单性在对不可否认协议的形式化分析中得到了广泛的应用,但它在时间描述能力上的不足使得它无法分析不可否认协议的时限性.通过向SVO逻辑添加一种简单的时间表达和分析方法扩展了SVO逻辑,并使用扩展后的逻辑对Zhou和Gollmann于1996年提出的一个公平不可否认协议及其一个改进协议进行了分析.分析结果表明,原协议不具有时限性,而改进协议具有时限性,因此也说明了扩展后的新逻辑能够分析不可否认协议的时限性.另外,新逻辑还能用来分析一般密码协议中的时间相关性质.
雖然SVO邏輯由于其簡單性在對不可否認協議的形式化分析中得到瞭廣汎的應用,但它在時間描述能力上的不足使得它無法分析不可否認協議的時限性.通過嚮SVO邏輯添加一種簡單的時間錶達和分析方法擴展瞭SVO邏輯,併使用擴展後的邏輯對Zhou和Gollmann于1996年提齣的一箇公平不可否認協議及其一箇改進協議進行瞭分析.分析結果錶明,原協議不具有時限性,而改進協議具有時限性,因此也說明瞭擴展後的新邏輯能夠分析不可否認協議的時限性.另外,新邏輯還能用來分析一般密碼協議中的時間相關性質.
수연SVO라집유우기간단성재대불가부인협의적형식화분석중득도료엄범적응용,단타재시간묘술능력상적불족사득타무법분석불가부인협의적시한성.통과향SVO라집첨가일충간단적시간표체화분석방법확전료SVO라집,병사용확전후적라집대Zhou화Gollmann우1996년제출적일개공평불가부인협의급기일개개진협의진행료분석.분석결과표명,원협의불구유시한성,이개진협의구유시한성,인차야설명료확전후적신라집능구분석불가부인협의적시한성.령외,신라집환능용래분석일반밀마협의중적시간상관성질.
