Graded Symbolic Verification with a Fuzzy Dolev-Yao Attacker Model Murat Moran April 20, 2026
arXiv:2604.15402v1 [cs.CR] 16 Apr 2026
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 µK ∈ [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 thresholddriven 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.
1
Introduction
The Dolev–Yao (DY) model [16] is a standard basis for symbolic protocol verification under perfect cryptography. Its attacker knowledge semantics are binary (known/unknown). However, in side-channel settings, observations are partial, noisy, and cumulative. This mismatch can hide attack paths that emerge only after multiple weak observations. A canonical historical example is Kocher’s timing attack line, which showed that repeated timing measurements can leak private-key information in RSA implementations [24]. The method in this paper extends symbolic analysis with a graded attacker view. Highassurance tools such as FDR-based checkers [32], ProVerif [11], Maude-NPA [18], and Murphi [15] are effective for crisp derivability, but they do not natively model incremental knowledgequality updates inside the attacker state. The Fuzzy Dolev-Yao (FuzzyDY) extension addresses this by replacing binary possession with a knowledge map µ : M → [0, 1], lifting deduction via Zadeh’s Extension Principle [35], and applying T-norm-based leak updates. This graded view is needed for three attack classes that crisp DY cannot represent directly. Cumulative sub-threshold observations capture multi-step evidence accumulation, where no single observation is sufficient, but the sequence is. Near-threshold attack transitions capture safe-to-fail behaviour after a small additional observation update. Ranked attack feasibility enables comparing attack paths by required knowledge quality rather than treating all partial knowledge as one unknown state. These attack classes are captured by our graded semantics and examined empirically.
1.1
Motivation and Aim
The primary motivation for this work is the rigorous capture of safe-to-fail transitions under incremental side-channel leakage. In the classical binary DY model, an attacker’s knowledge state is discrete, which masks threshold-driven vulnerabilities. By shifting to a graded symbolic framework, we expose three classes of attack dynamics that are not represented in binary explicit-state enumeration: 1
1. Cumulative sub-threshold observations: Multiple noisy observations may individually be insufficient to compromise a key, but under repeated fuzzy intersection, their cumulative evidence enables a protocol break. 2. Near-threshold safe-to-fail transitions: A protocol execution may switch from safe to unsafe following a minor observation that pushes the adversary’s epistemic certainty across an actionable threshold. 3. Ranked attack feasibility: Rather than collapsing all partial knowledge into a single "unknown" state, attack traces can be quantitatively ranked by the required quality of the adversary’s α-cut support. Crucially, our novelty boundary is not the rediscovery of classic algebraic flaws (e.g., the unfixed Needham-Schroeder impersonation attack). Instead, we show that a protocol verified as safe under binary DY semantics (such as fixed Needham–Schroeder–Lowe) can become vulnerable when graded side-channel evidence accumulates across steps. This paper is organised around the following three research questions: 1. Semantics: Can symbolic attacker knowledge be modelled as a graded state that accumulates side-channel observations while remaining consistent with crisp DY behaviour at binary endpoints? 2. Security Outcomes: Does this framework expose authentication/confidentiality threshold crossings that are not visible in binary runs of the same protocol logic? 3. Scalability: Can the concept-lattice [26] reduce fuzzy relation equations and state dimensionality while preserving encoded invariant outcomes?
1.2
Contributions and Scope
This paper contributes a graded extension of the classical DY adversary model for cumulative side-channel observations. Standard symbolic deduction is lifted with Zadeh’s Extension Principle and sequential updates are modelled with T-norms, producing a quantitative evolution law for adversary-view quality [35, 23]. For tractability in explicit-state checking, we integrate exact concept-lattice reduction to prune mathematically redundant state variables while preserving encoded verdicts. The article is realised through four contributions: (i) a graded symbolic semantics for attacker knowledge in which each term carries a degree of possession, (ii) graded confidentiality and authentication invariants under a fuzzy intruder model, (iii) a modified explicit-state Murphi workflow with finite-precision reals and a reusable fuzzy C++ core (including Product Tnorm accumulation and α-cut interval propagation), and (iv) executed validation on NSL (safe and leaky variants) and symmetric-key families (NSSK, Yahalom, Otway–Rees, Woo–Lam), including observed authentication boundary crossings. The remainder of this paper is organised as follows: Section 2 presents a comparison of our method against symbolic and computational methods on side-channel verification. Section 3 defines threat assumptions and the scope of the model. Section 4 presents preliminaries on fuzzy arithmetic, the formal model and security invariants. Section 5 presents operational semantics and formal guarantees. Section 6 presents explicit-state NSL concretisation, implementation boundaries, and state-space reduction mechanisms. Section 7 reports executed case studies. Section 8 discusses limits. Section 9 concludes and outlines future extensions, with reproducibility details in the appendices.
2
Related Work
Navigating the boundary between symbolic and computational verification requires distinguishing both the nature of the modelled uncertainty and the target security properties [3, 10]. Com2
putational formal methods, such as CryptoVerif, operate by computing aleatory uncertainty: the probabilistic chance of a polynomial-time adversary breaking a cryptographic primitive, validated via sequences of games [9]. While these tools provide rigorous computational soundness guarantees, they do not natively model the gradual accumulation of side-channel evidence within a discrete state-machine exploration. Modern symbolic tools (e.g., ProVerif [11], Tamarin [28], Scyther [13], FDR [32], and MaudeNPA [19]) are highly effective for crisp derivability and observational equivalence, but they model attacker knowledge as binary (derivable/non-derivable). Our framework stays within symbolic transition semantics under idealised cryptography and replaces the binary possession flag with a continuous knowledge map µK : M → [0, 1]. The result is an epistemic uncertainty process over attacker knowledge quality under repeated side-channel observations, obtained by lifting classical Dolev–Yao deduction with Zadeh’s Extension Principle [35]. The relation to Degrees of Security [8] is conceptual. Degrees of Security varies attacker capability classes (e.g., compromise classes), whereas this work varies accumulated observation quality within the same protocol run. This also complements compositional security lines by adding quantitative leakage-state semantics to a bounded symbolic setting [6]. More recent work on protocol engineering also emphasises a broader semantic divide between operational specifications and formal models [7]. The gap addressed in this paper is not reachability itself, but knowledge-quality evolution under repeated side-channel observations. Side-channel formal methods at lower abstraction layers include constant-time and relational non-interference analyses for implementations/binaries [5, 14], as well as quantitative symbolic leakage analysis for probabilistic programmes [27]. Leakage-resilient models in computational cryptography [4] address bounded leakage with game-based assumptions. For Murphi-based verification, early protocol analyses [29] evaluated NSL/NSPK in a binary setting. In contrast, this article evaluates protocol-level symbolic models, such as including NSL, with a graded attacker view, and shows pass/fail divergence between crisp and graded runs under accumulated side-channel observations.
3
Threat Model and Assumptions
This section defines network assumptions, attacker capabilities, leakage setting, and the model boundaries used by the formalisation in Section 4 and the explicit-state semantics in Section 5.
3.1
Network and Adversary Capabilities
We assume the standard Dolev–Yao network adversary: the attacker controls the channel and can intercept, block, replay, reorder, and inject messages [16]. Operationally, the adversary is encoded as an active protocol principal with interception and message-synthesis rules over current knowledge, matching the Murphi security-protocol modelling style introduced by Mitchell et al. [29]. We also retain the perfect-cryptography premise: cryptographic primitives are not broken algebraically unless the required keys or terms are already derivable in the symbolic model. Thus, attacks arise from protocol logic and leakage-enabled knowledge evolution, not from direct cryptanalytic breaks of idealised primitives. Historically, Murphi-based analysis has also been used to relax strict black-box assumptions and encode additional algebraic attacker effects when needed [29]. In this paper, we preserve the symbolic cryptographic abstraction but enrich attacker knowledge semantics with graded side-channel evidence accumulation.
3
3.2
The Side-Channel Leakage Model
The physical threat model targets shared compute deployments (cloud VMs, containerised services, edge devices), where timing, cache, and power effects can reveal partial information about secrets. In this setting, side-channel signal quality is typically noisy and incremental. Accordingly, we model observations as cumulative evidence: repeated measurements progressively refine the attacker candidate set for key-related terms. The main risk is a delayed threshold crossing, where individually weak measurements eventually reduce uncertainty enough to enable a symbolic protocol break.
3.3
Operational Assumptions and Scope
All claims are interpreted under the following explicit assumptions: • Bounded symbolic universe and finite discretization: Protocol sessions, agent instances, and the term algebra are strictly bounded to obtain finite-state transition systems. Fuzzy memberships are discretized and stored with finite precision (e.g., real(4,2)). • Abstraction preservation: The framework evaluates finite-state protocol models under an abstraction level, rather than full wire-format implementations. We intentionally abstract away non-critical message details that are not required to decide the encoded invariants. • Soundness and approximation risks: Because explicit-state abstractions are used, the model carries inherent approximation risks. If an omitted field contributes to a real attack precondition, the abstraction represents an under-approximation. Conversely, if replay/forgery abstractions are too permissive, discovered traces may not be deployment feasible attacks (over-approximation). To mitigate these risks, we conditionally bind our claims to explicit invariants and the provided over-approximation premise in Theorem 5.14.
4
Formalising the Fuzzy Dolev-Yao Model
The model extends classical Dolev–Yao by replacing binary attacker possession with graded adversary view over a finite symbolic universe. It captures epistemic uncertainty in attacker inference from protocol traffic and side-channel evidence while preserving finite-state executability through discretization and bounded sessions. Here, we first give preliminaries on fuzzy sets and arithmetic.
4.1
Preliminaries on Fuzzy Sets and Arithmetic
To formalise the gradual degradation of an adversary’s epistemic state, our framework relies on foundational concepts from fuzzy set theory and fuzzy arithmetic. We briefly review the relevant definitions and operators used throughout this paper. Fuzzy Sets and Fuzzy Numbers. Let U be a classical set of objects, termed the universe of discourse. A fuzzy set A in U is characterised by a membership function µA : U → [0, 1], where µA (x) represents the grade of membership of the element x in A. The closer the value of µA (x) is to 1, the more x belongs to A. A fuzzy number is a specific type of fuzzy set defined on the real line R that satisfies two additional constraints: it must be normalised (i.e., there exists at least one x such that µA (x) = 1) and it must be convex. In this work, fuzzy numbers are utilised to quantify the attacker’s continuous epistemic uncertainty regarding specific cryptographic terms. Fuzzy Set Operations and T-norms. Standard fuzzy set operations generalise classical crisp set logic. The standard intersection (which models logical conjunction) and standard union (which models logical disjunction) of two fuzzy sets A and B are defined pointwise us-
4
ing the min and max operators, respectively: µA∩B (x) = min(µA (x), µB (x)) and µA∪B (x) = max(µA (x), µB (x)). To model the accumulation of independent side-channel observations, we require a generalised conjunction operator. In fuzzy logic, generalised intersections are formulated via Triangular Norms (T-norms). A T-norm is a binary operation T that is commutative, associative, monotonic, and has 1 as an identity element. While min is the standard idempotent T-norm (Tmin ), our framework defaults to the Product T-norm (TΠ ), defined as: TΠ (a, b) = a · b,
µt+1 (M ) = D TΠ µt (M ), µL (M )
,
where D is a conservative discretization operator and leak L. In the context of iterative operations, D acts as a cell-to-cell mapping, projecting the continuous results of T-norm intersections back onto the finite grid G prior to state storage. This models the conjunction of prior adversary view and the new side-channel evidence. The Product T-norm is strictly monotonic and models the multiplicative contraction of probability-like membership mass, producing sharper candidate elimination under repeated observations. Zadeh’s Extension Principle and Sup-Min Composition. The extension principle [35] is a fundamental mechanism that allows classical mathematical functions to be extended to operate on fuzzy domains. Given a function f : X1 × · · · × Xn → Y and fuzzy sets A1 , . . . , An defined over X1 , . . . , Xn , the extension principle maps these sets to a fuzzy set B on Y via the sup-min composition: µB (y) =
sup
x1 ,...,xn y=f (x1 ,...,xn )
min µA1 (x1 ), . . . , µAn (xn )
(1)
where sup is the least upper bound over all decompositions yielding y. This is the sup-min mechanism used in graded deduction. If the inverse image f −1 (y) is empty, µB (y) = 0. In our execution model, the extension principle provides the rigorous mathematical basis for lifting the discrete Dolev-Yao term constructors into the fuzzy domain, enabling continuous arithmetic computations on cryptographic message derivations. α-Cuts and Threshold Semantics. To bridge the continuous fuzzy domain and binary verification verdicts, we use the concept of α-cuts. For a given threshold α ∈ (0, 1], the α-cut (or α-level set) of a fuzzy set A is the crisp set Aα = {x ∈ U | µA (x) ≥ α}. We employ α-cuts as strict operational boundaries (αthreshold ) to evaluate safe-to-fail transitions: an attack term is considered practically deducible by the adversary only when its fuzzy membership degree breaches the threshold, shrinking the continuous support down to a critical vulnerability bound.
4.2
Term Algebra and Syntax
To evaluate protocol security, we model messages as abstract terms generated by a term algebra M as in [2]. Let Σ be a signature consisting of a finite set of cryptographic function symbols, each with a specific arity. Given a set of atomic names A and a set of variables X , the universe of terms M is defined inductively by the following grammar: M, N ∈ M ::= a | x | f (M1 , . . . , Mk ) a, b, c, k ∈ A ::= k (Symmetric keys) | N (Nonces) | skA (Secret keys) | pkA (Public keys) x, y, z ∈ X ::= variables f ∈ Σ ::= senc | sdec | penc | pdec | sign | verify We denote the set of ground terms as MG ⊆ M and follow the standard notation in symbolic verification. 5
• {M }k denotes symmetric shared-key encryption, senc(M, k). • {M }pkA denotes asymmetric public-key encryption, penc(M, pkA ). • {M }skA denotes a digital signature, sign(M, skA ). In the verifier implementation, this abstract algebra is modelled as finite typed Murphi message records (e.g., source, dest, key, mType) so terms can be enumerated in explicit state space, consistent with the original Murphi protocol-analysis methodology [29].
4.3
Equational Theory and Crisp Deduction
The term algebra is quotiented by an equational theory = under perfect cryptography. The signature Σ is governed by cancellation equalities sdec(senc(M, k), k) = M , pdec(penc(M, pkA ), skA ) = M , and verify(sign(M, skA ), pkA ) = true. No other equalities exist, so adversary derivations cannot exploit unintended algebraic structures. We formalise the adversary’s computational capabilities via a deduction relation ⊢⊆ P(M)× M. Let S ⊆ M denote the set of terms currently possessed by the attacker. The statement S ⊢ M means that the attacker can derive the term M from S. The relation is the smallest set closed under the following inference rules: (Axiom)
(Composition)
(Decomposition)
M ∈S S⊢M
S⊢M1 S⊢M2 S⊢(M1 ,M2 )
S⊢(M1 ,M2 ) S⊢Mi (i∈{1,2})
(Symmetric Encryption)
(Symmetric Decryption)
(Equivalence)
S⊢M S⊢k S⊢senc(M,k)
S⊢senc(M,k) S⊢M
S⊢k
S⊢M
Σ⊢M =M ′ S⊢M ′
(Public-Key Encryption) (Public-Key Decryption) S⊢M S⊢pkA S⊢penc(M,pkA )
4.4
S⊢penc(M,pkA ) S⊢M
S⊢skA
The Graded Adversary Model and Epistemic Uncertainty
Classical Dolev–Yao can be viewed as a crisp knowledge algebra where the attacker’s possession (characteristic function over the knowledge set K) χK is Boolean: χK : M → {0, 1}. The graded model generalises this into a knowledge map µK : M → [0, 1], where µK (M ) encodes degree of possession of term M . This framing targets epistemic uncertainty (vagueness/imprecision in the adversary view) rather than aleatory uncertainty (randomness of events). In the executable Murphi model, attacker exposure is represented directly by global state variables (network slots, intruder buffers, and derivable-term flags). The graded map µK is interpreted over this explicit knowledge state at each reachable node. The transition relation is no longer just set expansion by the updated knowledge set K’, K ⊆ K ′ ; it becomes a graded evolution operator over [0, 1]-valued knowledge states. We denote this graded transition relation simply as →F . Operationally, →F is parametrised by the rule lifting mechanics (Zadeh’s Extension Principle), the discretization policy D, and the observation-combination operator T (T-norm). The modified Murphi engine executes this concrete semantics over the explicit state space. Intuitively, "degree of possession" represents an adversary confidence interval induced by noisy physical side-channel signals. For example, a side-channel trace may reduce an AESlike key search space from 2128 to approximately 250 candidates; the model captures this as a reduction in the fuzzy entropy of the key symbol and can trigger a violation once the remaining uncertainty drops below a modelled brute-force threshold.
6
4.4.1
Dimensions of Leakage
Following the compromise-dimension mindset in symbolic protocol analysis [8], we model sidechannel evidence along three explicit axes: (i) whose data is exposed (e.g., initiator vs. responder knowledge variables), (ii) what secret class is exposed (long-term keys, session keys, nonces, or derived terms), and (iii) what quality the attacker gains (membership degree and support narrowing in µK ). This provides a structured adversary description beyond a single binary reveal capability. 4.4.2
Accumulation Operator
Leakage accumulation is the graded counterpart of one-shot reveal actions. In this work we use Product T-norm (T (a, b) = a · b) with discretization after each update, so repeated observations progressively refine candidate sets and support safe-to-fail threshold analysis. The full update law is stated in Section 4.6.
4.5
Graded Deduction via Zadeh’s Extension Principle
Let µK : M → [0, 1] be the attacker knowledge map and f a constructor/destructor over symbolic terms. We lift crisp derivation by Zadeh’s Extension Principle: µf (A1 ,...,An ) (y) =
sup
min µA1 (x1 ), . . . , µAn (xn ) .
y=f (x1 ,...,xn )
Classical DY deduction rules are lifted to the fuzzy domain by applying conjunction through a T-norm (instantiated here via the standard min operator for conservative structural deduction). Let µS : M → [0, 1] be the abstract fuzzy knowledge state of the adversary. We formalise the graded deduction relation, denoted µS ⊢µ M = v, to express that a term M is derivable from state µS to a membership degree of v. The graded deduction system is the smallest relation closed under the following inference rules: (Axiom)
µS ⊢µ M = µS (M )
(Comp.)
µS ⊢µ M1 = v1 µS ⊢µ M2 = v2 µS ⊢µ (M1 , M2 ) = min(v1 , v2 )
(Decomp.)
µS ⊢µ (M1 , M2 ) = v µS ⊢µ Mi = v
(Sym-Enc)
µS ⊢µ M = v1 µS ⊢µ k = v2 µS ⊢µ senc(M, k) = min(v1 , v2 )
(Sym-Dec)
µS ⊢µ senc(M, k) = v1 µS ⊢µ k = v2 µS ⊢µ M = min(v1 , v2 )
7
(i ∈ {1, 2})
(Pub-Enc)
µS ⊢µ M = v1 µS ⊢µ pkA = v2 µS ⊢µ penc(M, pkA ) = min(v1 , v2 )
(Pub-Dec)
µS ⊢µ penc(M, pkA ) = v1 µS ⊢µ skA = v2 µS ⊢µ M = min(v1 , v2 )
(Equiv.)
µS ⊢µ M = v Σ ⊢ M = M ′ µS ⊢µ M ′ = v
These lifted rules rigorously define knowledge evolution from partial initial information. Operationally, during explicit-state exploration in the execution boundary, this generic premise map µS is instantiated by the concrete attacker knowledge variable µK at each reachable state q ∈ Q.
4.6
Leak Accumulation via T-Norm Dynamics
In binary DY models, attacker knowledge typically evolves purely by closure under crisp derivation rules. In our graded model, side-channel evidence accumulation is formalised as epistemic uncertainty reduction through fuzzy intersection. Let µKt (M ) denote the attacker’s knowledge quality of term M at step t, and let µLt (M ) denote the fractional value of a new side-channel observation. The state evolution is governed by the recursive law: µKt+1 (M ) = D(T (µKt (M ), µLt (M )))
(2)
where T is the specified T-norm (the Product T-norm TΠ by default in this article) and D is the finite discretization operator defined in Section4.1. 1 By applying TΠ , repeated observations iteratively contract the membership mass, yielding progressively sharper candidate elimination. To formally quantify the epistemic degradation of the adversary’s knowledge, we evaluate the Hartley non-specificity over the discretized state. Let Wα = |πα (µK )| denote the cardinality of the effective support of the α-cut projection of the fuzzy attacker knowledge. The Hartley nonspecificity at step t is defined as Ht = log2 |Suppαt |. Because the Product T-norm enforces strict monotonicity under repeated observations, the support Suppαt is non-increasing, guaranteeing that Ht monotonically decreases as side-channel evidence accumulates. Consequently, a 50% reduction in the support width Wα directly implies a 1-bit drop in the Hartley entropy: Wα′ = 1 ′ 2 Wα =⇒ H = H − 1.
4.7
Graded Security Invariants
To rigorously evaluate protocol security under the proposed semantics, classical binary invariants are lifted to graded forms over µK . We define both confidentiality and authentication conditions below. 4.7.1
Formal Definition of Graded Confidentiality (Secrecy)
In addition to authentication, we evaluate syntactic secrecy over our term algebra M. Let Msec ∈ M represent a target sensitive term generated during a protocol session between honest principals A, B ∈ Aagent . For instance, in the NSL case, the critical confidentiality target is the responder’s freshly generated nonce, Msec = Nb . In the classical binary DY model, the confidentiality invariant Φcrisp holds if the attacker sec cannot derive the target term from observed knowledge: Φcrisp sec (q) ≜ Kcrisp ̸⊢ Msec 1
The Min T-norm, Tmin , is preferable when conservative intersection behaviour is desired to avoid aggressive attenuation from multiple weak observations.
8
as:
Under graded analysis, binary possession is replaced by µK . We define graded confidentiality uzzy (q) ≜ µK (Msec ) < αthreshold Φfsec
4.7.2
Formal Definition of Graded Authentication
Authentication is defined as a correspondence property between protocol participant states over M. Let Aagent ⊂ A be the set of atomic names representing protocol participants (e.g., A, B). Define: • Commit(q, B, A, M ): Denotes that in state q, responder B has completed the protocol run, believing it has securely communicated with initiator A, agreeing on a specific payload term M ∈ M. • Running(q, A, B, M ): Denotes that in state q, initiator A has actively initiated a protocol run with B using the exact same term M ∈ M. In the classical binary DY model, the crisp authentication invariant Φcrisp auth is defined as a strict correspondence assertion: Φcrisp auth (q) ≜ ∀A, B ∈ Aagent , ∀M ∈ M : Commit(q, B, A, M ) =⇒ Running(q, A, B, M ). If Φcrisp auth (q) holds, the crisp attacker cannot deduce the required challenge response Mf orge ∈ M from their current knowledge base at state q to trick the responder into committing (i.e., Kq ̸⊢ Mf orge ). Under the graded analysis framework, we evaluate the Graded Authentication invariant, uzzy , over the same correspondence logic. However, its truth valuation within the explicitΦfauth state execution boundary is now determined by the epistemic knowledge map µK . A safe-to-fail uzzy transition occurs—resulting in ¬Φfauth (q)—if there exists a reachable state where Commit(q, B, A, M ) evaluates to true while Running(q, A, B, M ) evaluates to false. This violation is triggered precisely when the graded attacker accumulates enough side-channel evidence such that the membership degree of the required forged term crosses the actionable threshold: µKq (Mf orge ) ≥ αthreshold allowing the intruder to syntactically satisfy the responder’s cryptographic checks without the initiator’s true participation.
4.8
Threshold-Driven Violation Semantics
Because classical DY reasoning is restricted to the binary domain χK : M → {0, 1}, any safe-tofail transition requires a discrete, full-term derivation. Under our graded extension, reachability is governed by the continuous evolution of µK , enabling the formalisation of threshold-driven violation semantics. Let qt ∈ QF uzzyDY be the concrete state at step t, and let Φf uzzy be a graded security invariant evaluated at the operational threshold αthreshold . The graded framework formally exposes the following violation dynamics: • Cumulative Sub-Threshold Reachability: Let Mf orge ∈ M be a critical payload required to violate Φf uzzy . There exist trace sequences q0 →F · · · →F qt →F · · · →F qt+k such that at step t, µKt (Mf orge ) ≪ αthreshold (the invariant holds), but after k iterative side-channel updates via the T-norm accumulation operator, µKt+k (Mf orge ) = 9
D(T (µKt , µL1..k )) ≥ αthreshold . The crisp Tα projection—a bounding classical transition system that restricts Boolean Dolev-Yao derivations strictly to the α-level cut set of the fuzzy knowledge map—cannot capture this delayed satisfiability because no single discrete step i ∈ {1 . . . k} yields a full derivation. • Near-Threshold State Transitions: The framework captures stuttering control-state transitions that alter only the epistemic knowledge map. A transition qt →F qt+1 may execute no new protocol logic, but solely apply an observation update µLt such that the Hartley non-specificity drops (Ht+1 < Ht ), pushing the state immediately across the safety boundary ¬Φf uzzy (qt+1 ). • Graded Trace Ranking: For a set of violating runs leading to states Qviol ⊂ QF uzzyDY where ¬Φf uzzy holds, the explicit-state enumeration evaluates the terminal knowledge map µK at each violating node. This allows attack paths to be strictly ordered by the epistemic quality of the adversary’s view (e.g., maximizing µK (Msec ) or minimizing the α-cut support width Wtα ), a distinction inherently collapsed by binary verification models. These theoretical semantics are concretely instantiated in Section VI, where staged leakage uzzy uzzy boundaries in our explicit-state Murphi executions. updates trigger ¬Φfauth and ¬Φfsec
5
Operational Semantics and Explicit-State Verification
Executing the abstract continuous deduction framework within a finite verification engine requires strict operational bounds. This section formalises the explicit-state enumeration architecture and the finite-discretisation semantics necessary to compute the graded transition system TF uzzyDY .
5.1
Explicit-State Enumeration Rationale
Explicit-state enumeration is a verification technique that explores the global reachability graph by generating and storing each reachable state individually [15, 25]. Unlike symbolic approaches that reason over logic-defined state sets, explicit enumeration evaluates concrete values of state variables at each transition step. Mitchell et al. demonstrated that this bounded explicit-state style is effective for security protocols in Murphi [29]. This approach is necessary for graded analysis in this work because fuzzy updates are arithmetic on concrete state vectors: T-norm accumulation, α-cut/support computations, and entropy/Hartley calculations are executed directly on the current state before successor generation.
5.2
Operational Semantics: The Explicit-State Transition System
Definition 5.1 (Crisp DY Transition System). A crisp symbolic protocol model or transition system is a tuple TDY = (QDY , Q0 , →, Φ) (3) where each state q = (tr, K, th) contains trace tr, attacker knowledge K ⊆ M, and honestthread state th. The term algebra M is finite under bounded sessions. The transition relation → is induced by protocol actions and symbolic derivation rules (composition, decomposition, encryption/decryption), and Φ is a Boolean security predicate (e.g., authentication correspondence) [16, 15, 29]. Following Murphi’s explicit-state formulation, protocol execution is modelled as a finite guarded-command state machine A = (Q, Q0 , ∆), 10
where Q is the finite set of global states (assignments to all model variables), Q0 ⊆ Q is the set of initial states, and ∆ is the set of guarded rules. Each rule has a Boolean guard and an atomic action; if the guard is true in state q ∈ Q, the rule can fire to produce successor q ′ . Concurrency is asynchronous interleaving of enabled rules, including attacker rules for intercept, derive, leak-update, and inject actions [15, 29]. Definition 5.2 (FuzzyDY Transition System). The graded extension is formalised as the tuple: TF uzzyDY = (QF uzzyDY , QF,0 , →F , D, T, L)
(4)
where each concrete state q ∈ QF uzzyDY includes a fuzzy attacker knowledge map µKq : M → [0, 1]. For leakage-tracking variables, µKq is interpreted as a possibility distribution over candidates (representing knowledge quality), rather than a monotone DY term-inventory flag. The discretizer D : [0, 1] → {0, δ, 2δ, . . . , 1} is monotone and satisfies D(0) = 0 and D(1) = 1. The operator T is the chosen T-norm (e.g., TΠ ), and L is the set of possible side-channel leakage observation maps [35, 23]. For a cryptographic constructor f , graded structural derivation at a given state q follows the extension-principle form: !
µKq (z) = D
sup min(µKq (x), µKq (y))
(5)
z=f (x,y)
When the system executes a leakage transition q →F q ′ under an observation µL ∈ L, the epistemic update is modelled by the T-norm intersection:
µKq′ (M ) = D T µKq (M ), µL (M )
(6)
Definition 5.3 (α-cut Projection). For α ∈ (0, 1], define πα (µK ) = {M ∈ M | µK (M ) ≥ α} The projected crisp system Tα executes derivations over πα (µK ) using transitions compatible with this projection [35, 23].
5.3
Formal Guarantees and Proofs
Theorem 5.4 (Crisp Functional Equivalence (Deduction Fragment)). In the absence of fractional leakage (i.e., ∀M ∈ M, µK (M ) ∈ {0, 1}), the Graded Deduction relation ⊢µ is exactly equivalent to the classical DY deduction relation ⊢. Proof. Let Kcrisp = {M ∈ M | µK (M ) = 1} be the crisp attacker knowledge extracted from the current concrete state q. We must prove that Kcrisp ⊢ M ⇐⇒ µK (M ) = 1. ( =⇒ direction): We proceed by structural induction on the depth of the crisp derivation tree for Kcrisp ⊢ M . • Base case (Axiom): If M is derived via the Axiom rule, M ∈ Kcrisp . By definition, µK (M ) = 1. • Inductive step (Symmetric Encryption/Decryption): For senc, the premises Kcrisp ⊢ M ′ and Kcrisp ⊢ k imply µK (M ′ ) = µK (k) = 1, hence µK (senc(M ′ , k)) = min(1, 1) = 1 For sdec, the premises Kcrisp ⊢ senc(M, k) and Kcrisp ⊢ k imply µK (M ) = min(1, 1) = 1. 11
• Inductive step (Public-Key Encryption/Decryption): For penc, the premises Kcrisp ⊢ M ′ and Kcrisp ⊢ pkA imply µK (penc(M ′ , pkA )) = min(1, 1) = 1 For pdec, the premises Kcrisp ⊢ penc(M, pkA ) and Kcrisp ⊢ skA imply µK (M ) = min(1, 1) = 1. • Composition and Decomposition follow identically via the min operator. ( ⇐= direction): We proceed by structural induction on derivations of M in the guardedrule transition system. Because µK (M ) can evaluate to 1 only when M is in the initial attacker knowledge or produced by the sup-min operator with all premises at 1, each such step corresponds to a valid crisp rule application in ⊢. Hence any term with µK (M ) = 1 is strictly derivable in the crisp model. Theorem 5.5 (Monotone Knowledge-Quality Evolution). Under the Product T-norm T (a, b) = a · b, finite discretization D, and any fixed threshold α ∈ (0, 1], the effective attacker support Suppαt = {M ∈ M | µt (M ) ≥ α} is non-increasing under leakage updates. Consequently, Hartley non-specificity Ht = log2 |Suppαt | is monotonically non-increasing [23, 20, 17]. Proof. For any term M , µt+1 (M ) = D(µt (M ) · µL (M )), with µL (M ) ∈ [0, 1]. The key step follows standard T-norm axioms: monotonicity and boundary (T (a, 1) = a). Because µL (M ) ≤ 1, monotonicity gives T (µt (M ), µL (M )) ≤ T (µt (M ), 1) = µt (M ) For Product specifically, T (a, b) = a · b, so the inequality is immediate and is strict whenever 0 < a < 1 and 0 ≤ b < 1 [23, 17]. Monotonicity of D yields µt+1 (M ) ≤ D(µt (M )), and because state values are already discretised, D(µt (M )) = µt (M ). Hence µt+1 (M ) ≤ µt (M ). If x ∈ Suppαt+1 , then µt+1 (x) ≥ α, so µt (x) ≥ α, thus x ∈ Suppαt . Therefore Suppαt+1 ⊆ Suppαt , implying Suppαt+1 ≤ |Suppαt |. Since log2 (·) is monotone, Ht+1 ≤ Ht . Remark 5.6. Conceptually, the monotonic descent of the Hartley non-specificity (Ht+1 ≤ Ht ) mathematically guarantees that repeated side-channel observations strictly degrade the adversary’s epistemic uncertainty. This assures that the accumulation of graded evidence irreversibly drives the execution state toward the vulnerability threshold, accurately mirroring the candidateelimination dynamics of real-world physical cryptanalysis. Theorem 5.7 (Termination of Graded Verification). For bounded protocol sessions and a finite discretization grid G = {0, δ, 2δ, . . . , 1}, the graded verification algorithm terminates in finite time [15]. Proof. Let QDY denote the reachable state space of the bounded crisp model; under bounded sessions, QDY is finite. In the graded system, each relevant attacker-knowledge component is annotated by a membership value in [0, 1], and each transition applies fuzzy arithmetic followed by discretization D : [0, 1] → G. Equivalently, execution uses a finite cell-to-cell mapping over [0, 1]: each continuous update is projected back into one of finitely many cells before storage. Hence, every stored membership value lies in finite set G, where |G| = ⌊1/δ⌋ + 1. 12
Let NK be the maximum size of the attacker knowledge base, bounded by the finite term algebra M generated by the bounded sessions and roles (hence NK ≤ |M|). Then the graded state space embeds into QF uzzyDY ⊆ QDY × GNK (7) Because the underlying protocol control states are finite (bounded by QDY ), and the graded knowledge maps to a strictly finite grid, the resulting reachable graded state space QF uzzyDY is strictly bounded [15]. Explicit-state exploration over this finite bounded space QF uzzyDY therefore guarantees termination in finite time. Remark 5.8 (Bounded Exhaustiveness and Precision). General verification of cryptographic protocols is undecidable for unbounded sessions [10]. Under the bounded-session and finitediscretization assumptions in this paper, the method provides bounded exhaustiveness: the explicitstate Murphi backend explores the complete finite reachability graph induced by the model, which is strictly bounded by the finite state space QF uzzyDY . Consequently, within this bounded abstraction, reported violations are concrete reachable executions (protocol steps plus fuzzy leak updates), not purely symbolic artifacts; this is evidenced by the executed failing traces in Table 2. Proposition 5.9 (Hartley Threshold Semantics). Let Wtα = |πα (µKt )|, i.e., the cardinality of the effective α-cut support of fuzzy attacker knowledge at execution step t. A 50% reduction in support width across t → t + 1 implies exactly a 1-bit Hartley drop [20]: Ht = log2 Wtα ,
1 α Wt+1 = Wtα =⇒ Ht+1 = Ht − 1 2
Definition 5.10 (Fuzzy Relation Equations (FRE) / Concept-Lattice Context). To systematically identify and prune redundant state variables, protocol dependencies are encoded as a Fuzzy Relation Equation (FRE) formal context (U, V, R, λ). Here, the set of objects U represents the transition constraints and rules (including the target invariant Φ), the set of attributes V represents the explicit protocol state variables, and the fuzzy incidence relation R : U × V → [0, 1] encodes the mathematical dependency strength between constraints and variables [33]. By representing the protocol state space as a formal context, we can systematically identify the minimum subset of state variables required to preserve the system’s execution semantics. In concept lattice theory, this bounding mechanism is formalised as an exact attribute reduct (E-reduct) [26]. Definition 5.11 (Exact Attribute Reduct (E-reduct)). By representing the protocol state space as a formal context, we can systematically identify the minimum subset of state variables required to preserve the system’s execution semantics. In concept lattice theory, this bounding mechanism is formalised as an E-reduct [26]. Given an encoded formal context (U, V, R, λ), a subset of state variables V ′ ⊆ V is an E-consistent set if the concept lattice induced by the reduced context (U, V ′ , RV ′ , λV ′ ) is extentisomorphic (E-isomorphic) to the concept lattice of the original full context. An E-reduct is defined as a strictly minimal E-consistent set; that is, for any variable v ∈ V ′ , the further removal of v breaks the E-isomorphism. Operationally, an E-reduct isolates the minimal state dimensionality required to perfectly preserve the distinguishability of the protocol’s transition constraints. Because the lattice extents (which group the constraints U ) remain structurally identical, we can safely prune the redundant variables V \ V ′ without altering the truth valuation of the encoded security invariants. Remark 5.12 (Scope of Verification Guarantees). Guarantees in this paper hold under explicitstate symbolic assumptions: (i) bounded sessions and finite term algebra, (ii) finite discretization and real(m,n) precision, and (iii) exploration of the induced finite abstraction. The framework 13
quantifies epistemic knowledge quality within the symbolic model; it does not imply computational indistinguishability guarantees (e.g., indistinguishability under chosen-plaintext attack, INDCPA) against probabilistic polynomial-time adversaries. In particular, this lane differs from equivalence-based symbolic analyses and game-based computational proofs: the approach verifies bounded symbolic reachability with graded leakage semantics, rather than proving full equivalence properties or negligible attack probability in unbounded probabilistic settings [10, 9]. Lemma 5.13 (α-Cut Monotonicity of Fuzzy Deduction). Let DedFuzzyDY be one-step fuzzy deduction under the graded rules (composition, decomposition, encryption and decryption), and let DedDY be one-step crisp deduction on sets of terms. Fix α ∈ (0, 1]. Assume D is monotone and α-compatible (x ≥ α ⇒ D(x) ≥ α). Then πα (DedFuzzyDY (µK )) ⊇ DedDY (πα (µK )) Proof. Take any t ∈ DedDY (πα (µK )). By structural induction on the crisp rule instance deriving t from the current attacker knowledge state, there exists a premise set P ⊆ πα (µK ) with µK (p) ≥ α for all p ∈ P . By Zadeh’s Extension Principle, constructor lifting in the graded model has the form ! µnew (t) = D
sup min µK (p) ,
t=f (P ) p∈P
with rule-specific simplifications (e.g., decomposition as copy). Since minp∈P µK (p) ≥ α, the pre-discretization value is at least α. By α-compatibility, D(x) ≥ α whenever x ≥ α. Hence µnew (t) ≥ α, i.e., t ∈ πα (DedFuzzyDY (µK )). Theorem 5.14 (Conditional Projection Soundness). Let Tα be the α-projected crisp system and TF uzzyDY the fuzzy system. Assume: 1. Initial-state embedding: for every crisp initial state q0 , there exists a fuzzy initial state qF,0 with Kq0 ⊆ πα (µqF,0 ); 2. Step-wise simulation premise: each crisp protocol step has a corresponding fuzzy step over the same control action; 3. Deduction monotonicity: from Lemma 5.13; 4. Leakage-step compatibility: if Tα includes projected leakage transitions, each crisp leakage step q → q ′ has a corresponding fuzzy leak step qF →F qF′ such that Kq′ ⊆ πα (µqF′ ). (For standard DY projections with no explicit leakage transitions, this premise is vacuous.) Then for every crisp transition q → q ′ in Tα , there exists a fuzzy transition qF →F qF′ such that Kq ⊆ πα (µqF ) and Kq′ ⊆ πα (µqF′ ). Consequently, every crisp run in Tα is simulated by a graded-model run, and if the graded model is safe at threshold α, then Tα is safe. Proof. Define the simulation relation Rα (q, qF ) ⇐⇒ Kq ⊆ πα (µqF ) and the protocol-control components of q and qF are aligned. Base case. By Assumption 1, every crisp initial state has a related fuzzy initial state, so Rα (q0 , qF,0 ) holds. Step case. Assume Rα (q, qF ) and a crisp transition q → q ′ . • Case A (protocol control): by Assumption 2, qF →F qF′ exists with aligned control components, so the relation is preserved. • Case B (attacker deduction): apply Lemma 5.13, πα (DedFuzzyDY (µqF )) ⊇ DedDY (πα (µqF )), guaranteeing that every newly derived crisp term at level α is strictly subsumed by the projected fuzzy successor. 14
• Case C (projected leakage step, if present): by Assumption 4, there is a matching fuzzy leak step with Kq′ ⊆ πα (µqF′ ). For the standard projected crisp system with no explicit leakage transition, this is a stuttering refinement step (q ′ = q): crisp knowledge is unchanged while the fuzzy state sharpens (µqF →F µqF′ ). Hence Rα (q ′ , qF′ ) holds in all transition cases. By induction on run length, each crisp run has a simulating fuzzy run. So any crisp violation would be represented in the graded model. Contrapositively, if no graded violation exists at threshold α, no violation exists in Tα . Corollary 5.15 (Cut-Soundness). If the graded framework MF uzzyDY satisfies invariant Φ at threshold α, then no classical crisp attacker restricted to the projected knowledge base πα (µK ) can violate Φ. Proof. Immediate from Theorem 5.14: each projected crisp run is simulated by a graded-model run, so the absence of graded violations implies the absolute absence of projected crisp violations. Proposition 5.16 (Conditional Reduct Preservation). Let protocol dependencies be encoded as a multi-adjoint formal context (U, V, R, λ), where U contains transition constraints (including the target invariant Φ) and V contains state attributes. Let V ′ ⊆ V be an E-reduct of this encoded context. Eq. 8 defines state equivalence by projection strictly on the reduct attributes: q1 ∼V ′ q2 ⇐⇒ ∀v ∈ V ′ , q1 (v) = q2 (v)
(8)
Under this projection equivalence ∼V ′ , verification verdicts for Φ are strictly preserved after pruning the redundant attributes V \ V ′ . Specifically, safety (or violation reachability) evaluated over the full model is exactly equivalent to safety (or violation reachability) in the reduced quotient model. This conditional preservation claim follows the E-reduct FRE reduction results of Lobo et al. [26], with the framework by Wille [33] as the underlying lattice-theoretic basis. Proof. Because V ′ is an E-reduct, the reduced and full contexts preserve the same discernibility structure of objects (constraints), equivalently captured by concept-lattice isomorphism in the reduction framework. Thus removed attributes V \V ′ are redundant for distinguishing constraint behaviour in the encoded context. For FRE-based encoding, this is the operational content of exact reduction: restricting to V ′ preserves the solution structure relevant to U . Therefore, for each invariant-related object uΦ ∈ U , its truth valuation is determined by the V ′ -projection class. Consequently, if q1 ∼V ′ q2 , their invariant evaluations are mathematically identical (Φ(q1 ) = Φ(q2 )) within the encoded abstraction, guaranteeing strict preservation of the verification verdict. Theorem 5.17 (Leakage-Tolerance Separation (Existence by Counter-Example)). The graded framework MF uzzyDY yields a strictly finer security classification than standard binary Dolev– Yao MDY : there exists a protocol model P , safety invariant Φ, and leakage configuration leak (α, σleak ) such that MDY (P ) |= Φ and Mα,σ F uzzyDY (P ) ̸|= Φ. Equivalently, there exists a finite guarded-rule firing sequence r0 , . . . , rk ∈ ∆ from an initial state q0 ∈ Q0 to a reachable violating state qk with ¬Φ(qk ) in the graded model, while no such violating sequence exists in the crisp model for the same P . Proof. Let Tα be the α-projected classical system and TF uzzyDY be the graded transition system for a fixed protocol logic P . The proof proceeds by concrete existential witness. As empirically demonstrated by the Needham–Schroeder–Lowe (NSL) analysis in Section VII, there exists a reachable trace in the graded explicit-state execution, denoted strictly as the state sequence qF,0 →F qF,1 →F · · · →F qF,k . During this sequence, repeated side-channel observations recursively fuse via the Product T-norm, monotonically shrinking the leakage variance (σleak ) 15
and driving the Hartley non-specificity down (see Table 2 for the trace). At the terminal state qF,k , the accumulated epistemic certainty successfully crosses the αthreshold boundary, yielding a safe-to-fail transition ¬Φf uzzy (qF,k ). Conversely, an exhaustive state-space exploration of the classical projection Tα yields no reachable state satisfying ¬Φcrisp . Because the underlying protocol logic P remains strictly identical and only the adversary semantics differ, this pass/fail divergence serves as an exact model-separation witness. It formally guarantees that TF uzzyDY ̸|= Φf uzzy while Tα |= Φcrisp , proving that accumulated epistemic leakage constitutes a distinct reachability axis that is uncapturable by classical binary Dolev–Yao classification.
6
Implementation Architecture and State-Space Reduction
6.1
Explicit-State Modelling of NSL and the Graded Intruder
We separate Abstract Term Algebra from Explicit-State Concretisation. Conceptually, cryptographic constructors such as senc and penc are defined over M. Operationally, explicit-state Murphi execution requires a finite data-structure representation: abstract terms are concretised as typed message records (e.g., mType, key, payload fields), and cryptographic constraints are enforced by guarded commands [29, 15]. Because Murphi enumerates concrete global states, the symbolic/equational view is realised as follows. • Data-structure representation: constructors are mapped to typed record forms distinguished by mType and associated key/payload slots. • Operational execution: cancellation constraints (e.g., Σ ⊢ sdec(senc(M, k), k) = M ) are implemented as guarded commands that fire only when matching key conditions hold. To validate our framework, we concretise the NSL protocol and the Fuzzy Dolev-Yao adversary using the explicit-state enumeration methodology established by Mitchell et al. [29]. 6.1.1
Protocol Concretisation
To ensure a finite state space, the abstract term algebra M is mapped to finite Murphi data structures. Messages are encoded as a single typed record with fields source, dest, key, mType, and two bounded payload slots (nonce1, nonce2); principals are modelled by bounded interchangeable identifiers amenable to symmetry reduction. Honest principals are encoded as local role-state machines (e.g., I_SLEEP, I_WAIT, I_COMMIT) with guarded transitions that enforce cryptographic checks before state advancement, providing the operational counterpart of the abstract deduction/equational layer in Section 4. 6.1.2
The Graded Intruder
Consistent with Section 3, the adversary is implemented as an asynchronous network process with full channel control. In the baseline Murphi style, intruder rules handle interception, storage, and message injection. Our extension adds leakage-accumulation rules that apply the Product T-norm updates to the discretised knowledge state (µK ), tightening membership over target terms such as Nb . Therefore, forgery rules that depend on Nb remain disabled until repeated leak updates push uncertainty below αthreshold .
6.2
Implementation and Execution Boundary
The main text keeps semantics and proofs, while execution-heavy implementation details are summarized here and expanded in Appendix A.1. The implementation uses a modified Murphi 3.1 with finite real(m,n) precision and external C/C++ fuzzy operations [15, 21]; the external 16
layer computes Gaussian fuzzy numbers, the Product T-norm intersection, alpha-cut support metrics, and entropy values over a finite discretization grid (101 levels on [0, 1], clamped) with key-domain mapping on [0, 255]. Leak detection is based on alpha-cut support-width reduction (Hartley-style 1-bit event at 50% support reduction), and executed precision sweeps (real(4,2) vs real(4,4)) preserve the same authentication-failure verdict in the fixed leaky NSL run. These settings define the bounded execution environment used in Section 7. Operationally, entropy and Hartley calculations are executed directly on the concrete state vector before the generation of a successor state. The external C++ layer computes the α-cut support metrics continuously. To bridge the continuous entropy evaluation with the discrete transition system, leak detection is implemented via an α-cut support-width reduction trigger. Specifically, a Hartley-style 1-bit event is registered in the state machine whenever the external layer detects a 50% reduction in the support cardinality at α = 0.5.
6.3
The State-Space Reduction System
To mitigate explicit-state growth, verification is performed on quotient spaces that preserve invariant outcomes. First, we use Murphi’s native symmetry reduction: agent/nonces declared as scalarset-like interchangeable identities induce state permutations that are graph automorphisms, so only one canonical representative per equivalence class is explored [15, 22, 29]. Second, we apply exact concept-lattice reducts over the formal context (U, V, R, λ). If V ′ ⊆ V is an E-reduct, we map the explicit state space into the quotient space induced by the projection equivalence ∼V ′ established in Eq. (8). Under the encoded invariant class, pruning the redundant attributes V \ V ′ and verifying strictly over this quotient space preserves encoded verdicts while significantly reducing state dimensionality (as formally guaranteed by Proposition 5.16)).
7
Validation and Case Studies
To validate our graded verification framework, we evaluate the Needham–Schroeder–Lowe (NSL) public-key protocol [29]. The protocol aims to establish mutual authentication and the symmetric exchange of fresh secrets between an initiator A and a responder B over an insecure network. The core execution logic is defined by the following three message exchanges: A → B : {Na , A}pkB
(9)
B → A : {Na , Nb , B}pkA
(10)
A → B : {Nb }pkB
(11)
Here, Na and Nb represent freshly generated nonces, and {M }pk denotes asymmetric public-key encryption under the recipient’s public key [29]. Eq. (10) incorporates Lowe’s critical fix—the inclusion of the responder’s identity B inside the ciphertext—which formally guarantees that the classical Dolev–Yao intruder cannot successfully mount a man-in-the-middle impersonation attack. To execute this abstraction within our modified Murphi backend, the term algebra M is mapped to finite, typed data structures, and the communication steps are encoded as asynchronous guarded commands [29]. We strictly bound the symbolic universe by limiting the network capacity and using symmetry reduction (via interchangeability of agent identifiers [22]) to mitigate state-space explosion prior to concept-lattice pruning. Within this explicit-state architecture, the classical DY intruder is encoded as an active network process. We extend this baseline by embedding our continuous epistemic tracking— specifically, the knowledge map µK and its associated Gaussian variance σleak —directly into the
17
intruder’s local state. This enables physical side-channel observations over the encrypted payloads (e.g., {Nb }pkB ) to monotonically accumulate, ultimately triggering safe-to-fail boundaries without requiring the algebraic compromise of the underlying cryptographic primitives. We now present E-reduct computation, automated verification of Needham–Schroeder–Lowe (NSL) for confidentiality and authentication, and notes on the framework’s generalisation.
7.1
Exact Reduct Computation
To systematically evaluate the state-space optimization, we extracted the formal context (U, V, R, λ) directly from the unreduced, full-state NSL specification. We then applied our concept-lattice reduction algorithm to this protocol-labeled dependency matrix. The encoded incidence matrix R comprises |U | = 10 objects (representing the security-relevant transition rules and target invariants) mapped against |V | = 17 explicit state attributes. The computational reduction successfully identified 61 distinct exact attribute reducts (Ereducts). By evaluating the intersection of these reducts, the algorithm isolates the core, indispensable state variables (e.g., init_responder and net.address) while systematically flagging strictly redundant attributes. As guaranteed by Proposition 2, these redundant attributes can be safely pruned from the state vector prior to compilation, mapping the explicit state space into a lower-dimensional quotient space without altering the encoded verification verdicts. Within the FRE/formal-context encoding, attributes represent protocol/state variables and objects represent equations/constraints. The reduct therefore captures the minimal variable subset preserving the discernibility of the encoded constraints [26, 33]. We then pruned the redundant attributes in the NSL model and measured the effect. E-reducts mitigate dimensional state explosion while preserving verdicts for the encoded invariant class. In this NSL case, pruning it yields a median explored-state reduction of 55.27%, consistent with Proposition 5.16. Table 1 shows the normalised explored-state reduction. Naming note: nsl_safe* denotes the full-context/pruned reduct-benchmark variants, while ns_fuzzy_* denotes property-specific NSL verification variants used in the next sections.
Table 1: Executed Pruning vs. Full-Context Tradeoff (3 Runs, Median Reported) Model
States
Rules
Runtime (s)
State Range
nsl_safe_fullctx nsl_safe
13067693 5845349
14446084 5885853
2.34 0.54
12.98M–13.07M 4.83M–5.93M
7.2
Evaluating Graded Authentication (NSL)
Correctness conditions are encoded as Murphi invariants, consistent with the NS/NSL verification style used in early Murphi protocol research [29]. We verified NSL safe and leaky variants using Murphi3.1. The crisp-safe baseline (ns_fuzzy_auth_safe) explores 127, 742 states and reports no error, formally establishing that the classical transition system satisfies the crisp authentication invariant, TDY |= Φcrisp auth . Under the strictly identical honest protocol logic, the uzzy leaky variant (ns_fuzzy_auth) yields a safe-to-fail transition (TF uzzyDY ̸|= Φfauth ) once accumulated side-channel observations enable the intruder’s epistemic uncertainty to drop below the actionable threshold, allowing the deterministic forgery of the critical payload {N b}Kb . Table 2 provides the concrete witness for the safe-to-fail transition. It highlights coarse and fine leak updates, uncertainty reduction (σleak = 4.96 in the failing run), activation of the intruder-forge rule, and the final authentication violation.
18
Table 2: Executed NSL Leaky Attack Trace (Condensed) Step
Rule Fired
Leak Phase
σleak
Resp. State
1 2 3 4 5 6 7 8 9
Leak (coarse) Leak (fine) Initiator start (step 3) Intruder intercept Intruder replay to responder Responder nonce reaction (3/6) Intruder intercept Intruder forge {Nb}Kb Responder nonce check (7)
coarse-done fine-done fine-done fine-done fine-done fine-done fine-done fine-done fine-done
37.95 4.96 4.96 4.96 4.96 4.96 4.96 4.96 4.96
sleep sleep sleep sleep sleep wait wait wait commit
7.3
Evaluating Graded Confidentiality (NSL)
We execute confidentiality as a dedicated NSL pair (ns_fuzzy_conf_safe, ns_fuzzy_conf) using the invariant "Nb remains confidential from intruder" encoded in Appendix A. In the crisp baseline, the invariant holds. In the leaky variant, the verifier reports a direct confidentiality violation after staged coarse/fine observations and the subsequent responder message interception. Table 3: NSL Confidentiality Results from Executed Local Runs Model
Variant
Result
States / Rules
conf_safe conf_leaky
Fixed NSL, no leak Fixed NSL + leak rules
No error found Invariant failed (Nb confidentiality)
120359 / 122055 133 / 132
In the violating state, intr_known_nonce[B] = true immediately after the intruder intercepts responder message 6 ({Na , Nb , B}Ka ) with leak-evidence-enabled key knowledge, so confidentiality is lost before the later authentication-forgery step. Interpreted via Hartley nonspecificity, this run gives a concrete leakage-budget crossing for Nb : repeated sub-threshold observations drive uncertainty below the modelled secrecy boundary.
7.4
Generalisation Across Protocol Topologies
To test whether the observed threshold behaviour is specific to NSL, we evaluated a class of server-mediated symmetric-key authentication abstractions. We implemented models for Needham–Schroeder Symmetric Key (NSSK) [30] (see Table 4), and similarly for Yahalom [12], Otway-Rees [31], and Woo-Lam [34]. In this template-equivalent family, crisp baseline variants verify as safe, while leaky variants trigger invariant violations after cumulative observations cross the operational threshold. Full execution results, complexity profiles, and failing traces for NSSK are provided in Appendix B.2.
8
Discussion and Limitations
While the integration of concept-lattice E-reducts successfully mitigates dimensionality for the encoded invariants, our framework is subject to the universal bounds inherent to finite-state abstraction. We identify the following primary limitations: • Scalability and State-Space Explosion: The transition from a binary characteristic function to a graded epistemic knowledge map inherently exacerbates the state-space 19
explosion problem. Discretizing fuzzy membership values introduces massive new state dimensions into the reachability graph. Although our application of concept-lattice Ereducts achieves a critical 55.27% reduction in explored states for the NSL protocol by pruning redundant matrices, it mitigates rather than eliminates the exponential growth inherent to explicit-state model checking. Consequently, scaling this precise methodology to highly complex, multi-party industrial protocols remains a computational challenge. • Construct Validity of Leakage Parameterisation: The assignment of initial fuzzy membership values, Gaussian variance (σleak ), and the actionable vulnerability boundary (αthreshold ) currently relies on expert-driven parameterisation. While the Product Tnorm accurately models the multiplicative contraction of uncertainty, transitioning this framework to real-world physical side-channel deployments may require dynamic, tracederived parameterisation extracted directly from hardware execution logs. • Property Scope: The formal guarantees presented in this paper are bounded to explicitstate symbolic assumptions (finite discretization and bounded sessions). Our current prototype semantics and validation restrict focus strictly to syntactic secrecy and tracebased authentication reachability invariants. Verifying broader indistinguishability properties (e.g., computational IND-CPA against probabilistic polynomial-time adversaries) or process-equivalence privacy claims falls outside the scope of this continuous-state symbolic capability.
9
Conclusion and Future Work
This paper introduced a graded extension of the Dolev–Yao model for side-channel-aware symbolic verification. The method augments binary abstraction with an epistemic adversary-view representation and is executed in a modified Murphi workflow. The central result is a leakagethreshold boundary: protocols that pass under crisp DY can fail once cumulative observations are enabled. In the NSL case, staged observations reduce candidate uncertainty and activate attack traces not present in the corresponding binary run. We also showed that state growth from graded semantics can be mitigated through conceptlattice E-reducts, with a 55% explored-state reduction on NSL while preserving encoded invariant verdicts. Across tested configurations, discretisation and precision sweeps produced stable verdicts for both authentication and confidentiality. Future work will expand the verification scope beyond strict safety and correspondence assertions to encompass quantitative privacy analysis. This theoretical extension requires formalising a graded observational equivalence relation (≈f uzzy ) as a continuous analogue to classical labelled bisimilarity (≈l ), thereby enabling entropy-based unlinkability metrics over the adversary’s epistemic view. Empirically, the framework will be scaled to evaluate the 5G Authentication and Key Agreement (5G-AKA) protocol [1]. Applying the E-reduct explicit-state workflow to the 5G-AKA abstraction will allow us to systematically characterise state-space scalability and measure protocol-specific leakage-tolerance boundaries under progressive, power-analysisstyle physical observations.
A
Model Specification
A.1
Execution Boundary Configuration
Compiler and type support. The verifier uses a local modified Murphi 3.1 toolchain, based on the original Murphi line [15]. The compiler supports finite-precision real(m,n) handling and external C/C++ linkage for fuzzy operations, following the extension pattern used in prior
20
fuzzy-control model-checking adaptations [21]. Executed models use real(4,2) and real(4,4) variants. External fuzzy-logic boundary. Complex fuzzy operations are implemented in C++ and invoked from Murphi through external declarations. The external layer implements Gaussian fuzzy-number representation, the Product T-norm intersection, discrete entropy and alpha-cut support computations, and approximate fuzzy-encrypt uncertainty propagation [23, 35]. Discretization and leak metric. Membership degrees are discretised to 101 levels on [0, 1] with clamping; key-domain values are mapped to [0, 255]. This is a cell-to-cell mapping abstraction where each continuous update is projected to a finite cell before successor generation. Leak tracking uses entropy trend and support shrinkage at α = 0.5, with Hartley interpretation H = log2 |A| [20, 17]. Precision robustness. The Product T-norm updates use closed-form Gaussian-product parameter fusion followed by parameter quantisation (instead of repeated pointwise multiplication on discretised samples). Executed precision sweeps (real(4,2) vs real(4,4)) preserve the same fixed-leaky NSL authentication-failure verdict and explored-state counts.
A.2
Exact Murphi Invariants Used in Executed Models
A.2.1
Public-Key Needham–Schroeder Authentication Model
invariant "responder correctly authenticated" forall i: InitiatorId do init_state = I_COMMIT & init_responder = B -> resp_initiator = i & (resp_state = R_WAIT | resp_state = R_COMMIT) end; invariant "initiator correctly authenticated" forall r: ResponderId do resp_state = R_COMMIT & resp_initiator = A -> init_state = I_COMMIT & init_responder = r end; invariant "one-bit flag implies at least one leak step" leakOneBit -> leakPhase != LP_NONE; A.2.2
Public-Key Needham–Schroeder Confidentiality Model
invariant "responder correctly authenticated" forall i: InitiatorId do init_state = I_COMMIT & init_responder = B -> resp_initiator = i & (resp_state = R_WAIT | resp_state = R_COMMIT) end;
21
invariant "initiator correctly authenticated" forall r: ResponderId do resp_state = R_COMMIT & resp_initiator = A -> init_state = I_COMMIT & init_responder = r end; invariant "Nb remains confidential from intruder" !intr_known_nonce[B]; invariant "one-bit flag implies at least one leak step" leakOneBit -> leakPhase != LP_NONE; A.2.3
Symmetric-Key Families
invariant "responder authenticated initiator" forall i: InitiatorId do b_state = RB_COMMIT -> a_state = IA_COMMIT & a_partner = B & b_initiator = i end; invariant "initiator commits only for responder B" forall r: ResponderId do a_state = IA_COMMIT -> a_partner = r end; invariant "one-bit flag implies at least one leak" leakOneBit -> leakPhase != LP_NONE;
B
Extended Results: Symmetric-Key Families
B.1
Executed Symmetric-Key Results Table 4: Executed NSSK Results Result
Model
Variant
nssk_safe nssk_leaky
Baseline (no leak rules) Side-channel leak + accumulation
B.2
Symmetric-Key Failing Traces
B.2.1
NSSK Leaky Model Full Trace
1 2 3 4
No error found Invariant failed (auth.)
intruder side-channel leak (coarse session-key reading) intruder side-channel leak (fine session-key reading) A starts NSSK request to server intruder intercepts 22
States / Rules 36 / 35 1404 / 1403
5 6 7 8 9 10 11 12 13 14 15
intruder replays recorded message to server Server responds with package to initiator intruder intercepts intruder replays recorded message to initiator Initiator processes server package and sends ticket intruder intercepts intruder replays recorded message to responder Responder processes ticket and sends challenge intruder intercepts intruder forges challenge response after leakage Responder verifies challenge response
B.2.2
Additional Family Leaky Traces (Pattern Equivalence)
The executed leaky traces for Yahalom, Otway-Rees, and Woo-Lam are template-equivalent to the NSSK trace above under the current abstraction: each follows the same 15-step control pattern (coarse leak, fine leak, request/relay exchanges, then leakage-enabled forged challenge response and responder commit). Differences are limited to family labels and leak-parameter constants, so repeated full rule listings are omitted.
C
Supplemental Derivations
C.1
Worked Alpha-Cut Interval Propagation Example
Consider a scenario where the α = 0.5 cut of a targeted nonce interval evaluates to [38.23, 61.77]. For a monotone constructor f (x) = x + 10, interval propagation gives [48.23, 71.77]. Following conservative integer-grid discretization via ⌊·⌋ and ⌈·⌉, this maps to the finite cell [4, 5], yielding a discrete support cardinality of 25. The resulting Hartley non-specificity is calculated as H = log2 (25) ≈ 4.64 bits. As the execution progresses and the intruder accumulates further leak observations, the system dynamically monitors this discrete entropy. A discrete "leak event" rule fires exclusively when repeated sub-threshold observations drive the uncertainty down, causing |Supp0.5 | to drop by 50% (representing a 1-bit reduction in H).
References [1] 3GPP. 5g; security architecture and procedures for 5g system. Technical report, 2019. [2] 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. [3] Martín Abadi and Phillip Rogaway. Reconciling two views of cryptography (the computational and the formal). In International Conference on Formal Methods in Computer-Aided Design, pages 3–22. Springer, 2002. [4] Janaka Alawatugoda and Tatsuaki Okamoto. Standard model leakage-resilient authenticated key exchange using inner-product extractors. Cryptology ePrint Archive, Paper 2021/861, 2021. [5] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. Verifying constant-time implementations. In 25th USENIX Security Symposium (USENIX Security 16), pages 53–70, Austin, TX, 2016. USENIX Association.
23
[6] Michael Backes, Birgit Pfitzmann, and Michael Waidner. A general composition theorem for secure reactive systems. In Theory of Cryptography Conference, pages 336–354. Springer, 2006. [7] 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. [8] David A. Basin and Cas J. F. Cremers. Degrees of security: Protocol guarantees in the face of compromising adversaries. In Computer Science Logic (CSL), volume 6247 of Lecture Notes in Computer Science, pages 1–18, Berlin, Heidelberg, 2010. Springer. [9] 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. [10] Bruno Blanchet. Security protocol verification: Symbolic and computational models. In Principles of Security and Trust (POST), volume 7215 of Lecture Notes in Computer Science, pages 3–29, Berlin, Heidelberg, 2012. Springer. [11] 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. [12] Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. ACM Trans. Comput. Syst., 8(1):18–36, February 1990. [13] Cas Cremers. The scyther tool: Verification, falsification, and analysis of security protocols. In Computer Aided Verification (CAV), volume 5123 of Lecture Notes in Computer Science, pages 414–418, Berlin, Heidelberg, 2008. Springer. [14] Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1021–1038, 2020. [15] David L. Dill. The murphi verification system. In Computer Aided Verification (CAV), volume 1102 of Lecture Notes in Computer Science, pages 390–393, Berlin, Heidelberg, 1996. Springer. [16] Danny Dolev and Andrew C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983. [17] Didier Dubois and Henri Prade. Fuzzy Sets and Systems: Theory and Applications, volume 144 of Mathematics in Science and Engineering. Academic Press, New York, 1980. [18] Santiago Escobar, Catherine Meadows, and José Meseguer. Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, pages 1–50. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. [19] Santiago Escobar, Catherine Meadows, and José Meseguer. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Foundations of Security Analysis and Design V, volume 5705 of Lecture Notes in Computer Science, pages 1–50. Springer, Berlin, Heidelberg, 2009. [20] R. V. L. Hartley. Transmission of information. Bell System Technical Journal, 7(3):535– 563, 1928. 24
[21] Benedetto Intrigila, Daniele Magazzeni, Ilaria Melatti, Andrea Tofani, and Enrico Tronci. A model checking technique for the verification of fuzzy control systems. In IEEE International Conference on Computational Intelligence for Measurement Systems and Applications (CIMSA), pages 92–97, 2005. [22] C. Norris Ip and David L. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1-2):41–75, 1996. [23] George J. Klir and Bo Yuan. Fuzzy Sets and Fuzzy Logic: Theory and Applications. Prentice Hall, Upper Saddle River, NJ, 1995. [24] Paul C. Kocher. Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. In Advances in Cryptology – CRYPTO ’96, volume 1109 of Lecture Notes in Computer Science, pages 104–113. Springer, 1996. [25] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston, MA, 2002. [26] David Lobo, Víctor López-Marchante, and Jesús Medina. Reducing fuzzy relation equations via concept lattices. Fuzzy Sets and Systems, 463:108465, 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. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 313–327, 2018. [28] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. The Tamarin prover for the symbolic analysis of security protocols. In Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pages 696–701, Berlin, Heidelberg, 2013. Springer. [29] J.C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using mur/spl phi/. In Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097), pages 141–151, 1997. [30] 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. [31] David Otway and Omer Rees. Efficient and timely mutual authentication. ACM SIGOPS Operating Systems Review, 21(1):8–10, 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 of Lecture Notes in Computer Science, pages 187–201, 2014. [33] Rudolf Wille. Restructuring lattice theory: An approach based on hierarchies of concepts. In Ivan Rival, editor, Ordered Sets, pages 445–470. Springer, Dordrecht, 1982. [34] Thomas Y. C. Woo and Simon S. Lam. Authentication for distributed systems. Computer, 25(1):39–52, January 1992. [35] Lotfi A. Zadeh. Fuzzy sets. Information and Control, 8(3):338–353, 1965.
25