数字合同签署的假设-保证合成
计算机科学中的逻辑
2011-11-15 v4 密码学与安全
计算机科学与博弈论
编程语言
摘要
我们研究用于数字合同签署的一类公平交换协议——公平不可否认协议的自动合成。首先，我们展示如何将参与代理和可信第三方 (TTP) 的目标指定为 LTL 中的路径公式，并证明这些目标的满足蕴含公平性，这是公平交换协议所需的一个性质。然后，我们证明弱（合作式）协同合成和经典（严格竞争式）协同合成均失败，而假设-保证合成 (AGS) 则成功。我们通过以下方面展示假设-保证合成的成功：(a) 假设-保证合成的任何解都是无攻击的；没有任何参与者子集能违反其他参与者的目标；(b) 存在已知漏洞的 Asokan-Shoup-Waidner (ASW) 认证邮件协议不是 AGS 的解；(c) Kremer-Markowitch (KM) 不可否认协议是 AGS 的一个解；(d) AGS 提出了一个新的、对称的、无攻击的公平不可否认协议。据我们所知，这是合成技术首次应用于公平不可否认协议，我们的结果表明合成既能自动发现协议中的漏洞，也能生成正确的协议。假设-保证合成的解可以作为三人图博弈的安全均衡解被高效计算。
引用
@article{arxiv.1004.2697,
title = {Assume-Guarantee Synthesis for Digital Contract Signing},
author = {Krishnendu Chatterjee and Vishwanath Raman},
journal= {arXiv preprint arXiv:1004.2697},
year = {2011}
}
备注
40 pages, 1 figure, 3 tables and 3 algorithms