Output proof: FunkyPRGSymEncOTS.proof

Here is the proof file that was generated by Claude Code (Opus 4.6):

// Main result: FunkyPRGSymEnc satisfies OneTimeSecrecy.
//
// High-level proof idea:
// FunkyPRGSymEnc encrypts as: sample r, compute z = G(k + r), return r || (z + m).
// We show the left and right encryptions are indistinguishable via a sequence of
// game hops that (1) replace k + r with a uniform value using OTPUniform,
// (2) replace G(seed) with a uniform string using PRG security, (3) replace
// z + m with a uniform string using OTPUniform, arriving at a game independent
// of the message. The second half mirrors these hops to reintroduce mR.
//
// Game sequence:
// Game 0: OneTimeSecrecy.Left -- encrypt mL with G(k + r)
// Game 1: Replace k + r with uniform seed (OTPUniform on lambda bits)
// Game 2: Replace G(seed) with uniform z (PRG security)
// Game 3: Replace z + mL with uniform c (OTPUniform on 2*lambda bits)
// Game 4: Replace uniform c with z + mR (OTPUniform on 2*lambda bits, reverse)
// Game 5: Replace uniform z with G(seed) (PRG security, reverse)
// Game 6: Replace uniform seed with k + r (OTPUniform on lambda bits, reverse)
// Game 7: OneTimeSecrecy.Right -- encrypt mR with G(k + r)

import '../../Schemes/SymEnc/FunkyPRGSymEnc.scheme';
import '../../Primitives/PRG.primitive';
import '../../Games/SymEnc/OneTimeSecrecy.game';
import '../../Games/PRG/Security.game';
import '../../Games/Misc/OTPUniform.game';

// Reduction for OTPUniform hop on k + r (left side).
// Calls challenger.CTXT(r) to get either k + r (Real) or uniform s (Random),
// then evaluates G on the result and XORs with mL.
Reduction R_OTP_L1(FunkyPRGSymEnc E, PRG G) compose OTPUniform(G.lambda) against OneTimeSecrecy(E).Adversary {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        BitString<G.lambda> r <- BitString<G.lambda>;
        BitString<G.lambda> s = challenger.CTXT(r);
        BitString<2 * G.lambda> z = G.evaluate(s);
        return r || (z + mL);
    }
}

// Reduction for PRG hop (left side).
// Calls challenger.Query() to get either G(seed) (Real) or uniform z (Random),
// then XORs with mL.
Reduction R_PRG_L(FunkyPRGSymEnc E, PRG G) compose Security(G) against OneTimeSecrecy(E).Adversary {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        BitString<G.lambda> r <- BitString<G.lambda>;
        BitString<2 * G.lambda> z = challenger.Query();
        return r || (z + mL);
    }
}

// Reduction for OTPUniform hop on z + mL (left side).
// Calls challenger.CTXT(mL) to get either z + mL (Real) or uniform c (Random).
Reduction R_OTP_L2(FunkyPRGSymEnc E, PRG G) compose OTPUniform(2 * G.lambda) against OneTimeSecrecy(E).Adversary {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        BitString<G.lambda> r <- BitString<G.lambda>;
        BitString<2 * G.lambda> c = challenger.CTXT(mL);
        return r || c;
    }
}

// Reduction for OTPUniform hop on z + mR (right side).
// Calls challenger.CTXT(mR) to get either z + mR (Real) or uniform c (Random).
Reduction R_OTP_R2(FunkyPRGSymEnc E, PRG G) compose OTPUniform(2 * G.lambda) against OneTimeSecrecy(E).Adversary {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        BitString<G.lambda> r <- BitString<G.lambda>;
        BitString<2 * G.lambda> c = challenger.CTXT(mR);
        return r || c;
    }
}

// Reduction for PRG hop (right side).
// Calls challenger.Query() to get either G(seed) (Real) or uniform z (Random),
// then XORs with mR.
Reduction R_PRG_R(FunkyPRGSymEnc E, PRG G) compose Security(G) against OneTimeSecrecy(E).Adversary {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        BitString<G.lambda> r <- BitString<G.lambda>;
        BitString<2 * G.lambda> z = challenger.Query();
        return r || (z + mR);
    }
}

// Reduction for OTPUniform hop on k + r (right side).
// Calls challenger.CTXT(r) to get either k + r (Real) or uniform s (Random),
// then evaluates G on the result and XORs with mR.
Reduction R_OTP_R1(FunkyPRGSymEnc E, PRG G) compose OTPUniform(G.lambda) against OneTimeSecrecy(E).Adversary {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        BitString<G.lambda> r <- BitString<G.lambda>;
        BitString<G.lambda> s = challenger.CTXT(r);
        BitString<2 * G.lambda> z = G.evaluate(s);
        return r || (z + mR);
    }
}

proof:

let:
    Int lambda;
    PRG G = PRG(lambda, lambda);
    FunkyPRGSymEnc E = FunkyPRGSymEnc(G);

assume:
    Security(G);
    OTPUniform(lambda);
    OTPUniform(2 * lambda);

theorem:
    OneTimeSecrecy(E);

games:
    // Game 0: Original left game -- Enc(k, mL) = r || (G(k+r) + mL)
    OneTimeSecrecy(E).Left against OneTimeSecrecy(E).Adversary;

    // Hop 1: OTPUniform on k + r -- replace k + r with uniform seed
    OTPUniform(lambda).Real compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;
    OTPUniform(lambda).Random compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;

    // Hop 2: PRG security -- replace G(seed) with uniform z
    Security(G).Real compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;
    Security(G).Random compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;

    // Hop 3: OTPUniform on z + mL -- replace z + mL with uniform c
    OTPUniform(2 * lambda).Real compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;
    OTPUniform(2 * lambda).Random compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;

    // Middle: r || c with c uniform -- independent of message

    // Hop 4: OTPUniform on z + mR (reverse) -- reintroduce mR
    OTPUniform(2 * lambda).Random compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;
    OTPUniform(2 * lambda).Real compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;

    // Hop 5: PRG security (reverse) -- reintroduce G(seed)
    Security(G).Random compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;
    Security(G).Real compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;

    // Hop 6: OTPUniform on k + r (reverse) -- reintroduce k + r
    OTPUniform(lambda).Random compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;
    OTPUniform(lambda).Real compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;

    // Game 7: Original right game -- Enc(k, mR) = r || (G(k+r) + mR)
    OneTimeSecrecy(E).Right against OneTimeSecrecy(E).Adversary;