[STATEMENT]
lemma rsa_inv:
  assumes d: "d = nat (fst (bezw e ((P-1)*(Q-1))) mod int ((P-1)*(Q-1)))"
    and coprime: "coprime e ((P-1)*(Q-1))"
    and prime_P: "prime (P::nat)"
    and prime_Q: "prime Q"
    and P_neq_Q: "P \<noteq> Q"
    and e_gt_1: "e > 1"
    and d_gt_1: "d > 1"
  shows "((((x) ^ e) mod (P*Q)) ^ d) mod (P*Q) = x mod (P*Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
proof(cases "x = 0 \<or> x = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<or> x = 1 \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
 2. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0 \<or> x = 1

goal (2 subgoals):
 1. x = 0 \<or> x = 1 \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
 2. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0 \<or> x = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0 \<or> x = 1

goal (1 subgoal):
 1. (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
by (metis assms(6) assms(7) le_simps(1) nat_power_eq_Suc_0_iff neq0_conv not_one_le_zero numeral_nat(7) power_eq_0_iff power_mod)
[PROOF STATE]
proof (state)
this:
(x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (x = 0 \<or> x = 1)

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
hence x_gt_1: "x > 1"
[PROOF STATE]
proof (prove)
using this:
\<not> (x = 0 \<or> x = 1)

goal (1 subgoal):
 1. 1 < x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < x

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
define z where "z = (x ^ e) ^ d - x"
[PROOF STATE]
proof (state)
this:
z = (x ^ e) ^ d - x

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
hence z_gt_0: "z > 0"
[PROOF STATE]
proof (prove)
using this:
z = (x ^ e) ^ d - x

goal (1 subgoal):
 1. 0 < z
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z = (x ^ e) ^ d - x \<Longrightarrow> 0 < z
[PROOF STEP]
have "(x ^ e) ^ d - x = x ^ (e * d) - x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ^ e) ^ d - x = x ^ (e * d) - x
[PROOF STEP]
by (simp add: power_mult)
[PROOF STATE]
proof (state)
this:
(x ^ e) ^ d - x = x ^ (e * d) - x

goal (1 subgoal):
 1. z = (x ^ e) ^ d - x \<Longrightarrow> 0 < z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x ^ e) ^ d - x = x ^ (e * d) - x

goal (1 subgoal):
 1. z = (x ^ e) ^ d - x \<Longrightarrow> 0 < z
[PROOF STEP]
have "... > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x ^ (e * d) - x
[PROOF STEP]
by (metis x_gt_1 e_gt_1 d_gt_1 le_neq_implies_less less_one linorder_not_less n_less_m_mult_n not_less_zero numeral_nat(7) power_increasing_iff power_one_right zero_less_diff)
[PROOF STATE]
proof (state)
this:
0 < x ^ (e * d) - x

goal (1 subgoal):
 1. z = (x ^ e) ^ d - x \<Longrightarrow> 0 < z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x ^ e) ^ d - x = x ^ (e * d) - x
0 < x ^ (e * d) - x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x ^ e) ^ d - x = x ^ (e * d) - x
0 < x ^ (e * d) - x

goal (1 subgoal):
 1. 0 < z
[PROOF STEP]
using z_def
[PROOF STATE]
proof (prove)
using this:
(x ^ e) ^ d - x = x ^ (e * d) - x
0 < x ^ (e * d) - x
z = (x ^ e) ^ d - x

goal (1 subgoal):
 1. 0 < z
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
0 < z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < z

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
hence "[z = 0] (mod P)"
[PROOF STATE]
proof (prove)
using this:
0 < z

goal (1 subgoal):
 1. [z = 0] (mod P)
[PROOF STEP]
proof(cases "[x = 0] (mod P)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < z; [x = 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
 2. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
[x = 0] (mod P)

goal (2 subgoals):
 1. \<lbrakk>0 < z; [x = 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
 2. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x = 0] (mod P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[x = 0] (mod P)

goal (1 subgoal):
 1. [z = 0] (mod P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x = 0] (mod P) \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
have "0 \<noteq> d * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<noteq> d * e
[PROOF STEP]
by (metis (no_types) assms assms mult_is_0 not_one_less_zero)
[PROOF STATE]
proof (state)
this:
0 \<noteq> d * e

goal (1 subgoal):
 1. [x = 0] (mod P) \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> d * e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> d * e

goal (1 subgoal):
 1. [z = 0] (mod P)
[PROOF STEP]
by (metis (no_types) Groups.add_ac(2) True add_diff_inverse_nat cong_def cong_dvd_iff cong_mult_self_right dvd_0_right dvd_def dvd_trans mod_add_self2 more_arith_simps(5) nat_diff_split power_eq_if power_mult semiring_normalization_rules(7) z_def)
[PROOF STATE]
proof (state)
this:
[z = 0] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[z = 0] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
[x \<noteq> 0] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
have "[e * d = 1] (mod ((P - 1) * (Q - 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [e * d = 1] (mod (P - 1) * (Q - 1))
[PROOF STEP]
by (metis d bezw_inverse coprime coprime_imp_gcd_eq_1 nat_int)
[PROOF STATE]
proof (state)
this:
[e * d = 1] (mod (P - 1) * (Q - 1))

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
hence "[e * d = 1] (mod (P - 1))"
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod (P - 1) * (Q - 1))

goal (1 subgoal):
 1. [e * d = 1] (mod P - 1)
[PROOF STEP]
using assms cong_modulus_mult_nat
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod (P - 1) * (Q - 1))
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
1 < e
1 < d
[?x = ?y] (mod ?m * ?n) \<Longrightarrow> [?x = ?y] (mod ?m)

goal (1 subgoal):
 1. [e * d = 1] (mod P - 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[e * d = 1] (mod P - 1)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e * d = 1] (mod P - 1)
[PROOF STEP]
obtain k where k: "e*d = 1 + k*(P-1)"
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod P - 1)

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (P - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_k_mod assms
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod P - 1)
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); ?P \<noteq> ?Q; prime ?P; prime ?Q; ?d \<noteq> 0; [?e * ?d = 1] (mod ?P - 1)\<rbrakk> \<Longrightarrow> \<exists>k. ?e * ?d = 1 + k * (?P - 1)
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
1 < e
1 < d

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (P - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
e * d = 1 + k * (P - 1)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
hence "x ^ (e * d) = x * ((x ^ (P - 1)) ^ k)"
[PROOF STATE]
proof (prove)
using this:
e * d = 1 + k * (P - 1)

goal (1 subgoal):
 1. x ^ (e * d) = x * (x ^ (P - 1)) ^ k
[PROOF STEP]
by (metis power_add power_one_right mult.commute power_mult)
[PROOF STATE]
proof (state)
this:
x ^ (e * d) = x * (x ^ (P - 1)) ^ k

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
hence "[x ^ (e * d) = x * ((x ^ (P - 1)) ^ k)] (mod P)"
[PROOF STATE]
proof (prove)
using this:
x ^ (e * d) = x * (x ^ (P - 1)) ^ k

goal (1 subgoal):
 1. [x ^ (e * d) = x * (x ^ (P - 1)) ^ k] (mod P)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
x ^ (e * d) = x * (x ^ (P - 1)) ^ k
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. [x ^ (e * d) = x * (x ^ (P - 1)) ^ k] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x * (x ^ (P - 1)) ^ k] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x * (x ^ (P - 1)) ^ k] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
have "[x ^ (P - 1) = 1] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (P - 1) = 1] (mod P)
[PROOF STEP]
using prime_P fermat_theorem False
[PROOF STATE]
proof (prove)
using this:
prime P
\<lbrakk>prime ?p; \<not> ?p dvd ?a\<rbrakk> \<Longrightarrow> [?a ^ (?p - 1) = 1] (mod ?p)
[x \<noteq> 0] (mod P)

goal (1 subgoal):
 1. [x ^ (P - 1) = 1] (mod P)
[PROOF STEP]
by (simp add: cong_0_iff)
[PROOF STATE]
proof (state)
this:
[x ^ (P - 1) = 1] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[x ^ (P - 1) = 1] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
have "[x ^ (e * d) = x * ((1) ^ k)] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (e * d) = x * 1 ^ k] (mod P)
[PROOF STEP]
by (metis \<open>x ^ (e * d) = x * (x ^ (P - 1)) ^ k\<close> calculation(2) cong_pow cong_scalar_left)
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x * 1 ^ k] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
hence "[x ^ (e * d) = x] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = x * 1 ^ k] (mod P)

goal (1 subgoal):
 1. [x ^ (e * d) = x] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x] (mod P)

goal (1 subgoal):
 1. \<lbrakk>0 < z; [x \<noteq> 0] (mod P)\<rbrakk> \<Longrightarrow> [z = 0] (mod P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = x] (mod P)

goal (1 subgoal):
 1. [z = 0] (mod P)
[PROOF STEP]
using z_def z_gt_0
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = x] (mod P)
z = (x ^ e) ^ d - x
0 < z

goal (1 subgoal):
 1. [z = 0] (mod P)
[PROOF STEP]
by (simp add: cong_diff_iff_cong_0_nat power_mult)
[PROOF STATE]
proof (state)
this:
[z = 0] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[z = 0] (mod P)

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[z = 0] (mod P)

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
have "[z = 0] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [z = 0] (mod Q)
[PROOF STEP]
proof(cases "[x = 0] (mod Q)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [x = 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
 2. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
[x = 0] (mod Q)

goal (2 subgoals):
 1. [x = 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
 2. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x = 0] (mod Q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[x = 0] (mod Q)

goal (1 subgoal):
 1. [z = 0] (mod Q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x = 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
have "0 \<noteq> d * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<noteq> d * e
[PROOF STEP]
by (metis (no_types) assms mult_is_0 not_one_less_zero)
[PROOF STATE]
proof (state)
this:
0 \<noteq> d * e

goal (1 subgoal):
 1. [x = 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> d * e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> d * e

goal (1 subgoal):
 1. [z = 0] (mod Q)
[PROOF STEP]
by (metis (no_types) Groups.add_ac(2) True add_diff_inverse_nat cong_def cong_dvd_iff cong_mult_self_right dvd_0_right dvd_def dvd_trans mod_add_self2 more_arith_simps(5) nat_diff_split power_eq_if power_mult semiring_normalization_rules(7) z_def)
[PROOF STATE]
proof (state)
this:
[z = 0] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[z = 0] (mod Q)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
[x \<noteq> 0] (mod Q)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
have "[e * d = 1] (mod ((P - 1) * (Q - 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [e * d = 1] (mod (P - 1) * (Q - 1))
[PROOF STEP]
by (metis d bezw_inverse coprime coprime_imp_gcd_eq_1 nat_int)
[PROOF STATE]
proof (state)
this:
[e * d = 1] (mod (P - 1) * (Q - 1))

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
hence "[e * d = 1] (mod (Q - 1))"
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod (P - 1) * (Q - 1))

goal (1 subgoal):
 1. [e * d = 1] (mod Q - 1)
[PROOF STEP]
using assms cong_modulus_mult_nat mult.commute
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod (P - 1) * (Q - 1))
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
1 < e
1 < d
[?x = ?y] (mod ?m * ?n) \<Longrightarrow> [?x = ?y] (mod ?m)
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. [e * d = 1] (mod Q - 1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[e * d = 1] (mod Q - 1)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e * d = 1] (mod Q - 1)
[PROOF STEP]
obtain k where k: "e*d = 1 + k*(Q-1)"
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod Q - 1)

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (Q - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_k_mod assms
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod Q - 1)
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); ?P \<noteq> ?Q; prime ?P; prime ?Q; ?d \<noteq> 0; [?e * ?d = 1] (mod ?P - 1)\<rbrakk> \<Longrightarrow> \<exists>k. ?e * ?d = 1 + k * (?P - 1)
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
1 < e
1 < d

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (Q - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
e * d = 1 + k * (Q - 1)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
hence "x ^ (e * d) = x * ((x ^ (Q - 1)) ^ k)"
[PROOF STATE]
proof (prove)
using this:
e * d = 1 + k * (Q - 1)

goal (1 subgoal):
 1. x ^ (e * d) = x * (x ^ (Q - 1)) ^ k
[PROOF STEP]
by (metis power_add power_one_right mult.commute power_mult)
[PROOF STATE]
proof (state)
this:
x ^ (e * d) = x * (x ^ (Q - 1)) ^ k

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
hence "[x ^ (e * d) = x * ((x ^ (Q - 1)) ^ k)] (mod P)"
[PROOF STATE]
proof (prove)
using this:
x ^ (e * d) = x * (x ^ (Q - 1)) ^ k

goal (1 subgoal):
 1. [x ^ (e * d) = x * (x ^ (Q - 1)) ^ k] (mod P)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
x ^ (e * d) = x * (x ^ (Q - 1)) ^ k
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. [x ^ (e * d) = x * (x ^ (Q - 1)) ^ k] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x * (x ^ (Q - 1)) ^ k] (mod P)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x * (x ^ (Q - 1)) ^ k] (mod P)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
have "[x ^ (Q - 1) = 1] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (Q - 1) = 1] (mod Q)
[PROOF STEP]
using prime_Q fermat_theorem False
[PROOF STATE]
proof (prove)
using this:
prime Q
\<lbrakk>prime ?p; \<not> ?p dvd ?a\<rbrakk> \<Longrightarrow> [?a ^ (?p - 1) = 1] (mod ?p)
[x \<noteq> 0] (mod Q)

goal (1 subgoal):
 1. [x ^ (Q - 1) = 1] (mod Q)
[PROOF STEP]
by (simp add: cong_0_iff)
[PROOF STATE]
proof (state)
this:
[x ^ (Q - 1) = 1] (mod Q)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[x ^ (Q - 1) = 1] (mod Q)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
have "[x ^ (e * d) = x * ((1) ^ k)] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (e * d) = x * 1 ^ k] (mod Q)
[PROOF STEP]
by (metis \<open>x ^ (e * d) = x * (x ^ (Q - 1)) ^ k\<close> calculation(2) cong_pow cong_scalar_left)
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x * 1 ^ k] (mod Q)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
hence "[x ^ (e * d) = x] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = x * 1 ^ k] (mod Q)

goal (1 subgoal):
 1. [x ^ (e * d) = x] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = x] (mod Q)

goal (1 subgoal):
 1. [x \<noteq> 0] (mod Q) \<Longrightarrow> [z = 0] (mod Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = x] (mod Q)

goal (1 subgoal):
 1. [z = 0] (mod Q)
[PROOF STEP]
using z_def z_gt_0
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = x] (mod Q)
z = (x ^ e) ^ d - x
0 < z

goal (1 subgoal):
 1. [z = 0] (mod Q)
[PROOF STEP]
by (simp add: cong_diff_iff_cong_0_nat power_mult)
[PROOF STATE]
proof (state)
this:
[z = 0] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[z = 0] (mod Q)

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[z = 0] (mod P)
[z = 0] (mod Q)
[PROOF STEP]
have "Q dvd (x ^ e) ^ d - x"
                  "P dvd (x ^ e) ^ d - x"
[PROOF STATE]
proof (prove)
using this:
[z = 0] (mod P)
[z = 0] (mod Q)

goal (1 subgoal):
 1. Q dvd (x ^ e) ^ d - x &&& P dvd (x ^ e) ^ d - x
[PROOF STEP]
using z_def assms cong_0_iff
[PROOF STATE]
proof (prove)
using this:
[z = 0] (mod P)
[z = 0] (mod Q)
z = (x ^ e) ^ d - x
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
1 < e
1 < d
[?b = 0::?'a] (mod ?a) = (?a dvd ?b)

goal (1 subgoal):
 1. Q dvd (x ^ e) ^ d - x &&& P dvd (x ^ e) ^ d - x
[PROOF STEP]
by blast +
[PROOF STATE]
proof (state)
this:
Q dvd (x ^ e) ^ d - x
P dvd (x ^ e) ^ d - x

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
hence "P * Q dvd ((x ^ e) ^ d - x)"
[PROOF STATE]
proof (prove)
using this:
Q dvd (x ^ e) ^ d - x
P dvd (x ^ e) ^ d - x

goal (1 subgoal):
 1. P * Q dvd (x ^ e) ^ d - x
[PROOF STEP]
using assms divides_mult primes_coprime_nat
[PROOF STATE]
proof (prove)
using this:
Q dvd (x ^ e) ^ d - x
P dvd (x ^ e) ^ d - x
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
1 < e
1 < d
\<lbrakk>?a dvd ?c; ?b dvd ?c; coprime ?a ?b\<rbrakk> \<Longrightarrow> ?a * ?b dvd ?c
\<lbrakk>prime ?p; prime ?q; ?p \<noteq> ?q\<rbrakk> \<Longrightarrow> coprime ?p ?q

goal (1 subgoal):
 1. P * Q dvd (x ^ e) ^ d - x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P * Q dvd (x ^ e) ^ d - x

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
hence "[(x ^ e) ^ d = x] (mod (P * Q))"
[PROOF STATE]
proof (prove)
using this:
P * Q dvd (x ^ e) ^ d - x

goal (1 subgoal):
 1. [(x ^ e) ^ d = x] (mod P * Q)
[PROOF STEP]
using z_gt_0 cong_altdef_nat z_def
[PROOF STATE]
proof (prove)
using this:
P * Q dvd (x ^ e) ^ d - x
0 < z
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
z = (x ^ e) ^ d - x

goal (1 subgoal):
 1. [(x ^ e) ^ d = x] (mod P * Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(x ^ e) ^ d = x] (mod P * Q)

goal (1 subgoal):
 1. \<not> (x = 0 \<or> x = 1) \<Longrightarrow> (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[(x ^ e) ^ d = x] (mod P * Q)

goal (1 subgoal):
 1. (x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)
[PROOF STEP]
by (simp add: cong_def power_mod)
[PROOF STATE]
proof (state)
this:
(x ^ e mod (P * Q)) ^ d mod (P * Q) = x mod (P * Q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rsa_inv_set_spmf_I:
  assumes "((N, e), d) \<in> set_spmf I"
  shows "((((x::nat) ^ e) mod N) ^ d) mod N = x mod N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ^ e mod N) ^ d mod N = x mod N
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x ^ e mod N) ^ d mod N = x mod N
[PROOF STEP]
obtain P Q where "N = P * Q" and "d = nat (fst (bezw e ((P-1)*(Q-1))) mod int ((P-1)*(Q-1)))"
    and "prime P"
    and "prime Q"
    and "coprime e ((P - 1)*(Q - 1))"
    and "P \<noteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>N = P * Q; d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1))); prime P; prime Q; coprime e ((P - 1) * (Q - 1)); P \<noteq> Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms set_spmf_I_N
[PROOF STATE]
proof (prove)
using this:
((N, e), d) \<in> set_spmf I
\<lbrakk>((?N, ?e), ?d) \<in> set_spmf I; \<And>P Q. \<lbrakk>?N = P * Q; P \<noteq> Q; prime P; prime Q; coprime ?e ((P - 1) * (Q - 1)); ?d = nat (fst (bezw ?e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>N = P * Q; d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1))); prime P; prime Q; coprime e ((P - 1) * (Q - 1)); P \<noteq> Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
N = P * Q
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
prime P
prime Q
coprime e ((P - 1) * (Q - 1))
P \<noteq> Q

goal (1 subgoal):
 1. (x ^ e mod N) ^ d mod N = x mod N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
N = P * Q
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
prime P
prime Q
coprime e ((P - 1) * (Q - 1))
P \<noteq> Q

goal (1 subgoal):
 1. (x ^ e mod N) ^ d mod N = x mod N
[PROOF STEP]
have "e > 1" and "d > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < e &&& 1 < d
[PROOF STEP]
using set_spmf_I_e_d assms
[PROOF STATE]
proof (prove)
using this:
((?N, ?e), ?d) \<in> set_spmf I \<Longrightarrow> 1 < ?e
((?N, ?e), ?d) \<in> set_spmf I \<Longrightarrow> 1 < ?d
((N, e), d) \<in> set_spmf I

goal (1 subgoal):
 1. 1 < e &&& 1 < d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < e
1 < d

goal (1 subgoal):
 1. (x ^ e mod N) ^ d mod N = x mod N
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
N = P * Q
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
prime P
prime Q
coprime e ((P - 1) * (Q - 1))
P \<noteq> Q
1 < e
1 < d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N = P * Q
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
prime P
prime Q
coprime e ((P - 1) * (Q - 1))
P \<noteq> Q
1 < e
1 < d

goal (1 subgoal):
 1. (x ^ e mod N) ^ d mod N = x mod N
[PROOF STEP]
using rsa_inv
[PROOF STATE]
proof (prove)
using this:
N = P * Q
d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))
prime P
prime Q
coprime e ((P - 1) * (Q - 1))
P \<noteq> Q
1 < e
1 < d
\<lbrakk>?d = nat (fst (bezw ?e ((?P - 1) * (?Q - 1))) mod int ((?P - 1) * (?Q - 1))); coprime ?e ((?P - 1) * (?Q - 1)); prime ?P; prime ?Q; ?P \<noteq> ?Q; 1 < ?e; 1 < ?d\<rbrakk> \<Longrightarrow> (?x ^ ?e mod (?P * ?Q)) ^ ?d mod (?P * ?Q) = ?x mod (?P * ?Q)

goal (1 subgoal):
 1. (x ^ e mod N) ^ d mod N = x mod N
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x ^ e mod N) ^ d mod N = x mod N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma correctness_rsa: "etp.OT_12.correctness m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. etp.OT_12.correctness m1 m2
[PROOF STEP]
by (rule local.etp.correct)


[STATEMENT]
lemma P1_security_rsa: "etp.OT_12.perfect_sec_P1 m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. etp.OT_12.perfect_sec_P1 m1 m2
[PROOF STEP]
by(rule local.etp.P1_security_inf_the)


[STATEMENT]
lemma P2_security_rsa:
  assumes "\<forall> a. lossless_spmf (D a)"
    and "\<And>b\<^sub>\<sigma>. local.etp_rsa.HCP_adv etp.\<A> m2 b\<^sub>\<sigma> D \<le> HCP_ad"
  shows "etp.OT_12.adv_P2 m1 m2 D \<le> 2 * HCP_ad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. etp.OT_12.adv_P2 m1 m2 D \<le> 2 * HCP_ad
[PROOF STEP]
by(simp add: local.etp.P2_security assms)


[STATEMENT]
lemma correctness_rsa_asymp:
  shows "etp.OT_12.correctness n m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. etp.OT_12.correctness n m1 m2
[PROOF STEP]
by(rule correctness_rsa)


[STATEMENT]
lemma P1_sec_asymp: "etp.OT_12.perfect_sec_P1 n m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. etp.OT_12.perfect_sec_P1 n m1 m2
[PROOF STEP]
by(rule local.P1_security_rsa)


[STATEMENT]
lemma P2_sec_asym:
  assumes "\<forall> a. lossless_spmf (D a)"
    and HCP_adv_neg: "negligible (\<lambda> n. hcp_advantage n)"
    and hcp_adv_bound:  "\<forall>b\<^sub>\<sigma> n. local.etp_rsa.HCP_adv n etp.\<A> m2 b\<^sub>\<sigma> D \<le> hcp_advantage n"
  shows "negligible (\<lambda> n. etp.OT_12.adv_P2 n m1 m2 D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
have "negligible (\<lambda> n. 2 * hcp_advantage n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. 2 * hcp_advantage n)
[PROOF STEP]
using HCP_adv_neg
[PROOF STATE]
proof (prove)
using this:
Negligible.negligible hcp_advantage

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. 2 * hcp_advantage n)
[PROOF STEP]
by (simp add: negligible_cmultI)
[PROOF STATE]
proof (state)
this:
Negligible.negligible (\<lambda>n. 2 * hcp_advantage n)

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Negligible.negligible (\<lambda>n. 2 * hcp_advantage n)

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
have "\<bar>etp.OT_12.adv_P2 n m1 m2 D\<bar> = etp.OT_12.adv_P2 n m1 m2 D"
    for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>etp.OT_12.adv_P2 n m1 m2 D\<bar> = etp.OT_12.adv_P2 n m1 m2 D
[PROOF STEP]
unfolding sim_det_def.adv_P2_def local.etp.OT_12.adv_P2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<bar>spmf (etp.R2 n m1 m2 \<bind> D) True - spmf (funct_OT_12 m1 m2 \<bind> (\<lambda>(o1, o2). etp.S2 n m2 o2 \<bind> D)) True\<bar>\<bar> = \<bar>spmf (etp.R2 n m1 m2 \<bind> D) True - spmf (funct_OT_12 m1 m2 \<bind> (\<lambda>(o1, o2). etp.S2 n m2 o2 \<bind> D)) True\<bar>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<bar>etp.OT_12.adv_P2 ?n m1 m2 D\<bar> = etp.OT_12.adv_P2 ?n m1 m2 D

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>etp.OT_12.adv_P2 ?n m1 m2 D\<bar> = etp.OT_12.adv_P2 ?n m1 m2 D

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
have "etp.OT_12.adv_P2 n m1 m2 D \<le> 2 * hcp_advantage n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. etp.OT_12.adv_P2 n m1 m2 D \<le> 2 * hcp_advantage n
[PROOF STEP]
using P2_security_rsa assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>a. lossless_spmf (?D a); \<And>b\<^sub>\<sigma>. etp_rsa.HCP_adv ?n etp.\<A> ?m2.0 b\<^sub>\<sigma> ?D \<le> ?HCP_ad\<rbrakk> \<Longrightarrow> etp.OT_12.adv_P2 ?n ?m1.0 ?m2.0 ?D \<le> 2 * ?HCP_ad
\<forall>a. lossless_spmf (D a)
Negligible.negligible hcp_advantage
\<forall>b\<^sub>\<sigma> n. etp_rsa.HCP_adv n etp.\<A> m2 b\<^sub>\<sigma> D \<le> hcp_advantage n

goal (1 subgoal):
 1. etp.OT_12.adv_P2 n m1 m2 D \<le> 2 * hcp_advantage n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
etp.OT_12.adv_P2 ?n m1 m2 D \<le> 2 * hcp_advantage ?n

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Negligible.negligible (\<lambda>n. 2 * hcp_advantage n)
\<bar>etp.OT_12.adv_P2 ?n m1 m2 D\<bar> = etp.OT_12.adv_P2 ?n m1 m2 D
etp.OT_12.adv_P2 ?n m1 m2 D \<le> 2 * hcp_advantage ?n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Negligible.negligible (\<lambda>n. 2 * hcp_advantage n)
\<bar>etp.OT_12.adv_P2 ?n m1 m2 D\<bar> = etp.OT_12.adv_P2 ?n m1 m2 D
etp.OT_12.adv_P2 ?n m1 m2 D \<le> 2 * hcp_advantage ?n

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
using assms negligible_le
[PROOF STATE]
proof (prove)
using this:
Negligible.negligible (\<lambda>n. 2 * hcp_advantage n)
\<bar>etp.OT_12.adv_P2 ?n m1 m2 D\<bar> = etp.OT_12.adv_P2 ?n m1 m2 D
etp.OT_12.adv_P2 ?n m1 m2 D \<le> 2 * hcp_advantage ?n
\<forall>a. lossless_spmf (D a)
Negligible.negligible hcp_advantage
\<forall>b\<^sub>\<sigma> n. etp_rsa.HCP_adv n etp.\<A> m2 b\<^sub>\<sigma> D \<le> hcp_advantage n
\<lbrakk>Negligible.negligible ?g; \<And>\<eta>. \<bar>?f \<eta>\<bar> \<le> ?g \<eta>\<rbrakk> \<Longrightarrow> Negligible.negligible ?f

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
Negligible.negligible (\<lambda>n. etp.OT_12.adv_P2 n m1 m2 D)

goal:
No subgoals!
[PROOF STEP]
qed