Tactic eager while is unsound #771
Description
The eager while tactic allows to prove an equivalence between the following distinguishable functions:
module A : Test = {
proc f(b) = { (* f(true) = false *)
var x <- !b;
while (b) {
b <- !b;
}
return x;
}
}.
module B : Test = {
proc f(b) = { (* f(true) = true *)
var x;
while (b) {
b <- !b;
}
x <- !b;
return x;
}
}.as in:
equiv e_eq : A.f ~ B.f : ={arg} ==> ={res}.
proc.
eager while (
H: x <- !b;
~ x <- !b;
: ={b} ==> ={x}); auto.
qed.I did not investigate the logic of eager while for now, so I don't know how important the changes are to patch this.
Complete proof of false
falsePlease note that:
- The path I used is probably not the shortest but is quite intuitive: functions are supposed to be
indistinguishable yet they differ on the inputtrue, which can be used to make a distinguisher. - I am struggling with Phoare so I did use an ugly detour via
equivwith dummy modules that
respondtrueorfalseall the time. I'm sorry.
require import Real.
module type Test = {
proc f(b : bool) : bool
}.
module A : Test = {
proc f(b) = { (* f(true) = false *)
var x <- !b;
while (b) {
b <- !b;
}
return x;
}
}.
module B : Test = {
proc f(b) = { (* f(true) = true *)
var x;
while (b) {
b <- !b;
}
x <- !b;
return x;
}
}.
(* abnormal *)
equiv e_eq : A.f ~ B.f : ={arg} ==> ={res}.
proc.
eager while (
H: x <- !b;
~ x <- !b;
: ={b} ==> ={x}); auto.
qed.
module type Adversary (O : Test) = {
proc distinguish() : bool
}.
section Ind.
declare module Adv <: Adversary.
lemma ind_A_B &m :
Pr [ Adv(A).distinguish() @ &m : res ] =
Pr [ Adv(B).distinguish() @ &m : res ].
proof.
byequiv. proc (true); 1,2: by smt().
- exact e_eq.
- done.
done.
qed.
end section Ind.
module (D : Adversary)(O : Test) = {
proc distinguish() = {
var r;
r <@ O.f(true);
return r;
}
}.
module (Yes : Adversary)(O : Test) = {
(* I am very sorry for this... *)
proc distinguish() = {
return true;
}
}.
lemma D_on_B &m :
Pr [ D(B).distinguish() @ &m : res ] = 1%r.
proof.
have<-: Pr [ Yes(B).distinguish() @ &m : res ] = 1%r.
- byphoare; by try proc; auto => />.
byequiv; 2,3: by auto.
proc. inline B.f. wp. sp.
rcondt{1} ^while. auto. sp.
rcondf{1} ^while; auto.
qed.
module (No : Adversary)(O : Test) = {
(* I am very sorry for this... *)
proc distinguish() = {
return false;
}
}.
lemma D_on_A &m :
Pr [ D(A).distinguish() @ &m : res ] = 0%r.
proof.
have<-: Pr [ No(A).distinguish() @ &m : res ] = 0%r.
- byphoare; by try proc; auto => />.
byequiv; 2,3: by auto.
proc. inline A.f. wp. sp.
rcondt{1} ^while. auto. sp.
rcondf{1} ^while; auto.
qed.
lemma false: false.
have : forall &m, 0%r = 1%r; last by trivial.
move => &m.
rewrite -(D_on_A &m) -(D_on_B &m).
by apply (ind_A_B D).
qed.Metadata
Metadata
Assignees
Labels
No labels