arxiv: 2604.15402 · v1 · submitted 2026-04-16 · 💻 cs.CR · cs.FL· cs.LO· cs.SC

Recognition: unknown

Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model

Murat Moran

Authors on Pith no claims yet

Pith reviewed 2026-05-10 10:50 UTC · model grok-4.3

classification 💻 cs.CR cs.FLcs.LOcs.SC

keywords Dolev-Yaosymbolic verificationside-channel attacksfuzzy attacker modelprotocol securitygraded knowledgeNeedham-Schroeder-Lowe

0 comments

The pith

Protocols that pass binary Dolev-Yao verification can fail when cumulative side-channel leakage is modeled with graded attacker knowledge.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Classical symbolic verification treats attacker knowledge as binary, either known or unknown. This paper replaces that with a continuous grade from 0 to 1 that increases with each noisy observation through the product T-norm. The resulting model is executed on a finite grid using Modified Murphi and optimized by concept-lattice reducts. It identifies specific knowledge thresholds where protocols transition to failure, transitions invisible in binary runs. On the Needham-Schroeder-Lowe protocol and others, this shows that standard verifications can miss real vulnerabilities arising from repeated side-channel information.

Core claim

The central claim is that a graded Dolev-Yao attacker model, where knowledge grade μ_K is updated by the product T-norm on leak events within a finite discretization, exposes safe-to-fail transitions driven by cumulative leakage that do not appear in corresponding binary verification runs under bounded assumptions.

What carries the argument

Graded attacker knowledge μ_K in [0,1] updated via product T-norm on side-channel leaks, executed in explicit-state model checking with concept-lattice optimization.

Load-bearing premise

The product T-norm correctly represents the way repeated noisy observations build up attacker knowledge, and the chosen discretization grid captures all relevant threshold crossings.

What would settle it

A concrete experiment would be to perform side-channel attacks on an NSL implementation and check if the attack succeeds precisely when the graded model predicts the knowledge threshold is crossed, but the binary model still considers it safe.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper adds a graded [0,1] attacker knowledge level with product T-norm updates to symbolic verification and shows some binary-safe protocols fail under cumulative leakage, but the modeling choices lack grounding against real side-channel data.

read the letter

The core contribution is a graded Dolev-Yao model where attacker knowledge sits on a continuous scale rather than binary known/unknown. It updates this grade with a product T-norm on each noisy observation and uses concept-lattice reducts plus finite-grid discretization inside Modified Murphi to keep the state space tractable. On the Needham-Schroeder-Lowe protocol and a couple of symmetric cases, the graded runs expose threshold crossings that the crisp version misses under the same bounds. That difference is the main new observation the work reports. The lattice reduction step looks like a practical engineering choice that could help scale the approach beyond toy examples. The implementation is concrete enough that someone could re-run the NSL case and check the reported safe-to-fail points. The central claim—that binary models can pass while graded ones fail—follows directly from the setup once you accept the update rule and the grid. The paper does not over-claim formal soundness or completeness; it presents the graded view as an extension that captures gradual leakage the binary abstraction ignores. The main weakness is the absence of any check that the product T-norm and the chosen grid actually match measured side-channel behavior. Power and EM traces often show statistical dependence and non-multiplicative accumulation, so the reported transitions could be artifacts of the discretization or the independence assumption rather than evidence of new attacks. No error bounds on the grid resolution appear, and there is no comparison to statistical leakage models or real traces. The free parameter for grid size is acknowledged but not explored for sensitivity. This work is aimed at researchers who already use symbolic tools like Murphi or ProVerif and want to add a lightweight leakage dimension without moving to full probabilistic model checking. A reader looking for new attack scenarios on standard protocols will find concrete examples, but anyone needing validated leakage modeling will have to supply their own justification. It is worth sending to peer review because the idea is distinct from existing binary or probabilistic lines and the implementation is there to inspect, even though the validation gap means referees will likely ask for more empirical grounding on the T-norm and grid choices.

Referee Report

3 major / 2 minor

Summary. The paper proposes extending classical Dolev-Yao symbolic protocol verification to a graded (fuzzy) attacker model. Attacker knowledge is represented by a continuous value μ_K ∈ [0,1] that is updated multiplicatively via the product T-norm on each noisy side-channel observation. The approach is realized via finite-grid explicit-state model checking in Modified Murphi, with optimizations based on concept-lattice attribute reducts. On bounded runs of symmetric and asymmetric protocols (including Needham-Schroeder-Lowe), the method identifies threshold-driven “safe-to-fail” transitions that are invisible under the corresponding binary (crisp) attacker semantics.

Significance. If the modeling choices are sound, the work supplies a concrete, executable bridge between symbolic verification and cumulative side-channel leakage. It demonstrates that protocols previously certified safe under binary knowledge can become attackable once graded leakage is admitted, and it supplies an automated procedure (lattice reducts + grid execution) for locating the critical knowledge thresholds. The explicit-state implementation and the reported NSL counter-examples constitute the primary technical contribution.

major comments (3)

[model definition / leak-update rule] Model definition (product T-norm update rule): the central claim that crisp-passing protocols become unsafe under graded leakage rests on the product T-norm faithfully accumulating independent noisy observations. No derivation, sensitivity analysis, or comparison to additive/statistical side-channel models (e.g., Gaussian or template attacks) is supplied; if real leakage exhibits dependence or non-multiplicative accumulation, the reported safe-to-fail transitions may be modeling artifacts.
[finite-grid execution / NSL experiments] Finite-grid discretization of μ_K: the paper does not report grid resolution, error bounds, or a convergence study. Without such analysis it is impossible to exclude the possibility that narrow transition regions in the NSL or other case studies are missed or fabricated by the chosen discretization step size.
[experimental results / NSL case study] Validation against measured side-channel data: the abstract and results assert that baseline models fail once cumulative leakage is enabled, yet no comparison to real power/EM traces or statistical leakage models is provided. This leaves open whether the discovered thresholds correspond to observable attacks.

minor comments (2)

[experimental setup] The bounded assumptions (session bounds, message sizes, etc.) used for the Murphi runs are stated only at a high level; an explicit enumeration would improve reproducibility.
[preliminaries] Notation for the graded knowledge measure μ_K and the T-norm update should be introduced with a small illustrative example before the full protocol encodings.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive and detailed comments. We address each major comment below and indicate the revisions planned for the manuscript.

read point-by-point responses

Referee: [model definition / leak-update rule] Model definition (product T-norm update rule): the central claim that crisp-passing protocols become unsafe under graded leakage rests on the product T-norm faithfully accumulating independent noisy observations. No derivation, sensitivity analysis, or comparison to additive/statistical side-channel models (e.g., Gaussian or template attacks) is supplied; if real leakage exhibits dependence or non-multiplicative accumulation, the reported safe-to-fail transitions may be modeling artifacts.

Authors: The product T-norm is adopted because it implements the standard fuzzy-logic conjunction for independent propositions, yielding a multiplicative update that reduces to classical Dolev-Yao when knowledge is crisp. This choice is motivated by the desire for an associative, continuous operator that accumulates evidence without presupposing a particular noise distribution. We acknowledge that the manuscript provides neither an explicit derivation from statistical leakage models nor a sensitivity study. In the revised version we will insert a new subsection that (i) derives the update rule from the probabilistic interpretation of independent observations, (ii) compares the product T-norm with the minimum and Łukasiewicz t-norms, and (iii) discusses how the resulting thresholds relate to additive or Gaussian side-channel models, thereby clarifying the modeling assumptions. revision: yes
Referee: [finite-grid execution / NSL experiments] Finite-grid discretization of μ_K: the paper does not report grid resolution, error bounds, or a convergence study. Without such analysis it is impossible to exclude the possibility that narrow transition regions in the NSL or other case studies are missed or fabricated by the chosen discretization step size.

Authors: The manuscript indeed omits explicit reporting of the discretization parameters and any convergence analysis. We will revise the experimental section to state the uniform grid resolution employed for μ_K, supply analytic bounds on the maximum discretization error, and present a convergence study in which the NSL and other protocols are re-executed on successively finer grids. The study will confirm that the reported safe-to-fail thresholds remain stable under refinement, thereby ruling out discretization artifacts. revision: yes
Referee: [experimental results / NSL case study] Validation against measured side-channel data: the abstract and results assert that baseline models fail once cumulative leakage is enabled, yet no comparison to real power/EM traces or statistical leakage models is provided. This leaves open whether the discovered thresholds correspond to observable attacks.

Authors: The contribution of the work is the construction of a graded symbolic verification framework and the identification of threshold phenomena that are invisible under binary semantics. The thresholds are properties of the abstract model, not claims about concrete physical attacks. Empirical validation against power or EM traces lies outside the symbolic scope of the paper. We will add a paragraph in the conclusions that explicitly delineates this boundary and lists integration with statistical leakage models and trace data as planned future work. revision: partial

Circularity Check

0 steps flagged

No circularity: graded model and execution results are independent of the target claim

full rationale

The paper presents an explicit modeling extension (graded μ_K, product T-norm updates, finite-grid Murphi execution) and reports concrete execution outcomes on protocols such as NSL showing safe-to-fail transitions absent from crisp runs. No equation or step equates the reported failure transitions to a fitted parameter, a self-citation chain, or a renaming of the input model; the product T-norm and grid are introduced as modeling choices whose consequences are then observed, not presupposed. The derivation chain therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 1 invented entities

The central claim rests on the product T-norm as the update rule and on the finite-grid discretization being faithful to continuous leakage; both are introduced without external calibration data.

free parameters (1)

grid resolution for μ_K
Finite discretization of the continuous interval [0,1] must be chosen; its fineness affects which thresholds are detected.

axioms (1)

domain assumption Product T-norm correctly models cumulative noisy observations
Invoked to define leak updates; no justification or alternative norms are discussed in the abstract.

invented entities (1)

graded attacker knowledge μ_K no independent evidence
purpose: Replace binary known/unknown with continuous cumulative knowledge
New state variable introduced to capture gradual leakage; no independent falsifiable prediction supplied in the abstract.

pith-pipeline@v0.9.0 · 5420 in / 1256 out tokens · 30026 ms · 2026-05-10T10:50:31.129869+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

35 extracted references

[1]

5g; security architecture and procedures for 5g system

3GPP. 5g; security architecture and procedures for 5g system. Technical report, 2019

2019
[2]

The applied pi calculus: Mobile values, new names, and secure communication.Journal of the ACM, 65(1):1:1–1:41, 2018

Martín Abadi, Bruno Blanchet, and Cédric Fournet. The applied pi calculus: Mobile values, new names, and secure communication.Journal of the ACM, 65(1):1:1–1:41, 2018

2018
[3]

Reconciling two views of cryptography (the computa- tional and the formal)

Martín Abadi and Phillip Rogaway. Reconciling two views of cryptography (the computa- tional and the formal). InInternational Conference on Formal Methods in Computer-Aided Design, pages 3–22. Springer, 2002

2002
[4]

Standard model leakage-resilient authen- ticated key exchange using inner-product extractors

Janaka Alawatugoda and Tatsuaki Okamoto. Standard model leakage-resilient authen- ticated key exchange using inner-product extractors. Cryptology ePrint Archive, Paper 2021/861, 2021

2021
[5]

Verifying constant-time implementations

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. Verifying constant-time implementations. In25th USENIX Security Symposium (USENIX Security 16), pages 53–70, Austin, TX, 2016. USENIX Association. 23

2016
[6]

A general composition theorem forsecurereactivesystems

Michael Backes, Birgit Pfitzmann, and Michael Waidner. A general composition theorem forsecurereactivesystems. InTheory of Cryptography Conference, pages336–354.Springer, 2006

2006
[7]

McMillan, Kedar S

David Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, and Lenore D. Zuck. It takes a village: Bridging the gaps between current and formal specifications for protocols.Communications of the ACM, 68(8):50–61, 2025

2025
[8]

Basin and Cas J

David A. Basin and Cas J. F. Cremers. Degrees of security: Protocol guarantees in the face of compromising adversaries. InComputer Science Logic (CSL), volume 6247 ofLecture Notes in Computer Science, pages 1–18, Berlin, Heidelberg, 2010. Springer

2010
[9]

A computationally sound mechanized prover for security protocols

Bruno Blanchet. A computationally sound mechanized prover for security protocols. In Proceedings of the 2006 IEEE Symposium on Security and Privacy, SP ’06, page 140–154, USA, 2006. IEEE Computer Society

2006
[10]

Security protocol verification: Symbolic and computational models

Bruno Blanchet. Security protocol verification: Symbolic and computational models. In Principles of Security and Trust (POST), volume 7215 ofLecture Notes in Computer Sci- ence, pages 3–29, Berlin, Heidelberg, 2012. Springer

2012
[11]

Modeling and verifying security protocols with the applied pi calculus and ProVerif.Foundations and Trends in Privacy and Security, 1(1–2):1–135, 2016

Bruno Blanchet. Modeling and verifying security protocols with the applied pi calculus and ProVerif.Foundations and Trends in Privacy and Security, 1(1–2):1–135, 2016

2016
[12]

A logic of authentication.ACM Trans

Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication.ACM Trans. Comput. Syst., 8(1):18–36, February 1990

1990
[13]

The scyther tool: Verification, falsification, and analysis of security protocols

Cas Cremers. The scyther tool: Verification, falsification, and analysis of security protocols. InComputer Aided Verification (CAV), volume 5123 ofLecture Notes in Computer Science, pages 414–418, Berlin, Heidelberg, 2008. Springer

2008
[14]

Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level

Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level. In2020 IEEE Symposium on Security and Privacy (SP), pages 1021–1038, 2020

2020
[15]

David L. Dill. The murphi verification system. InComputer Aided Verification (CAV), volume 1102 ofLecture Notes in Computer Science, pages 390–393, Berlin, Heidelberg,
[16]

Danny Dolev and Andrew C. Yao. On the security of public key protocols.IEEE Trans- actions on Information Theory, 29(2):198–208, 1983

1983
[17]

Academic Press, New York, 1980

Didier Dubois and Henri Prade.Fuzzy Sets and Systems: Theory and Applications, volume 144 ofMathematics in Science and Engineering. Academic Press, New York, 1980

1980
[18]

Springer Berlin Heidelberg, Berlin, Heidelberg, 2009

Santiago Escobar, Catherine Meadows, and José Meseguer.Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, pages 1–50. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009

2009
[19]

Maude-NPA: Cryptographic protocol analysis modulo equational properties

Santiago Escobar, Catherine Meadows, and José Meseguer. Maude-NPA: Cryptographic protocol analysis modulo equational properties. InFoundations of Security Analysis and Design V, volume 5705 ofLecture Notes in Computer Science, pages 1–50. Springer, Berlin, Heidelberg, 2009

2009
[20]

R. V. L. Hartley. Transmission of information.Bell System Technical Journal, 7(3):535– 563, 1928. 24

1928
[21]

A model checking technique for the verification of fuzzy control systems

Benedetto Intrigila, Daniele Magazzeni, Ilaria Melatti, Andrea Tofani, and Enrico Tronci. A model checking technique for the verification of fuzzy control systems. InIEEE Inter- national Conference on Computational Intelligence for Measurement Systems and Appli- cations (CIMSA), pages 92–97, 2005

2005
[22]

Norris Ip and David L

C. Norris Ip and David L. Dill. Better verification through symmetry.Formal Methods in System Design, 9(1-2):41–75, 1996

1996
[23]

Prentice Hall, Upper Saddle River, NJ, 1995

GeorgeJ.KlirandBoYuan.Fuzzy Sets and Fuzzy Logic: Theory and Applications. Prentice Hall, Upper Saddle River, NJ, 1995

1995
[24]

Paul C. Kocher. Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. InAdvances in Cryptology – CRYPTO ’96, volume 1109 ofLecture Notes in Computer Science, pages 104–113. Springer, 1996

1996
[25]

Addison-Wesley, Boston, MA, 2002

Leslie Lamport.Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston, MA, 2002

2002
[26]

Reducingfuzzyrelationequations via concept lattices.Fuzzy Sets and Systems, 463:108465, 2023

DavidLobo, VíctorLópez-Marchante, andJesúsMedina. Reducingfuzzyrelationequations via concept lattices.Fuzzy Sets and Systems, 463:108465, 2023

2023
[27]

Pasquale Malacaria, M. H. R. Khouzani, Corina S. Pasareanu, Quoc-Sang Phan, and Kasper Søe Luckow. Symbolic side-channel analysis for probabilistic programs. In2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 313–327, 2018

2018
[28]

The Tamarin prover for the symbolic analysis of security protocols

Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. The Tamarin prover for the symbolic analysis of security protocols. InComputer Aided Verification (CAV), volume 8044 ofLecture Notes in Computer Science, pages 696–701, Berlin, Heidelberg,
[29]

Mitchell, M

J.C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using mur/spl phi/. InProceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097), pages 141–151, 1997

1997
[30]

Needham and Michael D

Roger M. Needham and Michael D. Schroeder. Using encryption for authentication in large networks of computers.Communications of the ACM, 21(12):993–999, 1978

1978
[31]

Efficient and timely mutual authentication.ACM SIGOPS Operating Systems Review, 21(1):8–10, 1987

David Otway and Omer Rees. Efficient and timely mutual authentication.ACM SIGOPS Operating Systems Review, 21(1):8–10, 1987

1987
[32]

Gibson-Robinson Thomas, Armstrong Philip, Boulgakov Alexandre, and A.W. Roscoe. FDR3 — A Modern Refinement Checker for CSP. In Erika Ábrahám and Klaus Havelund, editors,Tools and Algorithms for the Construction and Analysis of Systems, volume 8413 ofLecture Notes in Computer Science, pages 187–201, 2014

2014
[33]

Restructuring lattice theory: An approach based on hierarchies of concepts

Rudolf Wille. Restructuring lattice theory: An approach based on hierarchies of concepts. In Ivan Rival, editor,Ordered Sets, pages 445–470. Springer, Dordrecht, 1982

1982
[34]

Thomas Y. C. Woo and Simon S. Lam. Authentication for distributed systems.Computer, 25(1):39–52, January 1992

1992
[35]

Lotfi A. Zadeh. Fuzzy sets.Information and Control, 8(3):338–353, 1965. 25

1965