Theory tSDH_assumption

theory tSDH_assumption

imports "Sigma_Commit_Crypto.Commitment_Schemes" "Berlekamp_Zassenhaus.Finite_Field"

begin

section ‹The t-Strong Diffie-Hellman Assumption›

text‹The t-SDH game and advantage as in section 2.3 of the original KZG paper
``Constant-Size Commitments to Polynomials and Their Applications'' \<^cite>‹KZG10›.›

locale t_SDH = G : cyclic_group G
  for G:: "('a, 'b) cyclic_group_scheme" (structure) 
  and t::nat  
  and to_type :: "nat ⇒ ('c::prime_card) mod_ring"
  and exp :: "'a ⇒ 'c mod_ring ⇒ 'a"
begin

type_synonym ('grp,'mr) adversary = "'grp list ⇒ ('mr mod_ring *'grp) spmf"

text ‹The t-SDH game states that given a t+1-long tuple in the form of $(g, g^\alpha, g^{\alpha^2}, \ldots, g^{\alpha^t})$
the Adversary has to return an element c and $g^{1/(c+\alpha)}$.›
definition game :: "('a,'c) adversary ⇒ bool spmf" where 
  "game 𝒜 = TRY do { 
    α ← sample_uniform (Coset.order G);
    (c, g) ← 𝒜 (map (λt'. exp ❙g ((to_type α)^t')) [0..<t+1]);
    return_spmf (exp ❙g (1/((to_type α)+c)) = g) 
  } ELSE return_spmf False"

text ‹The advantage is that the Adversary wins the game. 
For the t-SDH assumption to hold this advantage should be negligible.›
definition advantage :: " ('a,'c) adversary ⇒ real"
  where "advantage 𝒜 = spmf (game 𝒜) True" 

text ‹An alternative but equivalent game for the t-SDH-game. This alternative game capsulates the 
event that the Adversary wins in the assert\_spmf statement.
adapted proof from Sigma\_Commit\_Crypto.Commitment\_Schemes bind\_game\_alt\_def›
lemma game_alt_def:
  "game 𝒜 = TRY do { 
    α ← sample_uniform (Coset.order G);
    (c, g) ← 𝒜 (map (λt'. exp ❙g ((to_type α)^t')) [0..<t+1]);
    _::unit ← assert_spmf (exp ❙g (1/((to_type α)+c)) = g);
    return_spmf True 
  } ELSE return_spmf False"
  (is "?lhs = ?rhs")
proof -
   have "?lhs = TRY do {
      α ← sample_uniform (Coset.order G);
      TRY do {
        (c, g) ← 𝒜 (map (λt'. exp ❙g ((to_type α)^t')) [0..<t+1]);
          TRY return_spmf (exp ❙g (1/((to_type α)+c)) = g) 
          ELSE return_spmf False
      } ELSE return_spmf False
    } ELSE return_spmf False"
    unfolding split_def game_def
    by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
  also have "… = TRY do {
      α ← sample_uniform (Coset.order G);
      TRY do {
        (c, g) ← 𝒜 (map (λt'. exp ❙g ((to_type α)^t')) [0..<t+1]);
          TRY do {
            _ :: unit ← assert_spmf (exp ❙g (1/((to_type α)+c)) = g);
            return_spmf True
        } ELSE return_spmf False
      } ELSE return_spmf False
    } ELSE return_spmf False"
    by(auto simp add: try_bind_assert_spmf try_spmf_return_spmf1 intro!: try_spmf_cong bind_spmf_cong)
  also have "… = ?rhs"
    unfolding split_def Let_def
    by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
  finally show ?thesis .
qed

end

end