基于进程代数的电子商务协议形式化研究

电子商务已成为网络技术应用新的发展方向。电子商务协议是保证客户和商家之间完成正常、可靠、安全交易活动的规则，是电子商务安全的基础。电子商务协议的设计极易出错，要设计一个正确、符合安全目标、没有冗余的协议十分困难。20年来，为了应对这一挑战，人们设计了不同种类的形式化分析方法，投入了大量的精力。进程代数对于协议的描述几乎接近协议的本身含义，因此它可以很精确地刻划协议的运行过程；同时，进程代数的类型系统和等价关系可以精确地验证协议的各项性质。我们要研究的是利用进程代数的等价关系性质和类型系统来验证电子商务协议的性质。首先，我们要建立一个适合于电子商务协议形式化研究的抽象模型Epi演算，围绕Epi演算能验证电子商务协议性质的目的，对其操作语义、类型系统、等价关系及表达能力进行研究和完善。在此基础上，尝试开发一个电子商务协议的自动验证工具。