Classical symbolic protocol verification under Dolev--Yao uses binary attacker knowledge (known/unknown). This abstraction misses cumulative side-channel settings, where repeated noisy observations progressively improve attacker knowledge. We model this process with a graded attacker view \(μ_K\in[0,1]\), product T-norm leak updates, and finite-grid explicit-state execution in Modified Murphi. The method is optimised with exact concept-lattice attribute reducts and exposes threshold-driven safe-to-fail transitions that are not represented in corresponding binary runs under the same bounded assumptions. Executed results on symmetric and asymmetric protocols, including Needham--Schroeder--Lowe (NSL), show that baseline models passing under crisp semantics can fail once cumulative side-channel leakage is enabled.

翻译：经典Dolev-Yao框架下的符号协议验证采用二元攻击者知识模型（已知/未知）。该抽象方法无法捕捉累积侧信道场景——重复的噪声观测会逐步提升攻击者知识。我们通过分层攻击者视图\(μ_K\in[0,1]\)、乘积T范数泄露更新机制以及改进的Murphi有限网格显式状态执行来建模该过程。该方法利用精确概念格属性约简进行优化，并揭示了在相同有界假设下对应二元运行中未体现的阈值驱动型安全-失败转换。对Needham-Schroeder-Lowe(NSL)等对称与非对称协议的执行结果表明，在清晰语义下通过验证的基准模型一旦启用累积侧信道泄露便会失效。