forked from GaloisInc/cryptol-specs
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTripleDES.cry
41 lines (31 loc) · 1.12 KB
/
TripleDES.cry
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
/*
* Copyright (c) 2013-2018 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module Primitive::Symmetric::Cipher::Block::TripleDES where
import Primitive::Symmetric::Cipher::Block::DES
blockEncrypt : ([64],[64],[64],[64]) -> [64]
blockEncrypt (k1,k2,k3,data) = result where
ex = DES.encrypt k1 data
dx = DES.decrypt k2 ex
result = DES.encrypt k3 dx
// Test vectors from NIST 800-67
Key1, Key2, Key3 : [64]
Key1 = 0x0123456789ABCDEF
Key2 = 0x23456789ABCDEF01
Key3 = 0x456789ABCDEF0123
P1, P2, P3 : [64]
PlainText = "The qufck brown fox jump"
// Yes, that's the correct phrase.. (see the 7th letter of the phrase).
// It's supposed to be "the quick..." but they made a mistake in transcribing
// the ASCII into hex.
[P1, P2, P3] = split`{3} (join PlainText)
// B.1
C1, C2, C3 : [64]
C1 = 0xA826FD8CE53B855F
C2 = 0xCCE21C8112256FE6
C3 = 0x68D5C05DD9B6B900
test_B1_1 = blockEncrypt (Key1, Key2, Key3, P1) == C1
test_B1_2 = blockEncrypt (Key1, Key2, Key3, P2) == C2
test_B1_3 = blockEncrypt (Key1, Key2, Key3, P3) == C3
property testsPass = and [test_B1_1, test_B1_2, test_B1_3]