diff options
Diffstat (limited to 'Test/secure/ObliviousTransfer.bpl')
-rw-r--r-- | Test/secure/ObliviousTransfer.bpl | 87 |
1 files changed, 87 insertions, 0 deletions
diff --git a/Test/secure/ObliviousTransfer.bpl b/Test/secure/ObliviousTransfer.bpl new file mode 100644 index 00000000..0f26062f --- /dev/null +++ b/Test/secure/ObliviousTransfer.bpl @@ -0,0 +1,87 @@ +type T = bv2; +function {:inline} xor(a: bool, b: bool) returns (bool) { (!a && b) || (a && !b) } +function {:bvbuiltin "bvxor"} xorT(p1: T, p2: T) : T; + +// Oblivious Transfer +procedure ObliviousTransfer_A( + {:visible} m0: T, {:visible} m1: T, + {:hidden} c: bool) +returns ({:hidden} m: T, + {:visible} m0p: T, {:visible} m1p: T, + {:visible} x: bool, + {:visible} y: T, {:visible} z: T + ) +// spec +ensures (m == if c then m1 else m0); +// Implementation +{ + var {:hidden} mp: T; + var {:hidden} cp: bool; + + havoc cp; + havoc m0p, m1p; + mp := if cp then m0p else m1p; + + x := xor(c, cp); + y := xorT(m0, if x then m0p else m1p); + z := xorT(m1, if x then m1p else m0p); + + m := xorT(if c then z else y, mp); +} + + +// Oblivious Transfer +procedure ObliviousTransfer_B( + {:hidden} m0: T, {:hidden} m1: T, + {:visible} c: bool) +returns ({:visible} m: T, + {:visible} mp: T, {:visible} cp: bool, + {:visible} x: bool, + {:visible} y: T, {:visible} z: T + ) +// spec +ensures (m == if c then m1 else m0); +// Implementation +{ + var {:hidden} m0p, m1p: T; + + havoc cp; + havoc m0p, m1p; + mp := if cp then m0p else m1p; + + x := xor(c, cp); + y := xorT(m0, if x then m0p else m1p); + z := xorT(m1, if x then m1p else m0p); + + m := xorT(if c then z else y, mp); + //y := m0; +} + +// Oblivious Transfer +procedure ObliviousTransfer_X( + {:hidden} m0: T, {:hidden} m1: T, + {:hidden} c: bool) +returns ({:hidden "B"} m: T) +// spec +ensures (m == if c then m1 else m0); +// Implementation +{ + var {:hidden} m0p, m1p: T; + var {:hidden} mp: T; + var {:hidden} cp: bool; + + var {:hidden} x: bool; + var {:hidden} y, z: T; + + havoc cp; + havoc m0p, m1p; + mp := if cp then m0p else m1p; + + x := xor(c, cp); + y := xorT(m0, if x then m0p else m1p); + z := xorT(m1, if x then m1p else m0p); + + m := xorT(if c then z else y, mp); +} + + |