基于项重写的安全电子交易形式化模型

摘要

构建一个安全电子交易的形式化模型,为实现对相关安全协议的自动化分析提供了理论基础和技术手段.该模型基于项重写理论进行构建,通过符号化和规则化的方式刻画电子交易的3个主要过程,不但体现交易双方能互相检验身份的安全机制,并且通过项重写系统终止性和会聚性的性质证明该模型具有完整性和一致性等特点,在安全性分析方面验证该模型满足认证性和发送非否认性.