网络支付协议的形式化安全需求及验证逻辑  

A logic for the formal requirements and verification of network payment protocols

作　　者：刘怡文[1] 李伟琴[1] 

机构地区：[1]北京航空航天大学计算机学院,北京100083

出　　处：《通信学报》2004年第4期174-182,共9页Journal on Communications

基　　金：国家"863"高科技发展计划基金资助项目(863-306-ZT05-05-6)

摘　　要：从整个网络支付协议的安全角度出发,提出网络支付协议的多层安全需求模型,包括以认证和密钥分配为基础的基层需求、网络支付协议固有的中层需求(包括保密性、原子性、公平性、完整性、匿名性、不可否认性、可追究性等)、以及面向具体应用的高层需求。基于一阶逻辑和时序逻辑,提出一种适合描述网络支付协议的形式化安全需求的逻辑,描述了该逻辑的语法结构和推理规则,并用该安全需求逻辑对网络支付协议的多层安全需求进行了形式化描述。最后,以SET协议为例进行需求验证。From the point of the security of the whole network payment protocols, a framework of the hierarchy security requirements was illustrated, which includes the base requirements based on authentication and key distribution, the middle requirements (such as security, atomicity, fairness, integrity, anonymity, non-repudiation, accountability), and the upper requirements faced on special applications. Based on first-order logic and temporal logic, a logic suitable for specifying the formal requirements for network payment protocols was presented, as well as its grammar and inference rules. Using this logic, the formal hierarchy requirements for network payment protocols were described. As an example, the formal requirements of the SET protocol was verified using this logic.

关 键 词：电子商务协议 形式化验证 安全性 原子性 公平性 匿名性 可追究性 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]