-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathaxioms.qrhl
140 lines (119 loc) · 6.63 KB
/
axioms.qrhl
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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
include "Adv_INDCCA_encFO.qrhl".
include "decapsQuery1.qrhl".
include "decapsQuery1_G.qrhl".
include "decapsQuery2.qrhl".
include "decapsQuery2_G.qrhl".
include "decapsQuery2_adv_cstar.qrhl".
include "queryH_Hq.qrhl".
include "decapsQuery1_badpk.qrhl".
include "queryG.qrhl".
include "queryG'.qrhl".
include "queryGmeasured.qrhl".
include "queryGPuncturedS.qrhl".
include "queryH.qrhl".
include "Count.qrhl".
# Axiom: adversary is lossless
# GRAPH: ONESIDED("Adv_INDCCA_encFO_lossless_dq2","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_lossless_dq2: {Cla[True]} call Adv_INDCCA_encFO(queryG,queryH,decapsQuery2); ~ skip; {Cla[True]}.
admit.
qed.
# Axiom: adversary is lossless
# GRAPH: ONESIDED("Adv_INDCCA_encFO_lossless_dq1","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_lossless_dq1: {Cla[True]} call Adv_INDCCA_encFO(queryG,queryH,decapsQuery1); ~ skip; {Cla[True]}.
admit.
qed.
# Axiom: adversary is lossless
# GRAPH: ONESIDED("Adv_INDCCA_encFO_lossless_bpk","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_lossless_bpk: {Cla[True]} call Adv_INDCCA_encFO(queryG,queryH,decapsQuery1_badpk); ~ skip; {Cla[True]}.
admit.
qed.
# Axiom: adversary is lossless
# GRAPH: ONESIDED("Adv_INDCCA_encFO_lossless_Gmeas_Hq_ac","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_lossless_Gmeas_Hq_ac: {Cla[True]} call Adv_INDCCA_encFO(Count(queryGmeasured),queryH_Hq(Count(queryGmeasured)),decapsQuery2_adv_cstar); ~ skip; {Cla[True]}.
admit.
qed.
# Axiom: adversary is lossless
# GRAPH: ONESIDED("Adv_INDCCA_encFO_lossless_Gmeas_Hq_dq1G","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_lossless_C_Gmeas_Hq_dq1G: {Cla[True]} call Adv_INDCCA_encFO(Count(queryGmeasured),queryH_Hq(Count(queryGmeasured)),decapsQuery1_G(Count(queryGmeasured))); ~ skip; {Cla[True]}.
admit.
qed.
# Axiom: adversary is lossless
# GRAPH: ONESIDED("Adv_INDCCA_encFO_lossless_Gmeas_Hq_dq2G","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_lossless_C_Gmeas_Hq_dq2G: {Cla[True]} call Adv_INDCCA_encFO(Count(queryGmeasured),queryH_Hq(Count(queryGmeasured)),decapsQuery2_G(Count(queryGmeasured))); ~ skip; {Cla[True]}.
admit.
qed.
# Axiom
# GRAPH: ONESIDED("Adv_INDCCA_encFO_countG","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_countG: {Cla[count1=0]} call Adv_INDCCA_encFO(Count(queryG),queryH_Hq(Count(queryG)),decapsQuery1); ~ skip; {Cla[count1 ≤ qG+2*qH]}.
admit.
qed.
# Axiom
# GRAPH: ONESIDED("Adv_INDCCA_encFO_countG_Hq_ac","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_countG_Hq_ac: {Cla[count1=0]} call Adv_INDCCA_encFO(Count(queryG),queryH_Hq(Count(queryG)),decapsQuery2_adv_cstar); ~ skip; {Cla[count1 ≤ qG+2*qH]}.
admit.
qed.
# Axiom
# GRAPH: ONESIDED("Adv_INDCCA_encFO_countG'_Hq_ac","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_countG'_Hq_ac: {Cla[count1=0]} call Adv_INDCCA_encFO(Count(queryG'),queryH_Hq(Count(queryG')),decapsQuery2_adv_cstar); ~ skip; {Cla[count1 ≤ qG+2*qH]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to G
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_decapsQuery1_G","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_decapsQuery1_G: {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryG),queryH_Hq(Count(queryG)),decapsQuery1_G(Count(queryG))); ~ skip; {Cla[count1 ≤ qG+2*qH+1+qD]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to G
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_decapsQuery2_G","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_decapsQuery2_G: {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryG),queryH_Hq(Count(queryG)),decapsQuery2_G(Count(queryG))); ~ skip; {Cla[count1 ≤ qG+2*qH+1+qD]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to G'
# GRAPH: ONESIDED("Adv_INDCCA_encFO_countG'","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_countG': {Cla[count1=0]} call Adv_INDCCA_encFO(Count(queryG'),queryH_Hq(Count(queryG')),decapsQuery1); ~ skip; {Cla[count1 ≤ qG+2*qH]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to G'
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_decapsQuery1_G'","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_decapsQuery1_G': {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryG'),queryH_Hq(Count(queryG')),decapsQuery1_G(Count(queryG'))); ~ skip; {Cla[count1 ≤ qG+2*qH+qD+1]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to G'
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_decapsQuery2_G'","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_decapsQuery2_G': {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryG'),queryH_Hq(Count(queryG')),decapsQuery2_G(Count(queryG'))); ~ skip; {Cla[count1 ≤ qG+2*qH+qD+1]}.
admit.
qed.
# Axiom
# GRAPH: ONESIDED("Adv_INDCCA_encFO_countGpunc","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_countGpunc: {Cla[count1=0]} call Adv_INDCCA_encFO(Count(queryGPuncturedS),queryH_Hq(Count(queryGPuncturedS)),decapsQuery1); ~ skip; {Cla[count1 ≤ qG+2*qH]}.
admit.
qed.
# Axiom
# GRAPH: ONESIDED("Adv_INDCCA_encFO_countGpunc_Hq_ac","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_countGpunc_Hq_ac: {Cla[count1=0]} call Adv_INDCCA_encFO(Count(queryGPuncturedS),queryH_Hq(Count(queryGPuncturedS)),decapsQuery2_adv_cstar); ~ skip; {Cla[count1 ≤ qG+2*qH]}.
admit.
qed.
# Axiom
# GRAPH: ONESIDED("Adv_INDCCA_encFO_countGmeas_Hq_ac","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_countGmeas_Hq_ac: {Cla[count1=0]} call Adv_INDCCA_encFO(Count(queryGmeasured),queryH_Hq(Count(queryGmeasured)),decapsQuery2_adv_cstar); ~ skip; {Cla[count1 ≤ qG+2*qH]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to Gpunctured
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_Gmeas_Hq_dq1G","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_Gmeas_Hq_dq1G_1: {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryGmeasured),queryH_Hq(Count(queryGmeasured)),decapsQuery1_G(Count(queryGmeasured))); ~ skip; {Cla[count1 ≤ qG+2*qH+qD+1]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to Gpunctured
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_Gmeas_Hq_dq2G","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_Gmeas_Hq_dq2G_1: {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryGmeasured),queryH_Hq(Count(queryGmeasured)),decapsQuery2_G(Count(queryGmeasured))); ~ skip; {Cla[count1 ≤ qG+2*qH+qD+1]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to Gpunctured
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_decapsQuery1_Gpunc","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_decapsQuery1_Gpunc: {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryGPuncturedS),queryH_Hq(Count(queryGPuncturedS)),decapsQuery1_G(Count(queryGPuncturedS))); ~ skip; {Cla[count1 ≤ qG+2*qH+qD+1]}.
admit.
qed.
# Axiom: adversary makes <= qG queries to Gpunctured
# GRAPH: ONESIDED("Adv_INDCCA_encFO_count_decapsQuery2_Gpunc","Adv_INDCCA_encFO")
qrhl Adv_INDCCA_encFO_count_decapsQuery2_Gpunc: {Cla[count1=1]} call Adv_INDCCA_encFO(Count(queryGPuncturedS),queryH_Hq(Count(queryGPuncturedS)),decapsQuery2_G(Count(queryGPuncturedS))); ~ skip; {Cla[count1 ≤ qG+2*qH+qD+1]}.
admit.
qed.