Create a scheme file for a symmetric encryption scheme called FunkyPRGSymEnc where the messages are bitstrings of length 2 * lambda, the key is a bitstring of length lambda, G is a PRG, and the encryption function is sample r <- bitstrings of length lambda, compute z = G(k + r), return r || (z + m)
Create a proof for a theorem that FunkyPRGSymEnc satisfies the OneTimeSecrecy security property. The only security assumptions we should need to use are the PRG security assumption and the OTPUniform assumption. The outline of the proof is as follows: - Hop to a game in which the Eavesdrop oracle evaluates G on k, not k + r. This hop should work because k + r is effectively a one-time pad encryption of r, so it looks uniform. - Hop to a game in which the Eavesdrop oracle returns r || (z + mL), where z is a randomly sampled bitstring. This hop should be based on a reduction to security of the PRG. - Hop to a game where the Eavesdrop oracle returns r || z, where z is a randomly sampled bitstring, again based on one-time pad. - The second half of the proof is a mirror of the first half, gradually reintroducing mR and G.
Let me start by understanding the existing codebase structure, particularly the examples and primitives available.
Todos have been modified successfully. Ensure that you continue to use the todo list to track your progress. Please proceed with the current tasks if applicable
{"name":"examples","path":"examples","type":"directory","children":[{"name":"Book","path":"examples/Book","type":"directory","children":[{"name":"2","path":"examples/Book/2","type":"directory","children":[{"name":"2_12_DoubleOTP.scheme","path":"examples/Book/2/2_12_DoubleOTP.scheme","type":"file"},{"name":"2_13.proof","path":"examples/Book/2/2_13.proof","type":"file"},{"name":"2_15.proof","path":"examples/Book/2/2_15.proof","type":"file"}]},{"name":"2_Exercises","path":"examples/Book/2_Exercises","type":"directory","children":[{"name":"2_13.proof","path":"examples/Book/2_Exercises/2_13.proof","type":"file"},{"name":"2_13_SymEncSquared.scheme","path":"examples/Book/2_Exercises/2_13_SymEncSquared.scheme","type":"file"},{"name":"2_14.game","path":"examples/Book/2_Exercises/2_14.game","type":"file"},{"name":"2_14_Backward.proof","path":"examples/Book/2_Exercises/2_14_Backward.proof","type":"file"},{"name":"2_14_Forward.proof","path":"examples/Book/2_Exercises/2_14_Forward.proof","type":"file"},{"name":"2_15.game","path":"examples/Book/2_Exercises/2_15.game","type":"file"},{"name":"2_15_Backward.proof","path":"examples/Book/2_Exercises/2_15_Backward.proof","type":"file"},{"name":"2_15_Forward.proof","path":"examples/Book/2_Exercises/2_15_Forward.proof","type":"file"}]},{"name":"5","path":"examples/Book/5","type":"directory","children":[{"name":"5_2_PseudoOTP.scheme","path":"examples/Book/5/5_2_PseudoOTP.scheme","type":"file"},{"name":"5_3.proof","path":"examples/Book/5/5_3.proof","type":"file"},{"name":"5_4_TriplingPRG.scheme","path":"examples/Book/5/5_4_TriplingPRG.scheme","type":"file"},{"name":"5_5_TriplingPRGSecure.proof","path":"examples/Book/5/5_5_TriplingPRGSecure.proof","type":"file"}]},{"name":"5_Exercises","path":"examples/Book/5_Exercises","type":"directory","children":[{"name":"5_10.proof","path":"examples/Book/5_Exercises/5_10.proof","type":"file"},{"name":"5_10.scheme","path":"examples/Book/5_Exercises/5_10.scheme","type":"file"},{"name":"5_8_a.proof","path":"examples/Book/5_Exercises/5_8_a.proof","type":"file"},{"name":"5_8_a.scheme","path":"examples/Book/5_Exercises/5_8_a.scheme","type":"file"},{"name":"5_8_b.proof","path":"examples/Book/5_Exercises/5_8_b.proof","type":"file"},{"name":"5_8_b.scheme","path":"examples/Book/5_Exercises/5_8_b.scheme","type":"file"},{"name":"5_8_e.proof","path":"examples/Book/5_Exercises/5_8_e.proof","type":"file"},{"name":"5_8_e.scheme","path":"examples/Book/5_Exercises/5_8_e.scheme","type":"file"},{"name":"5_8_f.proof","path":"examples/Book/5_Exercises/5_8_f.proof","type":"file"},{"name":"5_8_f.scheme","path":"examples/Book/5_Exercises/5_8_f.scheme","type":"file"},{"name":"5_8_PseudoOTP_OTUC.proof","path":"examples/Book/5_Exercises/5_8_PseudoOTP_OTUC.proof","type":"file"},{"name":"5_8_ThreePartBitStringSampling.game","path":"examples/Book/5_Exercises/5_8_ThreePartBitStringSampling.game","type":"file"}]},{"name":"7_Exercises","path":"examples/Book/7_Exercises","type":"directory","children":[{"name":"7_13.game","path":"examples/Book/7_Exercises/7_13.game","type":"file"},{"name":"7_13_Backward.proof","path":"examples/Book/7_Exercises/7_13_Backward.proof","type":"file"},{"name":"7_13_Forward.proof","path":"examples/Book/7_Exercises/7_13_Forward.proof","type":"file"}]},{"name":"9_Exercises","path":"examples/Book/9_Exercises","type":"directory","children":[{"name":"9_6_CCA$impliesCCA.proof","path":"examples/Book/9_Exercises/9_6_CCA$impliesCCA.proof","type":"file"}]}]},{"name":"Games","path":"examples/Games","type":"directory","children":[{"name":"DigitalSignature","path":"examples/Games/DigitalSignature","type":"directory","children":[{"name":"Security.game","path":"examples/Games/DigitalSignature/Security.game","type":"file"}]},{"name":"Hash","path":"examples/Games/Hash","type":"directory","children":[{"name":"Security.game","path":"examples/Games/Hash/Security.game","type":"file"}]},{"name":"KEM","path":"examples/Games/KEM","type":"directory","children":[{"name":"Correctness.game","path":"examples/Games/KEM/Correctness.game","type":"file"},{"name":"CPAKEM.game","path":"examples/Games/KEM/CPAKEM.game","type":"file"}]},{"name":"KeyAgreement","path":"examples/Games/KeyAgreement","type":"directory","children":[{"name":"Security.game","path":"examples/Games/KeyAgreement/Security.game","type":"file"}]},{"name":"MAC","path":"examples/Games/MAC","type":"directory","children":[{"name":"Security.game","path":"examples/Games/MAC/Security.game","type":"file"}]},{"name":"Misc","path":"examples/Games/Misc","type":"directory","children":[{"name":"BitStringSampling.game","path":"examples/Games/Misc/BitStringSampling.game","type":"file"},{"name":"OTPOTS.game","path":"examples/Games/Misc/OTPOTS.game","type":"file"},{"name":"OTPUniform.game","path":"examples/Games/Misc/OTPUniform.game","type":"file"},{"name":"Predict.game","path":"examples/Games/Misc/Predict.game","type":"file"},{"name":"Sample.game","path":"examples/Games/Misc/Sample.game","type":"file"}]},{"name":"PRF","path":"examples/Games/PRF","type":"directory","children":[{"name":"Security.game","path":"examples/Games/PRF/Security.game","type":"file"}]},{"name":"PRG","path":"examples/Games/PRG","type":"directory","children":[{"name":"Security.game","path":"examples/Games/PRG/Security.game","type":"file"}]},{"name":"PRP","path":"examples/Games/PRP","type":"directory","children":[{"name":"Correctness.game","path":"examples/Games/PRP/Correctness.game","type":"file"},{"name":"Security.game","path":"examples/Games/PRP/Security.game","type":"file"},{"name":"StrongSecurity.game","path":"examples/Games/PRP/StrongSecurity.game","type":"file"}]},{"name":"PubKeyEnc","path":"examples/Games/PubKeyEnc","type":"directory","children":[{"name":"Correctness.game","path":"examples/Games/PubKeyEnc/Correctness.game","type":"file"},{"name":"CPA$.game","path":"examples/Games/PubKeyEnc/CPA$.game","type":"file"},{"name":"CPA.game","path":"examples/Games/PubKeyEnc/CPA.game","type":"file"},{"name":"OneTimeSecrecy.game","path":"examples/Games/PubKeyEnc/OneTimeSecrecy.game","type":"file"}]},{"name":"SecretSharing","path":"examples/Games/SecretSharing","type":"directory","children":[{"name":"Correctness.game","path":"examples/Games/SecretSharing/Correctness.game","type":"file"},{"name":"Security.game","path":"examples/Games/SecretSharing/Security.game","type":"file"}]},{"name":"SymEnc","path":"examples/Games/SymEnc","type":"directory","children":[{"name":"AE.game","path":"examples/Games/SymEnc/AE.game","type":"file"},{"name":"CCA$.game","path":"examples/Games/SymEnc/CCA$.game","type":"file"},{"name":"CCA.game","path":"examples/Games/SymEnc/CCA.game","type":"file"},{"name":"CCABook.game","path":"examples/Games/SymEnc/CCABook.game","type":"file"},{"name":"Correctness.game","path":"examples/Games/SymEnc/Correctness.game","type":"file"},{"name":"CPA$.game","path":"examples/Games/SymEnc/CPA$.game","type":"file"},{"name":"CPA.game","path":"examples/Games/SymEnc/CPA.game","type":"file"},{"name":"KeyUniformity.game","path":"examples/Games/SymEnc/KeyUniformity.game","type":"file"},{"name":"OneTimeSecrecy.game","path":"examples/Games/SymEnc/OneTimeSecrecy.game","type":"file"},{"name":"OneTimeUniformCiphertexts.game","path":"examples/Games/SymEnc/OneTimeUniformCiphertexts.game","type":"file"}]}]},{"name":"Primitives","path":"examples/Primitives","type":"directory","children":[{"name":"DigitalSignature.primitive","path":"examples/Primitives/DigitalSignature.primitive","type":"file"},{"name":"Hash.primitive","path":"examples/Primitives/Hash.primitive","type":"file"},{"name":"KEM.primitive","path":"examples/Primitives/KEM.primitive","type":"file"},{"name":"KeyAgreement.primitive","path":"examples/Primitives/KeyAgreement.primitive","type":"file"},{"name":"MAC.primitive","path":"examples/Primitives/MAC.primitive","type":"file"},{"name":"NonNullableSymEnc.primitive","path":"examples/Primitives/NonNullableSymEnc.primitive","type":"file"},{"name":"PRF.primitive","path":"examples/Primitives/PRF.primitive","type":"file"},{"name":"PRG.primitive","path":"examples/Primitives/PRG.primitive","type":"file"},{"name":"PRP.primitive","path":"examples/Primitives/PRP.primitive","type":"file"},{"name":"PubKeyEnc.primitive","path":"examples/Primitives/PubKeyEnc.primitive","type":"file"},{"name":"SecretSharing.primitive","path":"examples/Primitives/SecretSharing.primitive","type":"file"},{"name":"SymEnc.primitive","path":"examples/Primitives/SymEnc.primitive","type":"file"}]},{"name":"Proofs","path":"examples/Proofs","type":"directory","children":[{"name":"Misc","path":"examples/Proofs/Misc","type":"directory","children":[{"name":"PredictIndistinguishable.proof.todo","path":"examples/Proofs/Misc/PredictIndistinguishable.proof.todo","type":"file"},{"name":"SampleIndistinguishable.proof.todo","path":"examples/Proofs/Misc/SampleIndistinguishable.proof.todo","type":"file"}]},{"name":"PRG","path":"examples/Proofs/PRG","type":"directory","children":[{"name":"CounterPRGSecure.proof.todo","path":"examples/Proofs/PRG/CounterPRGSecure.proof.todo","type":"file"},{"name":"TriplingPRGSecure.proof","path":"examples/Proofs/PRG/TriplingPRGSecure.proof","type":"file"}]},{"name":"PubEnc","path":"examples/Proofs/PubEnc","type":"directory","children":[{"name":"Hybrid.proof","path":"examples/Proofs/PubEnc/Hybrid.proof","type":"file"},{"name":"KEMDEMCPA.proof","path":"examples/Proofs/PubEnc/KEMDEMCPA.proof","type":"file"},{"name":"OTSimpliesCPA.proof","path":"examples/Proofs/PubEnc/OTSimpliesCPA.proof","type":"file"}]},{"name":"SecretSharing","path":"examples/Proofs/SecretSharing","type":"directory","children":[{"name":"OTPSecretSharingSecure.proof.todo","path":"examples/Proofs/SecretSharing/OTPSecretSharingSecure.proof.todo","type":"file"}]},{"name":"SymEnc","path":"examples/Proofs/SymEnc","type":"directory","children":[{"name":"CPA$impliesCPA.proof","path":"examples/Proofs/SymEnc/CPA$impliesCPA.proof","type":"file"},{"name":"DoubleCPA$.proof","path":"examples/Proofs/SymEnc/DoubleCPA$.proof","type":"file"},{"name":"EncryptThenMACCCA.proof","path":"examples/Proofs/SymEnc/EncryptThenMACCCA.proof","type":"file"},{"name":"GeneralDoubleOTUC.proof","path":"examples/Proofs/SymEnc/GeneralDoubleOTUC.proof","type":"file"},{"name":"OTUCimpliesDoubleOTUC.proof","path":"examples/Proofs/SymEnc/OTUCimpliesDoubleOTUC.proof","type":"file"},{"name":"OTUCimpliesOTS.proof","path":"examples/Proofs/SymEnc/OTUCimpliesOTS.proof","type":"file"},{"name":"SymEncPRFCPA$Secure.proof.todo","path":"examples/Proofs/SymEnc/SymEncPRFCPA$Secure.proof.todo","type":"file"}]}]},{"name":"Schemes","path":"examples/Schemes","type":"directory","children":[{"name":"PRG","path":"examples/Schemes/PRG","type":"directory","children":[{"name":"CounterPRG.scheme","path":"examples/Schemes/PRG/CounterPRG.scheme","type":"file"},{"name":"TriplingPRG.scheme","path":"examples/Schemes/PRG/TriplingPRG.scheme","type":"file"}]},{"name":"PubEnc","path":"examples/Schemes/PubEnc","type":"directory","children":[{"name":"Hybrid.scheme","path":"examples/Schemes/PubEnc/Hybrid.scheme","type":"file"},{"name":"KEMDEM.scheme","path":"examples/Schemes/PubEnc/KEMDEM.scheme","type":"file"}]},{"name":"SecretSharing","path":"examples/Schemes/SecretSharing","type":"directory","children":[{"name":"OTP.scheme","path":"examples/Schemes/SecretSharing/OTP.scheme","type":"file"}]},{"name":"SymEnc","path":"examples/Schemes/SymEnc","type":"directory","children":[{"name":"DoubleSymEnc.scheme","path":"examples/Schemes/SymEnc/DoubleSymEnc.scheme","type":"file"},{"name":"EncryptThenMAC.scheme","path":"examples/Schemes/SymEnc/EncryptThenMAC.scheme","type":"file"},{"name":"GeneralDoubleSymEnc.scheme","path":"examples/Schemes/SymEnc/GeneralDoubleSymEnc.scheme","type":"file"},{"name":"OFB.scheme","path":"examples/Schemes/SymEnc/OFB.scheme","type":"file"},{"name":"OTP.scheme","path":"examples/Schemes/SymEnc/OTP.scheme","type":"file"},{"name":"SymEncPRF.scheme","path":"examples/Schemes/SymEnc/SymEncPRF.scheme","type":"file"}]}]},{"name":"LICENSE","path":"examples/LICENSE","type":"file"},{"name":"README.md","path":"examples/README.md","type":"file"}]}Let me read the key files I need to understand: the SymEnc primitive, PRG primitive, OneTimeSecrecy game, PRG Security game, OTPUniform game, and an existing proof that uses PRG security for reference.
{"result":"Primitive SymEnc(Set MessageSpace, Set CiphertextSpace, Set KeySpace) {\n Set Message = MessageSpace;\n Set Ciphertext = CiphertextSpace;\n Set Key = KeySpace;\n\n Key KeyGen();\n Ciphertext Enc(Key k, Message m);\n Message? Dec(Key k, Ciphertext c);\n}\n"}{"result":"Primitive PRG(Int lambda, Int stretch) {\n Int lambda = lambda;\n Int stretch = stretch;\n\n BitString<lambda + stretch> evaluate(BitString<lambda> x);\n}\n"}{"result":"import '../../Primitives/SymEnc.primitive';\n\nGame Left(SymEnc E) {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n E.Key k = E.KeyGen();\n E.Ciphertext c = E.Enc(k, mL);\n return c;\n }\n}\n\nGame Right(SymEnc E) {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n E.Key k = E.KeyGen();\n E.Ciphertext c = E.Enc(k, mR);\n return c;\n }\n}\n\nexport as OneTimeSecrecy;\n"}{"result":"import '../../Primitives/PRG.primitive';\n\nGame Real(PRG G) {\n BitString<G.lambda + G.stretch> Query() {\n BitString<G.lambda> s <- BitString<G.lambda>;\n return G.evaluate(s);\n }\n}\n\nGame Random(PRG G) {\n BitString<G.lambda + G.stretch> Query() {\n BitString<G.lambda + G.stretch> r <- BitString<G.lambda + G.stretch>;\n return r;\n }\n}\n\nexport as Security;\n"}{"result":"Game Real(Int lambda) {\n BitString<lambda> CTXT(BitString<lambda> m) {\n BitString<lambda> k <- BitString<lambda>;\n return k + m;\n }\n}\n\nGame Random(Int lambda) {\n BitString<lambda> CTXT(BitString<lambda> m) {\n BitString<lambda> c <- BitString<lambda>;\n return c;\n }\n}\n\nexport as OTPUniform;\n"}{"result":"import '../../Primitives/SymEnc.primitive';\nimport '../../Primitives/PRG.primitive';\n\nScheme PseudoOTP(Int lambda, Int stretch, PRG G) extends SymEnc {\n requires G.lambda == lambda && G.stretch == stretch;\n\n Set Key = BitString<lambda>;\n Set Message = BitString<lambda + stretch>;\n Set Ciphertext = BitString<lambda + stretch>;\n\n Key KeyGen() {\n Key k <- Key;\n return k;\n }\n\n Ciphertext Enc(Key k, Message m) {\n return G.evaluate(k) + m;\n }\n\n Message Dec(Key k, Ciphertext c) {\n return G.evaluate(k) + c;\n }\n}\n"}{"result":"import '../../Book/5/5_2_PseudoOTP.scheme';\nimport '../../Primitives/PRG.primitive';\nimport '../../Games/SymEnc/OneTimeSecrecy.game';\nimport '../../Games/PRG/Security.game';\nimport '../../Games/Misc/OTPOTS.game';\n\nReduction R1(PseudoOTP P, PRG G) compose Security(G) against OneTimeSecrecy(P).Adversary {\n P.Ciphertext Eavesdrop(P.Message mL, P.Message mR) {\n P.Ciphertext c = challenger.Query() + mL;\n return c;\n }\n}\n\nGame Intermediate1(PseudoOTP P, PRG G) {\n P.Ciphertext Eavesdrop(P.Message mL, P.Message mR) {\n P.Ciphertext z <- P.Ciphertext;\n P.Ciphertext c = z + mL;\n return c;\n }\n}\n\nReduction R2(PseudoOTP P, Int size) compose OTPOTS(size) against OneTimeSecrecy(P).Adversary {\n P.Ciphertext Eavesdrop(P.Message mL, P.Message mR) {\n P.Ciphertext c = challenger.Eavesdrop(mL, mR);\n return c;\n }\n}\n\nGame Intermediate2(PseudoOTP P, PRG G) {\n P.Ciphertext Eavesdrop(P.Message mL, P.Message mR) {\n P.Ciphertext z <- P.Ciphertext;\n P.Ciphertext c = z + mR;\n return c;\n }\n}\n\nReduction R3(PseudoOTP P, PRG G) compose Security(G) against OneTimeSecrecy(P).Adversary {\n P.Ciphertext Eavesdrop(P.Message mL, P.Message mR) {\n P.Ciphertext c = challenger.Query() + mR;\n return c;\n }\n}\n\nproof:\n\nlet:\n Int lambda;\n Int stretch;\n PRG G = PRG(lambda, stretch);\n PseudoOTP P = PseudoOTP(lambda, stretch, G);\n\nassume:\n Security(G);\n OTPOTS(lambda + stretch);\n\ntheorem:\n OneTimeSecrecy(P);\n\ngames:\n OneTimeSecrecy(P).Left against OneTimeSecrecy(P).Adversary;\n\n Security(G).Real compose R1(P, G) against OneTimeSecrecy(P).Adversary;\n\n Security(G).Random compose R1(P, G) against OneTimeSecrecy(P).Adversary;\n\n Intermediate1(P, G) against OneTimeSecrecy(P).Adversary;\n\n OTPOTS(lambda + stretch).Left compose R2(P, lambda + stretch) against OneTimeSecrecy(P).Adversary;\n\n OTPOTS(lambda + stretch).Right compose R2(P, lambda + stretch) against OneTimeSecrecy(P).Adversary;\n\n Intermediate2(P, G) against OneTimeSecrecy(P).Adversary;\n\n Security(G).Random compose R3(P, G) against OneTimeSecrecy(P).Adversary;\n\n Security(G).Real compose R3(P, G) against OneTimeSecrecy(P).Adversary;\n\n OneTimeSecrecy(P).Right against OneTimeSecrecy(P).Adversary;\n"}Now let me also look at the OTPOTS game and another proof that uses OTPUniform to understand patterns better.
Let me also check a proof that uses OTPUniform and look at an existing scheme with randomized encryption for reference.
{"result":"import '../../Primitives/PRG.primitive';\n\nScheme PRG_5_8_a(PRG G) extends PRG {\n requires G.stretch == 2 * G.lambda;\n\n Int lambda = G.lambda;\n Int stretch = 5 * G.lambda;\n\n BitString<lambda + stretch> evaluate(BitString<lambda> s) {\n BitString<3 * lambda> result1 = G.evaluate(s);\n\n BitString<lambda> x = result1[0 : lambda];\n BitString<lambda> y = result1[lambda : 2*lambda];\n BitString<lambda> z = result1[2*lambda : 3*lambda];\n \n BitString<3 * lambda> result2 = G.evaluate(x);\n BitString<3 * lambda> result3 = G.evaluate(z);\n\n return result2 || result3;\n }\n}\n"}{"result":"import '../../Primitives/PRG.primitive';\nimport '../../Games/Misc/BitStringSampling.game';\nimport '../../Book/5_Exercises/5_8_a.scheme';\nimport '../../Book/5_Exercises/5_8_ThreePartBitStringSampling.game';\nimport '../../Games/PRG/Security.game';\n\nReduction R1(PRG G, PRG_5_8_a H) compose Security(G) against Security(H).Adversary {\n BitString<H.lambda + H.stretch> Query() {\n BitString<3 * H.lambda> result1 = challenger.Query();\n\n BitString<H.lambda> x = result1[0 : H.lambda];\n BitString<H.lambda> y = result1[H.lambda : 2*H.lambda];\n BitString<H.lambda> z = result1[2*H.lambda : 3*H.lambda];\n\n BitString<3 * H.lambda> result2 = G.evaluate(x);\n BitString<3 * H.lambda> result3 = G.evaluate(z);\n\n return result2 || result3;\n }\n}\n\nReduction R2(PRG G, PRG_5_8_a H, Int lambda) compose ThreePartBitStringSampling(lambda) against Security(H).Adversary {\n BitString<H.lambda + H.stretch> Query() {\n BitString<3 * H.lambda> result1 = challenger.Query();\n\n BitString<H.lambda> x = result1[0 : H.lambda];\n BitString<H.lambda> y = result1[H.lambda : 2*H.lambda];\n BitString<H.lambda> z = result1[2*H.lambda : 3*H.lambda];\n\n BitString<3 * H.lambda> result2 = G.evaluate(x);\n BitString<3 * H.lambda> result3 = G.evaluate(z);\n\n return result2 || result3;\n }\n}\n\nReduction R3(PRG G, PRG_5_8_a H) compose Security(G) against Security(H).Adversary {\n BitString<H.lambda + H.stretch> Query() {\n BitString<3 * H.lambda> result2 = challenger.Query();\n BitString<3 * H.lambda> result3 = challenger.Query();\n return result2 || result3;\n }\n}\n\nReduction R4(PRG_5_8_a H, Int lambda) compose BitStringSampling(3 * lambda, 3 * lambda) against Security(H).Adversary {\n BitString<H.lambda + H.stretch> Query() {\n return challenger.Query();\n }\n}\n\nproof:\n\nlet:\n Int lambda;\n PRG G = PRG(lambda, 2 * lambda);\n PRG_5_8_a H = PRG_5_8_a(G);\n\nassume:\n Security(G);\n ThreePartBitStringSampling(lambda);\n BitStringSampling(3 * lambda, 3 * lambda);\n\ntheorem:\n Security(H);\n\ngames:\n Security(H).Real against Security(H).Adversary;\n\n Security(G).Real compose R1(G, H) against Security(H).Adversary;\n\n Security(G).Random compose R1(G, H) against Security(H).Adversary;\n\n ThreePartBitStringSampling(lambda).SampleDirectly compose R2(G, H, lambda) against Security(H).Adversary;\n\n ThreePartBitStringSampling(lambda).Concatenate compose R2(G, H, lambda) against Security(H).Adversary;\n\n Security(G).Real compose R3(G, H) against Security(H).Adversary;\n\n Security(G).Random compose R3(G, H) against Security(H).Adversary;\n\n BitStringSampling(3 * lambda, 3 * lambda).Concatenate compose R4(H, lambda) against Security(H).Adversary;\n\n BitStringSampling(3 * lambda, 3 * lambda).SampleDirectly compose R4(H, lambda) against Security(H).Adversary;\n\n Security(H).Random against Security(H).Adversary;\n"}{
"path": "examples/Book/5_Exercises/5_8_PseudoOTP_OTUC.proof"
}{"result":"import '../../Primitives/PRG.primitive';\nimport '../../Book/5/5_2_PseudoOTP.scheme';\nimport '../../Games/SymEnc/OneTimeUniformCiphertexts.game';\nimport '../../Games/PRG/Security.game';\nimport '../../Schemes/SymEnc/OTP.scheme';\n\nReduction R1(OTP E, PRG G, PseudoOTP P) compose Security(G) against OneTimeUniformCiphertexts(P).Adversary {\n E.Ciphertext CTXT(E.Message m) {\n return challenger.Query() + m;\n }\n}\n\nReduction R2(OTP E, PseudoOTP P) compose OneTimeUniformCiphertexts(E) against OneTimeUniformCiphertexts(P).Adversary {\n E.Ciphertext CTXT(E.Message m) {\n E.Ciphertext result = challenger.CTXT(m);\n return result;\n }\n}\n\nproof:\n\nlet:\n Int lambda;\n PRG G = PRG(lambda, 2 * lambda);\n PseudoOTP P = PseudoOTP(lambda, 2 * lambda, G);\n OTP E = OTP(3 * lambda);\n\nassume:\n Security(G);\n OneTimeUniformCiphertexts(E);\n\ntheorem:\n OneTimeUniformCiphertexts(P);\n\ngames:\n OneTimeUniformCiphertexts(P).Real against OneTimeUniformCiphertexts(P).Adversary;\n\n Security(G).Real compose R1(E, G, P) against OneTimeUniformCiphertexts(P).Adversary;\n\n Security(G).Random compose R1(E, G, P) against OneTimeUniformCiphertexts(P).Adversary;\n\n OneTimeUniformCiphertexts(E).Real compose R2(E, P) against OneTimeUniformCiphertexts(P).Adversary;\n\n OneTimeUniformCiphertexts(E).Random compose R2(E, P) against OneTimeUniformCiphertexts(P).Adversary;\n\n OneTimeUniformCiphertexts(P).Random against OneTimeUniformCiphertexts(P).Adversary;\n"}Now I have a good understanding of the patterns. Let me also look at the OTP scheme to understand how randomized encryption schemes are defined.
{"result":"import '../../Primitives/SymEnc.primitive';\n\nScheme OTP(Int lambda) extends SymEnc {\n Set Key = BitString<lambda>;\n Set Message = BitString<lambda>;\n Set Ciphertext = BitString<lambda>;\n\n Key KeyGen() {\n Key k <- Key;\n return k;\n }\n\n Ciphertext Enc(Key k, Message m) {\n return k + m;\n }\n\n Message Dec(Key k, Ciphertext c) {\n return k + c;\n }\n}\n"}Now I need to understand how to create a scheme with randomized encryption (with a random r value sampled). Let me look at some other schemes that sample random values in Enc.
{
"pattern": "Enc\\(.*\\).*\\{",
"glob": "**/*.scheme",
"output_mode": "files_with_matches"
}Found 11 files examples/Schemes/SymEnc/OFB.scheme examples/Schemes/SymEnc/OTP.scheme examples/Schemes/SymEnc/SymEncPRF.scheme examples/Schemes/PubEnc/Hybrid.scheme examples/Schemes/PubEnc/KEMDEM.scheme examples/Schemes/SymEnc/DoubleSymEnc.scheme examples/Schemes/SymEnc/EncryptThenMAC.scheme examples/Schemes/SymEnc/GeneralDoubleSymEnc.scheme examples/Book/5/5_2_PseudoOTP.scheme examples/Book/2_Exercises/2_13_SymEncSquared.scheme examples/Book/2/2_12_DoubleOTP.scheme
{"result":"import '../../Primitives/SymEnc.primitive';\nimport '../../Primitives/PRF.primitive';\n\nScheme OFB(Int lambda, Int blocks, PRF F) extends SymEnc {\n requires F.lambda == lambda && F.in == lambda && F.out == lambda;\n\n Set Key = BitString<lambda>;\n Set Message = Array<BitString<lambda>, blocks>;\n Set Ciphertext = Array<BitString<lambda>, blocks + 1>;\n\n Key KeyGen() {\n Key k <- BitString<lambda>;\n return k;\n }\n\n Ciphertext Enc(Key k, Message m) {\n Ciphertext c;\n\n BitString<lambda> r <- BitString<lambda>;\n\n c[0] = r;\n for (Int i = 1 to blocks) {\n r = F.evaluate(k, r);\n c[i] = r + m[i-1];\n }\n return c;\n }\n\n Message Dec(Key k, Ciphertext c) {\n Array<BitString<lambda>, blocks> m;\n BitString<lambda> r = c[0];\n for (Int i = 0 to blocks - 1) {\n r = F.evaluate(k, r);\n m[i] = r + c[i + 1];\n }\n return m;\n }\n}\n"}Now I have a good understanding. The OFB scheme samples r inside Enc and concatenates it. But for the ciphertext type, it uses arrays. For our scheme, the ciphertext is a BitString<3 * lambda> (lambda for r, and 2*lambda for the XOR part). But wait - the message is BitString<2 * lambda> and the key is BitString<lambda>. The PRG maps BitString<lambda> to BitString<2 * lambda> (so stretch = lambda).
Wait, let me reconsider. The encryption is:
For messages of length 2lambda, we need G to output 2lambda bits. So G maps lambda bits to 2lambda bits, meaning stretch = lambda. The ciphertext is r || (z + m), which is lambda + 2lambda = 3*lambda bits. Now I'm ready to set up the scheme file and proof, defining the parameters with PRG G where G.lambda and G.stretch are both lambda.
For the types, the key is a lambda-bit string, messages are 2lambda bits, and ciphertexts are 3lambda bits total. I'm going to use BitString with concatenation to express this cleanly rather than arrays. Now I'm writing the scheme definition...
Defining the encryption scheme...
Now for the security proof—I need to show OneTimeSecrecy holds for this construction. The left game samples a key and random bits, then encrypts the left message using the PRG output. The key insight is that since the key is uniform and only used once, k+r is itself uniform, so I can replace the PRG evaluation with a uniform string instead. This transforms the game into one where we're just XORing the message with random bits, which is information-theoretically secure. sampling a fresh s.
Actually, let me think more carefully. The OTPUniform game says: k + m looks uniform when k is uniform. So k + r where k is uniform looks uniform. We want to replace G(k + r) with G(s) where s is sampled uniformly.
For the OTPUniform hop, I need to think about what the reduction looks like. Let me work through the game structure more carefully.
In Game 0, I'm sampling k and r independently, then computing G(k + r) and XORing with the left message. The key insight is that since k is uniform and independent, k + r is uniform regardless of what r is, so I can replace the entire "sample k, compute k + r" sequence with just sampling s uniformly. After this hop, I'm left with a game where s is uniform and I evaluate G(s) directly.
Next I'll apply PRG security to replace the pseudorandom output of G(s) with a truly random string.
Then I'll apply OTPUniform again to the XOR with the message, replacing the uniform string XORed with the message with just a uniform sample.
At this point I've reached the middle game where the output is independent of the left message. Now I need to mirror these steps for the right message to complete the proof. I need to set up the reduction carefully for the OTPUniform game. The CTXT oracle either returns k+m in the Real case or a random string in the Random case, so my reduction will query it with r and get back either k+r or a random value s, then apply the PRG evaluation to whichever result comes back.
Now I'm realizing the key insight: in OTPUniform, a fresh k is sampled on each CTXT call, which matches how the original game works. So the reduction is sound there.
Let me map out the full game sequence across all four reduction steps to see the pattern more clearly. Looking at the 5_3.proof structure, it seems like not every hop requires all four intermediate games—I should figure out which steps are actually necessary.
The standard pattern appears to be: swap the left game for the right using interchangeability, apply the assumption to justify the swap, then continue with interchangeability steps to reach the next assumption point. So each reduction block follows a 4-game pattern where intermediate games bridge between the Real and Random versions. For the OTP uniform hop, I need to construct a reduction R_OTP1 that works with OTPUniform by having the challenger sample k and return k + r, then I evaluate G on that sum and XOR with the left message.
When composed with the Random version, the challenger instead returns a uniformly random value, so I evaluate G on that random value instead. This gives me the game sequence: the original OneTimeSecrecy game, then OTPUniform Real composed with my reduction, then OTPUniform Random composed with my reduction as the assumption, and finally an intermediate game that's indistinguishable from the previous one.
Defining the intermediate game... Now I'm applying the second OTP uniform hop, replacing the random z with a challenger query to make the ciphertext indistinguishable from random. The reduction shows how the real game where z is uniform and added to the message maps to the OTP security game, and in the random case the challenger returns a truly random ciphertext instead.
Then I mirror this same argument for the right message mR, setting up two more game transitions where I swap out the uniform addition for mR with a random ciphertext, ultimately reaching a final game where both halves are uniformly random and independent of the actual messages. , reverse: Random -> Real)
Wait, the assumption is bidirectional, but I need to be careful about direction. The assumption says Real and Random are indistinguishable. So going from Random to Real is also valid.
Actually, looking at the pattern again: the direction matters for how the games are listed.
For the second half (introducing mR):
Where R_OTP3 takes the message pair and generates a random string r, then uses the challenger to encrypt mR, returning r concatenated with the ciphertext.
Now I'm looking at how OTPUniform works in both modes: when Random, the ciphertext is just a random value, which matches Intermediate3, but when Real, it XORs a uniform value with mR. Intermediate4 formalizes this by explicitly computing r and z, then returning r concatenated with z XORed to mR.
Continuing with the next reduction:
R_PRG2 uses the PRG to expand a seed and feeds the result into the eavesdropping game.
Then the final reduction introduces the one-time pad assumption:
This gives us 19 games total, which is the complete reduction chain from the original security game to the one-time secrecy game on the right.
Actually, let me reconsider whether I can skip some intermediate games by having the compositions match directly between steps. Looking back at the reference proof, they use intermediate games as bridges between different reductions, so I probably need them all. The question is whether the engine can verify that consecutive games are interchangeable without an explicit intermediate step, or if I need to spell out each transition.
Let me count what this would look like: starting with the Left game, then for each assumption hop I'd need games to transition from one reduction to the next. With three OTPUniform hops and one PRG hop, that's potentially a lot of games, but some might be shared or skippable depending on how the reductions compose.
Actually, looking back at the user's outline about hopping to a game where the Eavesdrop oracle evaluates G on k instead of k + r—that's the key insight since k + r acts as a one-time pad. Let me see if I can structure the hops more efficiently around that observation rather than mechanically applying four steps per assumption. of r, so it looks uniform.
Wait, the user says "G on k, not k + r". So the first hop replaces G(k + r) with G(k). The argument is that k + r is uniform when k is uniform, so replacing k + r with k (which is also uniform) is fine. Hmm but that's not quite the same as what I was planning.
Actually, thinking about it differently: the user wants to replace k + r with just k. Since k is uniform and independent, k + r and k have the same distribution (both uniform over BitString
After this hop, the code evaluates the PRG on k instead of k + r, making k the PRG seed. Then the PRG hop replaces G(k) with a random sample, followed by an OTP hop that replaces the XOR of that random sample with mL with another random sample. Finally, I mirror the argument for the right message. user's outline has: 1. OTPUniform: G(k+r) -> G(k) [argument: k+r is uniform same as k] 2. PRG Security: G(k) -> random z 3. OTPUniform: z + mL -> random [argument: z is uniform, so z + mL is uniform] 4-6. Mirror of 1-3 for mR
For hop 1, the OTPUniform argument works because k is uniform and independent of r, making k+r uniform as well, so G(k+r) and G(k) have the same distribution. But to formalize this reduction, I need to think about how OTPUniform actually applies here—the reduction would call the challenger on r to get either k+r or a fresh uniform value, then feed that to G, which shifts the hop from G(k+r) to G(k) into a hop from G(k+r) to G(s) where s is uniformly random.
Since G(s) and G(k) are identically distributed when both inputs are uniform, the intermediate game after applying OTPUniform would sample a fresh uniform value and evaluate G on it, which is syntactically equivalent to sampling k uniformly and evaluating G on k—the variable names get normalized in the canonical form anyway.
Let me be more precise about what the intermediate game should look like: the Eavesdrop oracle samples k uniformly, then r uniformly, evaluates G on k (not on k + r), and returns r concatenated with the result of G(k) plus the left message.
Now I'll write out the full reduction for the first OTP hop and verify it against the ProofFrog tools. The distributions are equivalent, so the intermediate game where I evaluate G on a fresh random value should be indistinguishable from evaluating it on k itself. Now I'm going to write out the actual scheme and proof files to verify this step by step using the tools available.
Setting up the scheme file... Finishing the decryption logic and now sketching out the security proof structure with a sequence of games that will bridge from the left encryption oracle down to the random case, using the PRG's stretch property as the key assumption. I'm continuing through the security reduction chain, moving from the left side to the middle and then the right side of the protocol. Each step either applies a cryptographic assumption or shows equivalence between game variants, progressively transforming the adversary's view until both message halves are equally hidden. I'm checking whether some of these intermediate games are actually redundant by seeing if adjacent compositions can be directly swapped. Specifically, I'm wondering if I even need the Intermediate_GkL game—the OTPUniform.Random and Security(G).Real compositions might be directly interchangeable if their canonical forms align. Let me trace through what OTPUniform.Random compose R_OTP_L1 actually produces when I inline everything.
Inlining the Security(G).Real composition...
Both step 3 and step 5 produce identical game code, so I can skip the intermediate step entirely—the transition should go directly from step 3 to step 5 since they're interchangeable. The question is whether the proof engine recognizes they're equivalent, since each adjacent pair of games should either be interchangeable or rely on an assumption hop.
Let me trace through all the transitions to identify which intermediate games are actually necessary and which ones I can eliminate. I'm verifying that both games reduce to the same canonical form—where we have a random lambda-bit string concatenated with a random 2*lambda-bit string—confirming no intermediate reduction is needed. Now checking the transition between the uniform random case and the middle game, where the challenger's response becomes purely random rather than dependent on the message. could potentially be matched directly with the middle game (which is the same thing) or with the reverse OTPUniform composition.
Actually, we DO need the middle game Intermediate_Mid because we need to transition from the "left" side to the "right" side. The OTPUniform.Random compose R_OTP_L2 and OTPUniform.Random compose R_OTP_R2 would both produce the same canonical form (both are r || c with c random), so they should be interchangeable directly! So we might be able to skip the middle game too:
These should be interchangeable.
So the optimized proof sequence would chain through the left OTP game with the first key, then the PRG security assumption, then the left OTP game with the expanded key, and finally jump directly to the right OTP game with the expanded key since they have the same canonical form, before concluding with the right OTP game in real mode.
Let me be more careful and pragmatic here. I'll write out the scheme first to make sure it's sound, then build the proof incrementally starting with just the endpoints and filling in intermediate games as needed.
Now I'm thinking through the reductions more carefully, particularly how the OTP uniform hop works on the left side.
I need to reconsider the parameter rules for reductions—the parameter list has to include everything needed to instantiate the composed security game, so if OTPUniform needs G.lambda from the PRG G, then G itself must be a parameter even though it comes from E.
Looking at the pattern, reduction parameters should cover the scheme, primitive, and any necessary integers. The key is making sure all dependencies for game instantiation are accounted for.
Now I'm setting up the PRG hop reduction on the left side...
Defining the reduction structure... Defining the remaining reductions... Writing the proof files...
Now I'm checking whether I need an intermediate game step between the left and right reductions, or if they both collapse to the same uniform output directly.
Good, I now have a solid understanding of the patterns. Let me create the scheme and proof.
Todos have been modified successfully. Ensure that you continue to use the todo list to track your progress. Please proceed with the current tasks if applicable
{
"path": "examples/Schemes/SymEnc/FunkyPRGSymEnc.scheme",
"content": "import '../../Primitives/SymEnc.primitive';\nimport '../../Primitives/PRG.primitive';\n\nScheme FunkyPRGSymEnc(PRG G) extends SymEnc {\n requires G.stretch == G.lambda;\n\n Int lambda = G.lambda;\n\n Set Key = BitString<lambda>;\n Set Message = BitString<2 * lambda>;\n Set Ciphertext = BitString<3 * lambda>;\n\n Key KeyGen() {\n Key k <- Key;\n return k;\n }\n\n Ciphertext Enc(Key k, Message m) {\n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> z = G.evaluate(k + r);\n return r || (z + m);\n }\n\n Message Dec(Key k, Ciphertext c) {\n BitString<lambda> r = c[0 : lambda];\n BitString<2 * lambda> y = c[lambda : 3 * lambda];\n BitString<2 * lambda> z = G.evaluate(k + r);\n return y + z;\n }\n}\n"
}{"success":true,"path":"/Users/dstebila/Downloads/tmp/ProofFrog-Fresh/examples/Schemes/SymEnc/FunkyPRGSymEnc.scheme"}{"output":"/Users/dstebila/Downloads/tmp/ProofFrog-Fresh/examples/Schemes/SymEnc/FunkyPRGSymEnc.scheme is well-formed.","success":true}Todos have been modified successfully. Ensure that you continue to use the todo list to track your progress. Please proceed with the current tasks if applicable
{
"path": "examples/Proofs/SymEnc/FunkyPRGSymEncOTS.proof",
"content": "// Main result: FunkyPRGSymEnc satisfies OneTimeSecrecy.\n//\n// High-level proof idea:\n// FunkyPRGSymEnc encrypts as: sample r, compute z = G(k + r), return r || (z + m).\n// We show the left and right encryptions are indistinguishable via a sequence of\n// game hops that (1) replace k + r with a uniform value using OTPUniform,\n// (2) replace G(seed) with a uniform string using PRG security, (3) replace\n// z + m with a uniform string using OTPUniform, arriving at a game independent\n// of the message. The second half mirrors these hops to reintroduce mR.\n//\n// Game sequence:\n// Game 0: OneTimeSecrecy.Left -- encrypt mL with G(k + r)\n// Game 1: Replace k + r with uniform seed (OTPUniform on lambda bits)\n// Game 2: Replace G(seed) with uniform z (PRG security)\n// Game 3: Replace z + mL with uniform c (OTPUniform on 2*lambda bits)\n// Game 4: Replace uniform c with z + mR (OTPUniform on 2*lambda bits, reverse)\n// Game 5: Replace uniform z with G(seed) (PRG security, reverse)\n// Game 6: Replace uniform seed with k + r (OTPUniform on lambda bits, reverse)\n// Game 7: OneTimeSecrecy.Right -- encrypt mR with G(k + r)\n\nimport '../../Schemes/SymEnc/FunkyPRGSymEnc.scheme';\nimport '../../Primitives/PRG.primitive';\nimport '../../Games/SymEnc/OneTimeSecrecy.game';\nimport '../../Games/PRG/Security.game';\nimport '../../Games/Misc/OTPUniform.game';\n\n// Reduction for OTPUniform hop on k + r (left side).\n// Calls challenger.CTXT(r) to get either k + r (Real) or uniform s (Random),\n// then evaluates G on the result and XORs with mL.\nReduction R_OTP_L1(FunkyPRGSymEnc E, PRG G) compose OTPUniform(G.lambda) against OneTimeSecrecy(E).Adversary {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n BitString<G.lambda> r <- BitString<G.lambda>;\n BitString<G.lambda> s = challenger.CTXT(r);\n BitString<2 * G.lambda> z = G.evaluate(s);\n return r || (z + mL);\n }\n}\n\n// Reduction for PRG hop (left side).\n// Calls challenger.Query() to get either G(seed) (Real) or uniform z (Random),\n// then XORs with mL.\nReduction R_PRG_L(FunkyPRGSymEnc E, PRG G) compose Security(G) against OneTimeSecrecy(E).Adversary {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n BitString<G.lambda> r <- BitString<G.lambda>;\n BitString<2 * G.lambda> z = challenger.Query();\n return r || (z + mL);\n }\n}\n\n// Reduction for OTPUniform hop on z + mL (left side).\n// Calls challenger.CTXT(mL) to get either z + mL (Real) or uniform c (Random).\nReduction R_OTP_L2(FunkyPRGSymEnc E, PRG G) compose OTPUniform(2 * G.lambda) against OneTimeSecrecy(E).Adversary {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n BitString<G.lambda> r <- BitString<G.lambda>;\n BitString<2 * G.lambda> c = challenger.CTXT(mL);\n return r || c;\n }\n}\n\n// Reduction for OTPUniform hop on z + mR (right side).\n// Calls challenger.CTXT(mR) to get either z + mR (Real) or uniform c (Random).\nReduction R_OTP_R2(FunkyPRGSymEnc E, PRG G) compose OTPUniform(2 * G.lambda) against OneTimeSecrecy(E).Adversary {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n BitString<G.lambda> r <- BitString<G.lambda>;\n BitString<2 * G.lambda> c = challenger.CTXT(mR);\n return r || c;\n }\n}\n\n// Reduction for PRG hop (right side).\n// Calls challenger.Query() to get either G(seed) (Real) or uniform z (Random),\n// then XORs with mR.\nReduction R_PRG_R(FunkyPRGSymEnc E, PRG G) compose Security(G) against OneTimeSecrecy(E).Adversary {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n BitString<G.lambda> r <- BitString<G.lambda>;\n BitString<2 * G.lambda> z = challenger.Query();\n return r || (z + mR);\n }\n}\n\n// Reduction for OTPUniform hop on k + r (right side).\n// Calls challenger.CTXT(r) to get either k + r (Real) or uniform s (Random),\n// then evaluates G on the result and XORs with mR.\nReduction R_OTP_R1(FunkyPRGSymEnc E, PRG G) compose OTPUniform(G.lambda) against OneTimeSecrecy(E).Adversary {\n E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {\n BitString<G.lambda> r <- BitString<G.lambda>;\n BitString<G.lambda> s = challenger.CTXT(r);\n BitString<2 * G.lambda> z = G.evaluate(s);\n return r || (z + mR);\n }\n}\n\nproof:\n\nlet:\n Int lambda;\n PRG G = PRG(lambda, lambda);\n FunkyPRGSymEnc E = FunkyPRGSymEnc(G);\n\nassume:\n Security(G);\n OTPUniform(lambda);\n OTPUniform(2 * lambda);\n\ntheorem:\n OneTimeSecrecy(E);\n\ngames:\n // Game 0: Original left game -- Enc(k, mL) = r || (G(k+r) + mL)\n OneTimeSecrecy(E).Left against OneTimeSecrecy(E).Adversary;\n\n // Hop 1: OTPUniform on k + r -- replace k + r with uniform seed\n OTPUniform(lambda).Real compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;\n OTPUniform(lambda).Random compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;\n\n // Hop 2: PRG security -- replace G(seed) with uniform z\n Security(G).Real compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;\n Security(G).Random compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;\n\n // Hop 3: OTPUniform on z + mL -- replace z + mL with uniform c\n OTPUniform(2 * lambda).Real compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;\n OTPUniform(2 * lambda).Random compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;\n\n // Middle: r || c with c uniform -- independent of message\n\n // Hop 4: OTPUniform on z + mR (reverse) -- reintroduce mR\n OTPUniform(2 * lambda).Random compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;\n OTPUniform(2 * lambda).Real compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;\n\n // Hop 5: PRG security (reverse) -- reintroduce G(seed)\n Security(G).Random compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;\n Security(G).Real compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;\n\n // Hop 6: OTPUniform on k + r (reverse) -- reintroduce k + r\n OTPUniform(lambda).Random compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;\n OTPUniform(lambda).Real compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;\n\n // Game 7: Original right game -- Enc(k, mR) = r || (G(k+r) + mR)\n OneTimeSecrecy(E).Right against OneTimeSecrecy(E).Adversary;\n"
}{"success":true,"path":"/Users/dstebila/Downloads/tmp/ProofFrog-Fresh/examples/Proofs/SymEnc/FunkyPRGSymEncOTS.proof"}{"output":"/Users/dstebila/Downloads/tmp/ProofFrog-Fresh/examples/Proofs/SymEnc/FunkyPRGSymEncOTS.proof is well-formed.","success":true}{"output":"===STEP 1===\nReduction to apply:\nReduction R_OTP_L1() compose OTPUniform(lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT(r);\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mL;\n }\n}\n\nChallenger:\nGame Real() {\n BitString<lambda> CTXT(BitString<lambda> m) { \n BitString<lambda> k <- BitString<lambda>;\n return k + m;\n }\n}\n\nCurrent: OneTimeSecrecy(E).Left against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(lambda).Real compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;\n\nSIMPLIFYING CURRENT GAME\nGame Left() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> E.KeyGen@k0 <- BitString<lambda>;\n BitString<lambda> k = E.KeyGen@k0;\n BitString<lambda> E.Enc@r2 <- BitString<lambda>;\n BitString<2 * lambda> E.Enc@z2 = G.evaluate(k + E.Enc@r2);\n BitString<3 * lambda> c = E.Enc@r2 || E.Enc@z2 + mL;\n return c;\n }\n}\n\nSIMPLIFYING NEXT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> challenger.CTXT@k1 <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT@k1 + r;\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mL;\n }\n}\n\nCURRENT\nGame Left() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2 + v1) + mL;\n }\n}\n\nNEXT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2 + v1) + mL;\n }\n}\n\nInline Success!\n===STEP 2===\nCurrent: OTPUniform(lambda).Real compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(lambda).Random compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;\n\nValid by assumption\n===STEP 3===\nReduction to apply:\nReduction R_OTP_L1() compose OTPUniform(lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT(r);\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mL;\n }\n}\n\nChallenger:\nGame Random() {\n BitString<lambda> CTXT(BitString<lambda> m) { \n BitString<lambda> c <- BitString<lambda>;\n return c;\n }\n}\n\nReduction to apply:\nReduction R_PRG_L() compose Security(G) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> z = challenger.Query();\n return r || z + mL;\n }\n}\n\nChallenger:\nGame Real() {\n BitString<lambda + lambda> Query() { \n BitString<lambda> s <- BitString<lambda>;\n return G.evaluate(s);\n }\n}\n\nCurrent: OTPUniform(lambda).Random compose R_OTP_L1(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: Security(G).Real compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;\n\nSIMPLIFYING CURRENT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> challenger.CTXT@c1 <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT@c1;\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mL;\n }\n}\n\nSIMPLIFYING NEXT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> challenger.Query@s1 <- BitString<lambda>;\n BitString<2 * lambda> z = G.evaluate(challenger.Query@s1);\n return r || z + mL;\n }\n}\n\nCURRENT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2) + mL;\n }\n}\n\nNEXT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2) + mL;\n }\n}\n\nInline Success!\n===STEP 4===\nCurrent: Security(G).Real compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: Security(G).Random compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;\n\nValid by assumption\n===STEP 5===\nReduction to apply:\nReduction R_PRG_L() compose Security(G) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> z = challenger.Query();\n return r || z + mL;\n }\n}\n\nChallenger:\nGame Random() {\n BitString<lambda + lambda> Query() { \n BitString<lambda + lambda> r <- BitString<lambda + lambda>;\n return r;\n }\n}\n\nReduction to apply:\nReduction R_OTP_L2() compose OTPUniform(2 * lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> c = challenger.CTXT(mL);\n return r || c;\n }\n}\n\nChallenger:\nGame Real() {\n BitString<2 * lambda> CTXT(BitString<2 * lambda> m) { \n BitString<2 * lambda> k <- BitString<2 * lambda>;\n return k + m;\n }\n}\n\nCurrent: Security(G).Random compose R_PRG_L(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(2 * lambda).Real compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;\n\nSIMPLIFYING CURRENT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda + lambda> challenger.Query@r1 <- BitString<lambda + lambda>;\n BitString<2 * lambda> z = challenger.Query@r1;\n return r || z + mL;\n }\n}\n\nSIMPLIFYING NEXT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> challenger.CTXT@k1 <- BitString<2 * lambda>;\n BitString<2 * lambda> c = challenger.CTXT@k1 + mL;\n return r || c;\n }\n}\n\nCURRENT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<2 * lambda> v2 <- BitString<2 * lambda>;\n return v1 || v2 + mL;\n }\n}\n\nNEXT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<2 * lambda> v2 <- BitString<2 * lambda>;\n return v1 || v2 + mL;\n }\n}\n\nInline Success!\n===STEP 6===\nCurrent: OTPUniform(2 * lambda).Real compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(2 * lambda).Random compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;\n\nValid by assumption\n===STEP 7===\nReduction to apply:\nReduction R_OTP_L2() compose OTPUniform(2 * lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> c = challenger.CTXT(mL);\n return r || c;\n }\n}\n\nChallenger:\nGame Random() {\n BitString<2 * lambda> CTXT(BitString<2 * lambda> m) { \n BitString<2 * lambda> c <- BitString<2 * lambda>;\n return c;\n }\n}\n\nReduction to apply:\nReduction R_OTP_R2() compose OTPUniform(2 * lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> c = challenger.CTXT(mR);\n return r || c;\n }\n}\n\nChallenger:\nGame Random() {\n BitString<2 * lambda> CTXT(BitString<2 * lambda> m) { \n BitString<2 * lambda> c <- BitString<2 * lambda>;\n return c;\n }\n}\n\nCurrent: OTPUniform(2 * lambda).Random compose R_OTP_L2(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(2 * lambda).Random compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;\n\nSIMPLIFYING CURRENT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> challenger.CTXT@c1 <- BitString<2 * lambda>;\n BitString<2 * lambda> c = challenger.CTXT@c1;\n return r || c;\n }\n}\n\nSIMPLIFYING NEXT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> challenger.CTXT@c1 <- BitString<2 * lambda>;\n BitString<2 * lambda> c = challenger.CTXT@c1;\n return r || c;\n }\n}\n\nCURRENT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<2 * lambda> v2 <- BitString<2 * lambda>;\n return v1 || v2;\n }\n}\n\nNEXT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<2 * lambda> v2 <- BitString<2 * lambda>;\n return v1 || v2;\n }\n}\n\nInline Success!\n===STEP 8===\nCurrent: OTPUniform(2 * lambda).Random compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(2 * lambda).Real compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;\n\nValid by assumption\n===STEP 9===\nReduction to apply:\nReduction R_OTP_R2() compose OTPUniform(2 * lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> c = challenger.CTXT(mR);\n return r || c;\n }\n}\n\nChallenger:\nGame Real() {\n BitString<2 * lambda> CTXT(BitString<2 * lambda> m) { \n BitString<2 * lambda> k <- BitString<2 * lambda>;\n return k + m;\n }\n}\n\nReduction to apply:\nReduction R_PRG_R() compose Security(G) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> z = challenger.Query();\n return r || z + mR;\n }\n}\n\nChallenger:\nGame Random() {\n BitString<lambda + lambda> Query() { \n BitString<lambda + lambda> r <- BitString<lambda + lambda>;\n return r;\n }\n}\n\nCurrent: OTPUniform(2 * lambda).Real compose R_OTP_R2(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: Security(G).Random compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;\n\nSIMPLIFYING CURRENT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> challenger.CTXT@k1 <- BitString<2 * lambda>;\n BitString<2 * lambda> c = challenger.CTXT@k1 + mR;\n return r || c;\n }\n}\n\nSIMPLIFYING NEXT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda + lambda> challenger.Query@r1 <- BitString<lambda + lambda>;\n BitString<2 * lambda> z = challenger.Query@r1;\n return r || z + mR;\n }\n}\n\nCURRENT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<2 * lambda> v2 <- BitString<2 * lambda>;\n return v1 || v2 + mR;\n }\n}\n\nNEXT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<2 * lambda> v2 <- BitString<2 * lambda>;\n return v1 || v2 + mR;\n }\n}\n\nInline Success!\n===STEP 10===\nCurrent: Security(G).Random compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: Security(G).Real compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;\n\nValid by assumption\n===STEP 11===\nReduction to apply:\nReduction R_PRG_R() compose Security(G) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<2 * lambda> z = challenger.Query();\n return r || z + mR;\n }\n}\n\nChallenger:\nGame Real() {\n BitString<lambda + lambda> Query() { \n BitString<lambda> s <- BitString<lambda>;\n return G.evaluate(s);\n }\n}\n\nReduction to apply:\nReduction R_OTP_R1() compose OTPUniform(lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT(r);\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mR;\n }\n}\n\nChallenger:\nGame Random() {\n BitString<lambda> CTXT(BitString<lambda> m) { \n BitString<lambda> c <- BitString<lambda>;\n return c;\n }\n}\n\nCurrent: Security(G).Real compose R_PRG_R(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(lambda).Random compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;\n\nSIMPLIFYING CURRENT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> challenger.Query@s1 <- BitString<lambda>;\n BitString<2 * lambda> z = G.evaluate(challenger.Query@s1);\n return r || z + mR;\n }\n}\n\nSIMPLIFYING NEXT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> challenger.CTXT@c1 <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT@c1;\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mR;\n }\n}\n\nCURRENT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2) + mR;\n }\n}\n\nNEXT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2) + mR;\n }\n}\n\nInline Success!\n===STEP 12===\nCurrent: OTPUniform(lambda).Random compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OTPUniform(lambda).Real compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;\n\nValid by assumption\n===STEP 13===\nReduction to apply:\nReduction R_OTP_R1() compose OTPUniform(lambda) against OneTimeSecrecy(E).Adversary {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT(r);\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mR;\n }\n}\n\nChallenger:\nGame Real() {\n BitString<lambda> CTXT(BitString<lambda> m) { \n BitString<lambda> k <- BitString<lambda>;\n return k + m;\n }\n}\n\nCurrent: OTPUniform(lambda).Real compose R_OTP_R1(E, G) against OneTimeSecrecy(E).Adversary;\nHop To: OneTimeSecrecy(E).Right against OneTimeSecrecy(E).Adversary;\n\nSIMPLIFYING CURRENT GAME\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> r <- BitString<lambda>;\n BitString<lambda> challenger.CTXT@k1 <- BitString<lambda>;\n BitString<lambda> s = challenger.CTXT@k1 + r;\n BitString<2 * lambda> z = G.evaluate(s);\n return r || z + mR;\n }\n}\n\nSIMPLIFYING NEXT GAME\nGame Right() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> E.KeyGen@k0 <- BitString<lambda>;\n BitString<lambda> k = E.KeyGen@k0;\n BitString<lambda> E.Enc@r2 <- BitString<lambda>;\n BitString<2 * lambda> E.Enc@z2 = G.evaluate(k + E.Enc@r2);\n BitString<3 * lambda> c = E.Enc@r2 || E.Enc@z2 + mR;\n return c;\n }\n}\n\nCURRENT\nGame Inlined() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2 + v1) + mR;\n }\n}\n\nNEXT\nGame Right() {\n BitString<3 * lambda> Eavesdrop(BitString<2 * lambda> mL, BitString<2 * lambda> mR) { \n BitString<lambda> v1 <- BitString<lambda>;\n BitString<lambda> v2 <- BitString<lambda>;\n return v1 || G.evaluate(v2 + v1) + mR;\n }\n}\n\nInline Success!\nProof Suceeded!\n","success":true,"hop_results":[{"step_num":1,"valid":true,"kind":"equivalent"},{"step_num":2,"valid":true,"kind":"by_assumption"},{"step_num":3,"valid":true,"kind":"equivalent"},{"step_num":4,"valid":true,"kind":"by_assumption"},{"step_num":5,"valid":true,"kind":"equivalent"},{"step_num":6,"valid":true,"kind":"by_assumption"},{"step_num":7,"valid":true,"kind":"equivalent"},{"step_num":8,"valid":true,"kind":"by_assumption"},{"step_num":9,"valid":true,"kind":"equivalent"},{"step_num":10,"valid":true,"kind":"by_assumption"},{"step_num":11,"valid":true,"kind":"equivalent"},{"step_num":12,"valid":true,"kind":"by_assumption"},{"step_num":13,"valid":true,"kind":"equivalent"}]}Todos have been modified successfully. Ensure that you continue to use the todo list to track your progress. Please proceed with the current tasks if applicable
Here's a summary of what was created:
Scheme: FunkyPRGSymEnc.scheme - A symmetric encryption scheme parameterized by a PRG G with stretch == lambda. Key is BitString<lambda>, message is BitString<2*lambda>, ciphertext is BitString<3*lambda>. Encryption samples r, computes z = G(k + r), and returns r || (z + m).
Proof: FunkyPRGSymEncOTS.proof - All 13 hops verified successfully. The proof uses 6 reductions and no explicit intermediate games (the compositions chain directly):
R_OTP_L1: Replace G(k+r) with G(s) where s is uniform (since k+r is a one-time pad of r)R_PRG_L: Replace G(s) with uniform zR_OTP_L2: Replace z + mL with uniform cR_OTP_R2 (reverse): Reintroduce mR as z + mRR_PRG_R (reverse): Reintroduce G(s)R_OTP_R1 (reverse): Reintroduce k+r