基于时间自动机的数据流通控制建模及验证  

Modeling and verification of data circulation control based on timed automata

作　　者：李恒 李凤华[1,2,3] 梁琬珩[1,5] 郭云川 张玲翠 周紫妍[1,2,3] LI Heng;LI Fenghua;LIANG Wanheng;GUO Yunchuan;ZHANG Lingcui;ZHOU Ziyan(Institute of Information Engineering,Chinese Academy of Sciences,Beijing 100085,China;School of Cyber Security,University of Chinese Academy of Sciences,Beijing 100049,China;State Key Laboratory of Cyberspace Security Defense,Beijing 100085,China;National Geomatics Center of China,Ministry of Natural Resources of the People’s Republic of China,Beijing 100830,China;School of Computer Science,School of Cyber Science and Engineering,Nanjing University of Information Sciences&Technology,Nanjing 210044,China)

机构地区：[1]中国科学院信息工程研究所,北京100085 [2]中国科学院大学网络空间安全学院,北京100049 [3]网络空间安全防御全国重点实验室,北京100085 [4]自然资源部国家基础地理信息中心,北京100830 [5]南京信息工程大学计算机学院、网络空间安全学院,江苏南京210044

出　　处：《通信学报》2025年第3期13-27,共15页Journal on Communications

基　　金：国家重点研发计划基金资助项目(No.2023YFB3106505);国家自然科学基金资助项目(No.U24A20240,No.62441226)。

摘　　要：为了解决数据跨域流通控制策略生成、传递与执行的可行性、正确性和安全性验证难题,提出了一种基于时间自动机和计算树时序逻辑的形式化建模及验证方法。该方法首先针对数据流通控制流程,以及数据交易场景(模式)下的数据提供者、数据使用者(含数据经纪人)和数据监管者等实体分别进行形式化建模;随后给出了数据交易过程中,安全需求性质和流通控制属性的计算树时序逻辑形式化规约描述;最后,对上述时间自动机模型进行仿真,并对其性质和属性进行形式化验证与分析。实例分析表明,所提方法可以有效验证数据流通控制机制的可行性、正确性和安全性。To address the challenges of verifying the feasibility,correctness,and security of cross-domain data circulation control policies in their generation,transmission,and execution,a formal modeling and verification method was proposed based on timed automata and computation tree logic(CTL).Firstly,the formal models were established for the data circulation control process and key entities in data transaction scene,including data providers,data consumers(encompassing data brokers),and data supervisors.Subsequently,the security requirements and circulation control properties were formalized during data transactions using CTL specifications.Finally,the aforementioned timed automaton model was simulated,with formal verification and analysis performed on its behavioral properties and structural attributes.The proposed method can effectively validate the feasibility,correctness,and security of data circulation control mechanisms.

关 键 词：数据要素流通 访问控制 时间自动机 延伸控制 形式化方法验证 

分 类 号：TN92[电子电信—通信与信息系统]