products/sources/formale Sprachen/Isabelle/HOL/SPARK/Examples/RIPEMD-160 image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: RMD.thy   Sprache: Isabelle

Original von: Isabelle©

(*  Title:      HOL/SPARK/Examples/RIPEMD-160/RMD.thy
    Author:     Fabian Immler, TU Muenchen

Verification of the RIPEMD-160 hash function
*)


theory RMD
imports "HOL-Library.Word"
begin


\<comment> \<open>all operations are defined on 32-bit words\<close>

type_synonym word32 = "32 word"
type_synonym byte = "8 word"
type_synonym perm = "nat \ nat"
type_synonym chain = "word32 * word32 * word32 * word32 * word32"
type_synonym block = "nat \ word32"
type_synonym message = "nat \ block"

\<comment> \<open>nonlinear functions at bit level\<close>

definition f::"[nat, word32, word32, word32] => word32"
where
"f j x y z =
      (if ( 0 <= j & j <= 15) then x XOR y XOR z
  else if (16 <= j & j <= 31) then (x AND y) OR (NOT x AND z)
  else if (32 <= j & j <= 47) then (x OR NOT y) XOR z
  else if (48 <= j & j <= 63) then (x AND z) OR (y AND NOT z)
  else if (64 <= j & j <= 79) then x XOR (y OR NOT z)
  else 0)"


\<comment> \<open>added constants (hexadecimal)\<close>

definition K::"nat => word32"
where
"K j =
      (if ( 0 <= j & j <= 15) then 0x00000000
  else if (16 <= j & j <= 31) then 0x5A827999
  else if (32 <= j & j <= 47) then 0x6ED9EBA1
  else if (48 <= j & j <= 63) then 0x8F1BBCDC
  else if (64 <= j & j <= 79) then 0xA953FD4E
  else 0)"

definition K'::"nat => word32"
where
"K' j =
      (if ( 0 <= j & j <= 15) then 0x50A28BE6
  else if (16 <= j & j <= 31) then 0x5C4DD124
  else if (32 <= j & j <= 47) then 0x6D703EF3
  else if (48 <= j & j <= 63) then 0x7A6D76E9
  else if (64 <= j & j <= 79) then 0x00000000
  else 0)"


\<comment> \<open>selection of message word\<close>

definition r_list :: "nat list"
  where "r_list = [
  0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15,
  7, 4, 13, 1, 10, 6, 15, 3, 12, 0, 9, 5, 2, 14, 11, 8,
  3, 10, 14, 4, 9, 15, 8, 1, 2, 7, 0, 6, 13, 11, 5, 12,
  1, 9, 11, 10, 0, 8, 12, 4, 13, 3, 7, 15, 14, 5, 6, 2,
  4, 0, 5, 9, 7, 12, 2, 10, 14, 1, 3, 8, 11, 6, 15, 13
  ]"

definition r'_list :: "nat list"
  where "r'_list = [
  5, 14, 7, 0, 9, 2, 11, 4, 13, 6, 15, 8, 1, 10, 3, 12,
  6, 11, 3, 7, 0, 13, 5, 10, 14, 15, 8, 12, 4, 9, 1, 2,
  15, 5, 1, 3, 7, 14, 6, 9, 11, 8, 12, 2, 10, 0, 4, 13,
  8, 6, 4, 1, 3, 11, 15, 0, 5, 12, 2, 13, 9, 7, 10, 14,
  12, 15, 10, 4, 1, 5, 8, 7, 6, 2, 13, 14, 0, 3, 9, 11
  ]"

definition r :: perm
  where "r j = r_list ! j"

definition r' :: perm
  where "r' j = r'_list ! j"


\<comment> \<open>amount for rotate left (rol)\<close>

definition s_list :: "nat list"
  where "s_list = [
  11, 14, 15, 12, 5, 8, 7, 9, 11, 13, 14, 15, 6, 7, 9, 8,
  7, 6, 8, 13, 11, 9, 7, 15, 7, 12, 15, 9, 11, 7, 13, 12,
  11, 13, 6, 7, 14, 9, 13, 15, 14, 8, 13, 6, 5, 12, 7, 5,
  11, 12, 14, 15, 14, 15, 9, 8, 9, 14, 5, 6, 8, 6, 5, 12,
  9, 15, 5, 11, 6, 8, 13, 12, 5, 12, 13, 14, 11, 8, 5, 6
  ]"

definition s'_list :: "nat list"
  where "s'_list = [
  8, 9, 9, 11, 13, 15, 15, 5, 7, 7, 8, 11, 14, 14, 12, 6,
  9, 13, 15, 7, 12, 8, 9, 11, 7, 7, 12, 7, 6, 15, 13, 11,
  9, 7, 15, 11, 8, 6, 6, 14, 12, 13, 5, 14, 13, 13, 7, 5,
  15, 5, 8, 11, 14, 14, 6, 14, 6, 9, 12, 9, 12, 5, 15, 8,
  8, 5, 12, 9, 12, 5, 14, 6, 8, 13, 6, 5, 15, 13, 11, 11
  ]"

definition s :: perm
  where "s j = s_list ! j"

definition s' :: perm
  where "s' j = s'_list ! j"


\<comment> \<open>Initial value (hexadecimal)\<close>

definition h0_0::word32 where "h0_0 = 0x67452301"
definition h1_0::word32 where "h1_0 = 0xEFCDAB89"
definition h2_0::word32 where "h2_0 = 0x98BADCFE"
definition h3_0::word32 where "h3_0 = 0x10325476"
definition h4_0::word32 where "h4_0 = 0xC3D2E1F0"
definition h_0::chain where "h_0 = (h0_0, h1_0, h2_0, h3_0, h4_0)"


definition step_l ::
  "[ block,
     chain,
     nat
  ] => chain"
  where
  "step_l X c j =
    (let (A, B, C, D, E) = c in
    (\<comment> \<open>\<open>A:\<close>\<close> E,
     \<comment> \<open>\<open>B:\<close>\<close> word_rotl (s j) (A + f j B C D + X (r j) + K j) + E,
     \<comment> \<open>\<open>C:\<close>\<close> B,
     \<comment> \<open>\<open>D:\<close>\<close> word_rotl 10 C,
     \<comment> \<open>\<open>E:\<close>\<close> D))"

definition step_r ::
  "[ block,
     chain,
     nat
   ] \<Rightarrow> chain"
where
  "step_r X c' j =
    (let (A', B', C', D', E') = c' in
    (\<comment> \<open>\<open>A':\<close>\<close> E',
     \<comment> \<open>\<open>B':\<close>\<close> word_rotl (s' j) (A' + f (79 - j) B' C' D' + X (r' j) + K' j) + E',
     \<comment> \<open>\<open>C':\<close>\<close> B',
     \<comment> \<open>\<open>D':\<close>\<close> word_rotl 10 C',
     \<comment> \<open>\<open>E':\<close>\<close> D'))"

definition step_both ::
  "[ block, chain * chain, nat ] \ chain * chain"
  where
  "step_both X cc j = (case cc of (c, c') \
  (step_l X c j, step_r X c' j))"

definition steps::"[ block, chain * chain, nat] \ chain * chain"
  where "steps X cc i = foldl (step_both X) cc [0..

definition round::"[ block, chain ] \ chain"
  where "round X h =
    (let (h0, h1, h2, h3, h4) = h in
     let ((A, B, C, D, E), (A', B', C', D', E')) = steps X (h, h) 80 in
      (\<comment> \<open>\<open>h0:\<close>\<close> h1 + C + D',
       \<comment> \<open>\<open>h1:\<close>\<close> h2 + D + E',
       \<comment> \<open>\<open>h2:\<close>\<close> h3 + E + A',
       \<comment> \<open>\<open>h3:\<close>\<close> h4 + A + B',
       \<comment> \<open>\<open>h4:\<close>\<close> h0 + B + C'))"

definition rmd_body::"[ message, chain, nat ] => chain"
where
  "rmd_body X h i = round (X i) h"

definition rounds::"message \ chain \ nat \ chain"
where
  "rounds X h i = foldl (rmd_body X) h_0 [0..

definition rmd :: "message \ nat \ chain"
where
  "rmd X len = rounds X h_0 len"

end

¤ Dauer der Verarbeitung: 0.14 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff