mirror of
https://github.com/GaloisInc/cryptol.git
synced 2025-01-05 15:07:12 +03:00
added most of the test cases
This commit is contained in:
Joey Dodds
parent
5faf927b3e
commit
00ad314681
515
examples/ChaChaPolyCryptolIETF.md
Normal file → Executable file
515
examples/ChaChaPolyCryptolIETF.md
Normal file → Executable file
@ -1458,33 +1458,526 @@ Email: dylan@galois.com
|
||||
|
||||
## The ChaCha20 Block Functions
|
||||
|
||||
```cryptol
|
||||
property TV_block_correct key nonce blockcounter result = ChaCha20Block key nonce blockcounter == result
|
||||
|
||||
property TV_block_Keystream_correct key nonce blockcounter keystream =
|
||||
take`{0x40} (groupBy`{8} (join (join (ChaCha20ExpandKey key nonce blockcounter)))) == keystream
|
||||
|
||||
property ChaCha20_block_correct key nonce blockcounter result keystream =
|
||||
TV_block_correct key nonce blockcounter result &&
|
||||
TV_block_Keystream_correct key nonce blockcounter keystream
|
||||
```
|
||||
|
||||
### Test Vector #1
|
||||
|
||||
```cryptol
|
||||
TV1Key = zero:ChaChaKey
|
||||
TV1Nonce = zero:[96]
|
||||
TV1InitState = BuildState TV1Key TV1Nonce 0
|
||||
TV1_block_Key = zero:ChaChaKey
|
||||
TV1_block_Nonce = zero:[96]
|
||||
TV1_block_BlockCounter = 0
|
||||
|
||||
TV1After20 = [
|
||||
TV1_block_After20 = [
|
||||
0xade0b876, 0x903df1a0, 0xe56a5d40, 0x28bd8653,
|
||||
0xb819d2bd, 0x1aed8da0, 0xccef36a8, 0xc70d778b,
|
||||
0x7c5941da, 0x8d485751, 0x3fe02477, 0x374ad8b8,
|
||||
0xf4b8436a, 0x1ca11815, 0x69b687c3, 0x8665eeb2]
|
||||
|
||||
TV1KeyStream = [
|
||||
TV1_block_KeyStream = [
|
||||
0x76, 0xb8, 0xe0, 0xad, 0xa0, 0xf1, 0x3d, 0x90, 0x40, 0x5d, 0x6a, 0xe5, 0x53, 0x86, 0xbd, 0x28,
|
||||
0xbd, 0xd2, 0x19, 0xb8, 0xa0, 0x8d, 0xed, 0x1a, 0xa8, 0x36, 0xef, 0xcc, 0x8b, 0x77, 0x0d, 0xc7,
|
||||
0xda, 0x41, 0x59, 0x7c, 0x51, 0x57, 0x48, 0x8d, 0x77, 0x24, 0xe0, 0x3f, 0xb8, 0xd8, 0x4a, 0x37,
|
||||
0x6a, 0x43, 0xb8, 0xf4, 0x15, 0x18, 0xa1, 0x1c, 0xc3, 0x87, 0xb6, 0x69, 0xb2, 0xee, 0x65, 0x86]
|
||||
|
||||
property TV1_correct = ChaCha20Block T1Key T1Nonce 0 == TV1After20
|
||||
property TV1_block_correct = ChaCha20_block_correct TV1_block_Key TV1_block_Nonce TV1_block_BlockCounter TV1_block_After20 TV1_block_KeyStream
|
||||
|
||||
property TV1Keystream_correct =
|
||||
take`{0x40} (groupBy`{8} (join (join (ChaCha20ExpandKey TV1Key TV1Nonce 0)))) ==
|
||||
TV1KeyStream
|
||||
|
||||
// TODO: port the rest
|
||||
```
|
||||
|
||||
### Test Vector #2
|
||||
|
||||
```cryptol
|
||||
TV2_block_Key = zero:ChaChaKey
|
||||
TV2_block_Nonce = zero:[96]
|
||||
TV2_block_BlockCounter = 1
|
||||
|
||||
TV2_block_After20 = [
|
||||
0xbee7079f, 0x7a385155, 0x7c97ba98, 0x0d082d73,
|
||||
0xa0290fcb, 0x6965e348, 0x3e53c612, 0xed7aee32,
|
||||
0x7621b729, 0x434ee69c, 0xb03371d5, 0xd539d874,
|
||||
0x281fed31, 0x45fb0a51, 0x1f0ae1ac, 0x6f4d794b]
|
||||
|
||||
TV2_block_KeyStream = [
|
||||
0x9f, 0x07, 0xe7, 0xbe, 0x55, 0x51, 0x38, 0x7a, 0x98, 0xba, 0x97, 0x7c, 0x73, 0x2d, 0x08, 0x0d,
|
||||
0xcb, 0x0f, 0x29, 0xa0, 0x48, 0xe3, 0x65, 0x69, 0x12, 0xc6, 0x53, 0x3e, 0x32, 0xee, 0x7a, 0xed,
|
||||
0x29, 0xb7, 0x21, 0x76, 0x9c, 0xe6, 0x4e, 0x43, 0xd5, 0x71, 0x33, 0xb0, 0x74, 0xd8, 0x39, 0xd5,
|
||||
0x31, 0xed, 0x1f, 0x28, 0x51, 0x0a, 0xfb, 0x45, 0xac, 0xe1, 0x0a, 0x1f, 0x4b, 0x79, 0x4d, 0x6f]
|
||||
|
||||
property TV2_block_correct = ChaCha20_block_correct TV2_block_Key TV2_block_Nonce TV2_block_BlockCounter TV2_block_After20 TV2_block_KeyStream
|
||||
|
||||
|
||||
```
|
||||
|
||||
### Test Vector #3
|
||||
|
||||
```cryptol
|
||||
TV3_block_Key = (zero # 0b1):ChaChaKey
|
||||
TV3_block_Nonce = zero:[96]
|
||||
TV3_block_BlockCounter = 1
|
||||
|
||||
TV3_block_After20 = [
|
||||
0x2452eb3a, 0x9249f8ec, 0x8d829d9b, 0xddd4ceb1,
|
||||
0xe8252083, 0x60818b01, 0xf38422b8, 0x5aaa49c9,
|
||||
0xbb00ca8e, 0xda3ba7b4, 0xc4b592d1, 0xfdf2732f,
|
||||
0x4436274e, 0x2561b3c8, 0xebdd4aa6, 0xa0136c00]
|
||||
|
||||
TV3_block_KeyStream = [
|
||||
0x3a, 0xeb, 0x52, 0x24, 0xec, 0xf8, 0x49, 0x92, 0x9b, 0x9d, 0x82, 0x8d, 0xb1, 0xce, 0xd4, 0xdd,
|
||||
0x83, 0x20, 0x25, 0xe8, 0x01, 0x8b, 0x81, 0x60, 0xb8, 0x22, 0x84, 0xf3, 0xc9, 0x49, 0xaa, 0x5a,
|
||||
0x8e, 0xca, 0x00, 0xbb, 0xb4, 0xa7, 0x3b, 0xda, 0xd1, 0x92, 0xb5, 0xc4, 0x2f, 0x73, 0xf2, 0xfd,
|
||||
0x4e, 0x27, 0x36, 0x44, 0xc8, 0xb3, 0x61, 0x25, 0xa6, 0x4a, 0xdd, 0xeb, 0x00, 0x6c, 0x13, 0xa0]
|
||||
|
||||
property TV3_block_correct = ChaCha20_block_correct TV3_block_Key TV3_block_Nonce TV3_block_BlockCounter TV3_block_After20 TV3_block_KeyStream
|
||||
|
||||
```
|
||||
|
||||
### Test Vector #4
|
||||
|
||||
```cryptol
|
||||
TV4_block_Key = ( 0x00ff # zero):ChaChaKey
|
||||
TV4_block_Nonce = zero:[96]
|
||||
TV4_block_BlockCounter = 2
|
||||
|
||||
TV4_block_After20 = [
|
||||
0xfb4dd572, 0x4bc42ef1, 0xdf922636, 0x327f1394,
|
||||
0xa78dea8f, 0x5e269039, 0xa1bebbc1, 0xcaf09aae,
|
||||
0xa25ab213, 0x48a6b46c, 0x1b9d9bcb, 0x092c5be6,
|
||||
0x546ca624, 0x1bec45d5, 0x87f47473, 0x96f0992e]
|
||||
|
||||
TV4_block_KeyStream = [
|
||||
0x72, 0xd5, 0x4d, 0xfb, 0xf1, 0x2e, 0xc4, 0x4b, 0x36, 0x26, 0x92, 0xdf, 0x94, 0x13, 0x7f, 0x32,
|
||||
0x8f, 0xea, 0x8d, 0xa7, 0x39, 0x90, 0x26, 0x5e, 0xc1, 0xbb, 0xbe, 0xa1, 0xae, 0x9a, 0xf0, 0xca,
|
||||
0x13, 0xb2, 0x5a, 0xa2, 0x6c, 0xb4, 0xa6, 0x48, 0xcb, 0x9b, 0x9d, 0x1b, 0xe6, 0x5b, 0x2c, 0x09,
|
||||
0x24, 0xa6, 0x6c, 0x54, 0xd5, 0x45, 0xec, 0x1b, 0x73, 0x74, 0xf4, 0x87, 0x2e, 0x99, 0xf0, 0x96]
|
||||
|
||||
property TV4_block_correct = ChaCha20_block_correct TV4_block_Key TV4_block_Nonce TV4_block_BlockCounter TV4_block_After20 TV4_block_KeyStream
|
||||
|
||||
```
|
||||
|
||||
### Test Vector #5
|
||||
|
||||
```cryptol
|
||||
TV5_block_Key = (zero):ChaChaKey
|
||||
TV5_block_Nonce = zero # 0x02:[96]
|
||||
TV5_block_BlockCounter = 0
|
||||
|
||||
TV5_block_After20 = [
|
||||
0x374dc6c2, 0x3736d58c, 0xb904e24a, 0xcd3f93ef,
|
||||
0x88228b1a, 0x96a4dfb3, 0x5b76ab72, 0xc727ee54,
|
||||
0x0e0e978a, 0xf3145c95, 0x1b748ea8, 0xf786c297,
|
||||
0x99c28f5f, 0x628314e8, 0x398a19fa, 0x6ded1b53]
|
||||
|
||||
TV5_block_KeyStream = [
|
||||
0xc2, 0xc6, 0x4d, 0x37, 0x8c, 0xd5, 0x36, 0x37, 0x4a, 0xe2, 0x04, 0xb9, 0xef, 0x93, 0x3f, 0xcd,
|
||||
0x1a, 0x8b, 0x22, 0x88, 0xb3, 0xdf, 0xa4, 0x96, 0x72, 0xab, 0x76, 0x5b, 0x54, 0xee, 0x27, 0xc7,
|
||||
0x8a, 0x97, 0x0e, 0x0e, 0x95, 0x5c, 0x14, 0xf3, 0xa8, 0x8e, 0x74, 0x1b, 0x97, 0xc2, 0x86, 0xf7,
|
||||
0x5f, 0x8f, 0xc2, 0x99, 0xe8, 0x14, 0x83, 0x62, 0xfa, 0x19, 0x8a, 0x39, 0x53, 0x1b, 0xed, 0x6d]
|
||||
|
||||
property TV5_block_correct = ChaCha20_block_correct TV5_block_Key TV5_block_Nonce TV5_block_BlockCounter TV5_block_After20 TV5_block_KeyStream
|
||||
|
||||
property all_block_tests_correct =
|
||||
TV1_block_correct &&
|
||||
TV2_block_correct &&
|
||||
TV3_block_correct &&
|
||||
TV4_block_correct &&
|
||||
TV5_block_correct
|
||||
|
||||
```
|
||||
|
||||
## ChaCha20 Encryption
|
||||
|
||||
```cryptol
|
||||
property ChaCha20_enc_correct key nonce blockcounter plaintext cyphertext = ChaCha20EncryptBytes plaintext key nonce blockcounter == cyphertext
|
||||
```
|
||||
|
||||
### Test Vector #1
|
||||
|
||||
```cryptol
|
||||
TV1_enc_Key = (zero):ChaChaKey
|
||||
TV1_enc_Nonce = zero:[96]
|
||||
TV1_enc_BlockCounter = 0
|
||||
|
||||
TV1_enc_plaintext = zero:[64][8]
|
||||
|
||||
TV1_enc_cyphertext = [
|
||||
0x76, 0xb8, 0xe0, 0xad, 0xa0, 0xf1, 0x3d, 0x90, 0x40, 0x5d, 0x6a, 0xe5, 0x53, 0x86, 0xbd, 0x28,
|
||||
0xbd, 0xd2, 0x19, 0xb8, 0xa0, 0x8d, 0xed, 0x1a, 0xa8, 0x36, 0xef, 0xcc, 0x8b, 0x77, 0x0d, 0xc7,
|
||||
0xda, 0x41, 0x59, 0x7c, 0x51, 0x57, 0x48, 0x8d, 0x77, 0x24, 0xe0, 0x3f, 0xb8, 0xd8, 0x4a, 0x37,
|
||||
0x6a, 0x43, 0xb8, 0xf4, 0x15, 0x18, 0xa1, 0x1c, 0xc3, 0x87, 0xb6, 0x69, 0xb2, 0xee, 0x65, 0x86]
|
||||
|
||||
property TV1_enc_correct = ChaCha20_enc_correct TV1_enc_Key TV1_enc_Nonce TV1_enc_BlockCounter TV1_enc_plaintext TV1_enc_cyphertext
|
||||
|
||||
```
|
||||
|
||||
### Test Vector #2
|
||||
|
||||
```cryptol
|
||||
TV2_enc_Key = (zero # 0x1):ChaChaKey
|
||||
TV2_enc_Nonce = zero # 0x2:[96]
|
||||
TV2_enc_BlockCounter = 1
|
||||
|
||||
IETF_submission_text = [
|
||||
0x41, 0x6e, 0x79, 0x20, 0x73, 0x75, 0x62, 0x6d, 0x69, 0x73, 0x73, 0x69, 0x6f, 0x6e, 0x20, 0x74,
|
||||
0x6f, 0x20, 0x74, 0x68, 0x65, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x69, 0x6e, 0x74, 0x65, 0x6e,
|
||||
0x64, 0x65, 0x64, 0x20, 0x62, 0x79, 0x20, 0x74, 0x68, 0x65, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72,
|
||||
0x69, 0x62, 0x75, 0x74, 0x6f, 0x72, 0x20, 0x66, 0x6f, 0x72, 0x20, 0x70, 0x75, 0x62, 0x6c, 0x69,
|
||||
0x63, 0x61, 0x74, 0x69, 0x6f, 0x6e, 0x20, 0x61, 0x73, 0x20, 0x61, 0x6c, 0x6c, 0x20, 0x6f, 0x72,
|
||||
0x20, 0x70, 0x61, 0x72, 0x74, 0x20, 0x6f, 0x66, 0x20, 0x61, 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46,
|
||||
0x20, 0x49, 0x6e, 0x74, 0x65, 0x72, 0x6e, 0x65, 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x20,
|
||||
0x6f, 0x72, 0x20, 0x52, 0x46, 0x43, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x73,
|
||||
0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x20, 0x6d, 0x61, 0x64, 0x65, 0x20, 0x77, 0x69,
|
||||
0x74, 0x68, 0x69, 0x6e, 0x20, 0x74, 0x68, 0x65, 0x20, 0x63, 0x6f, 0x6e, 0x74, 0x65, 0x78, 0x74,
|
||||
0x20, 0x6f, 0x66, 0x20, 0x61, 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x61, 0x63, 0x74, 0x69,
|
||||
0x76, 0x69, 0x74, 0x79, 0x20, 0x69, 0x73, 0x20, 0x63, 0x6f, 0x6e, 0x73, 0x69, 0x64, 0x65, 0x72,
|
||||
0x65, 0x64, 0x20, 0x61, 0x6e, 0x20, 0x22, 0x49, 0x45, 0x54, 0x46, 0x20, 0x43, 0x6f, 0x6e, 0x74,
|
||||
0x72, 0x69, 0x62, 0x75, 0x74, 0x69, 0x6f, 0x6e, 0x22, 0x2e, 0x20, 0x53, 0x75, 0x63, 0x68, 0x20,
|
||||
0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x73, 0x20, 0x69, 0x6e, 0x63, 0x6c, 0x75,
|
||||
0x64, 0x65, 0x20, 0x6f, 0x72, 0x61, 0x6c, 0x20, 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e,
|
||||
0x74, 0x73, 0x20, 0x69, 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x73, 0x65, 0x73, 0x73, 0x69,
|
||||
0x6f, 0x6e, 0x73, 0x2c, 0x20, 0x61, 0x73, 0x20, 0x77, 0x65, 0x6c, 0x6c, 0x20, 0x61, 0x73, 0x20,
|
||||
0x77, 0x72, 0x69, 0x74, 0x74, 0x65, 0x6e, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x65, 0x6c, 0x65, 0x63,
|
||||
0x74, 0x72, 0x6f, 0x6e, 0x69, 0x63, 0x20, 0x63, 0x6f, 0x6d, 0x6d, 0x75, 0x6e, 0x69, 0x63, 0x61,
|
||||
0x74, 0x69, 0x6f, 0x6e, 0x73, 0x20, 0x6d, 0x61, 0x64, 0x65, 0x20, 0x61, 0x74, 0x20, 0x61, 0x6e,
|
||||
0x79, 0x20, 0x74, 0x69, 0x6d, 0x65, 0x20, 0x6f, 0x72, 0x20, 0x70, 0x6c, 0x61, 0x63, 0x65, 0x2c,
|
||||
0x20, 0x77, 0x68, 0x69, 0x63, 0x68, 0x20, 0x61, 0x72, 0x65, 0x20, 0x61, 0x64, 0x64, 0x72, 0x65,
|
||||
0x73, 0x73, 0x65, 0x64, 0x20, 0x74, 0x6f ]
|
||||
|
||||
TV2_enc_plaintext = IETF_submission_text
|
||||
|
||||
|
||||
TV2_enc_cyphertext = [
|
||||
0xa3, 0xfb, 0xf0, 0x7d, 0xf3, 0xfa, 0x2f, 0xde, 0x4f, 0x37, 0x6c, 0xa2, 0x3e, 0x82, 0x73, 0x70,
|
||||
0x41, 0x60, 0x5d, 0x9f, 0x4f, 0x4f, 0x57, 0xbd, 0x8c, 0xff, 0x2c, 0x1d, 0x4b, 0x79, 0x55, 0xec,
|
||||
0x2a, 0x97, 0x94, 0x8b, 0xd3, 0x72, 0x29, 0x15, 0xc8, 0xf3, 0xd3, 0x37, 0xf7, 0xd3, 0x70, 0x05,
|
||||
0x0e, 0x9e, 0x96, 0xd6, 0x47, 0xb7, 0xc3, 0x9f, 0x56, 0xe0, 0x31, 0xca, 0x5e, 0xb6, 0x25, 0x0d,
|
||||
0x40, 0x42, 0xe0, 0x27, 0x85, 0xec, 0xec, 0xfa, 0x4b, 0x4b, 0xb5, 0xe8, 0xea, 0xd0, 0x44, 0x0e,
|
||||
0x20, 0xb6, 0xe8, 0xdb, 0x09, 0xd8, 0x81, 0xa7, 0xc6, 0x13, 0x2f, 0x42, 0x0e, 0x52, 0x79, 0x50,
|
||||
0x42, 0xbd, 0xfa, 0x77, 0x73, 0xd8, 0xa9, 0x05, 0x14, 0x47, 0xb3, 0x29, 0x1c, 0xe1, 0x41, 0x1c,
|
||||
0x68, 0x04, 0x65, 0x55, 0x2a, 0xa6, 0xc4, 0x05, 0xb7, 0x76, 0x4d, 0x5e, 0x87, 0xbe, 0xa8, 0x5a,
|
||||
0xd0, 0x0f, 0x84, 0x49, 0xed, 0x8f, 0x72, 0xd0, 0xd6, 0x62, 0xab, 0x05, 0x26, 0x91, 0xca, 0x66,
|
||||
0x42, 0x4b, 0xc8, 0x6d, 0x2d, 0xf8, 0x0e, 0xa4, 0x1f, 0x43, 0xab, 0xf9, 0x37, 0xd3, 0x25, 0x9d,
|
||||
0xc4, 0xb2, 0xd0, 0xdf, 0xb4, 0x8a, 0x6c, 0x91, 0x39, 0xdd, 0xd7, 0xf7, 0x69, 0x66, 0xe9, 0x28,
|
||||
0xe6, 0x35, 0x55, 0x3b, 0xa7, 0x6c, 0x5c, 0x87, 0x9d, 0x7b, 0x35, 0xd4, 0x9e, 0xb2, 0xe6, 0x2b,
|
||||
0x08, 0x71, 0xcd, 0xac, 0x63, 0x89, 0x39, 0xe2, 0x5e, 0x8a, 0x1e, 0x0e, 0xf9, 0xd5, 0x28, 0x0f,
|
||||
0xa8, 0xca, 0x32, 0x8b, 0x35, 0x1c, 0x3c, 0x76, 0x59, 0x89, 0xcb, 0xcf, 0x3d, 0xaa, 0x8b, 0x6c,
|
||||
0xcc, 0x3a, 0xaf, 0x9f, 0x39, 0x79, 0xc9, 0x2b, 0x37, 0x20, 0xfc, 0x88, 0xdc, 0x95, 0xed, 0x84,
|
||||
0xa1, 0xbe, 0x05, 0x9c, 0x64, 0x99, 0xb9, 0xfd, 0xa2, 0x36, 0xe7, 0xe8, 0x18, 0xb0, 0x4b, 0x0b,
|
||||
0xc3, 0x9c, 0x1e, 0x87, 0x6b, 0x19, 0x3b, 0xfe, 0x55, 0x69, 0x75, 0x3f, 0x88, 0x12, 0x8c, 0xc0,
|
||||
0x8a, 0xaa, 0x9b, 0x63, 0xd1, 0xa1, 0x6f, 0x80, 0xef, 0x25, 0x54, 0xd7, 0x18, 0x9c, 0x41, 0x1f,
|
||||
0x58, 0x69, 0xca, 0x52, 0xc5, 0xb8, 0x3f, 0xa3, 0x6f, 0xf2, 0x16, 0xb9, 0xc1, 0xd3, 0x00, 0x62,
|
||||
0xbe, 0xbc, 0xfd, 0x2d, 0xc5, 0xbc, 0xe0, 0x91, 0x19, 0x34, 0xfd, 0xa7, 0x9a, 0x86, 0xf6, 0xe6,
|
||||
0x98, 0xce, 0xd7, 0x59, 0xc3, 0xff, 0x9b, 0x64, 0x77, 0x33, 0x8f, 0x3d, 0xa4, 0xf9, 0xcd, 0x85,
|
||||
0x14, 0xea, 0x99, 0x82, 0xcc, 0xaf, 0xb3, 0x41, 0xb2, 0x38, 0x4d, 0xd9, 0x02, 0xf3, 0xd1, 0xab,
|
||||
0x7a, 0xc6, 0x1d, 0xd2, 0x9c, 0x6f, 0x21, 0xba, 0x5b, 0x86, 0x2f, 0x37, 0x30, 0xe3, 0x7c, 0xfd,
|
||||
0xc4, 0xfd, 0x80, 0x6c, 0x22, 0xf2, 0x21]
|
||||
|
||||
property TV2_enc_correct = ChaCha20_enc_correct TV2_enc_Key TV2_enc_Nonce TV2_enc_BlockCounter TV2_enc_plaintext TV2_enc_cyphertext
|
||||
|
||||
```
|
||||
|
||||
### Test Vector #3
|
||||
|
||||
```cryptol
|
||||
TV3_enc_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]):ChaChaKey
|
||||
TV3_enc_Nonce = zero # 0x2:[96]
|
||||
TV3_enc_BlockCounter = 42:[32]
|
||||
|
||||
jabberwock_text = [
|
||||
0x27, 0x54, 0x77, 0x61, 0x73, 0x20, 0x62, 0x72, 0x69, 0x6c, 0x6c, 0x69, 0x67, 0x2c, 0x20, 0x61,
|
||||
0x6e, 0x64, 0x20, 0x74, 0x68, 0x65, 0x20, 0x73, 0x6c, 0x69, 0x74, 0x68, 0x79, 0x20, 0x74, 0x6f,
|
||||
0x76, 0x65, 0x73, 0x0a, 0x44, 0x69, 0x64, 0x20, 0x67, 0x79, 0x72, 0x65, 0x20, 0x61, 0x6e, 0x64,
|
||||
0x20, 0x67, 0x69, 0x6d, 0x62, 0x6c, 0x65, 0x20, 0x69, 0x6e, 0x20, 0x74, 0x68, 0x65, 0x20, 0x77,
|
||||
0x61, 0x62, 0x65, 0x3a, 0x0a, 0x41, 0x6c, 0x6c, 0x20, 0x6d, 0x69, 0x6d, 0x73, 0x79, 0x20, 0x77,
|
||||
0x65, 0x72, 0x65, 0x20, 0x74, 0x68, 0x65, 0x20, 0x62, 0x6f, 0x72, 0x6f, 0x67, 0x6f, 0x76, 0x65,
|
||||
0x73, 0x2c, 0x0a, 0x41, 0x6e, 0x64, 0x20, 0x74, 0x68, 0x65, 0x20, 0x6d, 0x6f, 0x6d, 0x65, 0x20,
|
||||
0x72, 0x61, 0x74, 0x68, 0x73, 0x20, 0x6f, 0x75, 0x74, 0x67, 0x72, 0x61, 0x62, 0x65, 0x2e]
|
||||
|
||||
TV3_enc_plaintext = jabberwock_text
|
||||
|
||||
|
||||
TV3_enc_cyphertext = [
|
||||
0x62, 0xe6, 0x34, 0x7f, 0x95, 0xed, 0x87, 0xa4, 0x5f, 0xfa, 0xe7, 0x42, 0x6f, 0x27, 0xa1, 0xdf,
|
||||
0x5f, 0xb6, 0x91, 0x10, 0x04, 0x4c, 0x0d, 0x73, 0x11, 0x8e, 0xff, 0xa9, 0x5b, 0x01, 0xe5, 0xcf,
|
||||
0x16, 0x6d, 0x3d, 0xf2, 0xd7, 0x21, 0xca, 0xf9, 0xb2, 0x1e, 0x5f, 0xb1, 0x4c, 0x61, 0x68, 0x71,
|
||||
0xfd, 0x84, 0xc5, 0x4f, 0x9d, 0x65, 0xb2, 0x83, 0x19, 0x6c, 0x7f, 0xe4, 0xf6, 0x05, 0x53, 0xeb,
|
||||
0xf3, 0x9c, 0x64, 0x02, 0xc4, 0x22, 0x34, 0xe3, 0x2a, 0x35, 0x6b, 0x3e, 0x76, 0x43, 0x12, 0xa6,
|
||||
0x1a, 0x55, 0x32, 0x05, 0x57, 0x16, 0xea, 0xd6, 0x96, 0x25, 0x68, 0xf8, 0x7d, 0x3f, 0x3f, 0x77,
|
||||
0x04, 0xc6, 0xa8, 0xd1, 0xbc, 0xd1, 0xbf, 0x4d, 0x50, 0xd6, 0x15, 0x4b, 0x6d, 0xa7, 0x31, 0xb1,
|
||||
0x87, 0xb5, 0x8d, 0xfd, 0x72, 0x8a, 0xfa, 0x36, 0x75, 0x7a, 0x79, 0x7a, 0xc1, 0x88, 0xd1]
|
||||
|
||||
property TV3_enc_correct = ChaCha20_enc_correct TV3_enc_Key TV3_enc_Nonce TV3_enc_BlockCounter TV3_enc_plaintext TV3_enc_cyphertext
|
||||
|
||||
property all_enc_tests_correct =
|
||||
TV1_enc_correct &&
|
||||
TV2_enc_correct &&
|
||||
TV3_enc_correct
|
||||
```
|
||||
|
||||
## Poly1305 Message Authentication Code
|
||||
|
||||
```cryptol
|
||||
property poly1305_MAC_correct key text tag = Poly1305 key text == tag
|
||||
```
|
||||
|
||||
### Test Vector #1
|
||||
|
||||
```cryptol
|
||||
TV1_MAC_Key = zero:[256]
|
||||
|
||||
TV1_MAC_text = zero:[64][8]
|
||||
|
||||
TV1_MAC_tag = zero : [16][8]
|
||||
|
||||
property TV1_MAC_correct = poly1305_MAC_correct TV1_MAC_Key TV1_MAC_text TV1_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #2
|
||||
|
||||
```cryptol
|
||||
reused_key = [0x36, 0xe5, 0xf6, 0xb5, 0xc5, 0xe0, 0x60, 0x70, 0xf0, 0xef, 0xca, 0x96, 0x22, 0x7a, 0x86, 0x3e]
|
||||
TV2_MAC_Key = zero # join(reused_key):[256]
|
||||
|
||||
TV2_MAC_text = IETF_submission_text
|
||||
|
||||
TV2_MAC_tag = reused_key: [16][8]
|
||||
|
||||
property TV2_MAC_correct = poly1305_MAC_correct TV2_MAC_Key TV2_MAC_text TV2_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #3
|
||||
|
||||
```cryptol
|
||||
TV3_MAC_Key = join(reused_key) # 0:[256]
|
||||
|
||||
TV3_MAC_text = IETF_submission_text
|
||||
|
||||
TV3_MAC_tag = [0xf3, 0x47, 0x7e, 0x7c, 0xd9, 0x54, 0x17, 0xaf, 0x89, 0xa6, 0xb8, 0x79, 0x4c, 0x31, 0x0c, 0xf0]: [16][8]
|
||||
|
||||
property TV3_MAC_correct = poly1305_MAC_correct TV3_MAC_Key TV3_MAC_text TV3_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #4
|
||||
|
||||
```cryptol
|
||||
TV4_MAC_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]):[256]
|
||||
|
||||
TV4_MAC_text = jabberwock_text
|
||||
|
||||
TV4_MAC_tag = [0x45, 0x41, 0x66, 0x9a, 0x7e, 0xaa, 0xee, 0x61, 0xe7, 0x08, 0xdc, 0x7c, 0xbc, 0xc5, 0xeb, 0x62]: [16][8]
|
||||
|
||||
property TV4_MAC_correct = poly1305_MAC_correct TV4_MAC_Key TV4_MAC_text TV4_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #5
|
||||
|
||||
If one uses 130-bit partial reduction, does the code
|
||||
handle the case where partially reduced final result is not fully
|
||||
reduced?
|
||||
|
||||
```cryptol
|
||||
|
||||
TV5_MAC_Key = 0x02 # zero:[256]
|
||||
|
||||
FF_16 = [0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF]
|
||||
TV5_MAC_text = FF_16
|
||||
|
||||
TV5_MAC_tag = split(0x03 # zero): [16][8]
|
||||
|
||||
property TV5_MAC_correct = poly1305_MAC_correct TV5_MAC_Key TV5_MAC_text TV5_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #6
|
||||
|
||||
What happens if addition of s overflows modulo 2^128?
|
||||
|
||||
```cryptol
|
||||
TV6_MAC_Key = 0x02 # zero # join(FF_16):[256]
|
||||
|
||||
TV6_MAC_text = split(0x02 # zero) : [16][8]
|
||||
|
||||
TV6_MAC_tag = split(0x03 # 0): [16][8]
|
||||
|
||||
property TV6_MAC_correct = poly1305_MAC_correct TV6_MAC_Key TV6_MAC_text TV6_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #7
|
||||
|
||||
What happens if data limb is all ones and there is
|
||||
carry from lower limb?
|
||||
|
||||
```cryptol
|
||||
|
||||
TV7_MAC_Key = 0x01 # zero:[256]
|
||||
|
||||
TV7_MAC_text = [
|
||||
0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
|
||||
0xF0, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
|
||||
0x11, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
|
||||
|
||||
TV7_MAC_tag = split(0x05 # zero): [16][8]
|
||||
|
||||
property TV7_MAC_correct = poly1305_MAC_correct TV7_MAC_Key TV7_MAC_text TV7_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #8
|
||||
|
||||
What happens if final result from polynomial part is
|
||||
exactly 2^130-5?
|
||||
|
||||
```cryptol
|
||||
|
||||
TV8_MAC_Key = 0x01 # zero:[256]
|
||||
|
||||
TV8_MAC_text = [
|
||||
0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
|
||||
0xFB, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE,
|
||||
0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01]
|
||||
|
||||
TV8_MAC_tag = split(zero): [16][8]
|
||||
|
||||
property TV8_MAC_correct = poly1305_MAC_correct TV8_MAC_Key TV8_MAC_text TV8_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #9
|
||||
|
||||
What happens if final result from polynomial part is
|
||||
exactly 2^130-6?
|
||||
|
||||
```cryptol
|
||||
|
||||
TV9_MAC_Key = 0x02 # zero:[256]
|
||||
|
||||
TV9_MAC_text =
|
||||
[0xFD, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF]
|
||||
|
||||
TV9_MAC_tag = [0xFA, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF]: [16][8]
|
||||
|
||||
property TV9_MAC_correct = poly1305_MAC_correct TV9_MAC_Key TV9_MAC_text TV9_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #10
|
||||
|
||||
What happens if 5*H+L-type reduction produces 131-
|
||||
bit intermediate result?
|
||||
|
||||
```cryptol
|
||||
|
||||
TV10_MAC_Key = join([0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x04, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]) # 0 :[256]
|
||||
|
||||
TV10_MAC_text = [
|
||||
0xE3, 0x35, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0xB9, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
|
||||
0x33, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0x79, 0xCD, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
|
||||
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
|
||||
0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
|
||||
|
||||
TV10_MAC_tag = [0x14, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]: [16][8]
|
||||
|
||||
property TV10_MAC_correct = poly1305_MAC_correct TV10_MAC_Key TV10_MAC_text TV10_MAC_tag
|
||||
```
|
||||
|
||||
### Test Vector #11
|
||||
|
||||
What happens if 5*H+L-type reduction produces 131-
|
||||
bit final result?
|
||||
|
||||
```cryptol
|
||||
|
||||
TV11_MAC_Key = join([0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x04, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]) # 0 :[256]
|
||||
|
||||
TV11_MAC_text = [
|
||||
0xE3, 0x35, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0xB9, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
|
||||
0x33, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0x79, 0xCD, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
|
||||
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
|
||||
|
||||
TV11_MAC_tag = split(0x13 # 0): [16][8]
|
||||
|
||||
property TV11_MAC_correct = poly1305_MAC_correct TV11_MAC_Key TV11_MAC_text TV11_MAC_tag
|
||||
|
||||
property all_MAC_tests_correct =
|
||||
TV1_MAC_correct &&
|
||||
TV2_MAC_correct &&
|
||||
TV3_MAC_correct &&
|
||||
TV4_MAC_correct &&
|
||||
TV5_MAC_correct &&
|
||||
TV6_MAC_correct &&
|
||||
TV7_MAC_correct &&
|
||||
TV8_MAC_correct &&
|
||||
TV9_MAC_correct &&
|
||||
TV10_MAC_correct &&
|
||||
TV11_MAC_correct
|
||||
|
||||
```
|
||||
|
||||
## Poly1305 Key Generation Using ChaCha20
|
||||
|
||||
```cryptol
|
||||
Poly1305_key_correct key nonce otk = GeneratePolyKeyUsingChaCha key nonce 0 == otk
|
||||
```
|
||||
|
||||
### Test Vector #1
|
||||
|
||||
```cryptol
|
||||
TV1_key_Key = zero:ChaChaKey
|
||||
TV1_key_Nonce = zero:[96]
|
||||
|
||||
TV1_key_OneTimeKey = join([
|
||||
0x76, 0xb8, 0xe0, 0xad, 0xa0, 0xf1, 0x3d, 0x90, 0x40, 0x5d, 0x6a, 0xe5, 0x53, 0x86, 0xbd, 0x28,
|
||||
0xbd, 0xd2, 0x19, 0xb8, 0xa0, 0x8d, 0xed, 0x1a, 0xa8, 0x36, 0xef, 0xcc, 0x8b, 0x77, 0x0d, 0xc7])
|
||||
|
||||
property TV1_key_correct = Poly1305_key_correct TV1_key_Key TV1_key_Nonce TV1_key_OneTimeKey
|
||||
```
|
||||
|
||||
### Test Vector #2
|
||||
|
||||
```cryptol
|
||||
TV2_key_Key = zero # 0x01:ChaChaKey
|
||||
TV2_key_Nonce = zero # 0x02:[96]
|
||||
|
||||
TV2_key_OneTimeKey = join([
|
||||
0xec, 0xfa, 0x25, 0x4f, 0x84, 0x5f, 0x64, 0x74, 0x73, 0xd3, 0xcb, 0x14, 0x0d, 0xa9, 0xe8, 0x76,
|
||||
0x06, 0xcb, 0x33, 0x06, 0x6c, 0x44, 0x7b, 0x87, 0xbc, 0x26, 0x66, 0xdd, 0xe3, 0xfb, 0xb7, 0x39])
|
||||
|
||||
property TV2_key_correct = Poly1305_key_correct TV2_key_Key TV2_key_Nonce TV2_key_OneTimeKey
|
||||
```
|
||||
|
||||
### Test Vector #3
|
||||
|
||||
```cryptol
|
||||
TV3_key_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]):ChaChaKey
|
||||
TV3_key_Nonce = zero # 0x02:[96]
|
||||
|
||||
TV3_key_OneTimeKey = join([
|
||||
0x96, 0x5e, 0x3b, 0xc6, 0xf9, 0xec, 0x7e, 0xd9, 0x56, 0x08, 0x08, 0xf4, 0xd2, 0x29, 0xf9, 0x4b,
|
||||
0x13, 0x7f, 0xf2, 0x75, 0xca, 0x9b, 0x3f, 0xcb, 0xdd, 0x59, 0xde, 0xaa, 0xd2, 0x33, 0x10, 0xae])
|
||||
|
||||
property TV3_key_correct = Poly1305_key_correct TV3_key_Key TV3_key_Nonce TV3_key_OneTimeKey
|
||||
|
||||
property all_key_tests_correct =
|
||||
TV1_key_correct &&
|
||||
TV2_key_correct &&
|
||||
TV3_key_correct
|
||||
|
||||
property all_tests_correct =
|
||||
all_block_tests_correct &&
|
||||
all_enc_tests_correct &&
|
||||
all_MAC_tests_correct &&
|
||||
all_key_tests_correct
|
||||
```
|
||||
|
||||
|
||||
# Appendix: Utility functions
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user