Library Xor_analysis
Proof of robustness for bit-flipping watermarking
Add Rec LoadPath "../../ALEA/src" as ALEA.
Require Import Bernoulli.
Require Import BinCoeff.
Require Import RandomList.
Require Import RandomBV.
Require Import AACU.
Import Peano.
Close Scope bool_scope.
Set Implicit Arguments.
Parameter n k d_obs d_detect : nat.
Definition genkey := BVrandom_k n k.
Definition gensupport := BVrandom n.
Definition mark K O := BVxor n K O.
Definition n_marks (O K O' : Bvector n) := occs_1 (K && (O ++ O')).
Definition guess_key (A : Bvector n -> distr (Bvector n)) :=
Mlet genkey (fun K =>
Mlet gensupport (fun O =>
let O' := mark K O in
Mlet (A O') (fun K' =>
Munit (BVeq K K')))).
Definition and P Q R S (a:{P}+{Q}) (b:{R}+{S}) :=
match a,b with left _, left _ => true | _, _ => false end.
Definition attack_mark (A : Bvector n -> distr (Bvector n)) :=
Mlet genkey (fun K =>
Mlet gensupport (fun O =>
let O' := mark K O in
Mlet (A O') (fun O'' =>
Munit (and (lt_dec (dist O' O'') d_obs) (lt_dec (n_marks O K O'')%nat d_detect))))).
Axiom leq_2k_n : (2*k <= n)%nat.
Axiom d_detect_le_k : (d_detect <= k)%nat.
Axiom d_obs_le_n : (d_obs <= n)%nat.
Axiom k_le_obs_plus_detect : (k <= d_obs + d_detect)%nat.
Axiom d_obs_positive : (0 < d_obs)%nat.
Axiom d_detect_positive : (0 < d_detect)%nat.
Lemma leq_k_n : (k <= n)%nat.
Proof.
generalize leq_2k_n; omega.
Qed.
Open Scope nat_scope.
If there is an attack on the mark, we obtain an approximated key
K' := xor O' O''
such that error := dist K K' = dist O O'' can be bounded.
From that point we guess K from K' just by guessing the error,
deducing the number ki of incorrect 1-bits in K' and
the number km of missing 1-bits using the relationship between
those quantities, the error and the total number of flipped bits.
Relationship between ka, k (known) and
error, ki and km (unknown):
2*ki = error+ka-k and 2*km = error+k-ka.
Theorem ki_km : forall (K O O'' : Bvector n),
occs_1 K = k ->
let O' := mark K O in
let K' := BVxor _ O' O'' in
let ka := dist O' O'' in
let error := dist K K' in
let ki := missing K' K in
let km := missing K K' in
2 * ki + k = error + ka /\ 2 * km + ka = error + k.
Proof.
intros.
assert (error = ki + km).
change (error = ki + km)
with (occs_1 (BVxor _ K K') = missing K' K + missing K K').
apply occs_missing.
assert (ka + km = k + ki). change ka with (occs_1 (BVxor _ O' O''));
change km with (missing K K');
change ki with (missing K' K);
rewrite <- H.
apply occs_plus_missing.
omega.
Qed.
Require Import Div2.
Close Scope nat_scope.
occs_1 K = k ->
let O' := mark K O in
let K' := BVxor _ O' O'' in
let ka := dist O' O'' in
let error := dist K K' in
let ki := missing K' K in
let km := missing K K' in
2 * ki + k = error + ka /\ 2 * km + ka = error + k.
Proof.
intros.
assert (error = ki + km).
change (error = ki + km)
with (occs_1 (BVxor _ K K') = missing K' K + missing K K').
apply occs_missing.
assert (ka + km = k + ki). change ka with (occs_1 (BVxor _ O' O''));
change km with (missing K K');
change ki with (missing K' K);
rewrite <- H.
apply occs_plus_missing.
omega.
Qed.
Require Import Div2.
Close Scope nat_scope.
The reduction works as follows:
start with K' = O'+O'' where O'' is the unmarked support;
guess the value of error between 0 and error_max-1;
from error, compute ki and km;
guess which ki bits are incorrect, which km are missing,
to obtain the correct K with a decent probability.
We could further refine the reduction by skipping some values of error or km, because we must have km = n_marks O K O'' < d_detect so that error isn't too large, and km and ki must be integers so error+ka-k must be even. However, this wouldn't change the security bound significantly.
We could further refine the reduction by skipping some values of error or km, because we must have km = n_marks O K O'' < d_detect so that error isn't too large, and km and ki must be integers so error+ka-k must be even. However, this wouldn't change the security bound significantly.
Definition error_max := (d_obs + 2 * d_detect - k)%nat.
Definition A'_body (O' O'' : Bvector n) :=
let ka := dist O' O'' in
let K' := BVxor _ O' O'' in
let errors : list nat := lrange (error_max-1) in
Mlet (choose errors) (fun error =>
let km := div2 (error + k - ka) in
let ki := div2 (error + ka - k) in
correct K' ki km).
Definition A' A O' := Mlet (A O') (fun O'' => A'_body O' O'').
Definition delta' := ((comb (Div2.div2 d_obs) (d_obs)) *
(comb d_detect (n - k + d_detect)))%nat.
Definition delta := [1/]error_max * [1/]delta'.
Lemma delta'_pos : (0 < delta')%nat.
Proof.
unfold delta'.
change 0%nat with (0 * comb d_detect (n - k + d_detect))%nat.
apply mult_lt_compat_r.
apply comb_le_0_lt; auto.
apply lt_le_weak; apply lt_div2.
exact d_obs_positive.
apply comb_le_0_lt; auto.
omega.
Qed.
Lemma error_max_pos : (0 < error_max)%nat.
Proof.
unfold error_max.
generalize k_le_obs_plus_detect, d_detect_positive; omega.
Qed.
Hint Resolve error_max_pos.
Hint Resolve delta'_pos.
Ltac pose_r x M := pose (x := M) ; replace M with x by reflexivity.
Show that the correct error is in the filtered list,
that the correct ki, km are computed from it,
and finally obtain a lower-bound on the probability that
the secret key is found.
Theorem reduction : forall (A:Bvector n -> distr (Bvector n)),
(mu (attack_mark A) B2U) * delta <= mu (guess_key (A' A)) B2U.
Proof.
intros.
rewrite Umult_sym at 1.
rewrite <- mu_stable_mult.
(mu (attack_mark A) B2U) * delta <= mu (guess_key (A' A)) B2U.
Proof.
intros.
rewrite Umult_sym at 1.
rewrite <- mu_stable_mult.
Get rid of the common prologue
unfold attack_mark, guess_key, A';
repeat setoid_rewrite Mlet_simpl; setoid_rewrite Munit_simpl.
apply range_le with (1 := BVrandom_k_range leq_k_n); intros K Hk.
apply (mu_monotonic gensupport); intro O.
pose_r O' (mark K O).
apply compositional_reasoning; intros O'' H.
destruct (lt_dec (dist O' O'') d_obs) as [ Hobs | H1 ];
destruct (lt_dec (n_marks O K O'') d_detect) as [ Hdetect | H2 ];
first [ discriminate H | clear H ].
repeat setoid_rewrite Mlet_simpl; setoid_rewrite Munit_simpl.
apply range_le with (1 := BVrandom_k_range leq_k_n); intros K Hk.
apply (mu_monotonic gensupport); intro O.
pose_r O' (mark K O).
apply compositional_reasoning; intros O'' H.
destruct (lt_dec (dist O' O'') d_obs) as [ Hobs | H1 ];
destruct (lt_dec (n_marks O K O'') d_detect) as [ Hdetect | H2 ];
first [ discriminate H | clear H ].
At this point we are assuming a successful attack on the mark,
and have to show that the resulting attack on the key works
unfold A'_body; repeat setoid_rewrite Mlet_simpl.
pose_r K' (BVxor _ O' O'').
pose (error := dist K K').
pose_r ka (dist O' O'').
pose (ki := missing K' K).
pose (km := missing K K').
pose_r errors (lrange (error_max-1)).
transitivity ([1/](length errors) * [1/]delta').
pose_r K' (BVxor _ O' O'').
pose (error := dist K K').
pose_r ka (dist O' O'').
pose (ki := missing K' K).
pose (km := missing K K').
pose_r errors (lrange (error_max-1)).
transitivity ([1/](length errors) * [1/]delta').
Bound the number of attempts on the error by error_max
unfold delta; Usimpl; unfold Ole; apply Unth_le_compat.
change errors with (lrange (error_max - 1));
rewrite range_len.
omega.
change errors with (lrange (error_max - 1));
rewrite range_len.
omega.
The correct error can be found because error <= error_max.
apply choose_le_Nnth with (x:=error).
apply leq_in_range.
replace error with (ki+km)%nat by
(unfold error, dist, ki, km;
rewrite <- occs_missing; reflexivity).
assert (ka < d_obs)%nat by assumption.
assert (ka + km = ki + k)%nat. unfold dist, km, ki. rewrite <- Hk.
change ka with (occs_1 (BVxor _ O' O'')).
rewrite occs_plus_missing.
apply plus_comm.
assert (n_marks O K O'' = km). unfold n_marks, km, K', missing, O', mark.
f_equal.
aac_rewrite (BVneg_xor K) in_right.
rewrite <- BVand_xor_not.
aac_reflexivity.
unfold error_max.
omega.
apply leq_in_range.
replace error with (ki+km)%nat by
(unfold error, dist, ki, km;
rewrite <- occs_missing; reflexivity).
assert (ka < d_obs)%nat by assumption.
assert (ka + km = ki + k)%nat. unfold dist, km, ki. rewrite <- Hk.
change ka with (occs_1 (BVxor _ O' O'')).
rewrite occs_plus_missing.
apply plus_comm.
assert (n_marks O K O'' = km). unfold n_marks, km, K', missing, O', mark.
f_equal.
aac_rewrite (BVneg_xor K) in_right.
rewrite <- BVand_xor_not.
aac_reflexivity.
unfold error_max.
omega.
Assuming that the error is correct,
show that the computed ki/km are correct too,
then estimate success
assert (2 * ki + k = error + ka /\ 2 * km + ka = error + k)%nat.
destruct (ki_km K O O'' Hk).
split; assumption.
destruct H.
clear errors.
assert (ki = div2 (error + ka - k))%nat as Hi.
replace (error + ka - k)%nat with (2*ki)%nat.
rewrite div2_double; reflexivity.
apply plus_minus.
aac_rewrite H in_right; aac_reflexivity.
assert (km = div2 (error + k - ka)) as Hm.
replace (error + k - ka)%nat with (2*km)%nat.
rewrite div2_double; reflexivity.
apply plus_minus.
aac_rewrite H0 in_right; aac_reflexivity.
rewrite <- Hi; rewrite <- Hm.
unfold ki, km; rewrite correct_eq.
change (missing K' K) with ki; change (missing K K') with km.
apply Unth_le_compat.
destruct (ki_km K O O'' Hk).
split; assumption.
destruct H.
clear errors.
assert (ki = div2 (error + ka - k))%nat as Hi.
replace (error + ka - k)%nat with (2*ki)%nat.
rewrite div2_double; reflexivity.
apply plus_minus.
aac_rewrite H in_right; aac_reflexivity.
assert (km = div2 (error + k - ka)) as Hm.
replace (error + k - ka)%nat with (2*km)%nat.
rewrite div2_double; reflexivity.
apply plus_minus.
aac_rewrite H0 in_right; aac_reflexivity.
rewrite <- Hi; rewrite <- Hm.
unfold ki, km; rewrite correct_eq.
change (missing K' K) with ki; change (missing K K') with km.
apply Unth_le_compat.
Bound the number of attempts independently of ka and the error.
unfold delta'.
change (occs_1 K') with ka.
apply le_pred.
generalize leq_2k_n, d_obs_le_n, d_detect_le_k; intros.
assert (n_marks O K O'' = km).
unfold n_marks, km, K', missing, O', mark.
f_equal.
aac_rewrite (BVneg_xor K) in_right.
rewrite <- BVand_xor_not.
aac_reflexivity.
change (occs_1 K') with ka.
apply le_pred.
generalize leq_2k_n, d_obs_le_n, d_detect_le_k; intros.
assert (n_marks O K O'' = km).
unfold n_marks, km, K', missing, O', mark.
f_equal.
aac_rewrite (BVneg_xor K) in_right.
rewrite <- BVand_xor_not.
aac_reflexivity.
ka = ki + k-km
assert (dist O' O'' + km = ki + k)%nat.
unfold dist, km, ki. rewrite <- Hk.
rewrite occs_plus_missing.
apply plus_comm.
assert (km <= n-ka)%nat.
change ka with (occs_1 K').
apply missing_le_not_occs.
apply mult_le_compat.
unfold dist, km, ki. rewrite <- Hk.
rewrite occs_plus_missing.
apply plus_comm.
assert (km <= n-ka)%nat.
change ka with (occs_1 K').
apply missing_le_not_occs.
apply mult_le_compat.
comb ki ka
assert (ka <= d_obs)%nat by omega.
transitivity (comb ki d_obs)%nat.
apply comb_monotonic_n; try omega.
apply comb_max_half.
transitivity (comb ki d_obs)%nat.
apply comb_monotonic_n; try omega.
apply comb_max_half.
comb km (n-ka)
apply comb_monotonic; try omega.
Qed.
Qed.
Theorem secrecy : forall A, mu (guess_key A) B2U <= [1/] (comb k n).
Proof.
intro.
unfold guess_key, genkey, gensupport, mark.
assert ((fun K : vector bool n =>
Mlet (BVrandom n)
(fun O : vector bool n =>
Mlet (A (K ++ O)) (fun K' : Bvector n => Munit (BVeq K K'))))
== (fun K : vector bool n =>
Mlet (BVrandom n) (fun O' => Mlet (A O') (fun K' => Munit (BVeq K K'))))).
intros K f; si.
apply RandomBV.BVxor_noise_si
with (k := K) (f := fun x => mu (A x) (fun y => f (BVeq K y))).
rewrite H; clear H; si.
transitivity (mu (BVrandom n) (fun x0 : Bvector n => mu (A x0) (fun x1 => [1/] comb k n))).
setoid_rewrite is_discrete_swap_mu with (d1 := BVrandom_k n k); [| apply domain_is_discrete ].
apply mu_monotonic; intro.
setoid_rewrite is_discrete_swap_mu with (d1 := BVrandom_k n k); [| apply domain_is_discrete ].
apply mu_monotonic; intro.
rewrite BVrandom_k_eq by exact leq_k_n.
case (beq_nat (occurrences x0 true) k); auto.
rewrite <- fcte_def; setoid_rewrite mu_fcte.
rewrite <- fmult_def; setoid_rewrite mu_stable_mult.
auto.
Qed.
Theorem robustness : forall (A:Bvector n -> distr (Bvector n)),
(mu (attack_mark A) B2U) <= (error_max *
comb (Div2.div2 d_obs) d_obs *
comb d_detect (n - k + d_detect))%nat
*/ [1/](comb k n).
Proof.
intro A.
setoid_replace (mu (attack_mark A) B2U)
with ((error_max * delta') */ (mu (attack_mark A) B2U * delta)).
apply Nmult_le_compat.
unfold delta'; aac_reflexivity.
rewrite reduction.
apply secrecy.
generalize (mu (attack_mark A) B2U); intro p.
rewrite Nmult_Umult_assoc_right.
unfold delta.
rewrite Umult_Nnth by auto.
rewrite Nmult_n_Nnth; [auto|].
change 0%nat with (0 * delta')%nat.
apply mult_lt_compat_r; auto.
unfold delta.
rewrite Umult_Nnth; auto.
Qed.