Basic Hash Protocol: Perfect Authentication and the Unlinkability Counterexample

The Basic Hash RFID protocol from the proof-ladders benchmark. A tag holding a key k answers a reader challenge nonce n with the pair (n, H(k, n)); the reader recomputes H(k, n) and accepts iff it matches.

This file establishes the two distinctive facts of the challenge for the XOR hash H(k, n) = k ⊕ n:

1. Perfect authentication. For a bijection family hash — one where k ↦ H(k, n) is a bijection for each fixed nonce n — the authentication advantage of every adversary is exactly 0. The XOR hash is such a family (k ↦ k ⊕ n is a bijection), so it authenticates perfectly. The argument is the bijection-coupling technique shared with CatCrypt.Examples.OTP and CatCrypt.Examples.PRF: over a uniform key, H(k, n) is uniform and independent of n, coupling the real game with a fresh uniform sample.

2. The unlinkability counterexample. Perfect single-session authentication does not give multi-session unlinkability. The XOR outputs across two sessions are correlated: with a shared key, H(k, n₁) ⊕ H(k, n₂) = n₁ ⊕ n₂ deterministically. A distinguisher testing this fixed relation succeeds with certainty against the shared-key (real) game, whereas against independent keys the same relation can fail — so the two unlinkability games are distinguishable. This is why unlinkability needs a genuine PRF, not merely a bijection family.

Main definitions

• HashFunc — a keyed hash function Word → Word → Word.
• xorHash — the XOR hash H(k, n) = k ⊕ n.
• auth_real / auth_ideal — the authentication real/ideal games.
• PerfectAuth — perfect authentication as an rHoare coupling.
• unlink_real / unlink_ideal — the two-session unlinkability games.
• unlink_distinguisher — the correlation-testing distinguisher.

Main results

• auth_perfect_bij — any bijection-family hash authenticates perfectly.
• auth_perfect_xor — the XOR hash authenticates perfectly.
• auth_zero_advantage_xor — zero authentication advantage for the XOR hash.
• xorHash_correlated — H(k,n₁) ⊕ H(k,n₂) = n₁ ⊕ n₂ (the structural leak).
• unlink_real_always_true — the distinguisher always accepts the real game.
• unlink_ideal_not_always_true — the distinguisher can reject the ideal game.

References

• proof-ladders protocol-ladder benchmark
• [Vaudenay, On Privacy Models for RFID]
• [Rosulek, The Joy of Cryptography, §6 (pseudorandom functions)]

Type Definitions

@[reducible, inline]

abbrev CatCrypt.Examples.BasicHash.Word : Type

Word type (base type for keys, nonces, responses).

Equations

• CatCrypt.Examples.BasicHash.Word = Bool

Hash Function

structure CatCrypt.Examples.BasicHash.HashFunc : Type

A keyed hash function for the Basic Hash protocol.

• h : Word → Word → Word

  The hash function: key → nonce → response.

Protocol Operations

noncomputable def CatCrypt.Examples.BasicHash.tag_session (H : HashFunc) (k : Word) : Core.SPComp (Word × Word)

Tag session: sample a fresh nonce and compute the hash response.

Equations

• CatCrypt.Examples.BasicHash.tag_session H k = do let n ← CatCrypt.Core.SPComp.sample CatCrypt.Examples.BasicHash.Word CatCrypt.Core.SPComp.pure (n, H.h k n)

def CatCrypt.Examples.BasicHash.reader_verify (H : HashFunc) (k n r : Word) : Bool

Reader verification: check that the response matches the expected hash.

Equations

• CatCrypt.Examples.BasicHash.reader_verify H k n r = decide (H.h k n = r)

XOR Hash

def CatCrypt.Examples.BasicHash.xorHash : HashFunc

XOR-based hash: H(k, n) = k ⊕ n.

This is a perfect single-query hash (a bijection family) but fails unlinkability across sessions.

Equations

• CatCrypt.Examples.BasicHash.xorHash = { h := fun (k n : CatCrypt.Examples.BasicHash.Word) => k ^^ n }

theorem CatCrypt.Examples.BasicHash.xorHash_verify_correct (k n : Word) : reader_verify xorHash k n (xorHash.h k n) = true

XOR hash verification is correct: a tag's own response always verifies.

Authentication Game

noncomputable def CatCrypt.Examples.BasicHash.auth_real (H : HashFunc) (n : Word) : Core.SPComp Word

Authentication real game: sample a key and compute H(k, n) for the challenge nonce n.

Equations

• CatCrypt.Examples.BasicHash.auth_real H n = do let k ← CatCrypt.Core.SPComp.sample CatCrypt.Examples.BasicHash.Word CatCrypt.Core.SPComp.pure (H.h k n)

noncomputable def CatCrypt.Examples.BasicHash.auth_ideal : Core.SPComp Word

Authentication ideal game: return a uniformly random response.

Equations

• CatCrypt.Examples.BasicHash.auth_ideal = CatCrypt.Core.SPComp.sample CatCrypt.Examples.BasicHash.Word

noncomputable def CatCrypt.Examples.BasicHash.Auth_Advantage (H : HashFunc) (n : Word) (A : Word → Core.SPComp Bool) : ENNReal

Authentication advantage: distinguishing a real response from random.

Equations

• CatCrypt.Examples.BasicHash.Auth_Advantage H n A = CatCrypt.Crypto.AdvantageA (CatCrypt.Examples.BasicHash.auth_real H n) CatCrypt.Examples.BasicHash.auth_ideal A

def CatCrypt.Examples.BasicHash.PerfectAuth (H : HashFunc) : Prop

Perfect authentication: the real and ideal games are perfectly indistinguishable (coupled by eqPost).

Equations

• One or more equations did not get rendered due to their size.

Authentication Security Proofs

theorem CatCrypt.Examples.BasicHash.auth_perfect_bij (H : HashFunc) (hbij : ∀ (n : Word), Function.Bijective fun (x : Word) => H.h x n) : PerfectAuth H

Any hash whose per-nonce map k ↦ H(k, n) is a bijection achieves perfect authentication: the bijection carries the uniform key onto a uniform output, coupling the real game with the ideal uniform sample.

theorem CatCrypt.Examples.BasicHash.auth_perfect_xor : PerfectAuth xorHash

The XOR hash has perfect authentication: k ↦ k ⊕ n is a bijection for each nonce n.

theorem CatCrypt.Examples.BasicHash.auth_zero_advantage (H : HashFunc) (hPerf : PerfectAuth H) (n : Word) (A : Word → Core.SPComp Bool) : Auth_Advantage H n A = 0

Perfect authentication implies zero advantage for every adversary.

theorem CatCrypt.Examples.BasicHash.auth_zero_advantage_xor (n : Word) (A : Word → Core.SPComp Bool) : Auth_Advantage xorHash n A = 0

The XOR hash authenticates perfectly: zero authentication advantage for every nonce and every adversary.

Unlinkability Game (2 Sessions)

Unlinkability asks whether an adversary can tell if two sessions share a key. The real game uses one key for both sessions; the ideal game uses independent keys. Perfect authentication constrains only a single session, and — as the counterexample below shows — says nothing about correlation across sessions.

noncomputable def CatCrypt.Examples.BasicHash.unlink_real (H : HashFunc) (n1 n2 : Word) : Core.SPComp (Word × Word)

Unlinkability real game: one shared key for both sessions.

Equations

• CatCrypt.Examples.BasicHash.unlink_real H n1 n2 = do let k ← CatCrypt.Core.SPComp.sample CatCrypt.Examples.BasicHash.Word CatCrypt.Core.SPComp.pure (H.h k n1, H.h k n2)

noncomputable def CatCrypt.Examples.BasicHash.unlink_ideal (H : HashFunc) (n1 n2 : Word) : Core.SPComp (Word × Word)

Unlinkability ideal game: independent keys per session.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Examples.BasicHash.Unlink_Advantage (H : HashFunc) (n1 n2 : Word) (A : Word × Word → Core.SPComp Bool) : ENNReal

Unlinkability advantage.

Equations

• CatCrypt.Examples.BasicHash.Unlink_Advantage H n1 n2 A = CatCrypt.Crypto.AdvantageA (CatCrypt.Examples.BasicHash.unlink_real H n1 n2) (CatCrypt.Examples.BasicHash.unlink_ideal H n1 n2) A

XOR Hash Unlinkability Counterexample

The XOR outputs of two sessions under a shared key satisfy the fixed relation H(k,n₁) ⊕ H(k,n₂) = n₁ ⊕ n₂, independent of the key. A distinguisher testing this relation accepts the real game with certainty; against independent keys it can reject. Hence the XOR hash — though a perfect authenticator — is not unlinkable, motivating a genuine PRF for multi-session privacy.

theorem CatCrypt.Examples.BasicHash.xorHash_correlated (k n1 n2 : Word) : (k ^^ n1 ^^ (k ^^ n2)) = (n1 ^^ n2)

Key-correlation leak: with a shared key the XOR of the two responses is a fixed function of the nonces, independent of the key. This is the structural weakness that breaks unlinkability.

noncomputable def CatCrypt.Examples.BasicHash.unlink_distinguisher (n1 n2 : Word) : Word × Word → Core.SPComp Bool

Correlation-testing distinguisher: accept iff the XOR of the two responses equals the XOR of the two nonces (which holds exactly when the key is shared).

Equations

• CatCrypt.Examples.BasicHash.unlink_distinguisher n1 n2 (r1, r2) = CatCrypt.Core.SPComp.pure ((r1 ^^ r2) == (n1 ^^ n2))

theorem CatCrypt.Examples.BasicHash.unlink_real_always_true (n1 n2 : Word) : (unlink_real xorHash n1 n2).bind (unlink_distinguisher n1 n2) = (Core.SPComp.sample Word).bind fun (x : Word) => Core.SPComp.pure true

Against the real game the distinguisher always accepts: with a shared key the XOR of the outputs deterministically equals the XOR of the nonces, so the run reduces to sampling the (discarded) key and returning true.

theorem CatCrypt.Examples.BasicHash.unlink_ideal_not_always_true (n1 n2 : Word) (hne : n1 ≠ n2) : ∃ (k1 : Word) (k2 : Word), ((xorHash.h k1 n1 ^^ xorHash.h k2 n2) == (n1 ^^ n2)) = false

Against the ideal game the distinguisher can reject: for distinct nonces there are independent keys making the correlation check fail, so the real and ideal unlinkability games genuinely differ.