(* xor-loop.ec *) prover quorum=2 ["Z3" "Alt-Ergo"]. require import AllCore IntDiv. (* a type mybool with elements tt standing for "true" and ff standing for "false", and an exclusive or operator ^^: *) type mybool = [tt | ff]. op (^^) : mybool -> mybool -> mybool. (* we can write x ^^ y instead of (^^) x y ^^ is left associatve, so x ^^ y ^^ z means (x ^^ y) ^^ z *) (* axioms defining exclusive or (nosmt means these axioms aren't available to the SMT provers): *) axiom nosmt xor_tt_tt : tt ^^ tt = ff. axiom nosmt xor_tt_ff : tt ^^ ff = tt. axiom nosmt xor_ff_tt : ff ^^ tt = tt. axiom nosmt xor_ff_ff : ff ^^ ff = ff. (* lemmas for exclusive or: *) (* false on the right *) lemma xor_ff (x : mybool) : x ^^ ff = x. proof. case x. apply xor_tt_ff. apply xor_ff_ff. qed. (* cancelling *) lemma xorK (x : mybool) : x ^^ x = ff. proof. case x. apply xor_tt_tt. apply xor_ff_ff. qed. (* commutativity *) lemma xorC (x y : mybool) : x ^^ y = y ^^ x. case x. case y => //. by rewrite xor_tt_ff xor_ff_tt. case y => //. by rewrite xor_ff_tt xor_tt_ff. qed. (* associativity *) lemma xorA (x y z : mybool) : (x ^^ y) ^^ z = x ^^ (y ^^ z). proof. case x. case y. rewrite xor_tt_tt. case z. by rewrite xor_ff_tt xor_tt_tt xor_tt_ff. by rewrite xor_ff_ff xor_tt_ff xor_tt_tt. case z. by rewrite xor_tt_ff xor_tt_tt xor_ff_tt xor_tt_tt. by rewrite xor_tt_ff xor_tt_ff xor_ff_ff xor_tt_ff. case y. rewrite xor_ff_tt. case z. by rewrite xor_tt_tt xor_ff_ff. by rewrite xor_tt_ff xor_ff_tt. case z. by rewrite xor_ff_ff xor_ff_tt xor_ff_tt. by rewrite xor_ff_ff xor_ff_ff. qed. (* define even, odd : int -> bool SMT provers know about %%, so smt() can reason about even and odd *) op even (k : int) = k %% 2 = 0. (* %% is mod *) op odd (k : int) = ! even k. module M = { proc f(n : int, (* public *) x : mybool, (* public *) y : mybool) (* private *) : mybool = { (* public *) var i : int; (* not visible to observer *) var b : mybool; (* not visible to observer, but returned *) i <- 0; b <- x; if (0 <= n) { while (i < n) { b <- b ^^ y; i <- i + 1; } if (odd n) { b <- b ^^ y; } } return b; } }. (* four noninterference proofs are below: *) lemma noninter1 : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. proc => /=. seq 2 2 : (={n, i, b} /\ i{1} = 0). auto. if => //. seq 1 1 : (={n} /\ (even n{1} => ={b}) /\ (odd n{1} => b{1} ^^ y{1} = b{2} ^^ y{2})). while (={n, i} /\ i{1} <= n{1} /\ (even i{1} => ={b}) /\ (odd i{1} => b{1} ^^ y{1} = b{2} ^^ y{2})). auto; smt(xorA xorK). auto; smt(). auto; smt(). qed. lemma noninter1' : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. proc => /=. seq 2 2 : (={n, i, b} /\ i{1} = 0). auto. if => //. wp. while (={n, i} /\ i{1} <= n{1} /\ (even i{1} => ={b}) /\ (odd i{1} => b{1} ^^ y{1} = b{2} ^^ y{2})). auto; smt(xorA xorK). auto; smt(). qed. lemma noninter2 : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. proc => /=. seq 2 2 : (={n, x, i, b} /\ i{1} = 0 /\ b{1} = x{1}). auto. if => //. seq 1 1 : (={n, x} /\ (even n{1} => ={b} /\ b{1} = x{1}) /\ (odd n{1} => b{1} = x{1} ^^ y{1} /\ b{2} = x{2} ^^ y{2})). while (={n, x, i} /\ i{1} <= n{1} /\ (if even i{1} then b{1} = x{1} /\ b{2} = x{2} else b{1} = x{1} ^^ y{1} /\ b{2} = x{2} ^^ y{2})). auto; smt(xorA xorK xor_ff). auto; smt(). auto; smt(xorA xorK). qed. lemma noninter2' : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. proc => /=. seq 2 2 : (={n, x, i, b} /\ i{1} = 0 /\ b{1} = x{1}). auto. if => //. wp. while (={n, x, i} /\ i{1} <= n{1} /\ (if even i{1} then b{1} = x{1} /\ b{2} = x{2} else b{1} = x{1} ^^ y{1} /\ b{2} = x{2} ^^ y{2})). auto; smt(xorA xorK xor_ff). auto; smt(xorA xorK). qed.