Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Spec.Agile.CTR.fst
module Spec.Agile.CTR
open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence
open Spec.Agile.Cipher
#reset-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 1"
// So that clients don't need to open both modules
include Spec.Agile.Cipher
val counter_mode:
a:cipher_alg ->
k:key a ->
n:nonce a ->
plain:bytes { length plain <= max_size_t } ->
Tot (cipher:bytes { length cipher = length plain })
let counter_mode a k n plain =
let stream = ctr_stream a k n (length plain) in
map2 ( ^. ) (plain <: lbytes (length plain)) (stream <: lbytes (length plain))
Computing file changes ...
