基于模糊 Dolev-Yao 攻击者模型的分级符号化验证
密码学与安全
2026-04-28 v1 形式语言与自动机理论
计算机科学中的逻辑
符号计算
摘要
经典的 Dolev-Yao 符号化协议验证使用二值攻击者知识（已知/未知）。这种抽象忽略了累积侧信道场景，其中重复的噪声观测会逐步提升攻击者的知识。我们使用分级攻击者视图 、乘积 T-范数泄漏更新以及改进的 Murphi 中的有限网格显式状态执行来对该过程建模。该方法通过精确的概念格属性约简进行优化，并揭示了阈值驱动的安全-失效转换，这些转换在相同有界假设下的对应二值运行中并未出现。在包括 Needham-Schroeder-Lowe (NSL) 在内的对称和非对称协议上的执行结果表明，在清晰语义下通过的基线模型，一旦启用累积侧信道泄漏，就可能失效。
引用
@article{arxiv.2604.15402,
title = {Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model},
author = {Murat Moran},
journal= {arXiv preprint arXiv:2604.15402},
year = {2026}
}