基于Petri网的多主体网络交易系统交互行为安全分析方法研究

With the rapid development of online transaction, the issues of interactive behavior security have become the new security challenges in the business system. Starting from real and typical cases, this project mainly analyzes the issues of interactive behaviors in multi-party, distributed and multi-session online transaction business processes, and concisely proposes “how to formally depict multi-party online transaction business processes” and “how to formally analyze behavior security” that are two key scientific problems. In order to realize interactive behavior security of online transaction business processes, this project starts researching from modeling and analysis, to build online transaction data-session-process fusion model and related modeling methods based on Petri nets. Then, study description and expression methods of interactive behavior security, and explore formally analysis methods. This project emphasizes the interactive behavior security of business processes at system design phase and application level instead of that the systems are modified and maintained at the implementation and running phase, which is known to be extremely costly. Finally, multi-party and multi-session online transaction business process model and formally analysis methods are formed. Therefore, it can provide the theory and method foundation for trustworthy online transaction systems.

随着网络交易的迅猛发展，交互行为安全问题已成为网络交易系统中新的安全挑战。本项目深入研究网络交易系统在交互行为方面存在的问题，重点针对多主体、分布式、多会话的网络交易业务流程，从应用实际和典型案例出发，凝练提出“如何对多主体交互业务流程进行形式化描述”和“如何用形式化方法对交互行为安全进行分析”两个关键科学问题。以实现网络交易系统的交互行为安全为目标，从模型和分析的角度展开研究。建立基于Petri网的网络交易数据会话流程融合模型及相关建模方法，揭示其行为机理。在此基础上，研究交互行为安全的描述与表达方法，探索面向交互行为安全的分析和验证方法。着重在系统设计阶段及业务应用层上实现网络交易系统的交互行为安全，从而避免在线阶段因事故的发生以及对系统的修补和维护所导致的巨大经济损失。最终，形成多主体多会话网络交易模型和交互行为安全形式化分析验证方法，为保证网络交易系统的可信运行提供理论和方法基础。

通过技术手段确保网络交易系统的安全可信，是现代互联网发展的重要课题。本项目以交互行为安全为核心，面向开放网络环境下多方交互的交易流程行为和资金安全，提出了网络交易业务流程模型的建模方法；为了对网络交易业务流程模型进行有效的分析，建立了包括数据状态可达图，三维关联矩阵，以及化简等价方法等一套分析技术。为了减小分析复杂度，将切片思想应用于Petri网和EBPN模型，可以进一步提高复杂系统的分析效率，发现潜在的逻辑缺陷和脆弱区域。同时，开发了相应的验证原型系统。项目按计划执行，进展良好，获得了预期的研究成果，共发表论文12篇，包括《IEEE Transactions on Systems, Man, and Cybernetics: Systems》, 《Future Generation Computer Systems》等国际知名期刊。项目成果为保障网络交易软件系统的流程一致、行为可信提供了理论基础和技术支持。下一步课题组将进一步完善相关建模和分析技术，并尝试将项目成果进行转化及应用。