1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
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);
}
|
