当今时代已进入互联网络的时代,网络的飞速发展给社会带来了巨大的变革,电子商务以及电子政务的蓬勃发展应用就是一个典型的例子.但这种应用及网络的开放性也带来了新的信息安全问题.信息安全已成为影响国家安全、社会稳定和经济发展的重要因素.基于信息安全的电子商务协议的设计和应用,就是为了保证网络和信息的安全.协议涉及到两个方面的内容,一是加密技术的选用,二是协议逻辑的设计.通常加密技术倍受重视而忽略了协议逻辑设计,这就为黑客的攻击,留下了许多隐患和漏洞.针对协议逻辑出现的问题,为保证基于信息安全的电子商务协议设计的正确性,就需要用形式化的分析工具来精确描述和仿真协议的行为、协议所要达到的目标以及能否达到其预期的目标.该论文重点研究了目前流行的电子商务协议的形式化分析方法、基于电子商务安全认证的基本协议和交易协议、以及基于公钥基础设施PKI的安全认证协议.在此基础上,论文的作者完成了如下的工作:①提出了某工商管理部门电子商务的安全认证协议.②创新性地提出了用Petri网理论描述了①的认证协议,建立了该协议的Petri网模型.在此基础上对模型进行了仿真分析,证明了协议存在的隐患和漏洞,并进行了修改.最后得到了较为完善的适合某工商管理部门电子商务的安全认证协议.③提出了某工商管理部门电子商务在完成认证之后要进行交易的支付协议.④根据支付协议的特点,创新性地提出了用有穷自动机理论建立③的支付协议的自动机模型.通过对模型的仿真分析,证明了:·③的支付协议满足可追究性·③的支付协议不满足公平性根据结果,作者提出了同时满足可追究性和公平性的完善的支付协议.⑤作者将上述完善的②、④协议,成功地应用到了"基于信息安全的通用网络考试平台"软件产品中和某工商管理部门的电子商务中.