Doing expand get, insert and prove unique annotations... No change.
Doing simplify (non-expanded game)... No change.
Doing expand... Done.
Doing remove assignments of findcond... Done.
Doing simplify... Run simplify 1 time(s). Fixpoint reached.
No change.
Doing move all binders... No change.
Doing SA rename new without array accesses and remove assignments of findcond... No change.
Doing merge branches... No change.
Proof of (one-session) secrecy of s failed:
  at 16, bad usage(s) of c, which may depend on s.
Trying equivalence ind_cpa(enc)... Transf. OK Proba. computed Transf. done Succeeded.
Doing simplify (non-expanded game)... No change.
Doing expand... Done.
Doing remove assignments of findcond... Done.
Doing simplify... Run simplify 1 time(s). Fixpoint reached.
No change.
Doing move all binders... No change.
Doing SA rename new without array accesses and remove assignments of findcond... No change.
Doing merge branches... No change.
Proof of (one-session) secrecy of s failed:
  at 17, bad usage(s) of c, which may depend on s.
Sorry, the following queries remain unproved:
- secrecy of s
===================== Proof starts =======================
Initial state
Game 1 is
     cstart() :=
     k <-R key;
     return();
     foreach i <= N do
     cs() :=
     s <-R cleartext;
     c: ciphertext <- (m: cleartext <- s; k_1: key <- k; r <-R enc_seed; enc_r(m, k_1, r));
     return(c)


Applying expand
  - Expand if/find/let
yields

Game 2 is
     cstart() :=
     k <-R key;
     return();
     foreach i <= N do
     cs() :=
     s <-R cleartext;
     m: cleartext <- s;
     k_1: key <- k;
     r <-R enc_seed;
     c: ciphertext <- enc_r(m, k_1, r);
     return(c)


Applying remove assignments of findcond
  - Remove assignments on m (definition removed, all usages removed)
  - Remove assignments on k_1 (definition removed, all usages removed)
yields

Game 3 is
     cstart() :=
     k <-R key;
     return();
     foreach i <= N do
     cs() :=
     s <-R cleartext;
     r <-R enc_seed;
     c: ciphertext <- enc_r(s, k, r);
     return(c)


Applying equivalence ind_cpa(enc) [probability Penc(time_1, N)]
  - Equivalence ind_cpa(enc) with variables: k -> k_2, r -> r_1
yields

Game 4 is
     cstart() :=
     k_2 <-R key;
     return();
     foreach i <= N do
     cs() :=
     s <-R cleartext;
     r_1 <-R enc_seed;
     c: ciphertext <- (x: cleartext <- s; enc_r'(Z(x), k_2, r_1));
     return(c)


Applying expand
  - Expand if/find/let
yields

Game 5 is
     cstart() :=
     k_2 <-R key;
     return();
     foreach i <= N do
     cs() :=
     s <-R cleartext;
     r_1 <-R enc_seed;
     x: cleartext <- s;
     c: ciphertext <- enc_r'(Z(x), k_2, r_1);
     return(c)


Applying remove assignments of findcond
  - Remove assignments on x (definition removed, all usages removed)
yields

Game 6 is
     cstart() :=
     k_2 <-R key;
     return();
     foreach i <= N do
     cs() :=
     s <-R cleartext;
     r_1 <-R enc_seed;
     c: ciphertext <- enc_r'(Z(s), k_2, r_1);
     return(c)

RESULT time_1 = time
RESULT Could not prove secrecy of s.