Theory Crypt

(*  Title:      RSAPSS/Crypt.thy
    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
    Copyright:  2005 - Technische Universität Darmstadt 

section "Definition of rsacrypt"

theory Crypt
imports Main Mod

  This theory defines the rsacrypt function which implements RSA using fast
  exponentiation. An proof, that this function calculates RSA is also given

definition rsa_crypt :: "nat  nat  nat  nat"
  cryptcorrect: "rsa_crypt M e n = M ^ e mod n"

lemma rsa_crypt_code [code]:
  "rsa_crypt M e n = (if e = 0 then 1 mod n
    else if even e then rsa_crypt M (e div 2) n ^ 2 mod n
    else (M * rsa_crypt M (e div 2) n ^ 2 mod n) mod n)"
proof -
  { fix m
    have "(M ^ m mod n)2 mod n = (M ^ m)2 mod n"
      by (simp add: power_mod)
    then have "(M mod n) * ((M ^ m mod n)2 mod n) = (M mod n) * ((M ^ m)2 mod n)"
      by simp
    have "M * (M ^ m mod n)2 mod n = M * (M ^ m)2 mod n"
      by (metis mod_mult_right_eq power_mod)
  then show ?thesis
    by (auto simp add: cryptcorrect power_even_eq remainderexp elim!: evenE oddE)