Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917433992806400 |
|---|---|
| author | Moran, Murat |
| author_facet | Moran, Murat |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_15402 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model Moran, Murat Cryptography and Security Formal Languages and Automata Theory Logic in Computer Science Symbolic Computation 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. |
| title | Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model |
| topic | Cryptography and Security Formal Languages and Automata Theory Logic in Computer Science Symbolic Computation |
| url | https://arxiv.org/abs/2604.15402 |