mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-29 10:13:29 +03:00
finished test vectors
created function AeadConstruction that is used to generate tags in AEAD encryption and decryption
This commit is contained in:
Joey Dodds
parent
2636a0ca9e
commit
d248b50b40
@ -1073,10 +1073,17 @@ takes a 256-bit key and 96-bit nonce as follows:
|
||||
adlen : [8][8]
|
||||
adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64])))
|
||||
// compute padding
|
||||
type p1 = (16-m%16)%16
|
||||
type p2 = (16-n%16)%16
|
||||
tag : [16][8]
|
||||
tag = Poly1305 PolyKey (aad # (zero:[p1][8]) # ct # (zero:[p2][8]) # adlen # ptlen)
|
||||
tag = Poly1305 PolyKey (AeadConstruction aad ct)
|
||||
|
||||
//ct in this function has tag removed
|
||||
AeadConstruction (AAD : [n][8]) (CT : [m][8]) = (AAD # padding1 # CT # padding2 # adlen # ptlen) where
|
||||
padding1 = (zero:[(16-n%16)][8])
|
||||
padding2 = (zero:[(16-m%16)][8])
|
||||
adlen : [8][8]
|
||||
adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64])))
|
||||
ptlen : [8][8]
|
||||
ptlen = groupBy`{8}(littleendian (groupBy`{8}(`m:[64])))
|
||||
|
||||
```
|
||||
|
||||
The output from the AEAD is twofold:
|
||||
@ -1087,13 +1094,11 @@ The output from the AEAD is twofold:
|
||||
Decryption is pretty much the same thing.
|
||||
|
||||
```cryptol
|
||||
|
||||
AEAD_CHACHA20_POLY1305_DECRYPT : {m, n} (fin m, fin n
|
||||
,64 >= width m, 64 >= width n)
|
||||
=> [256] -> [96]
|
||||
-> [m+16][8] -> [n][8]
|
||||
-> ([m][8], Bit)
|
||||
|
||||
-> ([m][8], Bit)
|
||||
AEAD_CHACHA20_POLY1305_DECRYPT k nonce ct ad = (pt, valid) where
|
||||
inTag = drop`{m}ct
|
||||
inCt = take`{m}ct
|
||||
@ -1103,10 +1108,7 @@ AEAD_CHACHA20_POLY1305_DECRYPT k nonce ct ad = (pt, valid) where
|
||||
ptlen = groupBy`{8}(littleendian (groupBy`{8}(`m:[64])))
|
||||
adlen : [8][8]
|
||||
adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64])))
|
||||
// compute padding
|
||||
type p1 = (16-m%16)%16
|
||||
type p2 = (16-n%16)%16
|
||||
tag = Poly1305 PolyKey (ad # (zero:[p1][8]) # inCt # (zero:[p2][8]) # adlen # ptlen)
|
||||
tag = Poly1305 PolyKey (AeadConstruction ad inCt)
|
||||
valid = tag == inTag
|
||||
```
|
||||
|
||||
@ -1161,13 +1163,6 @@ AeadNonce = AeadC # AeadIV
|
||||
```cryptol
|
||||
AeadCT = ChaCha20EncryptBytes AeadPt AeadKey AeadNonce 1
|
||||
|
||||
type p1width = 4
|
||||
type p2width = 14
|
||||
|
||||
AeadConstruction AAD CT = (AeadAAD # padding1 # AeadCT # padding2 # ADleLen # CTleLen) where
|
||||
padding1 = zero:[p1width][8]
|
||||
padding2 = zero:[p2width][8]
|
||||
|
||||
AeadPolyKey = GeneratePolyKeyUsingChaCha AeadKey (AeadC # AeadIV) 0
|
||||
|
||||
ADleLen : [8][8]
|
||||
@ -1981,20 +1976,134 @@ particular protocol, we’ll assume that there is no padding of the
|
||||
plaintext.
|
||||
|
||||
```cryptol
|
||||
AEAD_correct key nonce cypherText AAD tag = ptMatches && isValid where
|
||||
AEAD_correct key nonce cypherText tag AAD = ptMatches && isValid where
|
||||
(pt,isValid) = AEAD_CHACHA20_POLY1305_DECRYPT key nonce cypherText AAD
|
||||
cypherText = (AEAD_CHACHA20_POLY1305 key nonce AeadPt AAD)
|
||||
ptMatches = tag == pt
|
||||
```
|
||||
|
||||
```cryptol
|
||||
//known
|
||||
TV1_AEAD_key = join([
|
||||
0x1c, 0x92, 0x40, 0xa5, 0xeb, 0x55, 0xd3, 0x8a, 0xf3, 0x33, 0x88, 0x86, 0x04, 0xf6, 0xb5, 0xf0,
|
||||
0x47, 0x39, 0x17, 0xc1, 0x40, 0x2b, 0x80, 0x09, 0x9d, 0xca, 0x5c, 0xbc, 0x20, 0x70, 0x75, 0xc0])
|
||||
|
||||
//sent
|
||||
TV1_AEAD_nonce = join([0x00, 0x00, 0x00, 0x00, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08])
|
||||
|
||||
//sent
|
||||
TV1_AEAD_AAD = [0xf3, 0x33, 0x88, 0x86, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x4e, 0x91]
|
||||
|
||||
// calculated
|
||||
TV1_AEAD_known_otk = join([
|
||||
0xbd, 0xf0, 0x4a, 0xa9, 0x5c, 0xe4, 0xde, 0x89, 0x95, 0xb1, 0x4b, 0xb6, 0xa1, 0x8f, 0xec, 0xaf,
|
||||
0x26, 0x47, 0x8f, 0x50, 0xc0, 0x54, 0xf5, 0x63, 0xdb, 0xc0, 0xa2, 0x1e, 0x26, 0x15, 0x72, 0xaa])
|
||||
|
||||
//sent
|
||||
TV1_AEAD_tag = [0xee, 0xad, 0x9d, 0x67, 0x89, 0x0c, 0xbb, 0x22, 0x39, 0x23, 0x36, 0xfe, 0xa1, 0x85, 0x1f, 0x38]
|
||||
|
||||
TV1_AEAD_cypherText = [
|
||||
0x64, 0xa0, 0x86, 0x15, 0x75, 0x86, 0x1a, 0xf4, 0x60, 0xf0, 0x62, 0xc7, 0x9b, 0xe6, 0x43, 0xbd,
|
||||
0x5e, 0x80, 0x5c, 0xfd, 0x34, 0x5c, 0xf3, 0x89, 0xf1, 0x08, 0x67, 0x0a, 0xc7, 0x6c, 0x8c, 0xb2,
|
||||
0x4c, 0x6c, 0xfc, 0x18, 0x75, 0x5d, 0x43, 0xee, 0xa0, 0x9e, 0xe9, 0x4e, 0x38, 0x2d, 0x26, 0xb0,
|
||||
0xbd, 0xb7, 0xb7, 0x3c, 0x32, 0x1b, 0x01, 0x00, 0xd4, 0xf0, 0x3b, 0x7f, 0x35, 0x58, 0x94, 0xcf,
|
||||
0x33, 0x2f, 0x83, 0x0e, 0x71, 0x0b, 0x97, 0xce, 0x98, 0xc8, 0xa8, 0x4a, 0xbd, 0x0b, 0x94, 0x81,
|
||||
0x14, 0xad, 0x17, 0x6e, 0x00, 0x8d, 0x33, 0xbd, 0x60, 0xf9, 0x82, 0xb1, 0xff, 0x37, 0xc8, 0x55,
|
||||
0x97, 0x97, 0xa0, 0x6e, 0xf4, 0xf0, 0xef, 0x61, 0xc1, 0x86, 0x32, 0x4e, 0x2b, 0x35, 0x06, 0x38,
|
||||
0x36, 0x06, 0x90, 0x7b, 0x6a, 0x7c, 0x02, 0xb0, 0xf9, 0xf6, 0x15, 0x7b, 0x53, 0xc8, 0x67, 0xe4,
|
||||
0xb9, 0x16, 0x6c, 0x76, 0x7b, 0x80, 0x4d, 0x46, 0xa5, 0x9b, 0x52, 0x16, 0xcd, 0xe7, 0xa4, 0xe9,
|
||||
0x90, 0x40, 0xc5, 0xa4, 0x04, 0x33, 0x22, 0x5e, 0xe2, 0x82, 0xa1, 0xb0, 0xa0, 0x6c, 0x52, 0x3e,
|
||||
0xaf, 0x45, 0x34, 0xd7, 0xf8, 0x3f, 0xa1, 0x15, 0x5b, 0x00, 0x47, 0x71, 0x8c, 0xbc, 0x54, 0x6a,
|
||||
0x0d, 0x07, 0x2b, 0x04, 0xb3, 0x56, 0x4e, 0xea, 0x1b, 0x42, 0x22, 0x73, 0xf5, 0x48, 0x27, 0x1a,
|
||||
0x0b, 0xb2, 0x31, 0x60, 0x53, 0xfa, 0x76, 0x99, 0x19, 0x55, 0xeb, 0xd6, 0x31, 0x59, 0x43, 0x4e,
|
||||
0xce, 0xbb, 0x4e, 0x46, 0x6d, 0xae, 0x5a, 0x10, 0x73, 0xa6, 0x72, 0x76, 0x27, 0x09, 0x7a, 0x10,
|
||||
0x49, 0xe6, 0x17, 0xd9, 0x1d, 0x36, 0x10, 0x94, 0xfa, 0x68, 0xf0, 0xff, 0x77, 0x98, 0x71, 0x30,
|
||||
0x30, 0x5b, 0xea, 0xba, 0x2e, 0xda, 0x04, 0xdf, 0x99, 0x7b, 0x71, 0x4d, 0x6c, 0x6f, 0x2c, 0x29,
|
||||
0xa6, 0xad, 0x5c, 0xb4, 0x02, 0x2b, 0x02, 0x70, 0x9b]
|
||||
|
||||
TV1_AEAD_Poly_input = [
|
||||
0xf3, 0x33, 0x88, 0x86, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x4e, 0x91, 0x00, 0x00, 0x00, 0x00,
|
||||
0x64, 0xa0, 0x86, 0x15, 0x75, 0x86, 0x1a, 0xf4, 0x60, 0xf0, 0x62, 0xc7, 0x9b, 0xe6, 0x43, 0xbd,
|
||||
0x5e, 0x80, 0x5c, 0xfd, 0x34, 0x5c, 0xf3, 0x89, 0xf1, 0x08, 0x67, 0x0a, 0xc7, 0x6c, 0x8c, 0xb2,
|
||||
0x4c, 0x6c, 0xfc, 0x18, 0x75, 0x5d, 0x43, 0xee, 0xa0, 0x9e, 0xe9, 0x4e, 0x38, 0x2d, 0x26, 0xb0,
|
||||
0xbd, 0xb7, 0xb7, 0x3c, 0x32, 0x1b, 0x01, 0x00, 0xd4, 0xf0, 0x3b, 0x7f, 0x35, 0x58, 0x94, 0xcf,
|
||||
0x33, 0x2f, 0x83, 0x0e, 0x71, 0x0b, 0x97, 0xce, 0x98, 0xc8, 0xa8, 0x4a, 0xbd, 0x0b, 0x94, 0x81,
|
||||
0x14, 0xad, 0x17, 0x6e, 0x00, 0x8d, 0x33, 0xbd, 0x60, 0xf9, 0x82, 0xb1, 0xff, 0x37, 0xc8, 0x55,
|
||||
0x97, 0x97, 0xa0, 0x6e, 0xf4, 0xf0, 0xef, 0x61, 0xc1, 0x86, 0x32, 0x4e, 0x2b, 0x35, 0x06, 0x38,
|
||||
0x36, 0x06, 0x90, 0x7b, 0x6a, 0x7c, 0x02, 0xb0, 0xf9, 0xf6, 0x15, 0x7b, 0x53, 0xc8, 0x67, 0xe4,
|
||||
0xb9, 0x16, 0x6c, 0x76, 0x7b, 0x80, 0x4d, 0x46, 0xa5, 0x9b, 0x52, 0x16, 0xcd, 0xe7, 0xa4, 0xe9,
|
||||
0x90, 0x40, 0xc5, 0xa4, 0x04, 0x33, 0x22, 0x5e, 0xe2, 0x82, 0xa1, 0xb0, 0xa0, 0x6c, 0x52, 0x3e,
|
||||
0xaf, 0x45, 0x34, 0xd7, 0xf8, 0x3f, 0xa1, 0x15, 0x5b, 0x00, 0x47, 0x71, 0x8c, 0xbc, 0x54, 0x6a,
|
||||
0x0d, 0x07, 0x2b, 0x04, 0xb3, 0x56, 0x4e, 0xea, 0x1b, 0x42, 0x22, 0x73, 0xf5, 0x48, 0x27, 0x1a,
|
||||
0x0b, 0xb2, 0x31, 0x60, 0x53, 0xfa, 0x76, 0x99, 0x19, 0x55, 0xeb, 0xd6, 0x31, 0x59, 0x43, 0x4e,
|
||||
0xce, 0xbb, 0x4e, 0x46, 0x6d, 0xae, 0x5a, 0x10, 0x73, 0xa6, 0x72, 0x76, 0x27, 0x09, 0x7a, 0x10,
|
||||
0x49, 0xe6, 0x17, 0xd9, 0x1d, 0x36, 0x10, 0x94, 0xfa, 0x68, 0xf0, 0xff, 0x77, 0x98, 0x71, 0x30,
|
||||
0x30, 0x5b, 0xea, 0xba, 0x2e, 0xda, 0x04, 0xdf, 0x99, 0x7b, 0x71, 0x4d, 0x6c, 0x6f, 0x2c, 0x29,
|
||||
0xa6, 0xad, 0x5c, 0xb4, 0x02, 0x2b, 0x02, 0x70, 0x9b, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
|
||||
0x0c, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x09, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
|
||||
```
|
||||
|
||||
First, we calculate the one-time Poly1305 key
|
||||
|
||||
```cryptol
|
||||
|
||||
//generate and check the one time key (leaving out the given states from the document, they will be correct if this is correct)
|
||||
property TV1_otk_correct = Poly1305_key_correct TV1_AEAD_key TV1_AEAD_nonce TV1_AEAD_known_otk
|
||||
|
||||
```
|
||||
|
||||
Next, we construct the AEAD buffer
|
||||
|
||||
```cryptol
|
||||
property poly_input_correct AeadAAD cypherText result = (AeadConstruction AeadAAD cypherText) == result
|
||||
|
||||
property TV1_poly_input_correct = (poly_input_correct TV1_AEAD_AAD TV1_AEAD_cypherText TV1_AEAD_Poly_input)
|
||||
```
|
||||
|
||||
We calculate the Poly1305 tag and find that it matches
|
||||
|
||||
```cryptol
|
||||
property TV1_tag_correct = poly1305_MAC_correct TV1_AEAD_known_otk (AeadConstruction TV1_AEAD_AAD TV1_AEAD_cypherText) TV1_AEAD_tag
|
||||
```
|
||||
|
||||
```cryptol
|
||||
property all_tests_correct =
|
||||
TV1_plaintext = [
|
||||
0x49, 0x6e, 0x74, 0x65, 0x72, 0x6e, 0x65, 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x73, 0x20,
|
||||
0x61, 0x72, 0x65, 0x20, 0x64, 0x72, 0x61, 0x66, 0x74, 0x20, 0x64, 0x6f, 0x63, 0x75, 0x6d, 0x65,
|
||||
0x6e, 0x74, 0x73, 0x20, 0x76, 0x61, 0x6c, 0x69, 0x64, 0x20, 0x66, 0x6f, 0x72, 0x20, 0x61, 0x20,
|
||||
0x6d, 0x61, 0x78, 0x69, 0x6d, 0x75, 0x6d, 0x20, 0x6f, 0x66, 0x20, 0x73, 0x69, 0x78, 0x20, 0x6d,
|
||||
0x6f, 0x6e, 0x74, 0x68, 0x73, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x6d, 0x61, 0x79, 0x20, 0x62, 0x65,
|
||||
0x20, 0x75, 0x70, 0x64, 0x61, 0x74, 0x65, 0x64, 0x2c, 0x20, 0x72, 0x65, 0x70, 0x6c, 0x61, 0x63,
|
||||
0x65, 0x64, 0x2c, 0x20, 0x6f, 0x72, 0x20, 0x6f, 0x62, 0x73, 0x6f, 0x6c, 0x65, 0x74, 0x65, 0x64,
|
||||
0x20, 0x62, 0x79, 0x20, 0x6f, 0x74, 0x68, 0x65, 0x72, 0x20, 0x64, 0x6f, 0x63, 0x75, 0x6d, 0x65,
|
||||
0x6e, 0x74, 0x73, 0x20, 0x61, 0x74, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x74, 0x69, 0x6d, 0x65, 0x2e,
|
||||
0x20, 0x49, 0x74, 0x20, 0x69, 0x73, 0x20, 0x69, 0x6e, 0x61, 0x70, 0x70, 0x72, 0x6f, 0x70, 0x72,
|
||||
0x69, 0x61, 0x74, 0x65, 0x20, 0x74, 0x6f, 0x20, 0x75, 0x73, 0x65, 0x20, 0x49, 0x6e, 0x74, 0x65,
|
||||
0x72, 0x6e, 0x65, 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x73, 0x20, 0x61, 0x73, 0x20, 0x72,
|
||||
0x65, 0x66, 0x65, 0x72, 0x65, 0x6e, 0x63, 0x65, 0x20, 0x6d, 0x61, 0x74, 0x65, 0x72, 0x69, 0x61,
|
||||
0x6c, 0x20, 0x6f, 0x72, 0x20, 0x74, 0x6f, 0x20, 0x63, 0x69, 0x74, 0x65, 0x20, 0x74, 0x68, 0x65,
|
||||
0x6d, 0x20, 0x6f, 0x74, 0x68, 0x65, 0x72, 0x20, 0x74, 0x68, 0x61, 0x6e, 0x20, 0x61, 0x73, 0x20,
|
||||
0x2f, 0xe2, 0x80, 0x9c, 0x77, 0x6f, 0x72, 0x6b, 0x20, 0x69, 0x6e, 0x20, 0x70, 0x72, 0x6f, 0x67,
|
||||
0x72, 0x65, 0x73, 0x73, 0x2e, 0x2f, 0xe2, 0x80, 0x9d]
|
||||
|
||||
|
||||
TV1_calculate_plaintext = AEAD_CHACHA20_POLY1305_DECRYPT TV1_AEAD_key TV1_AEAD_nonce (TV1_AEAD_cypherText # TV1_AEAD_tag) TV1_AEAD_AAD
|
||||
|
||||
property TV1_plaintext_correct = isValid && pt == TV1_plaintext where
|
||||
(pt,isValid) = TV1_calculate_plaintext
|
||||
|
||||
property decryption_vector_correct =
|
||||
TV1_plaintext_correct &&
|
||||
TV1_tag_correct &&
|
||||
TV1_otk_correct
|
||||
|
||||
|
||||
property all_test_vectors_correct =
|
||||
all_block_tests_correct &&
|
||||
all_enc_tests_correct &&
|
||||
all_MAC_tests_correct &&
|
||||
all_key_tests_correct
|
||||
all_key_tests_correct &&
|
||||
decryption_vector_correct
|
||||
```
|
||||
|
||||
|
||||
@ -2059,7 +2168,8 @@ property AllPropertiesPass =
|
||||
AeadTag_correct &&
|
||||
AeadConstruction_correct &&
|
||||
AeadDecrypt_correct &&
|
||||
parseHexString_check
|
||||
parseHexString_check &&
|
||||
all_test_vectors_correct
|
||||
|
||||
```
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user