Formal Verification of the Kali Invariant — ProVerif Models and Security Properties — ACSE Research Series

Abstract

Formal verification provides assurance that testing cannot: a mathematical proof that a security property holds for all possible executions of a protocol, not just the executions a tester thought to try. This paper presents three ProVerif models for ASMP/1.0 and the security properties verified against each.

All three models were verified. ZK authentication property: TRUE. Cascade authentication property: TRUE. MSG-005 TEE-binding properties: CORRECT across all queries.

Patent Notice

ASMP/1.0 and the verified security properties are covered by Indian Patent Published · IN202641070690 · 19/06/2026.

1. Why Formal Verification

1.1 The Limits of Testing

A test suite — however comprehensive — can only test the executions it covers. An adversary is not constrained to scenarios a test suite covers. A protocol with a logical flaw may pass all tests in normal operation and fail only under a specific adversary message sequence that no tester anticipated.

1.2 What ProVerif Provides

ProVerif models the protocol as Horn clauses and uses resolution to determine whether a stated security property can be violated by any adversary in the Dolev-Yao model — the adversary controls the entire network: it can read, block, replay, modify, and inject any message.

Scope of Formal Verification

The ProVerif models verify the PROTOCOL — the abstract specification of message exchanges and cryptographic operations. They do not verify the Rust implementation. Implementation correctness is addressed by the 683-test suite. Formal verification and implementation testing are complementary — neither is sufficient alone.

Figure 1: The Three-Pillar Evidence Triangle — Formal Verification · Empirical Testing · Performance Evidence

2. Cryptographic Assumptions

All three models assume: SHA3-256 is a perfect random oracle (collision resistance, preimage resistance); HMAC-SHA3-256 is a secure MAC; TEE attestation quotes are unforgeable without TEE hardware access. These assumptions are consistent with NIST assessments of SHA3-256.

Figure 2: Three ProVerif Models — Component, Query, and Result for each

3. Model 1 — MSG-002 ZK Authentication

The model represents Initiator, Responder, and a Dolev-Yao adversary controlling the network. The ally_channel_fp is modelled as private — not derivable from network observations.

(* ZK property — adversary cannot obtain ally_channel_fp *)
query attacker(ally_channel_fp_at_epoch_N).

(* Authentication — adversary cannot produce valid RESPONSE *)
query attacker(valid_response_epoch_N1).

Model 1 Result: ZK PROPERTY = TRUE

An adversary who observes all four MSG-002 messages cannot compute ally_channel_fp or produce a valid proof for any subsequent epoch. ASMP peer authentication cannot be impersonated by an adversary who observes any number of authentication exchanges.

4. Model 2 — MSG-004 Cascade Authentication

The model represents an origin node (threat detector) and receiving peers. The adversary may attempt to forge a Defensive Leap or prevent legitimate ones from being accepted.

(* Forgery resistance *)
query attacker(forged_leap_accepted_by_peer).

(* Legitimate leap always accepted by honest peers *)
query event(peerAcceptedLeap) ==> event(originBroadcastLeap).

Model 2 Result: CASCADE AUTHENTICATION = TRUE

Only a node with both the origin's current surface fingerprint AND a valid HMAC key can produce a Defensive Leap accepted by peers. An adversary cannot forge or replay a Defensive Leap.

5. Model 3 — MSG-005 TEE Management

(* TEE binding — trust_token requires TEE hardware access *)
query attacker(trust_token_without_tee).

(* Epoch scoping — token from epoch N rejected in epoch N+1 *)
query attacker(trust_token_epoch_N_accepted_in_N1).

(* Legitimate operator always gets valid token after TEE verification *)
query event(managementAccepted) ==> event(teeVerified).

Model 3 Result: ALL QUERIES CORRECT

trust_token requires a verifiable TEE attestation quote. Tokens are epoch-scoped: a token valid at epoch N is structurally rejected at N+1. This closes the attack vector used in Stryker-Handala — valid admin credentials are necessary but not sufficient.

6. Aggregate Security Claims

Property	Basis	Strength
ZK peer authentication	Model 1, ProVerif	Proven — all executions, Dolev-Yao adversary
Cascade authentication	Model 2, ProVerif	Proven — all executions, Dolev-Yao adversary
TEE-bound management	Model 3, ProVerif	Proven — all executions, Dolev-Yao adversary
Fingerprint unlinkability	Red team (WP-05)	Empirical: L=0.181 < 0.500 random floor
Kali Invariant (per-cycle)	683-test suite	Enforced on every mutation cycle
Audit chain integrity	683-test suite	Any tamper invalidates chain at tamper point
Power side-channel defeat	Red team (WP-05)	0.03% correlation — below exploitable threshold

7. Scope and Limitations

Computational model: ProVerif uses a symbolic model with perfect cryptographic primitives. Side-channel attacks and timing attacks are outside scope.
Rust implementation: The models verify the protocol specification, not the implementation. Implementation correctness is addressed by the 683-test suite.
Bounded sessions: These models verify a bounded number of protocol sessions.
TEE assumptions: Physical TEE attacks (cold boot, fault injection, microarchitectural side channels) are hardware-level threats outside ASMP's scope.

8. Conclusion

The three verified results — ZK authentication TRUE, cascade authentication TRUE, MSG-005 CORRECT — mean these properties hold for all possible executions of ASMP/1.0 against a Dolev-Yao adversary. In combination with the 683-test suite and red-team evaluation, they complete the evidence triangle: the protocol is logically sound, the implementation is functionally correct, and the system defeats real adversaries in practice.