fact: Definition B(g_xyz : (GroupElement * GroupElement * GroupElement)) : Comp bool := [gx, gy, gz] <-3 g_xyz; [p0, p1, s] <-$3 A1(gx); b <-$ {0,1}; pb <- if b then p0 else p1; c <- (gy, gz * pb); b' <-$ (A2 (c, s)); ret (b ?= b').
imports: FCF RndGrpElem Encryption_PK DiffieHellman OTP