Sweeping the moving-average detector threshold multiplier k shows that different adversary thresholds produce substantially different certified KL divergence lower bounds; more conservative thresholds (larger k) reduce FPR but can yield significantly larger KL lower bounds even as TPR also changes. The framework audits the HCS against a suite of statistical tests by reporting the maximum lower bound across the family.
From 2026-khoury-maude-hcs-model-checking — Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems
· §5.2
· 2026
· PoPETs 2026
Implications
Undetectability claims must be evaluated against a range of adversary detector thresholds, not a single chosen operating point — a protocol that passes one threshold can fail badly under a more conservative one.
Protocol designers should publish KL divergence lower bounds as a function of detector configuration, not just pass/fail against a single threshold, to give deployers an honest picture of the privacy envelope.