东南大学学报(自然科学版)
東南大學學報(自然科學版)
동남대학학보(자연과학판)
JOURNAL OF SOUTHEAST UNIVERSITY
2005年
5期
688-691
,共4页
不可否认%公平性%SVO逻辑%形式化分析
不可否認%公平性%SVO邏輯%形式化分析
불가부인%공평성%SVO라집%형식화분석
使用SVO逻辑对Zhou-Gollmann的公平不可否认协议的一个改进协议进行了形式化分析.在分析该协议的过程中,分析了使用SVO逻辑分析不可否认协议时存在的一些问题,这是分析过程无法发现Zhou-Gollmann不可否认协议的原因.这些问题包括协议目标的确定,协议时限性的描述与分析,协议初始假设集的确定等.分析协议时,不仅需要证明协议的最终目标,还需要证明中间目标.通过对SVO逻辑的语法进行扩展,使其具有显式的时间描述能力,从而能够分析不可否认协议的时限性.
使用SVO邏輯對Zhou-Gollmann的公平不可否認協議的一箇改進協議進行瞭形式化分析.在分析該協議的過程中,分析瞭使用SVO邏輯分析不可否認協議時存在的一些問題,這是分析過程無法髮現Zhou-Gollmann不可否認協議的原因.這些問題包括協議目標的確定,協議時限性的描述與分析,協議初始假設集的確定等.分析協議時,不僅需要證明協議的最終目標,還需要證明中間目標.通過對SVO邏輯的語法進行擴展,使其具有顯式的時間描述能力,從而能夠分析不可否認協議的時限性.
사용SVO라집대Zhou-Gollmann적공평불가부인협의적일개개진협의진행료형식화분석.재분석해협의적과정중,분석료사용SVO라집분석불가부인협의시존재적일사문제,저시분석과정무법발현Zhou-Gollmann불가부인협의적원인.저사문제포괄협의목표적학정,협의시한성적묘술여분석,협의초시가설집적학정등.분석협의시,불부수요증명협의적최종목표,환수요증명중간목표.통과대SVO라집적어법진행확전,사기구유현식적시간묘술능력,종이능구분석불가부인협의적시한성.