From 23f099c62e5ce88f10c5ef6d6d7b10162fe30919 Mon Sep 17 00:00:00 2001 From: ruofan <1328395562@qq.com> Date: Fri, 25 Oct 2024 12:16:51 +1100 Subject: [PATCH] update --- examples/Crypto/RC5/rc5Script.sml | 8 +- examples/Crypto/RC5/rc5Theory.html | 742 +++++++++++++++++++++++++++++ 2 files changed, 746 insertions(+), 4 deletions(-) create mode 100644 examples/Crypto/RC5/rc5Theory.html diff --git a/examples/Crypto/RC5/rc5Script.sml b/examples/Crypto/RC5/rc5Script.sml index f6fcd9486b..9036518dbb 100644 --- a/examples/Crypto/RC5/rc5Script.sml +++ b/examples/Crypto/RC5/rc5Script.sml @@ -1,5 +1,5 @@ (*===========================================================================*) -(* The Data Encryption Standard (DES) in HOL *) +(* The RC5 in HOL *) (*===========================================================================*) open HolKernel Parse boolLib bossLib; @@ -7,9 +7,9 @@ open HolKernel Parse boolLib bossLib; open arithmeticTheory numLib pairTheory fcpTheory fcpLib wordsTheory wordsLib listTheory listLib sortingTheory pred_setTheory combinTheory hurdUtils; -val _ = guessing_word_lengths := true; -val _ = new_theory "rc5"; +val _ = new_theory "rc5"; +val _ = guessing_word_lengths := true; val fcp_ss = std_ss ++ fcpLib.FCP_ss; Type block[pp] = “:word32 # word32” (* Data Table *) @@ -577,5 +577,5 @@ Proof QED val _ = export_theory(); -val _ = html_theory "RC5"; +val _ = html_theory "rc5"; diff --git a/examples/Crypto/RC5/rc5Theory.html b/examples/Crypto/RC5/rc5Theory.html new file mode 100644 index 0000000000..0ab583a8c7 --- /dev/null +++ b/examples/Crypto/RC5/rc5Theory.html @@ -0,0 +1,742 @@ + + +Theory: rc5 + + + +

Theory "rc5"

+Parents     + words   + sorting + +

Signature

+
+ + +
Constant Type
+ Join64 + + :block -> word64 +
Join64' :block -> word64 +
Lkeys :word64 -> word32 list +
LkeysIni :word32 list +
+ LkeysSup + + :α word -> num -> word32 list +
P32_data :α word +
Q32_data :α word +
+ RoundDe + + :num -> word32 list -> block -> block +
+ RoundDe' + + :num -> word32 -> word32 -> block -> block +
+ RoundDe64 + + :num -> word64 -> word64 -> word64 +
+ RoundDeSg + + :α word # α word -> α word -> α word -> α word # α word +
+ RoundEn + + :num -> word32 -> word32 -> word32 list -> block +
+ RoundEn' + + :num -> α word -> α word -> α word # α word -> α word # α word +
+ RoundEn64 + + :num -> word64 -> word64 -> word64 +
+ RoundEnSg + + :α word # α word -> α word -> α word -> α word # α word +
Skeys :num -> word32 list +
+ SkeysT32 + + :num -> num -> word32 list +
Split64 :word64 -> block +
+ half_messageDe + + :word32 -> word32 -> word32 list -> num -> word32 +
+ half_messageEn + + :word32 -> word32 -> word32 list -> num -> word32 +
+ keys + + :num -> + num -> word64 -> word32 # word32 # word32 list # word32 list # num # num +
keysIni :α word -> word32 list +
lenKeyw :num +
lenKinbyt :num +
lenWinbyt :num +
+ rc5keys + + :num -> word64 -> word32 # word32 # word32 list # word32 list # num # num + +
+
+ +

Definitions

+
+
Join64'_def +
+
+⊢ ∀b. Join64' b = (let (u,v) = b in u @@ v)
+
+ +
Join64_def +
+
+⊢ ∀u v. Join64 (u,v) = u @@ v
+
+ +
LkeysIni_def +
+
+⊢ LkeysIni = [0w; 0w]
+
+ +
LkeysSup_def +
+
+⊢ (∀k. LkeysSup k 0 =
+       (let
+          ks = LkeysIni;
+          keys = keysIni k
+        in
+          GENLIST
+            (λm. if m = 7 DIV 4 then EL m ks ⇆ 8 + EL 7 keys else EL m ks) 2)) ∧
+  ∀k r.
+    LkeysSup k (SUC r) =
+    (let
+       ks = LkeysSup k r;
+       keys = keysIni k;
+       i = 7 − SUC r
+     in
+       GENLIST (λm. if m = i DIV 4 then EL m ks ⇆ 8 + EL i keys else EL m ks)
+         2)
+
+ +
Lkeys_def +
+
+⊢ ∀k. Lkeys k = LkeysSup k 7
+
+ +
P32_data +
+
+⊢ P32_data = 0xB7E15163w
+
+ +
Q32_data +
+
+⊢ Q32_data = 0x9E3779B9w
+
+ +
RoundDe'_def +
+
+⊢ (∀ki ki2 b. RoundDe' 0 ki ki2 b = b) ∧
+  ∀n ki ki2 b.
+    RoundDe' (SUC n) ki ki2 b =
+    (let b' = RoundDe' n ki ki2 b in RoundDeSg b' ki ki2)
+
+ +
RoundDe64_def +
+
+⊢ ∀n w k.
+    RoundDe64 n w k =
+    (let
+       (w1,w2) = Split64 w;
+       (A,B,Lk,Sk,i,j) = rc5keys n k;
+       (w1',w2') = RoundDe n Sk (w1,w2);
+       k0 = EL 0 Sk;
+       k1 = EL 1 Sk
+     in
+       Join64' (w1' − k0,w2' − k1))
+
+ +
RoundDeSg_def +
+
+⊢ ∀b ki ki2.
+    RoundDeSg b ki ki2 =
+    (let
+       (w1,w2) = b;
+       B = (w2 − ki2) ⇄ w2n w1 ⊕ w1;
+       A = (w1 − ki) ⇄ w2n B ⊕ B
+     in
+       (A,B))
+
+ +
RoundEn'_def +
+
+⊢ (∀ki ki2 b. RoundEn' 0 ki ki2 b = b) ∧
+  ∀n ki ki2 b.
+    RoundEn' (SUC n) ki ki2 b =
+    (let b' = RoundEn' n ki ki2 b in RoundEnSg b' ki ki2)
+
+ +
RoundEn64_def +
+
+⊢ ∀n w k.
+    RoundEn64 n w k =
+    (let
+       (w1,w2) = Split64 w;
+       (A,B,Lk,Sk,i,j) = rc5keys n k;
+       k0 = EL 0 Sk;
+       k1 = EL 1 Sk
+     in
+       Join64' (RoundEn n (w1 + k0) (w2 + k1) Sk))
+
+ +
RoundEnSg_def +
+
+⊢ ∀b ki ki2.
+    RoundEnSg b ki ki2 =
+    (let
+       (w1,w2) = b;
+       A = (w1 ⊕ w2) ⇆ w2n w2 + ki;
+       B = (w2 ⊕ A) ⇆ w2n A + ki2
+     in
+       (A,B))
+
+ +
RoundEn_def +
+
+⊢ (∀w1 w2 ks. RoundEn 0 w1 w2 ks = (let s0 = EL 0 ks; s1 = EL 1 ks in (w1,w2))) ∧
+  ∀n w1 w2 ks.
+    RoundEn (SUC n) w1 w2 ks =
+    (let
+       (w1',w2') = RoundEn n w1 w2 ks;
+       ki = EL (2 * SUC n) ks;
+       ki2 = EL (2 * SUC n + 1) ks;
+       A = (w1' ⊕ w2') ⇆ w2n w2' + ki;
+       B = (w2' ⊕ A) ⇆ w2n A + ki2
+     in
+       (A,B))
+
+ +
SkeysT32_def +
+
+⊢ (∀l. SkeysT32 l 0 = [P32_data]) ∧
+  ∀l t.
+    SkeysT32 l (SUC t) =
+    (let ks = SkeysT32 l t; key = HD ks in key + Q32_data::ks)
+
+ +
Skeys_def +
+
+⊢ ∀r. Skeys r = REVERSE (SkeysT32 32 (2 * (r + 1) − 1))
+
+ +
Split64_def +
+
+⊢ ∀w. Split64 w = ((63 >< 32) w,(31 >< 0) w)
+
+ +
keysIni_def +
+
+⊢ ∀k. keysIni k =
+      [(7 >< 0) k; (15 >< 8) k; (23 >< 16) k; (31 >< 24) k; (39 >< 32) k;
+       (47 >< 40) k; (55 >< 48) k; (63 >< 56) k]
+
+ +
keys_def +
+
+⊢ (∀r k.
+     keys 0 r k =
+     (let
+        Lk = Lkeys k;
+        Sk = Skeys r;
+        A = EL 0 Sk;
+        B = EL 0 Lk
+      in
+        (A,B,Lk,Sk,0,0))) ∧
+  ∀n r k.
+    keys (SUC n) r k =
+    (let
+       (A,B,Lk,Sk,i,j) = keys n r k;
+       Anew = (EL i Sk + A + B) ⇆ 3;
+       Bnew = (EL i Lk + Anew + B) ⇆ w2n (Anew + B);
+       Sknew =
+         GENLIST (λm. if m = i then (EL i Sk + A + B) ⇆ 3 else EL m Sk)
+           (2 * (r + 1));
+       Lknew =
+         GENLIST
+           (λm.
+                if m = j then (EL j Lk + Anew + B) ⇆ w2n (Anew + B)
+                else EL m Lk) 2;
+       inew = (i + 1) MOD (2 * (r + 1));
+       jnew = (j + 1) MOD 2
+     in
+       (Anew,Bnew,Lknew,Sknew,inew,jnew))
+
+ +
lenKeyw_def +
+
+⊢ lenKeyw = 2
+
+ +
lenKinbyt_def +
+
+⊢ lenKinbyt = 8
+
+ +
lenWinbyt_def +
+
+⊢ lenWinbyt = 4
+
+ +
rc5keys_def +
+
+⊢ ∀r k. rc5keys r k = (let n = 3 * MAX (2 * (r + 1)) 2 in keys n r k)
+
+ +
+ + +
+ +
+

Theorems

+
+
Join64'_Split64 +
+
+⊢ ∀w. Join64' (Split64 w) = w
+
+ +
Join64_Split64 +
+
+⊢ ∀w. Join64 (Split64 w) = w
+
+ +
LENGTH_Lkeys +
+
+⊢ ∀k. LENGTH (Lkeys k) = 2
+
+ +
LENGTH_LkeysSup +
+
+⊢ ∀k r. LENGTH (LkeysSup k r) = 2
+
+ +
LENGTH_Skeys +
+
+⊢ ∀n. LENGTH (Skeys n) = 2 * (n + 1)
+
+ +
LENGTH_key_Lkeys +
+
+⊢ ∀n r k. (A,B,Lk,Sk,i,j) = keys n r k ⇒ LENGTH Lk = 2
+
+ +
LENGTH_key_Skeys +
+
+⊢ ∀n r k. (A,B,Lk,Sk,i,j) = keys n r k ⇒ LENGTH Sk = 2 * (r + 1)
+
+ +
LkeysSup_compute +
+
+⊢ (∀k. LkeysSup k 0 =
+       (let
+          ks = LkeysIni;
+          keys = keysIni k
+        in
+          GENLIST
+            (λm. if m = 7 DIV 4 then EL m ks ⇆ 8 + EL 7 keys else EL m ks) 2)) ∧
+  (∀k r.
+     LkeysSup k <..num comp'n..> =
+     (let
+        ks = LkeysSup k (<..num comp'n..> − 1);
+        keys = keysIni k;
+        i = 7 − <..num comp'n..>
+      in
+        GENLIST (λm. if m = i DIV 4 then EL m ks ⇆ 8 + EL i keys else EL m ks)
+          2)) ∧
+  ∀k r.
+    LkeysSup k <..num comp'n..> =
+    (let
+       ks = LkeysSup k <..num comp'n..> ;
+       keys = keysIni k;
+       i = 7 − <..num comp'n..>
+     in
+       GENLIST (λm. if m = i DIV 4 then EL m ks ⇆ 8 + EL i keys else EL m ks)
+         2)
+
+ +
RoundDe'_comm +
+
+⊢ ∀n b ks ki ki2.
+    RoundDeSg (RoundDe' n ki ki2 b) ki ki2 =
+    RoundDe' n ki ki2 (RoundDeSg b ki ki2)
+
+ +
RoundDe'_compute +
+
+⊢ (∀ki ki2 b. RoundDe' 0 ki ki2 b = b) ∧
+  (∀n ki ki2 b.
+     RoundDe' <..num comp'n..> ki ki2 b =
+     (let
+        b' = RoundDe' (<..num comp'n..> − 1) ki ki2 b
+      in
+        RoundDeSg b' ki ki2)) ∧
+  ∀n ki ki2 b.
+    RoundDe' <..num comp'n..> ki ki2 b =
+    (let b' = RoundDe' <..num comp'n..> ki ki2 b in RoundDeSg b' ki ki2)
+
+ +
RoundDe64_alt_half_messageDe +
+
+⊢ ∀w k r.
+    (w1,w2) = Split64 w ∧ (A,B,Lk,Sk,i,j) = rc5keys r k ∧ k0 = EL 0 Sk ∧
+    k1 = EL 1 Sk ⇒
+    RoundDe64 r w k =
+    Join64'
+      (half_messageDe w1 w2 Sk (2 * r + 1) − k0,
+       half_messageDe w1 w2 Sk (2 * r) − k1)
+
+ +
RoundDe_EnSg +
+
+⊢ ∀b ki ki2. RoundDeSg (RoundEnSg b ki ki2) ki ki2 = b
+
+ +
RoundDe_alt_half_messageDe +
+
+⊢ ∀w1 w2 ks n.
+    RoundDe n ks (w1,w2) =
+    (half_messageDe w1 w2 ks (2 * n + 1),half_messageDe w1 w2 ks (2 * n))
+
+ +
RoundDe_compute +
+
+⊢ (∀w2 w1 ks.
+     RoundDe 0 ks (w1,w2) = (let s1 = EL 1 ks; s0 = EL 0 ks in (w1,w2))) ∧
+  (∀w2 w1 n ks.
+     RoundDe <..num comp'n..> ks (w1,w2) =
+     (let
+        (w1',w2') = RoundDe (<..num comp'n..> − 1) ks (w1,w2);
+        ki = EL (2 * <..num comp'n..> − 2) (REVERSE ks);
+        ki2 = EL (2 * <..num comp'n..> − 1) (REVERSE ks);
+        B = (w2' − ki) ⇄ w2n w1' ⊕ w1';
+        A = (w1' − ki2) ⇄ w2n B ⊕ B
+      in
+        (A,B))) ∧
+  ∀w2 w1 n ks.
+    RoundDe <..num comp'n..> ks (w1,w2) =
+    (let
+       (w1',w2') = RoundDe <..num comp'n..> ks (w1,w2);
+       ki = EL (2 * <..num comp'n..> − 2) (REVERSE ks);
+       ki2 = EL (2 * <..num comp'n..> − 1) (REVERSE ks);
+       B = (w2' − ki) ⇄ w2n w1' ⊕ w1';
+       A = (w1' − ki2) ⇄ w2n B ⊕ B
+     in
+       (A,B))
+
+ +
RoundDe_def +
+
+⊢ (∀w2 w1 ks.
+     RoundDe 0 ks (w1,w2) = (let s1 = EL 1 ks; s0 = EL 0 ks in (w1,w2))) ∧
+  ∀w2 w1 n ks.
+    RoundDe (SUC n) ks (w1,w2) =
+    (let
+       (w1',w2') = RoundDe n ks (w1,w2);
+       ki = EL (2 * SUC n − 2) (REVERSE ks);
+       ki2 = EL (2 * SUC n − 1) (REVERSE ks);
+       B = (w2' − ki) ⇄ w2n w1' ⊕ w1';
+       A = (w1' − ki2) ⇄ w2n B ⊕ B
+     in
+       (A,B))
+
+ +
RoundDe_ind +
+
+⊢ ∀P. (∀ks w1 w2. P 0 ks (w1,w2)) ∧
+      (∀n ks w1 w2. P n ks (w1,w2) ⇒ P (SUC n) ks (w1,w2)) ⇒
+      ∀v v1 v2 v3. P v v1 (v2,v3)
+
+ +
RoundEe'_De' +
+
+⊢ ∀n b ki ki2. RoundDe' n ki ki2 (RoundEn' n ki ki2 b) = b
+
+ +
RoundEn'_comm +
+
+⊢ ∀n b ks ki ki2.
+    RoundEnSg (RoundEn' n ki ki2 b) ki ki2 =
+    RoundEn' n ki ki2 (RoundEnSg b ki ki2)
+
+ +
RoundEn'_compute +
+
+⊢ (∀ki ki2 b. RoundEn' 0 ki ki2 b = b) ∧
+  (∀n ki ki2 b.
+     RoundEn' <..num comp'n..> ki ki2 b =
+     (let
+        b' = RoundEn' (<..num comp'n..> − 1) ki ki2 b
+      in
+        RoundEnSg b' ki ki2)) ∧
+  ∀n ki ki2 b.
+    RoundEn' <..num comp'n..> ki ki2 b =
+    (let b' = RoundEn' <..num comp'n..> ki ki2 b in RoundEnSg b' ki ki2)
+
+ +
RoundEn64_alt_half_messageEn +
+
+⊢ ∀w k r.
+    (w1,w2) = Split64 w ∧ (A,B,Lk,Sk,i,j) = rc5keys r k ∧ k0 = EL 0 Sk ∧
+    k1 = EL 1 Sk ⇒
+    RoundEn64 r w k =
+    Join64'
+      (half_messageEn (w1 + k0) (w2 + k1) Sk (2 * r),
+       half_messageEn (w1 + k0) (w2 + k1) Sk (2 * r + 1))
+
+ +
RoundEn_alt_half_messageEn +
+
+⊢ ∀w1 w2 ks n.
+    RoundEn n w1 w2 ks =
+    (half_messageEn w1 w2 ks (2 * n),half_messageEn w1 w2 ks (2 * n + 1))
+
+ +
RoundEn_compute +
+
+⊢ (∀w1 w2 ks. RoundEn 0 w1 w2 ks = (let s0 = EL 0 ks; s1 = EL 1 ks in (w1,w2))) ∧
+  (∀n w1 w2 ks.
+     RoundEn <..num comp'n..> w1 w2 ks =
+     (let
+        (w1',w2') = RoundEn (<..num comp'n..> − 1) w1 w2 ks;
+        ki = EL (2 * <..num comp'n..> ) ks;
+        ki2 = EL (2 * <..num comp'n..> + 1) ks;
+        A = (w1' ⊕ w2') ⇆ w2n w2' + ki;
+        B = (w2' ⊕ A) ⇆ w2n A + ki2
+      in
+        (A,B))) ∧
+  ∀n w1 w2 ks.
+    RoundEn <..num comp'n..> w1 w2 ks =
+    (let
+       (w1',w2') = RoundEn <..num comp'n..> w1 w2 ks;
+       ki = EL (2 * <..num comp'n..> ) ks;
+       ki2 = EL (2 * <..num comp'n..> + 1) ks;
+       A = (w1' ⊕ w2') ⇆ w2n w2' + ki;
+       B = (w2' ⊕ A) ⇆ w2n A + ki2
+     in
+       (A,B))
+
+ +
SkeysT32_compute +
+
+⊢ (∀l. SkeysT32 l 0 = [P32_data]) ∧
+  (∀l t.
+     SkeysT32 l <..num comp'n..> =
+     (let
+        ks = SkeysT32 l (<..num comp'n..> − 1);
+        key = HD ks
+      in
+        key + Q32_data::ks)) ∧
+  ∀l t.
+    SkeysT32 l <..num comp'n..> =
+    (let ks = SkeysT32 l <..num comp'n..> ; key = HD ks in key + Q32_data::ks)
+
+ +
Split64_Join64 +
+
+⊢ ∀u v. Split64 (Join64 (u,v)) = (u,v)
+
+ +
Split64_Join64' +
+
+⊢ ∀b. Split64 (Join64' b) = b
+
+ +
half_messageDe_def +
+
+⊢ ∀w2 w1 n ks.
+    half_messageDe w1 w2 ks n =
+    (let
+       ki = EL (n − 2) (REVERSE ks);
+       ki2 = EL (n − 2) (REVERSE ks)
+     in
+       if n = 0 then w2
+       else if n = 1 then w1
+       else
+         (half_messageDe w1 w2 ks (n − 2) − ki) ⇄
+         w2n (half_messageDe w1 w2 ks (n − 1)) ⊕
+         half_messageDe w1 w2 ks (n − 1))
+
+ +
half_messageDe_ind +
+
+⊢ ∀P. (∀w1 w2 ks n.
+         (∀ki ki2.
+            ki = EL (n − 2) (REVERSE ks) ∧ ki2 = EL (n − 2) (REVERSE ks) ∧
+            n ≠ 0 ∧ n ≠ 1 ⇒
+            P w1 w2 ks (n − 1)) ∧
+         (∀ki ki2.
+            ki = EL (n − 2) (REVERSE ks) ∧ ki2 = EL (n − 2) (REVERSE ks) ∧
+            n ≠ 0 ∧ n ≠ 1 ⇒
+            P w1 w2 ks (n − 2)) ⇒
+         P w1 w2 ks n) ⇒
+      ∀v v1 v2 v3. P v v1 v2 v3
+
+ +
half_messageEn_def +
+
+⊢ ∀w2 w1 n ks.
+    half_messageEn w1 w2 ks n =
+    (let
+       ki = EL n ks;
+       ki2 = EL (n − 1) ks
+     in
+       if n = 0 then w1
+       else if n = 1 then w2
+       else
+         (half_messageEn w1 w2 ks (n − 2) ⊕ half_messageEn w1 w2 ks (n − 1)) ⇆
+         w2n (half_messageEn w1 w2 ks (n − 1)) + ki)
+
+ +
half_messageEn_ind +
+
+⊢ ∀P. (∀w1 w2 ks n.
+         (∀ki ki2.
+            ki = EL n ks ∧ ki2 = EL (n − 1) ks ∧ n ≠ 0 ∧ n ≠ 1 ⇒
+            P w1 w2 ks (n − 1)) ∧
+         (∀ki ki2.
+            ki = EL n ks ∧ ki2 = EL (n − 1) ks ∧ n ≠ 0 ∧ n ≠ 1 ⇒
+            P w1 w2 ks (n − 2)) ⇒
+         P w1 w2 ks n) ⇒
+      ∀v v1 v2 v3. P v v1 v2 v3
+
+ +
keys_compute +
+
+⊢ (∀r k.
+     keys 0 r k =
+     (let
+        Lk = Lkeys k;
+        Sk = Skeys r;
+        A = EL 0 Sk;
+        B = EL 0 Lk
+      in
+        (A,B,Lk,Sk,0,0))) ∧
+  (∀n r k.
+     keys <..num comp'n..> r k =
+     (let
+        (A,B,Lk,Sk,i,j) = keys (<..num comp'n..> − 1) r k;
+        Anew = (EL i Sk + A + B) ⇆ 3;
+        Bnew = (EL i Lk + Anew + B) ⇆ w2n (Anew + B);
+        Sknew =
+          GENLIST (λm. if m = i then (EL i Sk + A + B) ⇆ 3 else EL m Sk)
+            (2 * (r + 1));
+        Lknew =
+          GENLIST
+            (λm.
+                 if m = j then (EL j Lk + Anew + B) ⇆ w2n (Anew + B)
+                 else EL m Lk) 2;
+        inew = (i + 1) MOD (2 * (r + 1));
+        jnew = (j + 1) MOD 2
+      in
+        (Anew,Bnew,Lknew,Sknew,inew,jnew))) ∧
+  ∀n r k.
+    keys <..num comp'n..> r k =
+    (let
+       (A,B,Lk,Sk,i,j) = keys <..num comp'n..> r k;
+       Anew = (EL i Sk + A + B) ⇆ 3;
+       Bnew = (EL i Lk + Anew + B) ⇆ w2n (Anew + B);
+       Sknew =
+         GENLIST (λm. if m = i then (EL i Sk + A + B) ⇆ 3 else EL m Sk)
+           (2 * (r + 1));
+       Lknew =
+         GENLIST
+           (λm.
+                if m = j then (EL j Lk + Anew + B) ⇆ w2n (Anew + B)
+                else EL m Lk) 2;
+       inew = (i + 1) MOD (2 * (r + 1));
+       jnew = (j + 1) MOD 2
+     in
+       (Anew,Bnew,Lknew,Sknew,inew,jnew))
+
+ +
+ + + +
+ +