基于模型检测的多轮FR协议验证  

Verifying Multiple Runs of FR Protocol Using Model Checking

作　　者：郭华[1] 庄雷[2] 张习勇[3] 李舟军[1] 

机构地区：[1]北京航空航天大学计算机学院,北京100083 [2]郑州大学理论计算机研究所,郑州450052 [3]解放军信息工程大学,郑州450002

出　　处：《计算机科学》2008年第5期95-98,共4页Computer Science

基　　金：国家自然科学基金项目(60473057，69873040);河南省教育厅基础研究项目(2003520256)

摘　　要：随着网络的大规模应用,越来越多的协议在并发环境中执行,时间也成为协议中一个重要因素。本文对公平交换协议Franklin/Reiter协议加入了时间因素,用时间自动机对其建模,并用自动验证工具UPPAAL验证了单轮协议的性质。重点验证了并发环境中多轮协议的执行情况,最后给出了协议在多轮情况下正常执行需满足的条件。With the growing popularity of the Internet, more and more protocols run concurrently. In this paper, time is added to the FR protocol, and timed automata is used to model Franklin/Reiter protocol. Then UPPAAL is used to verify some properties of the protocol. This paper focuses on multiple runs of FR protocol, and gives some qualifications ensuring that the protocol runs successfully in the concurrent environment.

关 键 词：电子商务协议 模型检测 时间自动机 UPPAAL 多轮执行 

分 类 号：TP393[自动化与计算机技术—计算机应用技术] TN915.04[自动化与计算机技术—计算机科学与技术]