Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model

Computer Science > Cryptography and Security [Submitted on 16 Apr 2026] Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model Murat Moran 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. Subjects: Cryptography and Security (cs.CR) Cite as: arXiv:2604.15402 [cs.CR]   (or arXiv:2604.15402v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2604.15402 Focus to learn more Submission history From: Murat Moran [view email] [v1] Thu, 16 Apr 2026 14:09:50 UTC (33 KB) Access Paper: HTML (experimental) view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-04 Change to browse by: cs References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)