Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model

arXiv:2604.15402v1 Announce Type: new
Abstract: 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 (mu_Kin[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.