-
Notifications
You must be signed in to change notification settings - Fork 1
/
ECTemplateFull.txt
91 lines (62 loc) · 2.29 KB
/
ECTemplateFull.txt
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
88
89
90
prover alt-ergo, z3, cvc3.
type G_1.
type G_T.
type message.
cnst g_1_i : G_1.
cnst g_T_i : G_T.
cnst g_1 : G_1.
cnst g_T : G_T.
cnst q : int.
cnst limit_Hash : int.
op [*] : (G_1, G_1) -> G_1 as G_1_mul.
op [^] : (G_1, int) -> G_1 as G_1_pow.
op [*] : (G_T, G_T) -> G_T as G_T_mul.
op [^] : (G_T, int) -> G_T as G_T_pow.
op G_1_log : G_1 -> int.
op G_T_log : G_T -> int.
op e : (G_1, G_1) -> G_T as G_1_pair.
(*
From easycrypt ElGamal:
If we use the native modulo alt-ergo is not able
to perform the proof.
So we declare an operator (%%) which stand for the modulo ...
*)
op [%%] : (int,int) -> int as int_mod.
axiom q_pos : 0 < q.
(* Axioms largely pulled from ElGamal. Note that G_1 and G_T have the same order if the order is prime. *)
axiom G_1_mult_1 : forall (x : G_1), x * g_1_i = x.
axiom G_1_exp_0 : forall (x : G_1), x ^ 0 = g_1_i.
axiom G_1_exp_S : forall (x : G_1, k : int), k > 0 => x ^ k = x * (x^(k-1)).
axiom G_T_mult_1 : forall (x : G_T), x * g_T_i = x.
axiom G_T_exp_0 : forall (x : G_T), x ^ 0 = g_T_i.
axiom G_T_exp_S : forall (x : G_T, k : int), k > 0 => x ^ k = x * (x^(k-1)).
axiom bilinearity : forall (x : G_1, y : G_1, a : int, b : int), e(x ^ a, y ^ b) = e(x, y) ^ (a * b).
(* axiom non_degenerate : !(e(g_1, g_1) = g_T_i). *)
axiom G_1_pow_add :
forall (x, y:int), g_1 ^ (x + y) = g_1 ^ x * g_1 ^ y.
axiom G_T_pow_add :
forall (x, y:int), g_T ^ (x + y) = g_T ^ x * g_T ^ y.
axiom G_1_pow_mult :
forall (x, y:int), (g_1 ^ x) ^ y = g_1 ^ (x * y).
axiom G_T_pow_mult :
forall (x, y:int), (g_T ^ x) ^ y = g_T ^ (x * y).
axiom G_1_log_pow :
forall (g_1':G_1), g_1 ^ G_1_log(g_1') = g_1'.
axiom G_T_log_pow :
forall (g_T':G_T), g_T ^ G_T_log(g_T') = g_T'.
axiom G_1_pow_mod :
forall (z:int), g_1 ^ (z%%q) = g_1 ^ z.
axiom G_T_pow_mod :
forall (z:int), g_T ^ (z%%q) = g_T ^ z.
axiom mod_add :
forall (x,y:int), (x%%q + y)%%q = (x + y)%%q.
axiom mod_small :
forall (x:int), 0 <= x => x < q => x%%q = x.
axiom mod_sub :
forall (x, y:int), (x%%q - y)%%q = (x - y)%%q.
axiom mod_bound :
forall (x:int), 0 <= x%%q && x%%q < q.
pop Rand_G_1_exp : () -> (int).
pop Rand_G_1 : () -> (G_1).
(* axiom Rand_G_1_exp_def() : x = Rand_G_1_exp() ~ y = [0..q-1] : true ==> x = y. *)
axiom Rand_G_1_def() : x = Rand_G_1() ~ y = Rand_G_1_exp() : true ==> x = g_1 ^ y.