Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model
For security protocol verification, it addresses the gap of cumulative side-channel attacks that are missed by classical binary models.
The paper introduces a graded symbolic verification method using a fuzzy Dolev-Yao attacker model to capture cumulative side-channel leakage, showing that protocols passing under classical binary semantics can fail under graded leakage (e.g., Needham-Schroeder-Lowe).
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.