计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2007年
31期
115-118
,共4页
形式验证%合同签署协议%非滥用性%数字签名
形式驗證%閤同籤署協議%非濫用性%數字籤名
형식험증%합동첨서협의%비람용성%수자첨명
非滥用性是合同签署协议提出的新的安全需求,人们对它的描述还模糊不明.利用交互式定理证明器Isabelle/HOL推导了"TTP的aborted仲裁"与"失败的合同签约"的不等价关系,提出了"合同签约失败"的形式定义,提出了一个新的非滥用性的形式化描述,验证了BW多方合同签署协议的非滥用性.
非濫用性是閤同籤署協議提齣的新的安全需求,人們對它的描述還模糊不明.利用交互式定理證明器Isabelle/HOL推導瞭"TTP的aborted仲裁"與"失敗的閤同籤約"的不等價關繫,提齣瞭"閤同籤約失敗"的形式定義,提齣瞭一箇新的非濫用性的形式化描述,驗證瞭BW多方閤同籤署協議的非濫用性.
비람용성시합동첨서협의제출적신적안전수구,인문대타적묘술환모호불명.이용교호식정리증명기Isabelle/HOL추도료"TTP적aborted중재"여"실패적합동첨약"적불등개관계,제출료"합동첨약실패"적형식정의,제출료일개신적비람용성적형식화묘술,험증료BW다방합동첨서협의적비람용성.
