116 lines
3.7 KiB
Text
116 lines
3.7 KiB
Text
(* LO-Stream: Chunk Confidentiality + Integrity (Theorem 13, P1+P2)
|
|
*
|
|
* Adapted from CryptoVerif's TLS 1.3 Record Protocol example.
|
|
*
|
|
* IND-CPA: Bit-guessing game — adversary submits two equal-length plaintexts,
|
|
* receives encryption of one based on secret bit b0. Advantage = Pr[guess b0].
|
|
*
|
|
* INT-CTXT: Injective correspondence — if decryption succeeds at (count, msg),
|
|
* encryption must have produced (count, msg).
|
|
*
|
|
* Nonce uniqueness enforced via table lookup (nonce-respecting adversary, §9.11(f)).
|
|
* Nonce derivation: chunk_nonce = xor(base_nonce, count) with injectivity equation.
|
|
*
|
|
* Reduces to: XChaCha20-Poly1305 IND-CPA + INT-CTXT.
|
|
*)
|
|
|
|
type key [fixed, large].
|
|
type seqn [fixed].
|
|
type nonce_t [fixed, large].
|
|
type add_data [bounded].
|
|
|
|
param N_enc, N_dec.
|
|
|
|
(* ---------- Nonce derivation with injectivity ---------- *)
|
|
(* §15.2: chunk_nonce = base_nonce XOR mask(index, tag_byte)
|
|
* Modeled as xor(iv, count) per TLS 1.3 record protocol pattern.
|
|
* CryptoVerif needs the explicit injectivity equation. *)
|
|
|
|
fun xor(key, seqn): nonce_t.
|
|
|
|
equation forall k: key, n: seqn, n': seqn;
|
|
(xor(k, n) = xor(k, n')) = (n = n').
|
|
|
|
(* ---------- AEAD (IND-CPA + INT-CTXT under unique nonces) ---------- *)
|
|
|
|
proba P_cpa.
|
|
proba P_ctxt.
|
|
|
|
expand AEAD_nonce(key, bitstring, bitstring, add_data, nonce_t,
|
|
enc, dec, injbot, Z, P_cpa, P_ctxt).
|
|
|
|
(* Per-chunk AAD includes base_nonce + count (§15.4) *)
|
|
fun derive_aad(key, seqn): add_data [data].
|
|
|
|
letfun stream_encrypt(k: key, n: nonce_t, m: bitstring, aad: add_data) =
|
|
enc(m, aad, k, n).
|
|
letfun stream_decrypt(k: key, n: nonce_t, c: bitstring, aad: add_data) =
|
|
dec(c, aad, k, n).
|
|
|
|
(* ---------- Tables for nonce uniqueness (§9.11(f) game hypothesis) ---------- *)
|
|
|
|
table table_enc_nonce(seqn).
|
|
table table_dec_nonce(seqn).
|
|
|
|
(* ---------- Security queries ---------- *)
|
|
|
|
(* P1 (IND-CPA): secret bit indistinguishable *)
|
|
query secret b0 [cv_bit].
|
|
|
|
(* P2 (INT-CTXT): injective correspondence *)
|
|
event Sent(seqn, bitstring).
|
|
event Received(seqn, bitstring).
|
|
|
|
query count: seqn, msg: bitstring;
|
|
inj-event(Received(count, msg)) ==> inj-event(Sent(count, msg))
|
|
public_vars b0.
|
|
|
|
(* ---------- Channels ---------- *)
|
|
|
|
channel c_start, c_ready, c_enc_in, c_enc_out, c_dec_in, c_dec_out.
|
|
|
|
(* ---------- Encrypt oracle ---------- *)
|
|
(* Adversary submits (m0, m1, count). Oracle encrypts m_b where b = b0.
|
|
* Count must not have been used before (nonce-respecting). *)
|
|
|
|
let Encrypt(k: key, iv: key, b: bool) =
|
|
!N_enc
|
|
in(c_enc_in, (clear1: bitstring, clear2: bitstring, count: seqn));
|
|
(* Nonce-respecting: reject reused counter *)
|
|
get table_enc_nonce(=count) in yield else
|
|
insert table_enc_nonce(count);
|
|
(* Equal-length requirement for IND-CPA *)
|
|
if Z(clear1) = Z(clear2) then
|
|
let clear = if_fun(b, clear1, clear2) in
|
|
let aad: add_data = derive_aad(iv, count) in
|
|
let nonce = xor(iv, count) in
|
|
event Sent(count, clear);
|
|
let cipher = stream_encrypt(k, nonce, clear, aad) in
|
|
out(c_enc_out, cipher).
|
|
|
|
(* ---------- Decrypt oracle ---------- *)
|
|
(* Adversary submits (ciphertext, count). Must not reuse count. *)
|
|
|
|
let Decrypt(k: key, iv: key) =
|
|
!N_dec
|
|
in(c_dec_in, (cipher: bitstring, count: seqn));
|
|
get table_dec_nonce(=count) in yield else
|
|
insert table_dec_nonce(count);
|
|
let aad: add_data = derive_aad(iv, count) in
|
|
let nonce = xor(iv, count) in
|
|
let injbot(clear) = stream_decrypt(k, nonce, cipher, aad) in
|
|
event Received(count, clear).
|
|
|
|
(* ---------- Main process ---------- *)
|
|
|
|
process
|
|
in(c_start, ());
|
|
new b0: bool;
|
|
new k: key;
|
|
new iv: key; (* base_nonce — public *)
|
|
out(c_ready, iv);
|
|
(Encrypt(k, iv, b0) | Decrypt(k, iv))
|
|
|
|
(* EXPECTED
|
|
All queries proved.
|
|
END *)
|