随着Internet的日益发展与普及,电子商务已成为基于Internet的现代经济活动的主要形式之一。电子商务交易中通常涉及到互不信任的交易方。电子商务活动的主要问题之一就是在任意两个互不信任的主体之间以一种公平的方式来交换电子数据。公平性和可行性成为这类电子商务协议的基本要求。公平交换协议可以使得参与交换的双方以公平的方式交换信息,这样,要么任何一方都可以得到对方的信息,要么双方都得不到对方的信息。 安全协议的设计是一个众所周知的难题,常因一些细微的问题产生缺陷。一个安全协议是否能达到设计者所期望的安全目标,需要对其进行严格的形式化分析。目前已有众多分析认证协议的形式化分析方法。公平交换协议是更为复杂的安全协议,它不仅需要满足认证协议的安全需求,还要考虑认证协议中未涉及到的若干安全性质,例如公平性、适时中止性、可追究性等。分析认证协议的方法不再直接适用于分析公平交换协议。 目前已有一些分析公平交换协议的形式化方法,其中有将分析认证协议的方法稍做扩展,使之适用于分析公平交换协议的,如Paulson的归纳法[87],Schneider的CSP方法[85],Vitaly Shmatikov和John Mitchell的Mur φ[89]等;有将一般协议检测工具用于分析公平交换协议的,如Boyd和Kearny提出了用协议规范演示工具Possum分析公平交换协议[88],Steve Kremer使用ATS模型检测工具Mocha检测协议[92]等。这些方法有的不涉及协议的分支(branch),有的不能分析协议的可追究性。目前对公平交换协议的分析是一个新的领域,一些方法、技术还有待于完善。 本文主要研究公平交换协议的分析方法,包括对公平交换协议要满足的主要特性:公平性、可行性、适时中止性、可追究性的分析。