Revision 629fcb5dab3ab88d72d474ac126fe2345502bc97 authored by karthik.bhargavan on 01 April 2020, 17:05:13 UTC, committed by karthik.bhargavan on 01 April 2020, 17:05:13 UTC
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 ...
