summaryrefslogtreecommitdiffstats
path: root/security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst
diff options
context:
space:
mode:
authorwolfbeast <mcwerewolf@gmail.com>2018-04-25 21:33:33 +0200
committerwolfbeast <mcwerewolf@gmail.com>2018-04-25 21:33:33 +0200
commitfba28f19754f62b5227650143d5441fc86d4c7d7 (patch)
tree26629d73f83543ff92a060fd7b310bb748b13173 /security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst
parentb4154e043bfc0d2f301d88304efc896989d650bf (diff)
downloadUXP-fba28f19754f62b5227650143d5441fc86d4c7d7.tar
UXP-fba28f19754f62b5227650143d5441fc86d4c7d7.tar.gz
UXP-fba28f19754f62b5227650143d5441fc86d4c7d7.tar.lz
UXP-fba28f19754f62b5227650143d5441fc86d4c7d7.tar.xz
UXP-fba28f19754f62b5227650143d5441fc86d4c7d7.zip
Revert "Update NSS to 3.35-RTM"
This reverts commit f1a0f0a56fdd0fc39f255174ce08c06b91c66c94.
Diffstat (limited to 'security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst')
-rw-r--r--security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst107
1 files changed, 0 insertions, 107 deletions
diff --git a/security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst b/security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst
deleted file mode 100644
index f9d8a4cb2..000000000
--- a/security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst
+++ /dev/null
@@ -1,107 +0,0 @@
-/* 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.Poly1305
-
-module ST = FStar.HyperStack.ST
-
-open FStar.Math.Lib
-open FStar.Mul
-open FStar.Seq
-open FStar.UInt8
-open FStar.Endianness
-open Spec.Poly1305.Lemmas
-
-#set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
-
-(* Field types and parameters *)
-let prime = pow2 130 - 5
-type elem = e:int{e >= 0 /\ e < prime}
-let fadd (e1:elem) (e2:elem) = (e1 + e2) % prime
-let fmul (e1:elem) (e2:elem) = (e1 * e2) % prime
-let zero : elem = 0
-let one : elem = 1
-let op_Plus_At = fadd
-let op_Star_At = fmul
-(* Type aliases *)
-let op_Amp_Bar = UInt.logand #128
-type word = w:bytes{length w <= 16}
-type word_16 = w:bytes{length w = 16}
-type tag = word_16
-type key = lbytes 32
-type text = seq word
-
-(* Specification code *)
-let encode (w:word) =
- (pow2 (8 * length w)) `fadd` (little_endian w)
-
-let rec poly (txt:text) (r:e:elem) : Tot elem (decreases (length txt)) =
- if length txt = 0 then zero
- else
- let a = poly (Seq.tail txt) r in
- let n = encode (Seq.head txt) in
- (n `fadd` a) `fmul` r
-
-let encode_r (rb:word_16) =
- (little_endian rb) &| 0x0ffffffc0ffffffc0ffffffc0fffffff
-
-let finish (a:elem) (s:word_16) : Tot tag =
- let n = (a + little_endian s) % pow2 128 in
- little_bytes 16ul n
-
-let rec encode_bytes (txt:bytes) : Tot text (decreases (length txt)) =
- if length txt = 0 then createEmpty
- else
- let w, txt = split txt (min (length txt) 16) in
- append_last (encode_bytes txt) w
-
-let poly1305 (msg:bytes) (k:key) : Tot tag =
- let text = encode_bytes msg in
- let r = encode_r (slice k 0 16) in
- let s = slice k 16 32 in
- finish (poly text r) s
-
-
-(* ********************* *)
-(* RFC 7539 Test Vectors *)
-(* ********************* *)
-
-#reset-options "--initial_fuel 0 --max_fuel 0 --z3rlimit 20"
-
-unfold let msg = [
- 0x43uy; 0x72uy; 0x79uy; 0x70uy; 0x74uy; 0x6fuy; 0x67uy; 0x72uy;
- 0x61uy; 0x70uy; 0x68uy; 0x69uy; 0x63uy; 0x20uy; 0x46uy; 0x6fuy;
- 0x72uy; 0x75uy; 0x6duy; 0x20uy; 0x52uy; 0x65uy; 0x73uy; 0x65uy;
- 0x61uy; 0x72uy; 0x63uy; 0x68uy; 0x20uy; 0x47uy; 0x72uy; 0x6fuy;
- 0x75uy; 0x70uy ]
-
-unfold let k = [
- 0x85uy; 0xd6uy; 0xbeuy; 0x78uy; 0x57uy; 0x55uy; 0x6duy; 0x33uy;
- 0x7fuy; 0x44uy; 0x52uy; 0xfeuy; 0x42uy; 0xd5uy; 0x06uy; 0xa8uy;
- 0x01uy; 0x03uy; 0x80uy; 0x8auy; 0xfbuy; 0x0duy; 0xb2uy; 0xfduy;
- 0x4auy; 0xbfuy; 0xf6uy; 0xafuy; 0x41uy; 0x49uy; 0xf5uy; 0x1buy ]
-
-unfold let expected = [
- 0xa8uy; 0x06uy; 0x1duy; 0xc1uy; 0x30uy; 0x51uy; 0x36uy; 0xc6uy;
- 0xc2uy; 0x2buy; 0x8buy; 0xafuy; 0x0cuy; 0x01uy; 0x27uy; 0xa9uy ]
-
-let test () : Tot bool =
- assert_norm(List.Tot.length msg = 34);
- assert_norm(List.Tot.length k = 32);
- assert_norm(List.Tot.length expected = 16);
- let msg = createL msg in
- let k = createL k in
- let expected = createL expected in
- poly1305 msg k = expected