-
Notifications
You must be signed in to change notification settings - Fork 0
/
hpke.auth.outsider-cca.m4.ocv
141 lines (124 loc) · 5.94 KB
/
hpke.auth.outsider-cca.m4.ocv
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
141
(* Analysing the HPKE Standard - Supplementary Material
Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp;
Doreen Riepel
This is supplementary material accompanying the paper:
Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
Long version: https://eprint.iacr.org/2020/1499 *)
proof {
out_game "g00.out.cv";
remove_assign binder the_sk;
remove_assign binder the_pk;
crypto outsider_cca(AuthEncap) [variables: s->s_1];
out_game "g01.out.cv";
crypto eliminate_failing(AuthEncap) **;
out_game "g02.out.cv";
SArename k'_1;
out_game "g03.out.cv";
crypto prf(KeySchedule_auth) k'_3;
out_game "g04.out.cv";
crypto splitter(split) **;
out_game "g05.out.cv";
crypto int_ctxt(Seal_inner) part1;
simplify;
crypto ind_cpa(Seal_inner) **;
out_game "g06.out.cv";
success
}
(** Key Encapsulation Mechanism **)
type keypairseed_t [bounded,large].
type kemseed_t [fixed,large].
type skey_t [bounded,large].
type pkey_t [bounded,large].
type kemkey_t [fixed,large].
type kemciph_t [fixed,large].
type AuthEncap_res_t [fixed,large].
proba P_pk_coll.
proba Adv_Outsider_CCA.
fun kemkey2bitstr(kemkey_t): bitstring [data].
fun kemciph2bitstr(kemciph_t): bitstring [data].
expand Authenticated_KEM(keypairseed_t, pkey_t, skey_t, kemseed_t, AuthEncap_res_t, AuthDecap_res_t, kemkey_t, kemciph_t, skgen, pkgen, GenerateKeyPair, AuthEncap, AuthEncap_r, AuthEncap_key, AuthEncap_enc, AuthEncap_tuple, AuthEncap_None, AuthDecap, AuthDecap_Some, AuthDecap_None, P_pk_coll).
expand Outsider_CCA_Secure_Authenticated_KEM(keypairseed_t, pkey_t, skey_t, kemseed_t, AuthEncap_res_t, AuthDecap_res_t, kemkey_t, kemciph_t, skgen, pkgen, GenerateKeyPair, AuthEncap, AuthEncap_r, AuthEncap_key, AuthEncap_enc, AuthEncap_tuple, AuthEncap_None, AuthDecap, AuthDecap_Some, AuthDecap_None, Adv_Outsider_CCA).
include(`common.hpke.ocvl')
(* Define a function for choosing from two attacker-provided plaintexts based
on a bit. Also, defines some equations on it so CryptoVerif is able
to reason about it. *)
expand boolean_choice_for_encryption(
(* types *)
bitstring, (* type of the values *)
(* functions *)
Length, (* the Length function provided by the encryption scheme. *)
(* Needed for some equations about the function. *)
test (* Name of the choice function: *)
(* test(bool, bitstring, bitstring): bitstring *)
).
(* a set E used within the proof,
containing 6-tuples of the following type: *)
table E(
pkey_t, (* sender's public key *)
pkey_t, (* receiver's public key *)
kemciph_t, (* KEM ciphertext *)
bitstring, (* AEAD ciphertext *)
bitstring, (* AEAD additional authenticated data *)
bitstring (* application info string *)
).
param N. (* number of honest keypairs/users *)
param Qeperuser. (* number of calls to the Oaenc() oracle per keypair *)
param Qdperuser. (* number of calls to the Oadec() oracle per keypair *)
param Qcperuser. (* number of calls to the Ochall() oracle per keypair *)
(* This is the proof goal: prove that the adversary cannot guess
the boolean b with probability better than 1/2.
b is defined as a fresh random boolean inside the Ostart() oracle. *)
query secret b.
process
Ostart() := b <-R bool; return();
(* The adversary can generate up to N honest keypairs/users by calling
the Osetup() oracle. The nested oracles Oaenc(), Oadec(), Ochall()
will be available for each keypair. *)
(foreach i <= N do
Osetup() :=
let (the_sk: skey_t, the_pk: pkey_t) = GenerateKeyPair() in
(* The public key of each honest keypair is made available
to the adversary. *)
return(the_pk);
(
(* This defines the Oaenc() oracle with up to Qeperuser calls per keypair *)
(foreach iae <= Qeperuser do
Oaenc(pk: pkey_t, m: bitstring, aad: bitstring, info: bitstring) :=
return(SealAuth(pk, info, aad, m, the_sk))
) |
(* This defines the Oadec() oracle with up to Qdperuser calls per keypair *)
(foreach iad <= Qdperuser do
Oadec(pk: pkey_t, enc: kemciph_t, c: bitstring, aad: bitstring, info: bitstring) :=
get E(=pk, =the_pk, =enc, =c, =aad, =info) in (
return(OpenAuth_None)
) else (
return(OpenAuth(enc, the_sk, info, aad, c, pk))
)
) |
(* This defines the Ochall() oracle with up to Qcperuser calls per keypair *)
(foreach ic <= Qcperuser do
Ochall(pk: pkey_t, m0: bitstring, m1: bitstring, aad: bitstring, info: bitstring) :=
(* only accept challenge queries for honest public keys *)
find i' <= N suchthat defined(the_pk[i']) && the_pk[i'] = pk then (
(* only accept challenge queries for m0 and m1 of same length *)
if Length(m0) = Length(m1) then (
let SealAuth_Some(enc_star: kemciph_t, c_star: bitstring) =
SealAuth(pk, info, aad, test(b, m0, m1), the_sk) in (
insert E(the_pk, pk, enc_star, c_star, aad, info);
return((enc_star, c_star))
(* SealAuth does not fail, but CryptoVerif's language
requires we indicate the else branch. It will be
removed with the eliminate_failing step. *)
) else return(bottom)
) else return(bottom) (* ends the condition on m0 and m1 lengths *)
) else return(bottom) (* ends the find inside Ochall() *)
) (* This ends the definition of the Ochall() oracle *)
) (* This ends the block of oracles that are defined for each keypair *)
) (* This ends the definition of the Osetup() oracle and its nested oracles *)
(* EXPECTED FILENAME: examples/hpke/hpke.auth.outsider-cca.m4.ocv TAG: 1
All queries proved.
0.508s (user 0.500s + system 0.008s), max rss 27368K
END *)