Security Proof

Formal verification

The SymmetriQ authorization protocol is modeled in the Tamarin prover and verified against a Dolev–Yao adversary. Five lemmas — authentication, policy binding, no-replay, integrity, and executability — are discharged automatically.

Download proof PDF Tamarin source (.spthy)Prover output (.txt)

Tamarin v1.12.0 · processing time 1.16s

5 / 5 lemmas verified

All properties hold for every trace allowed by the protocol model, under a network attacker that controls every message.

Authentication

verified

6 steps

Integrity

verified

8 steps

01Threat model

Dolev–Yao network, optional HSM compromise

Network adversary

Controls every wire. Can intercept, drop, replay, reorder, and inject any message between Subject, Policy Engine, Signing Service, and Verifier.

Cryptographic primitives

Signatures and hashes are modeled as perfect — the only way to produce a valid signature is to hold the secret key.

HSM compromise (worst case)

Modeled explicitly: a Compromise_HSM rule leaks the signing key. Authentication then degrades gracefully — accepted intents are either honestly signed or post-compromise.

02Protocol model

Multiset rewriting rules

Five rules capture the entire authorization flow. The Allowed() fact is linear — once consumed by the signer it cannot be reused, which is what gives us policy binding.

Setup_Signer

rule

HSM provisions a long-term signing key; public key is published.

[ Fr(~sk) ]
--[ SignerInit($Signer) ]->
  [ !SignerKey($Signer, ~sk)
  , !Pk($Signer, pk(~sk))
  , Out(pk(~sk)) ]

Compromise_HSM

rule

Models the worst case — adversary obtains the signing key.

[ !SignerKey($Signer, sk) ]
--[ Compromised($Signer) ]->
  [ Out(sk) ]

Policy_Allow

rule

Policy engine emits a single-use Allowed() fact bound to the bundle hash and intent parameters.

let ph     = h(<'sq.treasury.v3', $did, $target, $recipient, $amount>)
    intent = <$did, $target, $recipient, $amount, ~nonce, $expiry, ph>
[ Fr(~nonce) ]
--[ PolicyAllowed($did, $target, $recipient, $amount, ~nonce, $expiry, ph) ]->
  [ Allowed(intent) ]

Sign_Intent

rule

Signing service signs ONLY intents the policy engine allowed. Linear consumption prevents reuse for a different intent.

[ Allowed(intent), !SignerKey($Signer, sk) ]
--[ Signed($Signer, did, target, recipient, amount, nonce, expiry, ph) ]->
  [ Out(<intent, sign(intent, sk)>) ]

Verify_OnChain

rule

On-chain verifier accepts iff signature verifies AND nonce has not been consumed.

[ In(<intent, sig>), !Pk($Signer, pk_s) ]
--[ Eq(verify(sig, intent, pk_s), true)
  , Verified($Signer, did, target, recipient, amount, nonce, expiry, ph)
  , UniqueNonce(nonce) ]->
  [ ]

03Properties proved

Five lemmas in first-order logic

Each lemma is stated over traces of the protocol. Tamarin discharges them automatically by symbolic backward search.

authentication

all-traces

✓ verified · 6 steps

Every intent the on-chain verifier accepts was signed earlier by the legitimate signer, unless the HSM was already compromised.

All s did t r a n e ph #i.
  Verified(s, did, t, r, a, n, e, ph) @ #i
  ==> (Ex #j. Signed(s, did, t, r, a, n, e, ph) @ #j & #j < #i)
    | (Ex #k. Compromised(s) @ #k & #k < #i)

policy_binding

all-traces

✓ verified · 3 steps

Nothing is signed without a prior matching allow decision from the policy engine. The policy engine is the sole source of authorization.

All s did t r a n e ph #i.
  Signed(s, did, t, r, a, n, e, ph) @ #i
  ==> Ex #j. PolicyAllowed(did, t, r, a, n, e, ph) @ #j & #j < #i

no_replay

all-traces

✓ verified · 2 steps

Each nonce is consumed at most once on-chain, even though the network adversary may resubmit (intent, signature) arbitrarily many times.

All n #i #j.
  UniqueNonce(n) @ #i & UniqueNonce(n) @ #j ==> #i = #j

integrity

all-traces

✓ verified · 8 steps

If a tuple (did, target, recipient, amount, nonce, expiry, policyHash) is accepted, those exact values were signed — no field can be tampered with in flight.

All s did t r a n e ph #i.
  Verified(s, did, t, r, a, n, e, ph) @ #i
  ==> ( (Ex #j. Signed(s, did, t, r, a, n, e, ph) @ #j & #j < #i)
      | (Ex #k. Compromised(s) @ #k & #k < #i) )
    & (All n2 #i2.
         UniqueNonce(n2) @ #i2 & UniqueNonce(n) @ #i & n2 = n
         ==> #i2 = #i)

executable

exists-trace

✓ verified · 6 steps

Sanity: at least one honest trace exists where an intent is policy-allowed, signed, and verified without HSM compromise. Confirms the model is not vacuously true.

Ex s did t r a n e ph #i #j.
    PolicyAllowed(did, t, r, a, n, e, ph) @ #j
  & Verified(s, did, t, r, a, n, e, ph) @ #i
  & not (Ex #k. Compromised(s) @ #k)

04Verbatim prover output

Tamarin v1.12.0

analyzed: SymmetriQ.spthy
  processing time: 1.16s

  authentication   (all-traces)  : verified (6 steps)
  policy_binding   (all-traces)  : verified (3 steps)
  no_replay        (all-traces)  : verified (2 steps)
  integrity        (all-traces)  : verified (8 steps)
  executable       (exists-trace): verified (6 steps)

Reproduce the proof

Run it yourself in under two seconds

Install Tamarin (nix run nixpkgs#tamarin-prover), download SymmetriQ.spthy, and run tamarin-prover --prove SymmetriQ.spthy.

Discuss the model