Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model

TL;DR

This paper introduces a graded attacker model for symbolic protocol verification that accounts for cumulative side-channel information, revealing safety failures in protocols previously deemed secure.

Contribution

It develops a novel graded attacker framework with optimized analysis techniques to detect safety issues caused by side-channel leakages in symbolic protocol verification.

Findings

Baseline models fail under cumulative leakage scenarios.

Threshold-driven safe-to-fail transitions are identified.

Method applied successfully to NSL protocol.

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_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.