Add Differential Cryptanalysis and RC5

[gengarrrr]

I added some Differential Cryptanalysis related properties and part of RC5 definitions.

[prob_uniform_on_finite_set]
  ⊢ ∀ p. FINITE (p_space p) ∧ p_space p ̸= { } ∧
      events p = POW (p_space p) ∧
     (∀ s. s ∈ events p ⇒
     prob p s = &CARD s / &CARD (p_space p)) ⇒
     prob_space p

 [prob_space_word6p]
  ⊢ prob_space word6p

  [prob_space_word48p]
  ⊢ prob_space word48p

 [XcauseYF’_def]
 ⊢ ∀ X Y .
     XcauseYF’ X Y = prob word48p { x | S x ⊕ S (x ⊕ E X ) = Y }

 [XcauseYFkey_def]
  ⊢ ∀ X Y x.
     XcauseYFkey X Y x =
     (let x′= x ⊕ E X
      in prob word48p { k | S (x ⊕ k) ⊕ S (x′ ⊕ k) = Y })

  [XcauseYF_convert]
  ⊢ ∀ X Y x. XcauseYFkey X Y x = XcauseYF’ X Y

   [XcauseYFp_eq]
   ⊢ ∀ X Y .
       Xe = E X ∧ Xl = splitXF Xe ∧ Yl = splitYF Y ⇒
       XcauseYF’ X Y =
       Π (λ i. XcauseY (EL i Xl) (EL i Yl) (SBox (EL i S_data)))
       (count 8)

They help define the probability space in HOL4, create partly the probability definition "X may cause Y with probability p by the F function " . Prove the lemma "In DES if X -> Y with probability p by the F function, then every fixed input pair Z, Z with Z' = Z -> Z = X causes the F function output XOR to be Y by the same fraction p of the possible subkey values." and "The probability p of X -> Y by the F function is the product of Pi in which Xi -> Yi by the S boxes Si (i ~ {1 ..... 8})"

Then I define the RC5 partly in HOL4

 [Skeys_def]

 [rc5keys_def]
  ⊢ ∀ r k.
     rc5keys r k =
     (let n = 3 × MAX (2 × (r + 1)) 2 in keys n r k)

 [RoundEn_def]

 [RoundDe_def]

 [RoundDe’_def]

 [RoundDe’_def]

 [RoundEe’_De’]
  ⊢ ∀ n b ki ki2. RoundDe’ n ki ki2 (RoundEn’ n ki ki2 b) = b

The " ' " version simplify the encrypt and decrypt process and show the correctness by encrypting and decrypting that return the originial message.

[binghe]

To @mn200: The student project has finished. I suggest we just merging the present work as is (please squash all commits to one), and I will handle the remaining work, including code cleanup.

[gengarrrr]

To @mn200: The student project has finished. I suggest we just merging the present work as is (please squash all commits to one), and I will handle the remaining work, including code cleanup.

Thanks a lot for the guidance and support