DES weak keys' fixed points' properties and cardinality. Xor property within F function in DES

[gengarrrr]

Hi, From "Each weak key w has 2^32 fixed points m where DESw(m)=m", I added the definition of fixed points, proved DESw(m)=m and cardinality of 2^32.

[Wtext_def]  Definition
  ⊢ ∀key.
      Wtext key = {x | ∃w. Split (IP (desCore 8 (KS key 8) x)) = (w,w)}

[Wtext1_def]  Theorem
  ⊢ Wtext1 = {x | ∃w. Split (IP (desCore 8 (KS Wkey1 8) x)) = (w,w)}

[Wtext2_def]  Theorem
  ⊢ Wtext2 = {x | ∃w. Split (IP (desCore 8 (KS Wkey2 8) x)) = (w,w)}

[Wtext3_def]  Theorem
  ⊢ Wtext3 = {x | ∃w. Split (IP (desCore 8 (KS Wkey3 8) x)) = (w,w)}

[Wtext4_def]  Theorem
  ⊢ Wtext4 = {x | ∃w. Split (IP (desCore 8 (KS Wkey4 8) x)) = (w,w)}

[Wtextlist_def]  Definition
  ⊢ Wtextlist = [Wtext1; Wtext2; Wtext3; Wtext4]

they defines fixed points for each weak key as a set, as the set of the property of DESw(m)=m and card of 2^32

[weakK_sup]  Theorem
  ⊢ ∀n k.
      MEM k Wkey ∧ 0 ≤ n ∧ n ≤ 8 ∧
      Split (IP (desCore 8 (KS k 8) x)) = (w,w) ⇒
      Round (8 − n) (KS k 16) (Split (IP x)) =
      Swap (Round (8 + n) (KS k 16) (Split (IP x)))

[wkey1_equal]  Theorem
  ⊢ ∀x n k.
      MEM k Wkey ∧ n ≤ 8 ⇒
      Round n (KS k 8) (Split x) = Round n (KS k 16) (Split x)

they support the prove of DESw(m)=m，proves round keys are the same in the same rounds and left part of round 8-k output equals right part of round 8+k output.

 [weakK1_proper2]  Theorem
  ⊢ ∀x. x ∈ Wtext1 ∧ FullDES Wkey1 = (encrypt,decrypt) ⇒ encrypt x = x

[weakK2_proper2]  Theorem
  ⊢ ∀x. x ∈ Wtext2 ∧ FullDES Wkey2 = (encrypt,decrypt) ⇒ encrypt x = x

[weakK3_proper2]  Theorem
  ⊢ ∀x. x ∈ Wtext3 ∧ FullDES Wkey3 = (encrypt,decrypt) ⇒ encrypt x = x

[weakK4_proper2]  Theorem
  ⊢ ∀x. x ∈ Wtext4 ∧ FullDES Wkey4 = (encrypt,decrypt) ⇒ encrypt x = x

These proves the property of fixed points that DESw(m)=m for each weak key

[BIJ_for_weak_keys]  Theorem
  ⊢ ∀x. MEM x Wtextlist ⇒ ∃f. BIJ f x 𝕌(:word32)

[BIJ_for_weak_keys_explicit]  Theorem
  ⊢ ∀i. i < 4 ⇒ BIJ (EL i wtrans1) (EL i Wtextlist) 𝕌(:word32)

[BIJ_wtext1]  Theorem
  ⊢ BIJ w1trans1 Wtext1 𝕌(:word32)

[BIJ_wtext2]  Theorem
  ⊢ BIJ w2trans1 Wtext2 𝕌(:word32)

[BIJ_wtext3]  Theorem
  ⊢ BIJ w3trans1 Wtext3 𝕌(:word32)

[BIJ_wtext4]  Theorem
  ⊢ BIJ w4trans1 Wtext4 𝕌(:word32)

These theorems prove that there are four functions that are bijective from the fixed points sets for each weak key to the universe of all words of 32.

 [DES_fp_non_weak_keys]  Theorem
  ⊢ ∀i. i < LENGTH non_weak_keys ⇒
        (let
           (key,plaintext) = EL i non_weak_keys;
           (encrypt,decrypt) = FullDES key
         in
           encrypt plaintext = plaintext)
  
 [text_num]  Theorem
  ⊢ ∀x. MEM x Wtextlist ⇒ CARD x = CARD 𝕌(:word32)

Thus, we can prove the fixed points sets have card equal to universe of all words of 32, 2^32.

[w1trans1_def]  Definition
  ⊢ ∀x. w1trans1 x = FST (Split (IP (desCore 8 (KS Wkey1 8) x)))

[w1trans2_def]  Definition
  ⊢ ∀x. w1trans2 x = desCore 8 (KS Wkey1 8) (IIP (Join (x,x)))

[w2trans1_def]  Definition
  ⊢ ∀x. w2trans1 x = FST (Split (IP (desCore 8 (KS Wkey2 8) x)))

[w2trans2_def]  Definition
  ⊢ ∀x. w2trans2 x = desCore 8 (KS Wkey2 8) (IIP (Join (x,x)))

[w3trans1_def]  Definition
  ⊢ ∀x. w3trans1 x = FST (Split (IP (desCore 8 (KS Wkey3 8) x)))

[w3trans2_def]  Definition
  
  ⊢ ∀x. w3trans2 x = desCore 8 (KS Wkey3 8) (IIP (Join (x,x)))

[w4trans1_def]  Definition
  ⊢ ∀x. w4trans1 x = FST (Split (IP (desCore 8 (KS Wkey4 8) x)))

[w4trans2_def]  Definition
  ⊢ ∀x. w4trans2 x = desCore 8 (KS Wkey4 8) (IIP (Join (x,x)))

These are the bijective functions from fixed points sets to universe of all words of 32, and vice versa

[non_weak_keys_def]  Definition
  ⊢ non_weak_keys =
    [(0xB0B351C802C83DE0w,0x4739A2F04B7EAB28w);
     (0x5D460701328F2962w,0x9FE10D2E8C496143w);
     (0x4F4CAE37FD37C21Fw,0xB8C65D0FB48154D7w);
     (0xA2B9F8FECD70D69Dw,0x601EF2D173B69EBCw)]

 [DES_fp_non_weak_keys]  Theorem
  ⊢ ∀i. i < LENGTH non_weak_keys ⇒
        (let
           (key,plaintext) = EL i non_weak_keys;
           (encrypt,decrypt) = FullDES key
         in
           encrypt plaintext = plaintext)

It defines some non weak keys and corresponding plaintexts that also follow the property of DESw(m)=m.

Then there are few theorems proves the linearity in DES

[xor_E]  Theorem
  ⊢ ∀x1 x2. E x1 ⊕ E x2 = E (x1 ⊕ x2)

[xor_P]  Theorem
  ⊢ ∀x1 x2. P x1 ⊕ P x2 = P (x1 ⊕ x2)

[xor_S1]  Theorem
  ⊢ ∃x1 x2. S1 x1 ⊕ S1 x2 ≠ S1 (x1 ⊕ x2)

They proves the E (extend) and P (permutation) functions are linear for xor, while S1 function is not. They are for further use.

-- Ruofan Yang

[binghe]

Yang, please merge from develop again to get the CI tests run again. I remember you only use stdknl and it's possible that the new code may not run in expk (you can clone another HOL repository and do bin/build --expk to test your code locally when sending new PRs).

[gengarrrr]

Yang, please merge from develop again to get the CI tests run again. I remember you only use stdknl and it's possible that the new code may not run in expk (you can clone another HOL repository and do bin/build --expk to test your code locally when sending new PRs).

Thanks, the tests are passed.

[mn200]

Thanks for all your work on this!