Des properties added

[gengarrrr]

add provings of some DES properties- complement property and weak/semi-weak key

[binghe]

Hi, a good style of sending PRs (here) is to put the main theorems (with statements copied from the generated des_propThery.sig) you have proved, with some informal descriptions (e.g. explain what is "complement property" and what are "weak/semi-weak keys" for DES).

[binghe]

And there's no need to create another deeper sub-directory. Please move your des_propScript.sml into the same directory with desScript.sml.

[gengarrrr]

[comple_property]  Theorem

  ⊢ ∀k m n. 0 < n ∧ n < 17 ⇒ ¬FST (DES n k) m = FST (DES n (¬k)) (¬m)

comple_property proves: The complement of the DES encryption of message m with key k is equal to the encryption of message m' (the bitwise complement of m) with key k' (the bitwise complement of k)

[weakK_proper]  Theorem

  ⊢ ∀k plaintext.
      MEM k Wkey ⇒
      FST (FullDES k) (FST (FullDES k) plaintext) = plaintext

weakK_proper shows: the property of the four weak keys in DES - Encrypting the message m with the same weak key twice will leave message m unchanged

[semiK_proper1]  Theorem

  ⊢ ∀plaintext pair.
      MEM pair Semiwkey ⇒
      FST (FullDES (FST pair)) (FST (FullDES (SND pair)) plaintext) =
      plaintext

[semiK_proper2]  Theorem

  ⊢ ∀plaintext pair.
      MEM pair Semiwkey ⇒
      FST (FullDES (SND pair)) (FST (FullDES (FST pair)) plaintext) =
      plaintext

semiK_proper1/2 show: the property of six pair of semi-weak keys in DES - Encrypting the message m twice with a pair of semi-weak key will leave message m unchanged

[mn200]

Thanks for the theorem statements! In my experience, when dealing with functions returning tuples (e.g., DES here) it is better to have an assumption DES args = (x,y) and to then state properties of x rather than FST (DES args).

[gengarrrr]

Thanks for the theorem statements! In my experience, when dealing with functions returning tuples (e.g., DES here) it is better to have an assumption DES args = (x,y) and to then state properties of x rather than FST (DES args).

Thanks, changes made.

[gengarrrr]

And there's no need to create another deeper sub-directory. Please move your des_propScript.sml into the same directory with desScript.sml.

Thanks, changes made as advised.

[mn200]

Thanks for making these changes! I think I'd prefer assumptions of the form

  DES ... = (..,..)

because it feels more natural to talk about constant functions (like DES) having particular values. (E.g., it reads better to me to write sin x = pi/2 rather than pi/2 = sin x.)

[binghe]

@mn200, please approve the CI test workflow for this new contributor. I suspect there are also trailing whitespaces to fix in the committing branch.

[mn200]

@binghe was right (unsurprisingly). @gengarrrr: you need to remove trailing whitespace from your file. To check that your sources are passing the test, please run HOL/bin/build -t (or HOL/tools/unicode-grep -l -u --nolinelen path-to-your-directory).

[binghe]

@gengarrrr In Emacs, the interactive command (first type M-x and then the command) delete-trailing-whitespace can be used to delete all trailing whitespace in the current buffer.

[mn200]

Or in perl on the command line :

perl -pi -e 's/[[:space:]]*$/\n/' file1 file2 file3 ... filen

[gengarrrr]

Hi. I changed it by deleting the trailing whitespaces and the way write tuples. Thanks for pointing out and teaching how to fix the error