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

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 ProVerif models of three ASMP/1.0 message types and the security properties analysed for each.

Results for the current models: handshake secrecy and mutual authentication (MSG-002): TRUE. Every accepted Defensive Leap was issued by the node it names, when the relay checks the per-node envelope (MSG-004): TRUE. Every executed protected action was granted by the node (MSG-005): TRUE. Not proved: a zero-knowledge property (none was stated), single acceptance of each leap (not provable in ProVerif; shown by tests), and forward secrecy (the protocol does not provide it).

Patent Notice

ASMP/1.0 and the verified security properties are covered by Indian patent application 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 2,130-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

The models assume: SHA3-256 is a perfect random oracle (collision resistance, preimage resistance); HMAC-SHA3-256 is a secure MAC; signatures are unforgeable without the private key. No TEE is modelled. These assumptions are consistent with NIST assessments of SHA3-256.

3. MSG-002 — Handshake Secrecy and Authentication

The current models (handshake v2, the relay envelope and MSG-005 v2) are not published; sections 3–5 describe what each establishes, and section 6 summarises the results.

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.

Result: SECRECY AND MUTUAL AUTHENTICATION = TRUE

An adversary who controls the network cannot learn ally_channel_fp, and each completed run of the current handshake authenticates both peers, once. This is a secrecy and authentication result, not a zero-knowledge proof.

4. MSG-004 — Leap Origin Authentication

The model represents an originating node, the Control Plane relay and receiving nodes. The adversary controls the network and, in one variant, holds a group member's epoch key and tries to forge a Defensive Leap in another member's name. Delivery (liveness) is not modelled.

Result: LEAP ORIGIN AUTHENTICATION = TRUE (with the envelope check)

With the relay checking each node's envelope signature, every Defensive Leap a node accepts was issued by the node it names. Without that check, a group member who knows the epoch key could forge another member's leap (FALSE in the model) — the reason the per-node envelope exists. That a leap is accepted only once cannot be proved in ProVerif; the receiver's replay guard is covered by unit tests and a lab gate.

5. MSG-005 — Node-Granted Protected Actions

Result: EVERY EXECUTED ACTION WAS GRANTED BY THE NODE = TRUE

In the current model, when the management tool carries out an action only after verifying the node's answer, every executed action was granted by the node; carried out on the operator's request alone, it is not. The one-interval token lifetime is covered by tests (ProVerif has no clock), and no TEE is modelled: on hosts without a TEE the quote is a software mock. In the shipped product MSG-005 gates one protected action (an operator's "rotate now") — MSG-005 is not currently wired into any live API authentication path, so it does not yet close the Stryker-Handala-style attack vector in production. Production API authentication today is API-key + RBAC; the audit-signing key is hardware-backed (TPM 2.0) but that protects the audit chain, not management-action gating.

6. Aggregate Security Claims

Property	Basis	Strength
Handshake secrecy and mutual authentication (MSG-002)	ProVerif, current model	Proven — Dolev-Yao adversary
Leap origin authentication, relay checks the envelope (MSG-004)	ProVerif, current model	Proven — Dolev-Yao adversary; without the envelope check: FALSE
Each leap accepted at most once (MSG-004)	Unit tests and a lab gate	Not provable in ProVerif (table-based guard)
Every executed protected action granted by the node (MSG-005)	ProVerif, current model	Proven — Dolev-Yao adversary; no TEE modelled
Zero knowledge; forward secrecy	—	Zero knowledge not proved (none claimed). Forward secrecy: Not provided — see Scope
Fingerprint unlinkability	Red team (WP-05)	Empirical: L=0.5230 (n = 9,000, 13 October 2026) against a claimed bound of ≤0.535 (inside the ideal-random control's range)
Kali Invariant (per-cycle)	2,130-test suite	Enforced on every mutation cycle
Audit chain integrity	2,130-test suite	Any tamper invalidates chain at tamper point
Power side-channel defeat (ElectricEelGrid)	Design only	Not yet independently measured; hardware side-channel validation is future work

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 2,130-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.
MSG-005 integration status: MSG-005 gates one protected action in the shipped product (an operator's "rotate now"); no TEE binding is shipped. It is not currently wired into any live API authentication path in the shipped product — production API authentication is API-key + RBAC. Hardware-backed (TPM 2.0) key custody is shipped for the audit-signing chain, which is a separate mechanism from management-action authentication.

8. Conclusion

The results — handshake secrecy and mutual authentication TRUE, leap origin authentication TRUE with the envelope check, node-granted protected actions TRUE — mean these properties hold for all executions of the modelled protocol against a Dolev-Yao adversary. They are not a zero-knowledge proof. These three message-type models do not themselves address forward secrecy; the protocol does not provide forward secrecy — see Scope for what group-secret rotation does and does not give. In combination with the 2,130-test suite and red-team evaluation, they complete the evidence triangle for the shipped, live parts of the protocol (MSG-001, MSG-002, MSG-004): logically sound, functionally correct, and subjected to an internal adversarial assessment. MSG-005 gates one protected action in the shipped product and is not yet wired into any live API authentication path; no TEE binding is shipped.