proposition: Theorem RF_Encrypt_bad_prob : forall x (a : list (Bvector eta * Bvector eta)) (b : Plaintext), (Pr [d <-$ RF_Encrypt_bad x (a, false) b; ret snd (snd d) ] <= 1 / (2 ^ eta))%rat.
proof: Proof. intuition. unfold RF_Encrypt_bad. assert ( Pr [d <-$ (r <-$ { 0 , 1 }^eta; z <-$ PRFE_RandomFunc a r; [pad, s0]<-2 z; ret (r, b xor pad, (s0, false || eqb x r))); ret snd (snd d) ] == Pr [r <-$ { 0 , 1 }^eta; ret eqb x r] ). inline_first. comp_skip. inline_first. comp_irr_l. eapply randomFunc_wf; wftac. comp_simp. simpl; intuition. rewrite H. clear H. Local Transparent evalDist. simpl. Local Opaque evalDist. rewrite (@sumList_exactly_one _ x). rewrite eqbBvector_complete. destruct (EqDec_dec bool_EqDec true true ); intuition. rewrite ratMult_1_r. eapply leRat_refl. eapply getAllBvectors_NoDup. eapply in_getAllBvectors. intuition. destruct ( EqDec_dec bool_EqDec (eqbBvector x b0) true); intuition. apply eqbBvector_sound in e; subst; intuition. eapply ratMult_0_r. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime