CAJ | 학술논문

为了描述非否认协议中的各种不确定因素,在Kailar逻辑系统中引入了表示缺省信息的否定词,以及相应的推理机制.提出了安全协议验证的新方法,主要特点是:可以直接对协议的动态运行过程进行推理;推理具有非单调性;避免过多的理想化假设;可以分析含有多个子协议的非否认协议,以及协议的可追究性和公平性.文中以一种基于离线TTP方式的非否认协议为例,验证了该协议在运行一次时具有可追究性,但多次运行时存在攻击.
위료묘술비부인협의중적각충불학정인소,재Kailar라집계통중인입료표시결성신식적부정사,이급상응적추리궤제.제출료안전협의험증적신방법,주요특점시:가이직접대협의적동태운행과정진행추리;추리구유비단조성;피면과다적이상화가설;가이분석함유다개자협의적비부인협의,이급협의적가추구성화공평성.문중이일충기우리선TTP방식적비부인협의위례,험증료해협의재운행일차시구유가추구성,단다차운행시존재공격.