量子科技中心_量科网

经典离散事件系统的不透明性理论严格依赖于可观测事件序列，本质上无法捕捉混合架构中的安全漏洞——攻击者可同时利用经典踪迹和局域量子关联。为弥补这一缺陷，该团队在安全部分观测量子Petri网框架中形式化了当前状态不透明性，通过展开配置引入真并发语义，将经典观测表示为偏序多重集。在此基础上，该团队将定量后态泄漏定义为攻击者局域量子态之间的迹距离，其评估条件取决于底层系统是否到达秘密标识。该形式化定义严格保留了经典不透明性语义。为实现计算可处理性，该团队采用稳定子形式体系并开发了精确符号验证算法。该方法结合定向展开探索、仅在最大不可观测到达处进行状态聚合以及稳定子表格传播，同时规避了并发交错爆炸和指数级密度矩阵开销。最后通过纠缠交换案例研究验证了精确泄漏评估，展示了显著计算优势，并为反例引导的泄漏强化建立了严格接口。