fact: Definition RF_Encrypt_bad (x : Bvector eta)(z : list (Bvector eta * Bvector eta) * bool) (p : Bvector eta):= [s, bad] <-2 z; r <-$ { 0 , 1 }^eta; z <-$ PRFE_RandomFunc s r; [pad, s0]<-2 z; ret (r, p xor pad, (s0, bad || eqb x r)).
imports: FCF PRF Encryption RndInList OTP WC_PolyTime