Chosen-message experiments for the leveled construction

The public-artifact experiment lets the adversary choose its messages after receiving the entire serialized key chain. The zero-link reduction places the base challenge public key first and generates every later key itself. A generated secret supplies the first zero link's length; when the chain has no links, that length is unused. Its guessing stage retains the adversary's exact state and adds the ordinary fresh-ciphertext tag to the base challenge.

Main definitions

• Cslib.Crypto.Homomorphic.Leveled.publicKeyGame: adaptive message selection on a public artifact.
• Cslib.Crypto.Homomorphic.Leveled.zeroLinkAdversary: the actual two-stage base reduction.

References

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

def Cslib.Crypto.Homomorphic.Leveled.publicKeyGame (E : Scheme) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) (artifact : List (List Bool) × List (List (List Bool))) : ProbComp Bool

Choose both messages after seeing every public key and encrypted link, then give the tagged challenge ciphertext to the guessing stage together with its unchanged saved state.

def Cslib.Crypto.Homomorphic.Leveled.zeroLinkAdversary (E : Scheme) (depth : ℕ → ℕ) (adversary : Encryption.Adversary) : Encryption.Adversary

Simulate the all-zero chain using the challenge key as its initial public key. The unknown challenge secret is never read or saved; only independently generated secrets supply lengths.