diff --git a/.github/workflows/library_rust_tests.yml b/.github/workflows/library_rust_tests.yml index 80de68152..17f77cdc0 100644 --- a/.github/workflows/library_rust_tests.yml +++ b/.github/workflows/library_rust_tests.yml @@ -202,9 +202,9 @@ jobs: unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0 - name: Test Rust - working-directory: ${{ matrix.library }} + working-directory: ${{ matrix.library }}/runtimes/rust shell: bash run: | # Without this, running test vectors fails due to `fatal runtime error: stack overflow` export RUST_MIN_STACK=104857600 - make test_rust + cargo test --release -- --test-threads 1 --nocapture diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy index d60bad22c..81bfc243f 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy @@ -147,6 +147,27 @@ module MessageBody { && MessageFramesAreForTheSameMessage(regularFrames) } + lemma IsMessageRegularFramesCanBeSplit( + regularFrames: seq + ) + requires IsMessageRegularFrames(regularFrames) + ensures forall accumulator + | accumulator <= regularFrames + :: + && IsMessageRegularFrames(accumulator) + { + forall accumulator + | accumulator <= regularFrames + ensures + && IsMessageRegularFrames(accumulator) + { + assert |accumulator| <= |regularFrames|; + assert 0 <= |accumulator| < ENDFRAME_SEQUENCE_NUMBER as nat; + assume {:axiom} MessageFramesAreMonotonic(accumulator); + assert MessageFramesAreForTheSameMessage(accumulator); + } + } + type NonFramedMessage = Frames.NonFramed datatype FramedMessageBody = FramedMessageBody( @@ -939,7 +960,7 @@ module MessageBody { WriteMessageRegularFrames(body.regularFrames) + Frames.WriteFinalFrame(body.finalFrame) } - function method WriteMessageRegularFrames( + function WriteMessageRegularFrames( frames: MessageRegularFrames ) :(ret: seq) @@ -954,6 +975,28 @@ module MessageBody { WriteMessageRegularFrames(Seq.DropLast(frames)) + Frames.WriteRegularFrame(Seq.Last(frames)) } + by method { // because Seq.DropLast makes a full copy + var result : seq := []; + for i := 0 to |frames| + invariant IsMessageRegularFrames(frames) + invariant IsMessageRegularFrames(frames[..i]) + invariant result == WriteMessageRegularFrames(frames[..i]) + { + result := result + Frames.WriteRegularFrame(frames[i]); + assert result == WriteMessageRegularFrames(frames[..i]) + Frames.WriteRegularFrame(frames[i]); + assert Seq.DropLast(frames[..i+1]) == frames[..i]; + assert result == WriteMessageRegularFrames(Seq.DropLast(frames[..i+1])) + Frames.WriteRegularFrame(Seq.Last(frames[..i+1])); + IsMessageRegularFramesCanBeSplit(frames); + assert IsMessageRegularFrames(frames[..i]); + assert IsMessageRegularFrames(frames[..i+1]); + assert result == WriteMessageRegularFrames(frames[..i+1]); + + } + assert result == WriteMessageRegularFrames(frames[..|frames|]); + assert frames == frames[..|frames|]; + assert result == WriteMessageRegularFrames(frames); + return result; + } function method {:recursive} {:vcs_split_on_every_assert} ReadFramedMessageBody( buffer: ReadableBuffer, diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy index cba5fc977..f7ce40874 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy @@ -22,6 +22,8 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys { + WriteShortLengthSeq(edk.ciphertext) } + // Seq.DropLast makes a full copy, but we seldom have more than one or two data keys, + // so no point in optimizing away the copy. function {:tailrecursion} WriteEncryptedDataKeys( edks: ESDKEncryptedDataKeys ): diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptionContext.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptionContext.dfy index 5d54b3c7d..3dfd4b600 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptionContext.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptionContext.dfy @@ -387,7 +387,7 @@ module {:options "/functionSyntax:4" } EncryptionContext { WriteUint16(|ec| as uint16) + WriteAADPairs(ec) } - function {:tailrecursion} WriteAADPairs( + function WriteAADPairs( ec: ESDKCanonicalEncryptionContext ): (ret: seq) @@ -406,6 +406,28 @@ module {:options "/functionSyntax:4" } EncryptionContext { assert LinearLength(Seq.DropLast(ec)) < LinearLength(ec); WriteAADPairs(Seq.DropLast(ec)) + WriteAADPair(Seq.Last(ec)) } + by method { // because Seq.DropLast makes a full copy + var result : seq := []; + for i := 0 to |ec| + invariant ESDKCanonicalEncryptionContext?(ec) + invariant ESDKCanonicalEncryptionContext?(ec[..i]) + invariant result == WriteAADPairs(ec[..i]) + { + result := result + WriteAADPair(ec[i]); + ESDKCanonicalEncryptionContextCanBeSplit(ec); + assert result == WriteAADPairs(ec[..i]) + WriteAADPair(ec[i]); + assert Seq.DropLast(ec[..i+1]) == ec[..i]; + assert result == WriteAADPairs(Seq.DropLast(ec[..i+1])) + WriteAADPair(Seq.Last(ec[..i+1])); + assert ESDKCanonicalEncryptionContext?(ec[..i]); + assert ESDKCanonicalEncryptionContext?(ec[..i+1]); + assert result == WriteAADPairs(ec[..i+1]); + + } + assert result == WriteAADPairs(ec[..|ec|]); + assert ec == ec[..|ec|]; + assert result == WriteAADPairs(ec); + return result; + } //= compliance/data-format/message-header.txt#2.5.1.7.2.2 //# The following table describes the fields that form each key value diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy index 39fb4413b..9660d947f 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy @@ -149,7 +149,7 @@ module SerializableTypes { ==> pairs[i].key != pairs[j].key) } - function method {:tailrecursion} LinearLength( + function LinearLength( pairs: Linear ): (ret: nat) @@ -162,6 +162,24 @@ module SerializableTypes { else LinearLength(Seq.DropLast(pairs)) + PairLength(Seq.Last(pairs)) } + by method { // because Seq.DropLast makes a full copy + var result : nat := 0; + for i := 0 to |pairs| + invariant result == LinearLength(pairs[..i]) + { + result := result + PairLength(pairs[i]); + assert result == LinearLength(pairs[..i]) + PairLength(pairs[i]); + assert Seq.DropLast(pairs[..i+1]) == pairs[..i]; + assert result == LinearLength(Seq.DropLast(pairs[..i+1])) + PairLength(Seq.Last(pairs[..i+1])); + assert result == LinearLength(pairs[..i+1]); + + } + assert result == LinearLength(pairs[..|pairs|]); + assert pairs == pairs[..|pairs|]; + assert result == LinearLength(pairs); + return result; + } + function method PairLength( pair: Pair diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go index 2be2a1ce7..705de566c 100644 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go @@ -159,14 +159,14 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -182,14 +182,14 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input func Aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -231,14 +231,14 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input func Aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -288,14 +288,14 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(input *int6 func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go index 6247c1cdc..69db81e75 100644 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -157,18 +157,15 @@ func NetV4_0_0_RetryPolicy_FromDafny(input interface{}) awscryptographyencryptio func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -188,18 +185,15 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(inp } func Aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -237,18 +231,15 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(inp } func Aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -299,18 +290,15 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(input int } func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go index 2be2a1ce7..705de566c 100644 --- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go @@ -159,14 +159,14 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -182,14 +182,14 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input func Aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -231,14 +231,14 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input func Aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -288,14 +288,14 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(input *int6 func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go index 6247c1cdc..69db81e75 100644 --- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -157,18 +157,15 @@ func NetV4_0_0_RetryPolicy_FromDafny(input interface{}) awscryptographyencryptio func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -188,18 +185,15 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(inp } func Aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -237,18 +231,15 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(inp } func Aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -299,18 +290,15 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(input int } func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { diff --git a/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy b/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy index a1cb26331..f0dfa06db 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy @@ -7,18 +7,37 @@ module {:options "-functionSyntax:4"} EsdkManifestOptions { import opened Wrappers import Types = AwsCryptographyEncryptionSdkTypes + datatype PerfReport = + | ReportNone + | ReportIndividual + | ReportFinal + | ReportAll + | ReportLoop(count : nat) + + predicate DoReportFinal(r : PerfReport) + { + r.ReportFinal? || r.ReportAll? + } + + predicate DoReportIndividual(r : PerfReport) + { + r.ReportIndividual? || r.ReportAll? + } + datatype ManifestOptions = | Decrypt( nameonly manifestPath: string, nameonly manifestFileName: string, nameonly retryPolicy: Types.NetV4_0_0_RetryPolicy, - nameonly testName: Option := None + nameonly testName: Option := None, + nameonly report: PerfReport := ReportNone ) | Encrypt( nameonly manifestPath: string, nameonly manifest: string, nameonly decryptManifestOutput: string, nameonly testName: Option := None, + nameonly report: PerfReport := ReportNone, nameonly legacyOutput: int := 5 ) | DecryptSingle( diff --git a/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy b/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy index 50b1bd081..9d46aa646 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy @@ -28,6 +28,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { import EsdkManifestOptions import opened EsdkTestVectors import WriteVectors + import Time method StartDecryptVectors( op: EsdkManifestOptions.ManifestOptions @@ -49,7 +50,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { decryptManifest.jsonTests ); - output := TestDecrypts(decryptManifest.keys, decryptVectors); + output := TestDecrypts(decryptManifest.keys, decryptVectors, op.report); } predicate TestDecryptVector?(v: EsdkDecryptTestVector) @@ -59,7 +60,8 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { method TestDecrypts( keys: KeyVectors.KeyVectorsClient, - vectors: seq + vectors: seq, + report: EsdkManifestOptions.PerfReport ) returns (manifest: Result, string>) requires keys.ValidState() @@ -70,12 +72,18 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { var hasFailure := false; var skipped := 0; + var time := Time.GetAbsoluteTime(); for i := 0 to |vectors| { var vector := vectors[i]; if TestDecryptVector?(vector) { - var pass := EsdkTestVectors.TestDecrypt(keys, vector); + var itime := Time.GetAbsoluteTime(); + var pass := EsdkTestVectors.TestDecrypt(keys, vector, report); + if EsdkManifestOptions.DoReportIndividual(report) { + var elapsed := Time.TimeSince(itime); + Time.PrintTimeLong(elapsed, "Decrypt " + vector.id, Some(LogFileName())); + } if !pass { hasFailure := true; } @@ -83,8 +91,12 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { skipped := skipped + 1; print "\nSKIP===> ", vector.id, "\n"; } - } + if EsdkManifestOptions.DoReportFinal(report) { + var elapsed := Time.TimeSince(time); + Time.PrintTimeLong(elapsed, "TestDecrypts ESDK", Some(LogFileName())); + } + print "\n=================== Completed ", |vectors|, " Decrypt Tests =================== \n\n"; if 0 < skipped { @@ -94,6 +106,15 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { manifest := if !hasFailure then Success([]) else Failure("Test Vectors failed, see errors above.\n"); } + method GetRandom(n : mplTypes.PositiveInteger) returns (out : seq) + { + var p :- expect AtomicPrimitives.AtomicPrimitives(); + out :- expect p.GenerateRandomBytes( + AtomicPrimitives.Types.GenerateRandomBytesInput( + length := n + )); + } + method {:vcs_split_on_every_assert} StartEncryptVectors( op: EsdkManifestOptions.ManifestOptions ) @@ -111,15 +132,11 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { encryptManifest.jsonTests ); - var p :- expect AtomicPrimitives.AtomicPrimitives(); var plaintext := map[]; for i := 0 to |encryptManifest.plaintext| { var (name, length) := encryptManifest.plaintext[i]; - var data :- expect p.GenerateRandomBytes( - AtomicPrimitives.Types.GenerateRandomBytesInput( - length := length - )); + var data := GetRandom(length); // Write the plaintext to disk. print op.decryptManifestOutput + plaintextPathRoot + name, "\n\n"; var _ :- WriteVectorsFile(op.decryptManifestOutput + plaintextPathRoot + name, data); @@ -128,7 +145,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { var encryptTests? := ToEncryptTests(encryptManifest.keys, encryptVectors); var encryptTests :- encryptTests?.MapFailure((e: KeyVectorsTypes.Error) => var _ := MplVectorPrintErr(e); "Cmm failure"); - var decryptVectors :- TestEncrypts(plaintext, encryptManifest.keys, encryptTests); + var decryptVectors :- TestEncrypts(plaintext, encryptManifest.keys, encryptTests, op.report); var _ :- WriteVectors.WriteDecryptManifest(op, encryptManifest.keys, decryptVectors); @@ -167,7 +184,8 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { method TestEncrypts( plaintexts: map>, keys: KeyVectors.KeyVectorsClient, - tests: seq + tests: seq, + report: EsdkManifestOptions.PerfReport ) returns (manifest: Result, string>) requires keys.ValidState() @@ -183,6 +201,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { var hasFailure := false; var decryptVectors := []; var skipped := []; + var time := Time.GetAbsoluteTime(); for i := 0 to |tests| invariant forall t <- tests :: @@ -199,7 +218,13 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { && test.vector.algorithmSuiteId.value.id.ESDK?, "Vector is using an algorithm suite other than ESDK" ); - var pass :- EsdkTestVectors.TestEncrypt(plaintexts, keys, test); + var itime := Time.GetAbsoluteTime(); + var pass :- EsdkTestVectors.TestEncrypt(plaintexts, keys, test, report); + if EsdkManifestOptions.DoReportIndividual(report) { + var elapsed := Time.TimeSince(itime); + Time.PrintTimeLong(elapsed, "Encrypt " + test.vector.id.UnwrapOr("unknown"), Some(LogFileName())); + } + if !pass.output { hasFailure := true; } else if pass.vector.Some? { @@ -210,6 +235,10 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { print "\nSKIP===> ", test.vector.id.value, "\n"; } } + if EsdkManifestOptions.DoReportFinal(report) { + var elapsed := Time.TimeSince(time); + Time.PrintTimeLong(elapsed, "TestEncrypts ESDK", Some(LogFileName())); + } print "\n=================== Completed ", |tests|, " Encrypt Tests =================== \n\n"; expect !hasFailure; diff --git a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy b/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy index 5496291de..ec4333bad 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy @@ -20,6 +20,18 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes import TestVectors import AllAlgorithmSuites + import EsdkManifestOptions + import Time + import OsLang + import StandardLibrary.String + + function LogFileName() : string + { + if OsLang.GetLanguageShort() == "Dotnet" then + "PerfLog.txt" + else + "../../PerfLog.txt" + } datatype EncryptTest = EncryptTest( cmm: mplTypes.ICryptographicMaterialsManager, @@ -192,20 +204,14 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { method {:vcs_split_on_every_assert} TestDecrypt( keys: KeyVectors.KeyVectorsClient, - vector: EsdkDecryptTestVector + vector: EsdkDecryptTestVector, + report: EsdkManifestOptions.PerfReport ) returns (output: bool) requires keys.ValidState() modifies keys.Modifies ensures keys.ValidState() { - if vector.algorithmSuiteId.Some? { - var id := AllAlgorithmSuites.ToHex(vector.algorithmSuiteId.value); - print "\nTEST-DECRYPT===> ", vector.id, "\n", id, " ", vector.description, "\n"; - } else { - print "\nTEST-DECRYPT===> ", vector.id, "\n", vector.description, "\n"; - } - // The decrypt test vectors also test initialization // This is because they were developed when the MPL // was still part of the ESDK @@ -213,6 +219,12 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { if test?.Failure? { print test?.error, "\n", "\nFAILED! <-----------\n"; + if vector.algorithmSuiteId.Some? { + var id := AllAlgorithmSuites.ToHex(vector.algorithmSuiteId.value); + print "\nTEST-DECRYPT===> ", vector.id, "\n", id, " ", vector.description, "\n\n"; + } else { + print "\nTEST-DECRYPT===> ", vector.id, "\n", vector.description, "\n\n"; + } return false; } @@ -234,6 +246,26 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { keyring := None ); + if report.ReportLoop? { + var pos := test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1OrV2DecryptTestVector? || test.vector.PositiveV4DecryptTestVector?; + var time := Time.GetAbsoluteTime(); + var total := report.count; + for i := 0 to report.count { + var result := test.client.Decrypt(input); + if pos && result.Failure? { + print "Aborting ReportLoop for ", test.vector.id, " because it was a positive test and it failed with ", result.error, "\n"; + total := i; + break; + } else if !pos && result.Success? { + print "Aborting ReportLoop for ", test.vector.id, " because it was a negative test and it succeeded\n"; + total := i; + break; + } + } + var elapsed := Time.TimeSince(time); + Time.PrintTimeLong(elapsed, "Decrypt(" + String.Base10Int2String(total) + ") " + test.vector.id, Some(LogFileName())); + } + var result := test.client.Decrypt(input); output := match test.vector @@ -331,7 +363,8 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { method {:vcs_split_on_every_assert} TestEncrypt( plaintexts: map>, keys: KeyVectors.KeyVectorsClient, - test: EncryptTest + test: EncryptTest, + report: EsdkManifestOptions.PerfReport ) returns (output: Result) requires keys.ValidState() && test.ValidState() @@ -344,9 +377,6 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { requires test.vector.algorithmSuiteId.Some? && test.vector.algorithmSuiteId.value.id.ESDK? requires test.vector.id.Some? { - var id := AllAlgorithmSuites.ToHex(test.vector.algorithmSuiteId.value); - print "\nTEST-ENCRYPT===> ", test.vector.id.value, "\n", id, " ", test.vector.description, "\n"; - // The encrypt test vectors also test initialization // This is because they were developed when the MPL // was still part of the ESDK @@ -364,6 +394,26 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { frameLength := frameLength, algorithmSuiteId := Some(test.vector.algorithmSuiteId.value.id.ESDK) ); + + if report.ReportLoop? { + var pos := test.vector.PositiveEncryptTestVector? || test.vector.PositiveEncryptNegativeDecryptTestVector?; + var time := Time.GetAbsoluteTime(); + var total := report.count; + for i := 0 to report.count { + var result := test.client.Encrypt(input); + if pos && result.Failure? { + print "Aborting ReportLoop for ", test.vector.id.UnwrapOr("unknown"), " because it was a positive test and it failed with ", result.error, "\n"; + total := i; + break; + } else if !pos && result.Success? { + print "Aborting ReportLoop for ", test.vector.id.UnwrapOr("unknown"), " because it was a negative test and it succeeded\n"; + total := i; + break; + } + } + var elapsed := Time.TimeSince(time); + Time.PrintTimeLong(elapsed, "Encrypt(" + String.Base10Int2String(total) + ") " + test.vector.id.UnwrapOr("unknown"), Some(LogFileName())); + } var result := test.client.Encrypt(input); if @@ -386,6 +436,8 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { print result.error; } print "\nFAILED! <-----------\n"; + var id := AllAlgorithmSuites.ToHex(test.vector.algorithmSuiteId.value); + print "\nTEST-ENCRYPT===> ", test.vector.id.value, "\n", id, " ", test.vector.description, "\n\n"; } } diff --git a/TestVectors/dafny/TestVectors/src/Index.dfy b/TestVectors/dafny/TestVectors/src/Index.dfy index 933345cb5..9167afc8c 100644 --- a/TestVectors/dafny/TestVectors/src/Index.dfy +++ b/TestVectors/dafny/TestVectors/src/Index.dfy @@ -54,13 +54,13 @@ module {:options "-functionSyntax:4"} WrappedESDKMain { if op?.Success? { var op := op?.value; match op - case Decrypt(_, _, _, _) => + case Decrypt(_, _, _, _, _) => var result := EsdkTestManifests.StartDecryptVectors(op); if result.Failure? { print result.error; } expect result.Success?; - case Encrypt(_, _, _, _, _) => + case Encrypt(_, _, _, _, _, _) => var result := EsdkTestManifests.StartEncryptVectors(op); if result.Failure? { print result.error; diff --git a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy index a73fd0f46..7b156889e 100644 --- a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy +++ b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy @@ -216,10 +216,16 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { var encryptionContextStrings :- SmallObjectToStringStringMap(encryptionContextJsonKey, scenario); var encryptionContext :- utf8EncodeMap(encryptionContextStrings); - var reproducedEncryptionContextString :- SmallObjectToStringStringMap(reproducedEncryptionContextJsonKey, scenario); - var reproducedEncryptionContext :- utf8EncodeMap(reproducedEncryptionContextString); + var reproducedEncryptionContextString := SmallObjectToStringStringMap(reproducedEncryptionContextJsonKey, scenario); var description :- GetString("description", scenario); + // If no reproducedEncryptionContext, default to regular encryptionContext + var reproducedEncryptionContext :- + if reproducedEncryptionContextString.Success? then + utf8EncodeMap(reproducedEncryptionContextString.value) + else + Success(encryptionContext); + match typ case "positive-esdk" => var encryptKeyDescription :- ParseJsonManifests.GetKeyDescription(keys, encryptKeyDescription, scenario); diff --git a/TestVectors/dafny/TestVectors/test/RunMain.dfy b/TestVectors/dafny/TestVectors/test/RunMain.dfy index 48492e6d6..2672b4308 100644 --- a/TestVectors/dafny/TestVectors/test/RunMain.dfy +++ b/TestVectors/dafny/TestVectors/test/RunMain.dfy @@ -14,12 +14,35 @@ module {:extern} TestWrappedESDKMain { import WriteVectors import opened Wrappers import Types = AwsCryptographyEncryptionSdkTypes - + import WrappedESDK + import opened StandardLibrary.UInt + import Time + import MPL = AwsCryptographyMaterialProvidersTypes + import MaterialProviders + import OsLang + import FileIO // Test execution directory is different for different runtimes. // Runtime should define an extern to return the expected test execution directory. method {:extern} GetTestVectorExecutionDirectory() returns (res: string) + method GetDirPrefix() returns (res: string) + { + if OsLang.GetLanguageShort() == "Java" { + res := "../../"; + } else { + res := GetTestVectorExecutionDirectory(); + } + } + + function method AllowRetry() : Types.NetV4_0_0_RetryPolicy + { + if OsLang.GetLanguageShort() == "Java" then + Types.NetV4_0_0_RetryPolicy.FORBID_RETRY + else + Types.NetV4_0_0_RetryPolicy.ALLOW_RETRY + } + method {:test} RunManifestTests() { TestGenerateEncryptManifest(5); TestEncryptManifest(5); @@ -36,7 +59,7 @@ module {:extern} TestWrappedESDKMain { // These messages are expected to successfully decrypt without // having to retry. method {:test} TestNetRetryFlagVectorsExpectSuccess() { - var directory := GetTestVectorExecutionDirectory(); + var directory := GetDirPrefix(); var result := EsdkTestManifests.StartDecryptVectors( EsdkManifestOptions.Decrypt( manifestPath := directory + "dafny/TestVectors/test/valid-Net-4.0.0/", @@ -50,6 +73,65 @@ module {:extern} TestWrappedESDKMain { expect result.Success?; } + method {:test} TestPerfManifest() { + var directory := GetDirPrefix(); + var result := EsdkTestManifests.StartEncryptVectors( + EsdkManifestOptions.Encrypt( + manifestPath := directory + "dafny/TestVectors/test/", + manifest := "perf-encrypt-manifest.json", + decryptManifestOutput := directory + "dafny/TestVectors/test/perf/", + report := EsdkManifestOptions.ReportAll + ) + ); + if result.Failure? { + print "\nTestPerfManifest Encrypt Failure\n", result.error, "\n"; + } + expect result.Success?; + + var result2 := EsdkTestManifests.StartDecryptVectors( + EsdkManifestOptions.Decrypt( + manifestPath := directory + "dafny/TestVectors/test/perf/", + manifestFileName := "manifest.json", + retryPolicy := AllowRetry(), + report := EsdkManifestOptions.ReportAll + ) + ); + if result2.Failure? { + print "\nTestPerfManifest Decrypt Failure\n", result2.error, "\n"; + } + expect result2.Success?; + } + + method {:test} TestThousandManifest() { + var directory := GetDirPrefix(); + var result := EsdkTestManifests.StartEncryptVectors( + EsdkManifestOptions.Encrypt( + manifestPath := directory + "dafny/TestVectors/test/", + manifest := "thousand-encrypt-manifest.json", + decryptManifestOutput := directory + "dafny/TestVectors/test/thousand/", + report := EsdkManifestOptions.ReportLoop(10000) + ) + ); + if result.Failure? { + print "\nTestThousandManifest Encrypt Failure\n", result.error, "\n"; + } + expect result.Success?; + + var result2 := EsdkTestManifests.StartDecryptVectors( + EsdkManifestOptions.Decrypt( + manifestPath := directory + "dafny/TestVectors/test/thousand/", + manifestFileName := "manifest.json", + retryPolicy := AllowRetry(), + report := EsdkManifestOptions.ReportLoop(10000) + ) + ); + if result2.Failure? { + print "\nTestThousandManifest Decrypt Failure\n", result2.error, "\n"; + } + expect result2.Success?; + } + + // Read encrypt manifests for invalid ESDK .NET v4.0.0 messages // These messages are expected to fail if retry option is set to FORBID_RETRY // As of 12-7-2024, I can't think of an easy way to reuse all the test vector framework @@ -57,7 +139,7 @@ module {:extern} TestWrappedESDKMain { // The errors that we get back from the MPL are opaque errors, not opaque with text... // This means that in dafny code we cannot check the error message :( method {:test} TestNetInvalidTestVectorsExpectFailure() { - var directory := GetTestVectorExecutionDirectory(); + var directory := GetDirPrefix(); var result := EsdkTestManifests.StartDecryptVectors( EsdkManifestOptions.Decrypt( manifestPath := directory + "dafny/TestVectors/test/invalid-Net-4.0.0/", @@ -72,12 +154,16 @@ module {:extern} TestWrappedESDKMain { } method {:test} TestNetInvalidTestVectorsExpectSuccessOnRetry() { - var directory := GetTestVectorExecutionDirectory(); + // we can't retry in Java + if OsLang.GetLanguageShort() == "Java" { + return; + } + var directory := GetDirPrefix(); var result := EsdkTestManifests.StartDecryptVectors( EsdkManifestOptions.Decrypt( manifestPath := directory + "dafny/TestVectors/test/invalid-Net-4.0.0/", manifestFileName := "manifest.json", - retryPolicy := Types.NetV4_0_0_RetryPolicy.ALLOW_RETRY + retryPolicy := AllowRetry() ) ); if result.Failure? { @@ -87,7 +173,7 @@ module {:extern} TestWrappedESDKMain { } method {:test} TestNet401ValidTestVectorsExpectSuccess() { - var directory := GetTestVectorExecutionDirectory(); + var directory := GetDirPrefix(); var result := EsdkTestManifests.StartDecryptVectors( EsdkManifestOptions.Decrypt( manifestPath := directory + "dafny/TestVectors/test/v4-Net-4.0.1/", @@ -102,7 +188,7 @@ module {:extern} TestWrappedESDKMain { } method TestGenerateEncryptManifest(version: nat) { - var directory := GetTestVectorExecutionDirectory(); + var directory := GetDirPrefix(); var result := WriteVectors.WriteTestVectors( EsdkManifestOptions.EncryptManifest( encryptManifestOutput := directory + "dafny/TestVectors/test/", @@ -115,12 +201,13 @@ module {:extern} TestWrappedESDKMain { } method TestEncryptManifest(version: int) { - var directory := GetTestVectorExecutionDirectory(); + var directory := GetDirPrefix(); var result := EsdkTestManifests.StartEncryptVectors( EsdkManifestOptions.Encrypt( manifestPath := directory + "dafny/TestVectors/test/", manifest := "encrypt-manifest.json", decryptManifestOutput := directory + "dafny/TestVectors/test/", + report := EsdkManifestOptions.ReportFinal, legacyOutput := version ) ); @@ -132,12 +219,13 @@ module {:extern} TestWrappedESDKMain { method TestDecryptManifest() { - var directory := GetTestVectorExecutionDirectory(); + var directory := GetDirPrefix(); var result := EsdkTestManifests.StartDecryptVectors( EsdkManifestOptions.Decrypt( manifestPath := directory + "dafny/TestVectors/test/", manifestFileName := "manifest.json", - retryPolicy := Types.NetV4_0_0_RetryPolicy.FORBID_RETRY + retryPolicy := Types.NetV4_0_0_RetryPolicy.FORBID_RETRY, + report := EsdkManifestOptions.ReportFinal ) ); diff --git a/TestVectors/dafny/TestVectors/test/perf-encrypt-manifest.json b/TestVectors/dafny/TestVectors/test/perf-encrypt-manifest.json new file mode 100644 index 000000000..6bf3f9d56 --- /dev/null +++ b/TestVectors/dafny/TestVectors/test/perf-encrypt-manifest.json @@ -0,0 +1,63 @@ +{ + "manifest": { + "type": "awses-encrypt", + "version": 5 + }, + "client": { + "name": "aws-encryption-sdk-dafny", + "version": "4.1.0" + }, + "keys": "file://keys.json", + "plaintexts": { + "large": 1000000, + "giant": 100000000 + }, + "tests": { + "giant-raw-aes-256": { + "encryption-scenario": { + "type": "positive-esdk", + "plaintext": "giant", + "description": "Generated RawAES aes-256", + "algorithmSuiteId": "0078", + "frame-size": 512, + "encryptKeyDescription": { + "type": "raw", + "key": "aes-256", + "provider-id": "aws-raw-vectors-persistent-aes-256", + "encryption-algorithm": "aes" + }, + "decryptKeyDescription": { + "type": "raw", + "key": "aes-256", + "provider-id": "aws-raw-vectors-persistent-aes-256", + "encryption-algorithm": "aes" + }, + "encryption-context": {}, + "reproduced-encryption-context": {} + } + }, + "giant-raw-aes-256-tiny-frame": { + "encryption-scenario": { + "type": "positive-esdk", + "plaintext": "large", + "description": "Generated RawAES aes-256", + "algorithmSuiteId": "0078", + "frame-size": 4, + "encryptKeyDescription": { + "type": "raw", + "key": "aes-256", + "provider-id": "aws-raw-vectors-persistent-aes-256", + "encryption-algorithm": "aes" + }, + "decryptKeyDescription": { + "type": "raw", + "key": "aes-256", + "provider-id": "aws-raw-vectors-persistent-aes-256", + "encryption-algorithm": "aes" + }, + "encryption-context": {}, + "reproduced-encryption-context": {} + } + } + } +} \ No newline at end of file diff --git a/TestVectors/dafny/TestVectors/test/perf/keys.json b/TestVectors/dafny/TestVectors/test/perf/keys.json new file mode 100644 index 000000000..27ee2cd6a --- /dev/null +++ b/TestVectors/dafny/TestVectors/test/perf/keys.json @@ -0,0 +1,220 @@ +{ + "manifest": { + "type": "keys", + "version": 2 + }, + "keys": { + "no-plaintext-data-key": { + "type": "static-material", + "algorithmSuiteId": "0014", + "encryptionContext": {}, + "encryptedDataKeys": [ + { + "keyProviderId": "static-material-keyring", + "keyProviderInfo": "c3RhdGljLXBsYWludGV4dA==", + "ciphertext": "AQEBAQEBAQEBAQEBAQEBAQ==" + } + ], + "requiredEncryptionContextKeys": [] + }, + "static-plaintext-data-key": { + "type": "static-material", + "algorithmSuiteId": "0014", + "encryptionContext": {}, + "encryptedDataKeys": [ + { + "keyProviderId": "static-material-keyring", + "keyProviderInfo": "c3RhdGljLXBsYWludGV4dA==", + "ciphertext": "AQEBAQEBAQEBAQEBAQEBAQ==" + } + ], + "requiredEncryptionContextKeys": [], + "plaintextDataKey": "AQEBAQEBAQEBAQEBAQEBAQ==" + }, + "static-cashable-plaintext-data-key": { + "type": "static-material", + "algorithmSuiteId": "0478", + "encryptionContext": {}, + "encryptedDataKeys": [ + { + "keyProviderId": "static-material-keyring", + "keyProviderInfo": "c3RhdGljLXBsYWludGV4dA==", + "ciphertext": "AQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQE=" + } + ], + "requiredEncryptionContextKeys": [], + "plaintextDataKey": "AQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQE=" + }, + "static-branch-key-1": { + "type": "static-branch-key", + "encrypt": true, + "decrypt": true, + "key-id": "bd3842ff-3076-4092-9918-4395730050b8", + "branchKeyVersion": "e9ce18a3-edb5-4272-9f86-1cacb7997ff6", + "branchKey": "tJwf65epYvUt5HMiQsl/6jlvLxS0tgdjIuvFy2BLIwg=", + "beaconKey": "RJiXTa/rJf+CLHAVyE652v3uhKreOuYjV+a7SVOugow=" + }, + "aes-128": { + "encrypt": true, + "decrypt": true, + "algorithm": "aes", + "type": "symmetric", + "bits": 128, + "encoding": "base64", + "material": "AAECAwQFBgcICRAREhMUFQ==", + "key-id": "aes-128" + }, + "aes-192": { + "encrypt": true, + "decrypt": true, + "algorithm": "aes", + "type": "symmetric", + "bits": 192, + "encoding": "base64", + "material": "AAECAwQFBgcICRAREhMUFRYXGBkgISIj", + "key-id": "aes-192" + }, + "aes-256": { + "encrypt": true, + "decrypt": true, + "algorithm": "aes", + "type": "symmetric", + "bits": 256, + "encoding": "base64", + "material": "AAECAwQFBgcICRAREhMUFRYXGBkgISIjJCUmJygpMDE=", + "key-id": "aes-256" + }, + "rsa-4096-private": { + "encrypt": true, + "decrypt": true, + "algorithm": "rsa", + "type": "private", + "bits": 4096, + "encoding": "pem", + "material": "-----BEGIN PRIVATE KEY-----\nMIIJQgIBADANBgkqhkiG9w0BAQEFAASCCSwwggkoAgEAAoICAQCztGg1gQ8AjCzz\n1VX6StqtW//jBt2ZQBoApaBa7FmLmdr0YlKaeEKSrItGbvA9tBjgsKhrn8gxTGQc\nuxgM92651jRCbQZyjE6W8kodijhGMXsfKJLfgPp2/I7gZ3dqrSZkejFIYLFb/uF/\nTfAQzNyJUldYdeFojSUPqevMgSAusTgv7dXYt4BCO9mxMp35tgyp5k4vazKJVUgB\nTw87AAYZUGugmi94Wb9JSnqUKI3QzaRN7JADZrHdBO1lIBryfCsjtTnZc7NWZ0yJ\nwmzLY+C5b3y17cy44N0rbjI2QciRhqZ4/9SZ/9ImyFQlB3lr9NSndcT4eE5YC6bH\nba0gOUK9lLXVy6TZ+nRZ4dSddoLX03mpYp+8cQpK6DO3L/PeUY/si0WGsXZfWokd\n4ACwvXWSOjotzjwqwTW8q9udbhUvIHfB02JW+ZQ07b209fBpHRDkZuveOTedTN2Q\nQei4dZDjWW5s4cIIE3dXXeaH8yC02ERIeN+aY6eHngSsP2xoDV3sKNN/yDbCqaMS\nq8ZJbo2rvOFxZHa2nWiV+VLugfO6Xj8jeGeR8vopvbEBZZpAq+Dea2xjY4+XMUQ/\nS1HlRwc9+nkJ5LVfODuE3q9EgJbqbiXe7YckWV3ZqQMybW+dLPxEJs9buOntgHFS\nRYmbKky0bti/ZoZlcZtS0zyjVxlqsQIDAQABAoICAEr3m/GWIXgNAkPGX9PGnmtr\n0dgX6SIhh7d1YOwNZV3DlYAV9HfUa5Fcwc1kQny7QRWbHOepBI7sW2dQ9buTDXIh\nVjPP37yxo6d89EZWfxtpUP+yoXL0D4jL257qCvtJuJZ6E00qaVMDhXbiQKABlo8C\n9sVEiABhwXBDZsctpwtTiykTgv6hrrPy2+H8R8MAm0/VcBCAG9kG5r8FCEmIvQKa\ndgvNxrfiWNZuZ6yfLmpJH54SbhG9Kb4WbCKfvh4ihqyi0btRdSM6fMeLgG9o/zrc\ns54B0kHeLOYNVo0j7FQpZBFeSIbmHfln4RKBh7ntrTke/Ejbh3NbiPvxWSP0P067\nSYWPkQpip2q0ION81wSQZ1haP2GewFFu4IEjG3DlqqpKKGLqXrmjMufnildVFpBx\nir+MgvgQfEBoGEx0aElyO7QuRYaEiXeb/BhMZeC5O65YhJrWSuTVizh3xgJWjgfV\naYwYgxN8SBXBhXLIVvnPhadTqsW1C/aevLOk110eSFWcHf+FCK781ykIzcpXoRGX\nOwWcZzC/fmSABS0yH56ow+I0tjdLIEEMhoa4/kkamioHOJ4yyB+W1DO6/DnMyQlx\ng7y2WsAaIEBoWUARy776k70xPPMtYAxzFXI9KhqRVrPfeaRZ+ojeyLyr3GQGyyoo\ncuGRdMUblsmODv4ixmOxAoIBAQDvkznvVYNdP3Eg5vQeLm/qsP6dLejLijBLeq9i\n7DZH2gRpKcflXZxCkRjsKDDE+fgDcBYEp2zYfRIVvgrxlTQZdaSG+GoDcbjbNQn3\ndjCCtOOACioN/vg2zFlX4Bs6Q+NaV7g5qP5SUaxUBjuHLe7Nc+ZkyheMHuNYVLvk\nHL/IoWyANpZYjMUU3xMbL/J29Gz7CPGr8Si28TihAHGfcNgn8S04OQZhTX+bU805\n/+7B4XW47Mthg/u7hlqFl+YIAaSJYvWkEaVP1A9I7Ve0aMDSMWwzTg9cle2uVaL3\n+PTzWY5coBlHKjqAg9ufhYSDhAqBd/JOSlv8RwcA3PDXJ6C/AoIBAQDABmXXYQky\n7phExXBvkLtJt2TBGjjwulf4R8TC6W5F51jJuoqY/mTqYcLcOn2nYGVwoFvPsy/Q\nCTjfODwJBXzbloXtYFR3PWAeL1Y6+7Cm+koMWIPJyVbD5Fzm+gZStM0GwP8FhDt2\nWt8fWEyXmoLdAy6RAwiEmCagEh8o+13oBfwnBllbz7TxaErsUuR+XVgl/iHwztdv\ncdJKyRgaFfWSh9aiO7EMV2rBGWsoX09SRvprPFAGx8Ffm7YcqIk34QXsQyc45Dyn\nCwkvypxHoaB3ot/48FeFm9IubApb/ctv+EgkBfL4S4bdwRXS1rt+0+QihBoFyP2o\nJ91cdm4hEWCPAoIBAQC6l11hFaYZo0bWDGsHcr2B+dZkzxPoKznQH76n+jeQoLIc\nwgjJkK4afm39yJOrZtEOxGaxu0CgIFFMk9ZsL/wC9EhvQt02z4TdXiLkFK5VrtMd\nr0zv16y06VWQhqBOMf/KJlX6uq9RqADi9HO6pkC+zc0cpPXQEWKaMmygju+kMG2U\nMm/IieMZjWCRJTfgBCE5J88qTsqaKagkZXcZakdAXKwOhQN+F2EStiM6UCZB5PrO\nS8dfrO8ML+ki8Zqck8L1qhiNb5zkXtKExy4u+gNr8khGcT6vqqoSxOoH3mPRgOfL\nJnppne8wlwIf7Vq3H8ka6zPSXEHma999gZcmy9t7AoIBAGbQhiLl79j3a0wXMvZp\nVf5IVYgXFDnAbG2hb7a06bhAAIgyexcjzsC4C2+DWdgOgwHkuoPg+062QV8zauGh\nsJKaa6cHlvIpSJeg3NjD/nfJN3CYzCd0yCIm2Z9Ka6xI5iYhm+pGPNhIG4Na8deS\ngVL46yv1pc/o73VxfoGg5UzgN3xlp97Cva0sHEGguHr4W8Qr59xZw3wGQ4SLW35M\nF6qXVNKUh12GSMCPbZK2RXBWVKqqJmca+WzJoJ6DlsT2lQdFhXCus9L007xlDXxF\nC/hCmw1dEl+VaNo2Ou26W/zdwTKYhNlxBwsg4SB8nPNxXIsmlBBY54froFhriNfn\nx/0CggEAUzz+VMtjoEWw2HSHLOXrO4EmwJniNgiiwfX3DfZE4tMNZgqZwLkq67ns\nT0n3b0XfAOOkLgMZrUoOxPHkxFeyLLf7pAEJe7QNB+Qilw8e2zVqtiJrRk6uDIGJ\nSv+yM52zkImZAe2jOdU3KeUZxSMmb5vIoiPBm+tb2WupAg3YdpKn1/jWTpVmV/+G\nUtTLVE6YpAyFp1gMxhutE9vfIS94ek+vt03AoEOlltt6hqZfv3xmY8vGuAjlnj12\nzHaq+fhCRPsbsZkzJ9nIVdXYnNIEGtMGNnxax7tYRej/UXqyazbxHiJ0iPF4PeDn\ndzxtGxpeTBi+KhKlca8SlCdCqYwG6Q==\n-----END PRIVATE KEY-----", + "key-id": "rsa-4096" + }, + "rsa-4096-public": { + "encrypt": true, + "decrypt": false, + "algorithm": "rsa", + "type": "public", + "bits": 4096, + "encoding": "pem", + "material": "-----BEGIN PUBLIC KEY-----\nMIICIjANBgkqhkiG9w0BAQEFAAOCAg8AMIICCgKCAgEAs7RoNYEPAIws89VV+kra\nrVv/4wbdmUAaAKWgWuxZi5na9GJSmnhCkqyLRm7wPbQY4LCoa5/IMUxkHLsYDPdu\nudY0Qm0GcoxOlvJKHYo4RjF7HyiS34D6dvyO4Gd3aq0mZHoxSGCxW/7hf03wEMzc\niVJXWHXhaI0lD6nrzIEgLrE4L+3V2LeAQjvZsTKd+bYMqeZOL2syiVVIAU8POwAG\nGVBroJoveFm/SUp6lCiN0M2kTeyQA2ax3QTtZSAa8nwrI7U52XOzVmdMicJsy2Pg\nuW98te3MuODdK24yNkHIkYameP/Umf/SJshUJQd5a/TUp3XE+HhOWAumx22tIDlC\nvZS11cuk2fp0WeHUnXaC19N5qWKfvHEKSugzty/z3lGP7ItFhrF2X1qJHeAAsL11\nkjo6Lc48KsE1vKvbnW4VLyB3wdNiVvmUNO29tPXwaR0Q5Gbr3jk3nUzdkEHouHWQ\n41lubOHCCBN3V13mh/MgtNhESHjfmmOnh54ErD9saA1d7CjTf8g2wqmjEqvGSW6N\nq7zhcWR2tp1olflS7oHzul4/I3hnkfL6Kb2xAWWaQKvg3mtsY2OPlzFEP0tR5UcH\nPfp5CeS1Xzg7hN6vRICW6m4l3u2HJFld2akDMm1vnSz8RCbPW7jp7YBxUkWJmypM\ntG7Yv2aGZXGbUtM8o1cZarECAwEAAQ==\n-----END PUBLIC KEY-----", + "key-id": "rsa-4096" + }, + "ecc-256-private":{ + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "ecc-private", + "bits": 256, + "encoding": "pem", + "sender-material": "-----BEGIN PRIVATE KEY-----\nMIGHAgEAMBMGByqGSM49AgEGCCqGSM49AwEHBG0wawIBAQQgw+7YSKEOEAh8/DFZ\n22oSTm/D3jo4nH5tN48IUp0WjyuhRANCAASnUgx7SrlHhPIn3McZfc3cEIs8+XFf\n7JvhcuV1wWELGZ8AjuwnKjE0ielEwSY5HYzWCF773FvJaWGYGYGhSba8\n-----END PRIVATE KEY-----", + "recipient-material": "-----BEGIN PRIVATE KEY-----\nMIGHAgEAMBMGByqGSM49AgEGCCqGSM49AwEHBG0wawIBAQQgYvB/1CVSgfQDrE6A\nDz7pdgxcOb+AHnsaI4LQMY6s8JChRANCAARYxf/AeERu2Z3VtDokplDs/atuGIbW\n7IGhknbK2MP+NV/mbcaxl8Xki9FegBslxCbM66KaoOZR1bCxPpGub2aS\n-----END PRIVATE KEY-----", + "public-key-encoding": "base64-der", + "sender-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAEp1IMe0q5R4TyJ9zHGX3N3BCLPPlxX+yb4XLldcFhCxmfAI7sJyoxNInpRMEmOR2M1ghe+9xbyWlhmBmBoUm2vA==", + "recipient-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAEWMX/wHhEbtmd1bQ6JKZQ7P2rbhiG1uyBoZJ2ytjD/jVf5m3GsZfF5IvRXoAbJcQmzOuimqDmUdWwsT6Rrm9mkg==", + "key-id": "ecc-256" + }, + "ecc-384-private":{ + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "ecc-private", + "bits": 384, + "encoding": "pem", + "sender-material": "-----BEGIN PRIVATE KEY-----\nMIG2AgEAMBAGByqGSM49AgEGBSuBBAAiBIGeMIGbAgEBBDAx0jhFAVQX2zykSLO/\n3VvDDaQJspek3404TtDZupcxi2rThfnxh96u8CYD6XfHikehZANiAAR2W/Cc8slJ\ngYSGi3e+38UUW6dFi1mJBNEZEbJ4vljgEzBo7FecTsCOQH8Zu2nX3eQpuboD8Fb7\nARpqq7rug5jKBMQLUbvridjLBRLuFsfaLpZ07ih4/+VduqQom7D31ik=\n-----END PRIVATE KEY-----", + "recipient-material": "-----BEGIN PRIVATE KEY-----\nMIG2AgEAMBAGByqGSM49AgEGBSuBBAAiBIGeMIGbAgEBBDALwMcT5K2IOUK5Ww5o\nqYrYLzKHuAvFs0VLuKvJOCmWa3NK2WXtUIJ2fPYzp2Y9oTShZANiAATXUn2WMiLB\nbf665ikArOEAOFgruhqAwlxy58BP42nodBZFFf4L7cy7vPLpasp3fFroN57tYfjy\nXL5Wc0vb+xJaTZLBTU/tRGvtjHH0hQgMib2ch6akUJAT6zuMgNNdd7A=\n-----END PRIVATE KEY-----", + "public-key-encoding": "base64-der", + "sender-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEdlvwnPLJSYGEhot3vt/FFFunRYtZiQTRGRGyeL5Y4BMwaOxXnE7AjkB/Gbtp193kKbm6A/BW+wEaaqu67oOYygTEC1G764nYywUS7hbH2i6WdO4oeP/lXbqkKJuw99Yp", + "recipient-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAE11J9ljIiwW3+uuYpAKzhADhYK7oagMJccufAT+Np6HQWRRX+C+3Mu7zy6WrKd3xa6Dee7WH48ly+VnNL2/sSWk2SwU1P7URr7Yxx9IUIDIm9nIempFCQE+s7jIDTXXew", + "key-id": "ecc-384" + }, + "ecc-521-private":{ + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "ecc-private", + "bits": 521, + "encoding": "pem", + "sender-material": "-----BEGIN PRIVATE KEY-----\nMIHuAgEAMBAGByqGSM49AgEGBSuBBAAjBIHWMIHTAgEBBEIANn8j3pIu1wiwkz7z\niPKuqj2MEVWKe/UW/8NEtvD9tKQmMlAzwY/QN93k+0TNlXpvJTUvjI2NZDKNoQ2b\n0B44YfyhgYkDgYYABAHfgnF9LoYBRWwXKKEFQa+Xfg+ztDRdTVTqNZ8roUYmNvLL\nLz2F8oEOhDbMJZ5r1B1C9w5uJqeF6tE8a3yzm47R/wAs0k6dY3wfDKD013Wnn+6e\nNw1mtrvTi6+Pej/ukYOuCjCwm8B0AvxBzdHk8Q/nCcspO9pIsRl/I4qNz4tPaGjJ\nTA==\n-----END PRIVATE KEY-----", + "recipient-material": "-----BEGIN PRIVATE KEY-----\nMIHuAgEAMBAGByqGSM49AgEGBSuBBAAjBIHWMIHTAgEBBEIBjhdIxb49QXi4OsOH\n5PNWnp/KePiuICqC+fxJJ6ceUgPr5SMlLxhHcfHSVZBCkGLP0Rjd1D9gi7Va1oxe\nIHmWRu2hgYkDgYYABAAmg0dilFc6FiO9OE8t1el92KdPo9WYu1hXYnjGYT7OuGj3\nbD9lr0KMNCm3wTPCiLjPb4Iqnk+g0SgrsQ4NvU7nygFBlgz8xXLzIXPqVICthcHX\nRWRB8HnXmyzeF0iCs12F/6vYn/uZfxp3IV/KCR4LwSzbiFzxsV9GYoCoUE30LDVb\nXg==\n-----END PRIVATE KEY-----", + "public-key-encoding": "base64-der", + "sender-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQB34JxfS6GAUVsFyihBUGvl34Ps7Q0XU1U6jWfK6FGJjbyyy89hfKBDoQ2zCWea9QdQvcObianherRPGt8s5uO0f8ALNJOnWN8Hwyg9Nd1p5/unjcNZra704uvj3o/7pGDrgowsJvAdAL8Qc3R5PEP5wnLKTvaSLEZfyOKjc+LT2hoyUw=", + "recipient-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQAJoNHYpRXOhYjvThPLdXpfdinT6PVmLtYV2J4xmE+zrho92w/Za9CjDQpt8Ezwoi4z2+CKp5PoNEoK7EODb1O58oBQZYM/MVy8yFz6lSArYXB10VkQfB515ss3hdIgrNdhf+r2J/7mX8adyFfygkeC8Es24hc8bFfRmKAqFBN9Cw1W14=", + "key-id": "ecc-521" + }, + "us-west-2-decryptable": { + "encrypt": true, + "decrypt": true, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f" + }, + "us-west-2-encrypt-only": { + "encrypt": true, + "decrypt": false, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-west-2:658956600833:key/590fd781-ddde-4036-abec-3e1ab5a5d2ad" + }, + "us-west-2-mrk": { + "encrypt": true, + "decrypt": true, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-west-2:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7" + }, + "us-east-1-mrk": { + "encrypt": true, + "decrypt": true, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-east-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7" + }, + "us-west-2-rsa-mrk": { + "encrypt": true, + "decrypt": true, + "algorithm": "rsa", + "type": "aws-kms-rsa", + "key-id": "arn:aws:kms:us-west-2:370957321024:key/mrk-63d386cb70614ea59b32ad65c9315297", + "bits": 2048, + "encoding": "pem", + "material": "-----BEGIN PUBLIC KEY-----\nMIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEA27Uc/fBaMVhxCE/SpCMQ\noSBRSzQJw+o2hBaA+FiPGtiJ/aPy7sn18aCkelaSj4kwoC79b/arNHlkjc7OJFsN\n/GoFKgNvaiY4lOeJqEiWQGSSgHtsJLdbO2u4OOSxh8qIRAMKbMgQDVX4FR/PLKeK\nfc2aCDvcNSpAM++8NlNmv7+xQBJydr5ce91eISbHkFRkK3/bAM+1iddupoRw4Wo2\nr3avzrg5xBHmzR7u1FTab22Op3Hgb2dBLZH43wNKAceVwKqKA8UNAxashFON7xK9\nyy4kfOL0Z/nhxRKe4jRZ/5v508qIzgzCksYy7Y3QbMejAtiYnr7s5/d5KWw0swou\ntwIDAQAB\n-----END PUBLIC KEY-----" + }, + "us-west-2-256-ecc": { + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "aws-kms-ecdh", + "sender-material": "arn:aws:kms:us-west-2:370957321024:key/eabdf483-6be2-4d2d-8ee4-8c2583d416e9", + "recipient-material": "arn:aws:kms:us-west-2:370957321024:key/0265c8e9-5b6a-4055-8f70-63719e09fda5", + "encoding": "base64-der", + "sender-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE18m54QsLUnhWU7gT8hkAceNbZ/WBGNUUSPCeIKqOyX5psiqyC1TXPOJXqKKaVv5Mg91WV9UjpboblOhNU35nRw==", + "recipient-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE9istdPCuX9nF8EmA4tioe/k0TCa2M9VeBW1N9n0sxPA6uPVOfLtE4+KuYxAGT0dYoK6CY93nowUy1yS+R7A+wA==", + "key-id": "ecc-256" + }, + "us-west-2-384-ecc": { + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "aws-kms-ecdh", + "sender-material": "arn:aws:kms:us-west-2:370957321024:key/7f35a704-f4fb-469d-98b1-62a1fa2cc44e", + "recipient-material": "arn:aws:kms:us-west-2:370957321024:key/29f0bef9-1677-4e74-b67e-acefab1295ff", + "encoding": "base64-der", + "sender-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEfQ0OHFvwskFVjQwfqV7jpo62I6uyGY+5SPRZb6CuJ96bVreLZXh485BcPv09O/DWnpTBm8LL+YcfsqM3ECvi2ee3bDGpH6xIdr28uvyG75t5wqBjYYtZQFDf/ydfG9mm", + "recipient-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEWgGNWQ+vEwlMxyMQkSsOAYGfT6IlgEkcanEOSjbeEpEnh8JHEiBHQ6QaROxJ7c3nEkbjbi0m+7ejBEGtkiqaY5Dsv5u1iV4fc/2v1RzPba1ZtudEmM16Eyy9LHswdJ7v", + "key-id": "ecc-384" + }, + "us-west-2-521-ecc": { + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "aws-kms-ecdh", + "sender-material": "arn:aws:kms:us-west-2:370957321024:key/41b502e3-cc9d-442f-bd7b-d67faed0f22e", + "recipient-material": "arn:aws:kms:us-west-2:370957321024:key/c45f1043-53bb-4f37-adc5-4d25d4a84f9d", + "encoding": "base64-der", + "sender-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQAz86qnfp3s0cl+73PQhlUstfdg9EZDA/jtLjBTWYp/1EB7RHNm8q5hMg5kBfjRDUFhbRBMlUV1xBOTgqzoSWj4oAABnQKiXXGGyu6PMN4D9nVMDsOpJ1pWU7rQexWDahBrK+5hx3beFXUpvvFRQrGAt2icUXm18VO6Qwbp0da9jyGDSY=", + "recipient-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQAxLxcjtYfqc4+4oJZY0gGv2Ehu++CnVFea6uwXgEgLifq4eDSSVmQYvU8majsufpBXQwVjnDlQ7pGRw1j6K4FaLAAgYuMrmrwKtx/ZZtkbXzCwrqJY+sfCk8U5m89DX331cdBAhR2uVSPL2d5hp8up5v+EBpNArtdC5lZMx2ZrwKKYuQ=", + "key-id": "ecc-521" + } + } +} diff --git a/TestVectors/dafny/TestVectors/test/thousand-encrypt-manifest.json b/TestVectors/dafny/TestVectors/test/thousand-encrypt-manifest.json new file mode 100644 index 000000000..a88738ab0 --- /dev/null +++ b/TestVectors/dafny/TestVectors/test/thousand-encrypt-manifest.json @@ -0,0 +1,87 @@ +{ + "manifest": { + "type": "awses-encrypt", + "version": 5 + }, + "client": { + "name": "aws-encryption-sdk-dafny", + "version": "4.1.0" + }, + "keys": "file://keys.json", + "plaintexts": { + "small": 1000 + }, + "tests": { + "small-aes-256": { + "encryption-scenario": { + "type": "positive-esdk", + "plaintext": "small", + "description": "Generated RawAES aes-256", + "algorithmSuiteId": "0078", + "frame-size": 512, + "encryptKeyDescription": { + "type": "raw", + "key": "aes-256", + "provider-id": "aws-raw-vectors-persistent-aes-256", + "encryption-algorithm": "aes" + }, + "decryptKeyDescription": { + "type": "raw", + "key": "aes-256", + "provider-id": "aws-raw-vectors-persistent-aes-256", + "encryption-algorithm": "aes" + }, + "encryption-context": {}, + "reproduced-encryption-context": {} + } + }, + "small-aws-kms-hierarchy": { + "encryption-scenario": { + "type": "positive-esdk", + "plaintext": "small", + "description": "Generated Hierarchy KMS static-branch-key-1", + "algorithmSuiteId": "0478", + "frame-size": 512, + "encryptKeyDescription": { + "type": "aws-kms-hierarchy", + "key": "static-branch-key-1" + }, + "decryptKeyDescription": { + "type": "aws-kms-hierarchy", + "key": "static-branch-key-1" + }, + "encryption-context": {}, + "reproduced-encryption-context": {} + } + }, + "small-hierarchy-large-ec": { + "encryption-scenario": { + "type": "positive-esdk", + "plaintext": "small", + "description": "Generated Hierarchy KMS static-branch-key-1", + "algorithmSuiteId": "0478", + "frame-size": 512, + "encryptKeyDescription": { + "type": "aws-kms-hierarchy", + "key": "static-branch-key-1" + }, + "decryptKeyDescription": { + "type": "aws-kms-hierarchy", + "key": "static-branch-key-1" + }, + "encryption-context": { + "AabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "BabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "CabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "DabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "EabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "FabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "GabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "HabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "IabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ", + "JabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ": "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ" + } + } + } + } +} diff --git a/TestVectors/dafny/TestVectors/test/thousand/keys.json b/TestVectors/dafny/TestVectors/test/thousand/keys.json new file mode 100644 index 000000000..31ede7eb2 --- /dev/null +++ b/TestVectors/dafny/TestVectors/test/thousand/keys.json @@ -0,0 +1,230 @@ +{ + "manifest": { + "type": "keys", + "version": 2 + }, + "keys": { + "no-plaintext-data-key": { + "type": "static-material", + "algorithmSuiteId": "0014", + "encryptionContext": {}, + "encryptedDataKeys": [ + { + "keyProviderId": "static-material-keyring", + "keyProviderInfo": "c3RhdGljLXBsYWludGV4dA==", + "ciphertext": "AQEBAQEBAQEBAQEBAQEBAQ==" + } + ], + "requiredEncryptionContextKeys": [] + }, + "static-plaintext-data-key": { + "type": "static-material", + "algorithmSuiteId": "0014", + "encryptionContext": {}, + "encryptedDataKeys": [ + { + "keyProviderId": "static-material-keyring", + "keyProviderInfo": "c3RhdGljLXBsYWludGV4dA==", + "ciphertext": "AQEBAQEBAQEBAQEBAQEBAQ==" + } + ], + "requiredEncryptionContextKeys": [], + "plaintextDataKey": "AQEBAQEBAQEBAQEBAQEBAQ==" + }, + "static-cashable-plaintext-data-key": { + "type": "static-material", + "algorithmSuiteId": "0478", + "encryptionContext": {}, + "encryptedDataKeys": [ + { + "keyProviderId": "static-material-keyring", + "keyProviderInfo": "c3RhdGljLXBsYWludGV4dA==", + "ciphertext": "AQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQE=" + } + ], + "requiredEncryptionContextKeys": [], + "plaintextDataKey": "AQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQE=" + }, + "static-branch-key-1": { + "type": "static-branch-key", + "encrypt": true, + "decrypt": true, + "key-id": "bd3842ff-3076-4092-9918-4395730050b8", + "branchKeyVersion": "e9ce18a3-edb5-4272-9f86-1cacb7997ff6", + "branchKey": "tJwf65epYvUt5HMiQsl/6jlvLxS0tgdjIuvFy2BLIwg=", + "beaconKey": "RJiXTa/rJf+CLHAVyE652v3uhKreOuYjV+a7SVOugow=" + }, + "aes-128": { + "encrypt": true, + "decrypt": true, + "algorithm": "aes", + "type": "symmetric", + "bits": 128, + "encoding": "base64", + "material": "AAECAwQFBgcICRAREhMUFQ==", + "key-id": "aes-128" + }, + "aes-192": { + "encrypt": true, + "decrypt": true, + "algorithm": "aes", + "type": "symmetric", + "bits": 192, + "encoding": "base64", + "material": "AAECAwQFBgcICRAREhMUFRYXGBkgISIj", + "key-id": "aes-192" + }, + "aes-256": { + "encrypt": true, + "decrypt": true, + "algorithm": "aes", + "type": "symmetric", + "bits": 256, + "encoding": "base64", + "material": "AAECAwQFBgcICRAREhMUFRYXGBkgISIjJCUmJygpMDE=", + "key-id": "aes-256" + }, + "𝟁-nonascii-𐀂-aes-256-𝟁-with-�": { + "encrypt": true, + "decrypt": true, + "algorithm": "aes", + "type": "symmetric", + "bits": 256, + "encoding": "base64", + "material": "AAECAwQFBgcICRAREhMUFRYXGBkgISIjJCUmJygpMDE=", + "key-id": "aes-256" + }, + "rsa-4096-private": { + "encrypt": true, + "decrypt": true, + "algorithm": "rsa", + "type": "private", + "bits": 4096, + "encoding": "pem", + "material": "-----BEGIN PRIVATE KEY-----\nMIIJQgIBADANBgkqhkiG9w0BAQEFAASCCSwwggkoAgEAAoICAQCztGg1gQ8AjCzz\n1VX6StqtW//jBt2ZQBoApaBa7FmLmdr0YlKaeEKSrItGbvA9tBjgsKhrn8gxTGQc\nuxgM92651jRCbQZyjE6W8kodijhGMXsfKJLfgPp2/I7gZ3dqrSZkejFIYLFb/uF/\nTfAQzNyJUldYdeFojSUPqevMgSAusTgv7dXYt4BCO9mxMp35tgyp5k4vazKJVUgB\nTw87AAYZUGugmi94Wb9JSnqUKI3QzaRN7JADZrHdBO1lIBryfCsjtTnZc7NWZ0yJ\nwmzLY+C5b3y17cy44N0rbjI2QciRhqZ4/9SZ/9ImyFQlB3lr9NSndcT4eE5YC6bH\nba0gOUK9lLXVy6TZ+nRZ4dSddoLX03mpYp+8cQpK6DO3L/PeUY/si0WGsXZfWokd\n4ACwvXWSOjotzjwqwTW8q9udbhUvIHfB02JW+ZQ07b209fBpHRDkZuveOTedTN2Q\nQei4dZDjWW5s4cIIE3dXXeaH8yC02ERIeN+aY6eHngSsP2xoDV3sKNN/yDbCqaMS\nq8ZJbo2rvOFxZHa2nWiV+VLugfO6Xj8jeGeR8vopvbEBZZpAq+Dea2xjY4+XMUQ/\nS1HlRwc9+nkJ5LVfODuE3q9EgJbqbiXe7YckWV3ZqQMybW+dLPxEJs9buOntgHFS\nRYmbKky0bti/ZoZlcZtS0zyjVxlqsQIDAQABAoICAEr3m/GWIXgNAkPGX9PGnmtr\n0dgX6SIhh7d1YOwNZV3DlYAV9HfUa5Fcwc1kQny7QRWbHOepBI7sW2dQ9buTDXIh\nVjPP37yxo6d89EZWfxtpUP+yoXL0D4jL257qCvtJuJZ6E00qaVMDhXbiQKABlo8C\n9sVEiABhwXBDZsctpwtTiykTgv6hrrPy2+H8R8MAm0/VcBCAG9kG5r8FCEmIvQKa\ndgvNxrfiWNZuZ6yfLmpJH54SbhG9Kb4WbCKfvh4ihqyi0btRdSM6fMeLgG9o/zrc\ns54B0kHeLOYNVo0j7FQpZBFeSIbmHfln4RKBh7ntrTke/Ejbh3NbiPvxWSP0P067\nSYWPkQpip2q0ION81wSQZ1haP2GewFFu4IEjG3DlqqpKKGLqXrmjMufnildVFpBx\nir+MgvgQfEBoGEx0aElyO7QuRYaEiXeb/BhMZeC5O65YhJrWSuTVizh3xgJWjgfV\naYwYgxN8SBXBhXLIVvnPhadTqsW1C/aevLOk110eSFWcHf+FCK781ykIzcpXoRGX\nOwWcZzC/fmSABS0yH56ow+I0tjdLIEEMhoa4/kkamioHOJ4yyB+W1DO6/DnMyQlx\ng7y2WsAaIEBoWUARy776k70xPPMtYAxzFXI9KhqRVrPfeaRZ+ojeyLyr3GQGyyoo\ncuGRdMUblsmODv4ixmOxAoIBAQDvkznvVYNdP3Eg5vQeLm/qsP6dLejLijBLeq9i\n7DZH2gRpKcflXZxCkRjsKDDE+fgDcBYEp2zYfRIVvgrxlTQZdaSG+GoDcbjbNQn3\ndjCCtOOACioN/vg2zFlX4Bs6Q+NaV7g5qP5SUaxUBjuHLe7Nc+ZkyheMHuNYVLvk\nHL/IoWyANpZYjMUU3xMbL/J29Gz7CPGr8Si28TihAHGfcNgn8S04OQZhTX+bU805\n/+7B4XW47Mthg/u7hlqFl+YIAaSJYvWkEaVP1A9I7Ve0aMDSMWwzTg9cle2uVaL3\n+PTzWY5coBlHKjqAg9ufhYSDhAqBd/JOSlv8RwcA3PDXJ6C/AoIBAQDABmXXYQky\n7phExXBvkLtJt2TBGjjwulf4R8TC6W5F51jJuoqY/mTqYcLcOn2nYGVwoFvPsy/Q\nCTjfODwJBXzbloXtYFR3PWAeL1Y6+7Cm+koMWIPJyVbD5Fzm+gZStM0GwP8FhDt2\nWt8fWEyXmoLdAy6RAwiEmCagEh8o+13oBfwnBllbz7TxaErsUuR+XVgl/iHwztdv\ncdJKyRgaFfWSh9aiO7EMV2rBGWsoX09SRvprPFAGx8Ffm7YcqIk34QXsQyc45Dyn\nCwkvypxHoaB3ot/48FeFm9IubApb/ctv+EgkBfL4S4bdwRXS1rt+0+QihBoFyP2o\nJ91cdm4hEWCPAoIBAQC6l11hFaYZo0bWDGsHcr2B+dZkzxPoKznQH76n+jeQoLIc\nwgjJkK4afm39yJOrZtEOxGaxu0CgIFFMk9ZsL/wC9EhvQt02z4TdXiLkFK5VrtMd\nr0zv16y06VWQhqBOMf/KJlX6uq9RqADi9HO6pkC+zc0cpPXQEWKaMmygju+kMG2U\nMm/IieMZjWCRJTfgBCE5J88qTsqaKagkZXcZakdAXKwOhQN+F2EStiM6UCZB5PrO\nS8dfrO8ML+ki8Zqck8L1qhiNb5zkXtKExy4u+gNr8khGcT6vqqoSxOoH3mPRgOfL\nJnppne8wlwIf7Vq3H8ka6zPSXEHma999gZcmy9t7AoIBAGbQhiLl79j3a0wXMvZp\nVf5IVYgXFDnAbG2hb7a06bhAAIgyexcjzsC4C2+DWdgOgwHkuoPg+062QV8zauGh\nsJKaa6cHlvIpSJeg3NjD/nfJN3CYzCd0yCIm2Z9Ka6xI5iYhm+pGPNhIG4Na8deS\ngVL46yv1pc/o73VxfoGg5UzgN3xlp97Cva0sHEGguHr4W8Qr59xZw3wGQ4SLW35M\nF6qXVNKUh12GSMCPbZK2RXBWVKqqJmca+WzJoJ6DlsT2lQdFhXCus9L007xlDXxF\nC/hCmw1dEl+VaNo2Ou26W/zdwTKYhNlxBwsg4SB8nPNxXIsmlBBY54froFhriNfn\nx/0CggEAUzz+VMtjoEWw2HSHLOXrO4EmwJniNgiiwfX3DfZE4tMNZgqZwLkq67ns\nT0n3b0XfAOOkLgMZrUoOxPHkxFeyLLf7pAEJe7QNB+Qilw8e2zVqtiJrRk6uDIGJ\nSv+yM52zkImZAe2jOdU3KeUZxSMmb5vIoiPBm+tb2WupAg3YdpKn1/jWTpVmV/+G\nUtTLVE6YpAyFp1gMxhutE9vfIS94ek+vt03AoEOlltt6hqZfv3xmY8vGuAjlnj12\nzHaq+fhCRPsbsZkzJ9nIVdXYnNIEGtMGNnxax7tYRej/UXqyazbxHiJ0iPF4PeDn\ndzxtGxpeTBi+KhKlca8SlCdCqYwG6Q==\n-----END PRIVATE KEY-----", + "key-id": "rsa-4096" + }, + "rsa-4096-public": { + "encrypt": true, + "decrypt": false, + "algorithm": "rsa", + "type": "public", + "bits": 4096, + "encoding": "pem", + "material": "-----BEGIN PUBLIC KEY-----\nMIICIjANBgkqhkiG9w0BAQEFAAOCAg8AMIICCgKCAgEAs7RoNYEPAIws89VV+kra\nrVv/4wbdmUAaAKWgWuxZi5na9GJSmnhCkqyLRm7wPbQY4LCoa5/IMUxkHLsYDPdu\nudY0Qm0GcoxOlvJKHYo4RjF7HyiS34D6dvyO4Gd3aq0mZHoxSGCxW/7hf03wEMzc\niVJXWHXhaI0lD6nrzIEgLrE4L+3V2LeAQjvZsTKd+bYMqeZOL2syiVVIAU8POwAG\nGVBroJoveFm/SUp6lCiN0M2kTeyQA2ax3QTtZSAa8nwrI7U52XOzVmdMicJsy2Pg\nuW98te3MuODdK24yNkHIkYameP/Umf/SJshUJQd5a/TUp3XE+HhOWAumx22tIDlC\nvZS11cuk2fp0WeHUnXaC19N5qWKfvHEKSugzty/z3lGP7ItFhrF2X1qJHeAAsL11\nkjo6Lc48KsE1vKvbnW4VLyB3wdNiVvmUNO29tPXwaR0Q5Gbr3jk3nUzdkEHouHWQ\n41lubOHCCBN3V13mh/MgtNhESHjfmmOnh54ErD9saA1d7CjTf8g2wqmjEqvGSW6N\nq7zhcWR2tp1olflS7oHzul4/I3hnkfL6Kb2xAWWaQKvg3mtsY2OPlzFEP0tR5UcH\nPfp5CeS1Xzg7hN6vRICW6m4l3u2HJFld2akDMm1vnSz8RCbPW7jp7YBxUkWJmypM\ntG7Yv2aGZXGbUtM8o1cZarECAwEAAQ==\n-----END PUBLIC KEY-----", + "key-id": "rsa-4096" + }, + "ecc-256-private":{ + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "ecc-private", + "bits": 256, + "encoding": "pem", + "sender-material": "-----BEGIN PRIVATE KEY-----\nMIGHAgEAMBMGByqGSM49AgEGCCqGSM49AwEHBG0wawIBAQQgw+7YSKEOEAh8/DFZ\n22oSTm/D3jo4nH5tN48IUp0WjyuhRANCAASnUgx7SrlHhPIn3McZfc3cEIs8+XFf\n7JvhcuV1wWELGZ8AjuwnKjE0ielEwSY5HYzWCF773FvJaWGYGYGhSba8\n-----END PRIVATE KEY-----", + "recipient-material": "-----BEGIN PRIVATE KEY-----\nMIGHAgEAMBMGByqGSM49AgEGCCqGSM49AwEHBG0wawIBAQQgYvB/1CVSgfQDrE6A\nDz7pdgxcOb+AHnsaI4LQMY6s8JChRANCAARYxf/AeERu2Z3VtDokplDs/atuGIbW\n7IGhknbK2MP+NV/mbcaxl8Xki9FegBslxCbM66KaoOZR1bCxPpGub2aS\n-----END PRIVATE KEY-----", + "public-key-encoding": "base64-der", + "sender-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAEp1IMe0q5R4TyJ9zHGX3N3BCLPPlxX+yb4XLldcFhCxmfAI7sJyoxNInpRMEmOR2M1ghe+9xbyWlhmBmBoUm2vA==", + "recipient-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAEWMX/wHhEbtmd1bQ6JKZQ7P2rbhiG1uyBoZJ2ytjD/jVf5m3GsZfF5IvRXoAbJcQmzOuimqDmUdWwsT6Rrm9mkg==", + "key-id": "ecc-256" + }, + "ecc-384-private":{ + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "ecc-private", + "bits": 384, + "encoding": "pem", + "sender-material": "-----BEGIN PRIVATE KEY-----\nMIG2AgEAMBAGByqGSM49AgEGBSuBBAAiBIGeMIGbAgEBBDAx0jhFAVQX2zykSLO/\n3VvDDaQJspek3404TtDZupcxi2rThfnxh96u8CYD6XfHikehZANiAAR2W/Cc8slJ\ngYSGi3e+38UUW6dFi1mJBNEZEbJ4vljgEzBo7FecTsCOQH8Zu2nX3eQpuboD8Fb7\nARpqq7rug5jKBMQLUbvridjLBRLuFsfaLpZ07ih4/+VduqQom7D31ik=\n-----END PRIVATE KEY-----", + "recipient-material": "-----BEGIN PRIVATE KEY-----\nMIG2AgEAMBAGByqGSM49AgEGBSuBBAAiBIGeMIGbAgEBBDALwMcT5K2IOUK5Ww5o\nqYrYLzKHuAvFs0VLuKvJOCmWa3NK2WXtUIJ2fPYzp2Y9oTShZANiAATXUn2WMiLB\nbf665ikArOEAOFgruhqAwlxy58BP42nodBZFFf4L7cy7vPLpasp3fFroN57tYfjy\nXL5Wc0vb+xJaTZLBTU/tRGvtjHH0hQgMib2ch6akUJAT6zuMgNNdd7A=\n-----END PRIVATE KEY-----", + "public-key-encoding": "base64-der", + "sender-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEdlvwnPLJSYGEhot3vt/FFFunRYtZiQTRGRGyeL5Y4BMwaOxXnE7AjkB/Gbtp193kKbm6A/BW+wEaaqu67oOYygTEC1G764nYywUS7hbH2i6WdO4oeP/lXbqkKJuw99Yp", + "recipient-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAE11J9ljIiwW3+uuYpAKzhADhYK7oagMJccufAT+Np6HQWRRX+C+3Mu7zy6WrKd3xa6Dee7WH48ly+VnNL2/sSWk2SwU1P7URr7Yxx9IUIDIm9nIempFCQE+s7jIDTXXew", + "key-id": "ecc-384" + }, + "ecc-521-private":{ + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "ecc-private", + "bits": 521, + "encoding": "pem", + "sender-material": "-----BEGIN PRIVATE KEY-----\nMIHuAgEAMBAGByqGSM49AgEGBSuBBAAjBIHWMIHTAgEBBEIANn8j3pIu1wiwkz7z\niPKuqj2MEVWKe/UW/8NEtvD9tKQmMlAzwY/QN93k+0TNlXpvJTUvjI2NZDKNoQ2b\n0B44YfyhgYkDgYYABAHfgnF9LoYBRWwXKKEFQa+Xfg+ztDRdTVTqNZ8roUYmNvLL\nLz2F8oEOhDbMJZ5r1B1C9w5uJqeF6tE8a3yzm47R/wAs0k6dY3wfDKD013Wnn+6e\nNw1mtrvTi6+Pej/ukYOuCjCwm8B0AvxBzdHk8Q/nCcspO9pIsRl/I4qNz4tPaGjJ\nTA==\n-----END PRIVATE KEY-----", + "recipient-material": "-----BEGIN PRIVATE KEY-----\nMIHuAgEAMBAGByqGSM49AgEGBSuBBAAjBIHWMIHTAgEBBEIBjhdIxb49QXi4OsOH\n5PNWnp/KePiuICqC+fxJJ6ceUgPr5SMlLxhHcfHSVZBCkGLP0Rjd1D9gi7Va1oxe\nIHmWRu2hgYkDgYYABAAmg0dilFc6FiO9OE8t1el92KdPo9WYu1hXYnjGYT7OuGj3\nbD9lr0KMNCm3wTPCiLjPb4Iqnk+g0SgrsQ4NvU7nygFBlgz8xXLzIXPqVICthcHX\nRWRB8HnXmyzeF0iCs12F/6vYn/uZfxp3IV/KCR4LwSzbiFzxsV9GYoCoUE30LDVb\nXg==\n-----END PRIVATE KEY-----", + "public-key-encoding": "base64-der", + "sender-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQB34JxfS6GAUVsFyihBUGvl34Ps7Q0XU1U6jWfK6FGJjbyyy89hfKBDoQ2zCWea9QdQvcObianherRPGt8s5uO0f8ALNJOnWN8Hwyg9Nd1p5/unjcNZra704uvj3o/7pGDrgowsJvAdAL8Qc3R5PEP5wnLKTvaSLEZfyOKjc+LT2hoyUw=", + "recipient-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQAJoNHYpRXOhYjvThPLdXpfdinT6PVmLtYV2J4xmE+zrho92w/Za9CjDQpt8Ezwoi4z2+CKp5PoNEoK7EODb1O58oBQZYM/MVy8yFz6lSArYXB10VkQfB515ss3hdIgrNdhf+r2J/7mX8adyFfygkeC8Es24hc8bFfRmKAqFBN9Cw1W14=", + "key-id": "ecc-521" + }, + "us-west-2-decryptable": { + "encrypt": true, + "decrypt": true, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f" + }, + "us-west-2-encrypt-only": { + "encrypt": true, + "decrypt": false, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-west-2:658956600833:key/590fd781-ddde-4036-abec-3e1ab5a5d2ad" + }, + "us-west-2-mrk": { + "encrypt": true, + "decrypt": true, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-west-2:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7" + }, + "us-east-1-mrk": { + "encrypt": true, + "decrypt": true, + "type": "aws-kms", + "key-id": "arn:aws:kms:us-east-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7" + }, + "us-west-2-rsa-mrk": { + "encrypt": true, + "decrypt": true, + "algorithm": "rsa", + "type": "aws-kms-rsa", + "key-id": "arn:aws:kms:us-west-2:370957321024:key/mrk-63d386cb70614ea59b32ad65c9315297", + "bits": 2048, + "encoding": "pem", + "material": "-----BEGIN PUBLIC KEY-----\nMIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEA27Uc/fBaMVhxCE/SpCMQ\noSBRSzQJw+o2hBaA+FiPGtiJ/aPy7sn18aCkelaSj4kwoC79b/arNHlkjc7OJFsN\n/GoFKgNvaiY4lOeJqEiWQGSSgHtsJLdbO2u4OOSxh8qIRAMKbMgQDVX4FR/PLKeK\nfc2aCDvcNSpAM++8NlNmv7+xQBJydr5ce91eISbHkFRkK3/bAM+1iddupoRw4Wo2\nr3avzrg5xBHmzR7u1FTab22Op3Hgb2dBLZH43wNKAceVwKqKA8UNAxashFON7xK9\nyy4kfOL0Z/nhxRKe4jRZ/5v508qIzgzCksYy7Y3QbMejAtiYnr7s5/d5KWw0swou\ntwIDAQAB\n-----END PUBLIC KEY-----" + }, + "us-west-2-256-ecc": { + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "aws-kms-ecdh", + "sender-material": "arn:aws:kms:us-west-2:370957321024:key/eabdf483-6be2-4d2d-8ee4-8c2583d416e9", + "recipient-material": "arn:aws:kms:us-west-2:370957321024:key/0265c8e9-5b6a-4055-8f70-63719e09fda5", + "encoding": "base64-der", + "sender-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE18m54QsLUnhWU7gT8hkAceNbZ/WBGNUUSPCeIKqOyX5psiqyC1TXPOJXqKKaVv5Mg91WV9UjpboblOhNU35nRw==", + "recipient-material-public-key": "MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE9istdPCuX9nF8EmA4tioe/k0TCa2M9VeBW1N9n0sxPA6uPVOfLtE4+KuYxAGT0dYoK6CY93nowUy1yS+R7A+wA==", + "key-id": "ecc-256" + }, + "us-west-2-384-ecc": { + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "aws-kms-ecdh", + "sender-material": "arn:aws:kms:us-west-2:370957321024:key/7f35a704-f4fb-469d-98b1-62a1fa2cc44e", + "recipient-material": "arn:aws:kms:us-west-2:370957321024:key/29f0bef9-1677-4e74-b67e-acefab1295ff", + "encoding": "base64-der", + "sender-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEfQ0OHFvwskFVjQwfqV7jpo62I6uyGY+5SPRZb6CuJ96bVreLZXh485BcPv09O/DWnpTBm8LL+YcfsqM3ECvi2ee3bDGpH6xIdr28uvyG75t5wqBjYYtZQFDf/ydfG9mm", + "recipient-material-public-key": "MHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEWgGNWQ+vEwlMxyMQkSsOAYGfT6IlgEkcanEOSjbeEpEnh8JHEiBHQ6QaROxJ7c3nEkbjbi0m+7ejBEGtkiqaY5Dsv5u1iV4fc/2v1RzPba1ZtudEmM16Eyy9LHswdJ7v", + "key-id": "ecc-384" + }, + "us-west-2-521-ecc": { + "encrypt": true, + "decrypt": true, + "algorithm": "ecdh", + "type": "aws-kms-ecdh", + "sender-material": "arn:aws:kms:us-west-2:370957321024:key/41b502e3-cc9d-442f-bd7b-d67faed0f22e", + "recipient-material": "arn:aws:kms:us-west-2:370957321024:key/c45f1043-53bb-4f37-adc5-4d25d4a84f9d", + "encoding": "base64-der", + "sender-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQAz86qnfp3s0cl+73PQhlUstfdg9EZDA/jtLjBTWYp/1EB7RHNm8q5hMg5kBfjRDUFhbRBMlUV1xBOTgqzoSWj4oAABnQKiXXGGyu6PMN4D9nVMDsOpJ1pWU7rQexWDahBrK+5hx3beFXUpvvFRQrGAt2icUXm18VO6Qwbp0da9jyGDSY=", + "recipient-material-public-key": "MIGbMBAGByqGSM49AgEGBSuBBAAjA4GGAAQAxLxcjtYfqc4+4oJZY0gGv2Ehu++CnVFea6uwXgEgLifq4eDSSVmQYvU8majsufpBXQwVjnDlQ7pGRw1j6K4FaLAAgYuMrmrwKtx/ZZtkbXzCwrqJY+sfCk8U5m89DX331cdBAhR2uVSPL2d5hp8up5v+EBpNArtdC5lZMx2ZrwKKYuQ=", + "key-id": "ecc-521" + } + } +} diff --git a/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/wrapped/TestESDK.java b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/wrapped/TestESDK.java index e5e7fbd56..0742e8265 100644 --- a/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/wrapped/TestESDK.java +++ b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/wrapped/TestESDK.java @@ -62,11 +62,6 @@ public Result Decrypt(DecryptInput dafnyInput) { final CryptoResult decryptResult; if (_prefer_mkp_over_keyring && provider != null) { - // Logging - // TODO: Make logging optional - System.out.println( - "Decrypted with MasterKeyProvider: " + provider.getClass().getName() - ); decryptResult = this._impl.decryptData(provider, nativeInput.ciphertext().array()); if (!Objects.isNull(nativeInput.encryptionContext())) { @@ -95,8 +90,6 @@ public Result Decrypt(DecryptInput dafnyInput) { } } } else { - // Logging - System.out.println("Decrypted with MPL Keyring/CMM"); if (Objects.isNull(nativeInput.materialsManager())) { // Call decrypt with keyring if (Objects.isNull(nativeInput.encryptionContext())) { @@ -195,8 +188,6 @@ public Result Encrypt(EncryptInput dafnyInput) { this._impl.setEncryptionAlgorithm(cryptoAlgorithm); if (_prefer_mkp_over_keyring && provider != null) { - // Logging - System.out.println("Encrypted with: " + provider.getClass().getName()); // Call decrypt with MKP if (Objects.isNull(nativeInput.encryptionContext())) { encryptResult = @@ -210,8 +201,6 @@ public Result Encrypt(EncryptInput dafnyInput) { ); } } else { - // Logging - System.out.println("Encrypted with MPL Keyring/CMM"); // If the CMM is null, it MUST be a Keyring if (Objects.isNull(nativeInput.materialsManager())) { // Call decrypt with keyring diff --git a/mpl b/mpl index 377de796f..d808fd88d 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit 377de796f001ae21f69ac0e10f57709d0e6fa1ef +Subproject commit d808fd88df92acf64fb9ca0e7c652d72e05fa50a