Make Programming Great Again

tea.agda

-- Implentation of TEA encrpytion in agda.
-- Very nearly a word for word clone of https://github.com/wmoss/haskell-Crypto/blob/80d25c75fff189acfd32a7383659dea0f6a61be8/Codec/Encryption/TEA.hs

module TEA where

open import Streams
open import Ops
open import Poly
open import Data.String hiding (_++_)
open import Data.Bool
open import Data.Vec hiding (split)
open import Relation.Binary.PropositionalEquality

-- delta hexword
Δ : Word 32 
Δ = hexWord 32 "0x9e3779b9"

-- number of rounds to use
rounds : ℕ 
rounds = 32

encrypt : Word 128 → Word 64 → Word 64
encrypt key word with (split 32 4 key) 
... | (k₀ ∷ k₁ ∷ k₂ ∷ k₃ ∷ []) = f rounds (zWord 32) (take 32 word) (drop 32 word)
  where 
  f : ℕ → Word 32 → Word 32 → Word 32 → Word 64
  f zero sum v₀ v₁ = v₁ ++ v₀ 
  f (suc n₂) sum v₀ v₁ = let sum' = sum ⟨+⟩ Δ 
                             v₀' = (v₀ ⟨+⟩ (((v₁ << 4) ⟨+⟩ k₀) ⊕ ((v₁ ⟨+⟩ sum') ⊕ ((v₁ >> 5) ⟨+⟩ k₁))))
                             v₁' = (v₁ ⟨+⟩ (((v₀' << 4) ⟨+⟩ k₂) ⊕ ((v₀' ⟨+⟩ sum') ⊕ ((v₀' >> 5) ⟨+⟩ k₃))))
                         in f n₂ sum' v₀' v₁'

decrypt : Word 128 → Word 64 → Word 64 
decrypt key word with (split 32 4 key)
... | (k₀ ∷ k₁ ∷ k₂ ∷ k₃ ∷ []) = f rounds (hexWord 32 "0xc6ef3720") (take 32 word) (drop 32 word)
  where 
  f : ℕ → Word 32 → Word 32 → Word 32 → Word 64
  f zero sum v₀ v₁ = v₁ ++ v₀ 
  f (suc n) sum v₀ v₁ = let v₁' = v₁ ⟨-⟩ (((v₀ << 4) ⟨+⟩ k₂) ⊕ ((v₀ ⟨+⟩ sum) ⊕ ((v₀ >> 5) ⟨+⟩ k₃)))
                            v₀' = v₀ ⟨-⟩ (((v₁' << 4) ⟨+⟩ k₀) ⊕ ((v₁' ⟨+⟩ sum) ⊕ ((v₁' >> 5) ⟨+⟩ k₁)))
                        in f n (sum ⟨-⟩ Δ) v₀' v₁'