Maude-HCS：评估隐藏通信系统的不可检测性-性能权衡
密码学与安全
2026-03-05 v1
摘要
隐藏通信系统 (HCS) 将潜在信息嵌入普通网络活动中以隐藏通信的存在。实际中，HCS 的不可检测性通常通过 ad hoc 交通统计或特定探测器进行评估，这导致安全论断紧密依赖实验设置和隐式对抗性假设。在本文中，我们将不可检测性形式化为在两种部署下：无隐藏通信的基线系统与携带隐式流量的 HCS 部署之间的可观测执行轨迹的统计不可辨识性。不可检测性以对两种执行产生的轨迹分布之间距离度量的上界进行表达。我们开发了 Maude-HCS，一个可执行的建模与分析框架，为关于 HCS 设计中不可检测性-性能权衡提供原则化且可执行的基础。Maude-HCS 允许设计者指定协议行为、对抗性观察者以及环境假设，并生成由这些执行所诱导的轨迹分布的蒙特卡洛样本。我们展示了 Maude-HCS 可用于审计不可检测性主张，通过估计统计检验的真阳性率和假阳性率，并将这些估计转换为不可检测性度量（如 KL 散度）的下界。这使得在明确建模假设下系统评估不可检测性及其与性能的权衡成为可能。最后，我们在基于隧道的 HCS 实现上评估了 Maude-HCS，并将模型预测与物理测试台的测量结果进行了验证。对于被动对抗者观察 timing 和流量统计，我们量化了不可检测性和性能随协议配置、背景流量和网络丢包率的变化情况，并在模型保证与实证结果之间展示了强大的语义一致性。
引用
@article{arxiv.2603.03369,
title = {Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems},
author = {Joud Khoury and Minyoung Kim and Christophe Merlin and Jose Meseguer and Zachary Ratliff and Carolyn Talcott},
journal= {arXiv preprint arXiv:2603.03369},
year = {2026}
}