Theory Pairing

theory Pairing 

imports  "CryptHOL.CryptHOL" "CryptHOL.Cyclic_Group" Berlekamp_Zassenhaus.Finite_Field
  "Sigma_Commit_Crypto.Cyclic_Group_Ext" "HOL-Number_Theory.Cong"
begin

section ‹Pairings›

hide_const Polynomial.order

text‹We formalize symmetric pairings for cryptography following the textbook
``A Graduate Course in Applied Cryptography'' by Boneh and Shoup \<^cite>‹BonehShoup›.›

locale pairing =
G⇩p : cyclic_group G⇩p + G⇩T : cyclic_group G⇩T 
for G⇩p :: "('a, 'b) cyclic_group_scheme" (structure) 
and G⇩T:: "('c, 'd) cyclic_group_scheme"  (structure) 
+
fixes p::int
  and e
assumes
p_prime : "prime p" and
CARD_G⇩p: "int (order G⇩p) = p" and
CARD_G⇩T: "int (order G⇩T) = p" and
e_symmetric: "e ∈ carrier G⇩p → carrier G⇩p → carrier G⇩T" and 
e_bilinearity[simp]: "∀a b::int . ∀P Q. P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p ⟶ 
   e (P [^]⇘G⇩p⇙ a) (Q [^]⇘G⇩p⇙ b) 
= (e P Q) [^]⇘G⇩T⇙ (a*b)" and 
e_non_degeneracy[simp]: "¬(∀P Q. P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p ⟶ e P Q = 𝟭⇘G⇩T⇙)"
begin

text ‹The pairing function e is linear in the first component›
lemma e_linear_in_fst: 
  assumes "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p"
  shows "e (P [^]⇘G⇩p⇙ (a::int)) Q = (e P Q) [^]⇘G⇩T⇙ a"
proof -
  have "e (P [^]⇘G⇩p⇙ a) Q = e (P [^]⇘G⇩p⇙ a) (Q [^]⇘G⇩p⇙ (1::int))" using assms by simp
  also have "... = (e P Q) [^]⇘G⇩T⇙ (a*(1::int))" using assms e_bilinearity by fast
  also have "…=(e P Q) [^]⇘G⇩T⇙ a" by simp
  finally show "e (P [^]⇘G⇩p⇙ a) Q = (e P Q) [^]⇘G⇩T⇙ a" .
qed

text ‹The pairing function e is linear in the second component›
lemma e_linear_in_snd: 
  assumes "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p"
  shows "e P (Q [^]⇘G⇩p⇙ (a::int)) = (e P Q) [^]⇘G⇩T⇙ a"
proof -
  have "e P (Q  [^]⇘G⇩p⇙ a) = e (P [^]⇘G⇩p⇙ (1::int)) (Q [^]⇘G⇩p⇙ a)" using assms by simp
  also have "... = (e P Q) [^]⇘G⇩T⇙ ((1::int)*a)" using assms e_bilinearity by fast
  also have "…=(e P Q) [^]⇘G⇩T⇙ a" by simp
  finally show "e P (Q [^]⇘G⇩p⇙ a) = (e P Q) [^]⇘G⇩T⇙ a" .
qed

lemma addition_in_exponents_on_e[simp]: 
  assumes "x ∈ carrier G⇩p ∧ y ∈ carrier G⇩p "
  shows "(e x y) [^]⇘G⇩T⇙ (a::int) ⊗⇘G⇩T⇙ (e x y) [^]⇘G⇩T⇙ (b::int) = (e x y) [^]⇘G⇩T⇙ (a+b)"
  by (metis G⇩T.int_pow_mult assms PiE e_symmetric)

text ‹this follows from non-degeneracy›
lemma e_from_generators_ne_1: "e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ≠ 𝟭⇘G⇩T⇙"
proof 
  assume asm: "e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ = 𝟭⇘G⇩T⇙"
  have "∀P Q. P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p ⟶ e P Q = 𝟭⇘G⇩T⇙" 
  proof(intro allI)
    fix P Q
    show "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p ⟶ e P Q = 𝟭⇘G⇩T⇙ "
    proof 
      assume "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p"
      then obtain p q::int where "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ p = P ∧ ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ q = Q"
        by (metis G⇩p.generatorE int_pow_int)
      then have "e P Q = e (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ p) (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ q)"
        by blast
      also have "… = e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ [^]⇘G⇩T⇙ (p*q)"
        by force
      also have "… =  𝟭⇘G⇩T⇙ [^]⇘G⇩T⇙ (p*q)"
        using asm by argo
      also have "… =  𝟭⇘G⇩T⇙"
        by fastforce
      finally show "e P Q = 𝟭⇘G⇩T⇙" .
    qed
  qed
  then show "False" using e_non_degeneracy by blast
qed

lemma e_g_g_in_carrier_GT[simp]: "e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ∈ carrier G⇩T"
  using e_symmetric by fast

text ‹mod relations on the exponent (typically useful for cryptographic proofs)›

lemma pow_on_eq_card_GT[simp]: "(❙g⇘G⇩T⇙ [^]⇘G⇩T⇙ (x::int) = ❙g⇘G⇩T⇙ [^]⇘G⇩T⇙ (y::int)) = ([x= y] (mod p))"
 by (metis (no_types, lifting) CARD_G⇩T G⇩T.finite_carrier G⇩T.gen_power_0 G⇩T.generator_closed G⇩T.int_pow_eq G⇩T.ord_ge_1 G⇩T.ord_le_group_order G⇩T.pow_ord_eq_1 One_nat_def add_diff_inverse_nat arith_extra_simps(6) cong_iff_dvd_diff diff_is_0_eq' less_eq_Suc_le
      zero_order(5))

lemma pow_on_eq_card_GT_carrier_ext'[simp]: 
  "((e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙)) [^]⇘G⇩T⇙ x = ((e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙)) [^]⇘G⇩T⇙ y ⟷ [x= y] (mod p)"
  by (metis CARD_G⇩T G⇩T.finite_carrier G⇩T.int_pow_eq G⇩T.ord_dvd_group_order G⇩T.ord_eq_1 G⇩T.ord_id G⇩T.pow_ord_eq_ord_iff G⇩T.pow_order_eq_1 cong_iff_dvd_diff dvd_antisym e_from_generators_ne_1 e_g_g_in_carrier_GT p_prime prime_imp_coprime prime_nat_int_transfer)

end

end