| /* Copyright 2016-2017 INRIA and Microsoft Corporation |
| * |
| * Licensed under the Apache License, Version 2.0 (the "License"); |
| * you may not use this file except in compliance with the License. |
| * You may obtain a copy of the License at |
| * |
| * http://www.apache.org/licenses/LICENSE-2.0 |
| * |
| * Unless required by applicable law or agreed to in writing, software |
| * distributed under the License is distributed on an "AS IS" BASIS, |
| * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| * See the License for the specific language governing permissions and |
| * limitations under the License. |
| */ |
| |
| module Spec.Chacha20 |
| |
| module ST = FStar.HyperStack.ST |
| |
| open FStar.Mul |
| open FStar.Seq |
| open FStar.UInt32 |
| open FStar.Endianness |
| open Spec.Lib |
| open Spec.Chacha20.Lemmas |
| open Seq.Create |
| |
| #set-options "--max_fuel 0 --z3rlimit 100" |
| |
| (* Constants *) |
| let keylen = 32 (* in bytes *) |
| let blocklen = 64 (* in bytes *) |
| let noncelen = 12 (* in bytes *) |
| |
| type key = lbytes keylen |
| type block = lbytes blocklen |
| type nonce = lbytes noncelen |
| type counter = UInt.uint_t 32 |
| |
| // using @ as a functional substitute for ; |
| // internally, blocks are represented as 16 x 4-byte integers |
| type state = m:seq UInt32.t {length m = 16} |
| type idx = n:nat{n < 16} |
| type shuffle = state -> Tot state |
| |
| let line (a:idx) (b:idx) (d:idx) (s:t{0 < v s /\ v s < 32}) (m:state) : Tot state = |
| let m = m.[a] <- (m.[a] +%^ m.[b]) in |
| let m = m.[d] <- ((m.[d] ^^ m.[a]) <<< s) in m |
| |
| let quarter_round a b c d : shuffle = |
| line a b d 16ul @ |
| line c d b 12ul @ |
| line a b d 8ul @ |
| line c d b 7ul |
| |
| let column_round : shuffle = |
| quarter_round 0 4 8 12 @ |
| quarter_round 1 5 9 13 @ |
| quarter_round 2 6 10 14 @ |
| quarter_round 3 7 11 15 |
| |
| let diagonal_round : shuffle = |
| quarter_round 0 5 10 15 @ |
| quarter_round 1 6 11 12 @ |
| quarter_round 2 7 8 13 @ |
| quarter_round 3 4 9 14 |
| |
| let double_round: shuffle = |
| column_round @ diagonal_round (* 2 rounds *) |
| |
| let rounds : shuffle = |
| iter 10 double_round (* 20 rounds *) |
| |
| let chacha20_core (s:state) : Tot state = |
| let s' = rounds s in |
| Spec.Loops.seq_map2 (fun x y -> x +%^ y) s' s |
| |
| (* state initialization *) |
| let c0 = 0x61707865ul |
| let c1 = 0x3320646eul |
| let c2 = 0x79622d32ul |
| let c3 = 0x6b206574ul |
| |
| let setup (k:key) (n:nonce) (c:counter): Tot state = |
| create_4 c0 c1 c2 c3 @| |
| uint32s_from_le 8 k @| |
| create_1 (UInt32.uint_to_t c) @| |
| uint32s_from_le 3 n |
| |
| let chacha20_block (k:key) (n:nonce) (c:counter): Tot block = |
| let st = setup k n c in |
| let st' = chacha20_core st in |
| uint32s_to_le 16 st' |
| |
| let chacha20_ctx: Spec.CTR.block_cipher_ctx = |
| let open Spec.CTR in |
| { |
| keylen = keylen; |
| blocklen = blocklen; |
| noncelen = noncelen; |
| counterbits = 32; |
| incr = 1 |
| } |
| |
| let chacha20_cipher: Spec.CTR.block_cipher chacha20_ctx = chacha20_block |
| |
| let chacha20_encrypt_bytes key nonce counter m = |
| Spec.CTR.counter_mode chacha20_ctx chacha20_cipher key nonce counter m |
| |
| |
| unfold let test_plaintext = [ |
| 0x4cuy; 0x61uy; 0x64uy; 0x69uy; 0x65uy; 0x73uy; 0x20uy; 0x61uy; |
| 0x6euy; 0x64uy; 0x20uy; 0x47uy; 0x65uy; 0x6euy; 0x74uy; 0x6cuy; |
| 0x65uy; 0x6duy; 0x65uy; 0x6euy; 0x20uy; 0x6fuy; 0x66uy; 0x20uy; |
| 0x74uy; 0x68uy; 0x65uy; 0x20uy; 0x63uy; 0x6cuy; 0x61uy; 0x73uy; |
| 0x73uy; 0x20uy; 0x6fuy; 0x66uy; 0x20uy; 0x27uy; 0x39uy; 0x39uy; |
| 0x3auy; 0x20uy; 0x49uy; 0x66uy; 0x20uy; 0x49uy; 0x20uy; 0x63uy; |
| 0x6fuy; 0x75uy; 0x6cuy; 0x64uy; 0x20uy; 0x6fuy; 0x66uy; 0x66uy; |
| 0x65uy; 0x72uy; 0x20uy; 0x79uy; 0x6fuy; 0x75uy; 0x20uy; 0x6fuy; |
| 0x6euy; 0x6cuy; 0x79uy; 0x20uy; 0x6fuy; 0x6euy; 0x65uy; 0x20uy; |
| 0x74uy; 0x69uy; 0x70uy; 0x20uy; 0x66uy; 0x6fuy; 0x72uy; 0x20uy; |
| 0x74uy; 0x68uy; 0x65uy; 0x20uy; 0x66uy; 0x75uy; 0x74uy; 0x75uy; |
| 0x72uy; 0x65uy; 0x2cuy; 0x20uy; 0x73uy; 0x75uy; 0x6euy; 0x73uy; |
| 0x63uy; 0x72uy; 0x65uy; 0x65uy; 0x6euy; 0x20uy; 0x77uy; 0x6fuy; |
| 0x75uy; 0x6cuy; 0x64uy; 0x20uy; 0x62uy; 0x65uy; 0x20uy; 0x69uy; |
| 0x74uy; 0x2euy |
| ] |
| |
| unfold let test_ciphertext = [ |
| 0x6euy; 0x2euy; 0x35uy; 0x9auy; 0x25uy; 0x68uy; 0xf9uy; 0x80uy; |
| 0x41uy; 0xbauy; 0x07uy; 0x28uy; 0xdduy; 0x0duy; 0x69uy; 0x81uy; |
| 0xe9uy; 0x7euy; 0x7auy; 0xecuy; 0x1duy; 0x43uy; 0x60uy; 0xc2uy; |
| 0x0auy; 0x27uy; 0xafuy; 0xccuy; 0xfduy; 0x9fuy; 0xaeuy; 0x0buy; |
| 0xf9uy; 0x1buy; 0x65uy; 0xc5uy; 0x52uy; 0x47uy; 0x33uy; 0xabuy; |
| 0x8fuy; 0x59uy; 0x3duy; 0xabuy; 0xcduy; 0x62uy; 0xb3uy; 0x57uy; |
| 0x16uy; 0x39uy; 0xd6uy; 0x24uy; 0xe6uy; 0x51uy; 0x52uy; 0xabuy; |
| 0x8fuy; 0x53uy; 0x0cuy; 0x35uy; 0x9fuy; 0x08uy; 0x61uy; 0xd8uy; |
| 0x07uy; 0xcauy; 0x0duy; 0xbfuy; 0x50uy; 0x0duy; 0x6auy; 0x61uy; |
| 0x56uy; 0xa3uy; 0x8euy; 0x08uy; 0x8auy; 0x22uy; 0xb6uy; 0x5euy; |
| 0x52uy; 0xbcuy; 0x51uy; 0x4duy; 0x16uy; 0xccuy; 0xf8uy; 0x06uy; |
| 0x81uy; 0x8cuy; 0xe9uy; 0x1auy; 0xb7uy; 0x79uy; 0x37uy; 0x36uy; |
| 0x5auy; 0xf9uy; 0x0buy; 0xbfuy; 0x74uy; 0xa3uy; 0x5buy; 0xe6uy; |
| 0xb4uy; 0x0buy; 0x8euy; 0xeduy; 0xf2uy; 0x78uy; 0x5euy; 0x42uy; |
| 0x87uy; 0x4duy |
| ] |
| |
| unfold let test_key = [ |
| 0uy; 1uy; 2uy; 3uy; 4uy; 5uy; 6uy; 7uy; |
| 8uy; 9uy; 10uy; 11uy; 12uy; 13uy; 14uy; 15uy; |
| 16uy; 17uy; 18uy; 19uy; 20uy; 21uy; 22uy; 23uy; |
| 24uy; 25uy; 26uy; 27uy; 28uy; 29uy; 30uy; 31uy |
| ] |
| unfold let test_nonce = [ |
| 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0x4auy; 0uy; 0uy; 0uy; 0uy |
| ] |
| |
| unfold let test_counter = 1 |
| |
| let test() = |
| assert_norm(List.Tot.length test_plaintext = 114); |
| assert_norm(List.Tot.length test_ciphertext = 114); |
| assert_norm(List.Tot.length test_key = 32); |
| assert_norm(List.Tot.length test_nonce = 12); |
| let test_plaintext = createL test_plaintext in |
| let test_ciphertext = createL test_ciphertext in |
| let test_key = createL test_key in |
| let test_nonce = createL test_nonce in |
| chacha20_encrypt_bytes test_key test_nonce test_counter test_plaintext |
| = test_ciphertext |
