The encrypted-link reduction algorithms

The reduction embeds the challenge public key immediately after a freshly generated predecessor key. It saves only keys it generated itself, the challenge public key, and the selected bit index. Its guessing stage replaces the unknown target secret by a zero word of the predecessor secret's length and runs the actual boundary-link splicing sampler.

The target key's outgoing link is already zeroed. Fixed supported secret-key length will justify the substitution in the separate game proof; neither that hypothesis nor a security conclusion is built into these algorithms. Random link selection runs from the end of the chain towards its beginning. Dyadic padding coordinates reject, and decoding is total on every saved word.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme.LinkState: the explicitly encoded simulation context.
• Cslib.Crypto.Homomorphic.Scheme.chooseLinkAt: generate the known keys and challenge messages.
• Cslib.Crypto.Homomorphic.Scheme.guessLink: splice the challenge into the public artifact.
• Cslib.Crypto.Homomorphic.Scheme.linkAdversaryAt: the reduction at supplied index families.
• Cslib.Crypto.Homomorphic.Scheme.linkAdversary: select link and bit indices uniformly.

Main results

• Cslib.Crypto.Homomorphic.Scheme.guessLink_active: the exact response to an encoded context.
• Cslib.Crypto.Homomorphic.Scheme.guessLink_reject: a rejected coordinate always returns false.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 11.2

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.Scheme.LinkState : Type

Active flag, earlier keys, predecessor, challenge public key, later keys, and unary bit index. Every saved secret belongs to a key generated by the reduction itself.

def Cslib.Crypto.Homomorphic.Scheme.encLinkState : LinkState ↪ List Bool

Frame every saved component, including all simulator-generated secret keys.

def Cslib.Crypto.Homomorphic.Scheme.linkStateDecoder : Turing.MultiTapeTM.Decoder encLinkState

Total saved-state parsing, reusing the standard component decoders.

def Cslib.Crypto.Homomorphic.Scheme.activeLinkState (before : List (List Bool × List Bool)) (predecessor : List Bool × List Bool) (challengePk : List Bool) (after : List (List Bool × List Bool)) (bitIndex : ℕ) : List Bool

Serialize an active simulation context.

def Cslib.Crypto.Homomorphic.Scheme.rejectLinkState : List Bool

A fixed inactive saved state.

def Cslib.Crypto.Homomorphic.Scheme.rejectLinkChoice : (Bool × Bool) × List Bool

Both challenge messages are equal when the coordinate is rejected.

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.linkStateDecoder_decode_active (before : List (List Bool × List Bool)) (predecessor : List Bool × List Bool) (challengePk : List Bool) (after : List (List Bool × List Bool)) (bitIndex : ℕ) : linkStateDecoder.decode (activeLinkState before predecessor challengePk after bitIndex) = (true, before, predecessor, challengePk, after, bitIndex)

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.linkStateDecoder_decode_reject : linkStateDecoder.decode rejectLinkState = (false, [], ([], []), [], [], 0)

def Cslib.Crypto.Homomorphic.Scheme.chooseLinkAt (E : Scheme) (n beforeCount afterCount bitIndex : ℕ) (challengePk : List Bool) : ProbComp ((Bool × Bool) × List Bool)

Sample every known key before choosing the predecessor's selected bit against zero. Out-of-range bit indices return the fixed reject state.

def Cslib.Crypto.Homomorphic.Scheme.guessLink (E : Scheme) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) (n : ℕ) (state challengeCiphertext : List Bool) : ProbComp Bool

Decode the saved state and run the actual public-artifact test. The replacement secret is used only to supply the already-zeroed outgoing link's length.

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.guessLink_active (E : Scheme) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor : List Bool × List Bool) (challengePk : List Bool) (after : List (List Bool × List Bool)) (bitIndex : ℕ) (challengeCiphertext : List Bool) : E.guessLink test n (activeLinkState before predecessor challengePk after bitIndex) challengeCiphertext = have target := (challengePk, List.replicate predecessor.2.length false); do let links ← E.spliceEncryptedKeyLink n before predecessor target after bitIndex challengeCiphertext test n (List.map Prod.fst (before ++ predecessor :: target :: after), links)

An encoded active context executes the concrete splicing sampler and exposes only public keys and encrypted links to the test.

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.guessLink_reject (E : Scheme) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) (n : ℕ) (challengeCiphertext : List Bool) : E.guessLink test n rejectLinkState challengeCiphertext = pure false

Rejecting a coordinate discards the ciphertext and never invokes the test.

def Cslib.Crypto.Homomorphic.Scheme.linkAdversaryAt (E : Scheme) (beforeCount afterCount bitIndex : ℕ → ℕ) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) : Encryption.Adversary

The complete two-stage reduction at parameter-dependent link and bit positions.

noncomputable def Cslib.Crypto.Homomorphic.Scheme.linkAdversary (E : Scheme) (depth capacity : ℕ → ℕ) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) : Encryption.Adversary

Select a reverse link index and a bit index with exact dyadic samplers. Padding link indices reject immediately; padding bit indices are rejected by chooseLinkAt.