Created
September 16, 2017 19:53
-
-
Save peixian/9c29c7fa41db0963fc8776fe7d5a7042 to your computer and use it in GitHub Desktop.
Make Programming Great Again
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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₁' |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment