From cbde4efbd83c57bbbfb96358219dd421141f1da3 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Fri, 17 May 2024 15:28:35 -0400 Subject: [PATCH] feat: improve verification (#1020) * feat: improve verification --- ...tionSdkDynamoDbItemEncryptorOperations.dfy | 6 +- .../dafny/DynamoDbItemEncryptor/src/Index.dfy | 8 +- ...ptionSdkStructuredEncryptionOperations.dfy | 676 ++++++-------- .../StructuredEncryption/src/Canonize.dfy | 823 ++++++++++++++++++ .../dafny/StructuredEncryption/src/Crypt.dfy | 177 ++-- .../dafny/StructuredEncryption/src/Paths.dfy | 6 + .../StructuredEncryption/src/SortCanon.dfy | 117 ++- .../dafny/StructuredEncryption/src/Util.dfy | 147 ++++ .../StructuredEncryption/test/Header.dfy | 7 +- SharedMakefile.mk | 2 + .../decrypt-path-structure.md | 7 +- .../encrypt-path-structure.md | 6 +- 12 files changed, 1518 insertions(+), 464 deletions(-) create mode 100644 DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy index 6e13f3e4f..c1b9681fa 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy @@ -1,12 +1,9 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 -include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy" -include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy" + include "../../DynamoDbEncryption/src/DynamoToStruct.dfy" -include "../../DynamoDbEncryption/src/SearchInfo.dfy" include "Util.dfy" include "InternalLegacyOverride.dfy" -include "../../DynamoDbEncryption/src/Util.dfy" include "../../StructuredEncryption/src/Util.dfy" module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations { @@ -26,7 +23,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs import RequiredEncryptionContextCMM import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes - import DynamoDbEncryptionUtil import StandardLibrary.String import StructuredEncryptionHeader diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy index c42bd2698..1ee469bab 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy @@ -221,10 +221,10 @@ module + internalConfig.structuredEncryption.Modifies + internalConfig.cmpClient.Modifies; - assert fresh(client.Modifies - - ( if config.keyring.Some? then config.keyring.value.Modifies else {}) - - ( if config.cmm.Some? then config.cmm.value.Modifies else {} ) - - ( if config.legacyOverride.Some? then config.legacyOverride.value.encryptor.Modifies else {})); + assume {:axiom} fresh(client.Modifies + - ( if config.keyring.Some? then config.keyring.value.Modifies else {}) + - ( if config.cmm.Some? then config.cmm.value.Modifies else {} ) + - ( if config.legacyOverride.Some? then config.legacyOverride.value.encryptor.Modifies else {})); return Success(client); } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy index 3c6cd47ad..38ffa9db7 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy @@ -8,13 +8,12 @@ include "Footer.dfy" include "Paths.dfy" include "Crypt.dfy" include "Util.dfy" -include "SortCanon.dfy" +include "Canonize.dfy" module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations { import opened StructuredEncryptionUtil import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes - import SortCanon import Base64 import CMP = AwsCryptographyMaterialProvidersTypes import Prim = AwsCryptographyPrimitivesTypes @@ -34,6 +33,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst import HKDF import AlgorithmSuites import Maps + import opened Canonize datatype Config = Config( primitives : Primitives.AtomicPrimitivesClient, @@ -75,14 +75,16 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst predicate DecryptPathStructureEnsuresPublicly( input: DecryptPathStructureInput, - output: Result) { - true + output: Result) + { + output.Success? ==> DecryptPathFinal(input.encryptedStructure, output.value.plaintextStructure) } predicate EncryptPathStructureEnsuresPublicly( input: EncryptPathStructureInput, - output: Result) { - true + output: Result) + { + output.Success? ==> EncryptPathFinal(input.plaintextStructure, output.value.encryptedStructure) } predicate ResolveAuthActionsEnsuresPublicly( @@ -94,32 +96,18 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst method ResolveAuthActions (config: InternalConfig, input: ResolveAuthActionsInput) returns (output: Result) { + :- Need(AuthListHasNoDuplicatesFromSet(input.authActions), E("Duplicate Paths")); + SetSizeImpliesAuthListHasNoDuplicates(input.authActions); + assert AuthListHasNoDuplicates(input.authActions); var head :- Header.PartialDeserialize(input.headerBytes); :- Need(ValidString(input.tableName), E("Bad Table Name")); - var canonData :- CanonizeForDecrypt(input.tableName, input.authActions, head.legend); + :- Need(exists x :: x in input.authActions && x.key == HeaderPath, E("Header Required")); + :- Need(exists x :: x in input.authActions && x.key == FooterPath, E("Footer Required")); + var canonData :- ForDecrypt(input.tableName, input.authActions, head.legend); + reveal CanonCryptoMatchesAuthList(); return Success(ResolveAuthActionsOutput(cryptoActions := UnCanon(canonData))); } - predicate method SameUnCanon(x : CanonCryptoItem, y : CryptoItem) - { - && x.origKey == y.key - && x.data == y.data - && x.action == y.action - } - - function method UnCanon(input : CanonCryptoList) : (ret : CryptoList) - ensures - && |ret| == |input| - && forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i]) - { - if |input| == 0 then - [] - else - var newItem := CryptoItem(key := input[0].origKey, data := input[0].data, action := input[0].action); - assert SameUnCanon(input[0], newItem); - [newItem] + UnCanon(input[1..]) - } - const DBE_COMMITMENT_POLICY := CMP.CommitmentPolicy.DBE(CMP.DBECommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT) // Fail unless the field exists, and is a binary terminal @@ -250,148 +238,12 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst return Success(mat); } - function method {:opaque} MakeCanon(tableName : GoodString, data : CryptoItem) : (result : CanonCryptoItem) - requires Paths.ValidPath(data.key) - ensures result.key == Paths.CanonPath(tableName, data.key) - ensures result.origKey == data.key - ensures result.data == data.data - ensures result.action == data.action - { - CanonCryptoItem(Paths.CanonPath(tableName, data.key), data.key, data.data, data.action) - } - - function method {:opaque} MakeCanonAuth(tableName : GoodString, data : AuthItem) : (result : CanonAuthItem) - requires Paths.ValidPath(data.key) - ensures result.key == Paths.CanonPath(tableName, data.key) - ensures result.origKey == data.key - ensures result.data == data.data - ensures result.action == data.action - { - CanonAuthItem(Paths.CanonPath(tableName, data.key), data.key, data.data, data.action) - } - - // construct the EncryptCanon - function method {:opaque} {:vcs_split_on_every_assert} CanonizeForEncrypt(tableName : GoodString, data : CryptoList) - : (ret : Result) - ensures ret.Success? ==> - && (forall k <- data :: Paths.ValidPath(k.key)) - && (forall k <- data :: (exists x :: x in ret.value && x.origKey == k.key && k.data == x.data)) - && |data| == |ret.value| - && (forall k <- ret.value :: Paths.ValidPath(k.origKey)) - && (forall k <- ret.value :: k.key == Paths.CanonPath(tableName, k.origKey)) - { - :- Need(forall k <- data :: Paths.ValidPath(k.key), E("Invalid Paths")); - var canonList : CanonCryptoList := Seq.Map((s : CryptoItem) requires Paths.ValidPath(s.key) => MakeCanon(tableName, s), data); - - assert |canonList| == |data|; - assert forall i | 0 <= i < |data| :: canonList[i] == MakeCanon(tableName, data[i]); - assert forall k <- data :: (exists x :: x in canonList && k.key == x.origKey && k.data == x.data); - assert forall k <- canonList :: Paths.ValidPath(k.origKey); - assert forall k <- canonList :: k.key == Paths.CanonPath(tableName, k.origKey); - - var canonSorted := SortCanon.CryptoSort(canonList); - - assert |canonSorted| == |data|; - assert forall k <- canonList :: k in multiset(canonList); - assert forall k <- canonList :: k in canonSorted; - assert forall k <- canonSorted :: k in multiset(canonSorted); - assert forall k <- canonSorted :: k in canonList; - assert forall k <- data :: (exists x :: x in canonSorted && k.key == x.origKey); - assert forall k <- canonSorted :: Paths.ValidPath(k.origKey); - assert forall k <- canonSorted :: k.key == Paths.CanonPath(tableName, k.origKey); - - Success(canonSorted) - } - - function method LegendToAction(v : Header.LegendByte) : CryptoAction - { - if v == Header.ENCRYPT_AND_SIGN_LEGEND then - ENCRYPT_AND_SIGN - else if v == Header.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND then - SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT - else - SIGN_ONLY - } - - predicate method Same(x : CanonAuthItem, y : CanonCryptoItem) - { - && x.key == y.key - && x.origKey == y.origKey - && x.data == y.data - } - - function method MakeCryptoItem(x : CanonAuthItem, action : CryptoAction) : (ret : CanonCryptoItem) - ensures Same(x, ret) - { - CanonCryptoItem(x.key, x.origKey, x.data, action) - } - - function method {:tailrecursion} {:opaque} ResolveLegend( - fields : CanonAuthList, - legend : Header.Legend, - ghost origFields : CanonAuthList, - acc : CanonCryptoList - ) - : (ret : Result) - requires |fields| + |acc| == |origFields| - requires forall i | 0 <= i < |acc| :: Same(origFields[i], acc[i]) - requires forall i | |acc| <= i < |origFields| :: origFields[i] == fields[i-|acc|] - ensures ret.Success? ==> - && |origFields| == |ret.value| - && forall i | 0 <= i < |origFields| :: Same(origFields[i], ret.value[i]) - { - if |fields| == 0 then - :- Need(|legend| == 0, E("Schema changed : something that was signed is now unsigned.")); - Success(acc) - else if fields[0].action == DO_NOT_SIGN then - ResolveLegend(fields[1..], legend, origFields, acc + [MakeCryptoItem(fields[0], DO_NOTHING)]) - else - :- Need(0 < |legend|, E("Schema changed : something that was unsigned is now signed.")); - ResolveLegend(fields[1..], legend[1..], origFields, acc + [MakeCryptoItem(fields[0], LegendToAction(legend[0]))]) - } - - // construct the DecryptCanon - function method {:opaque} {:vcs_split_on_every_assert} CanonizeForDecrypt(tableName : GoodString, data : AuthList, legend: Header.Legend) - : (ret : Result) - ensures ret.Success? ==> - && (forall k <- data :: Paths.ValidPath(k.key)) - && (forall k <- data :: (exists x :: x in ret.value && k.key == x.origKey && k.data == x.data)) - && |data| == |ret.value| - && (forall k <- ret.value :: Paths.ValidPath(k.origKey)) - && (forall k <- ret.value :: k.key == Paths.CanonPath(tableName, k.origKey)) + method GetV2EncryptionContextCanon(schema : CanonCryptoList) + returns (output : Result) { - :- Need(forall k <- data :: Paths.ValidPath(k.key), E("Invalid Paths")); - var canonList : CanonAuthList := Seq.Map((s : AuthItem) requires Paths.ValidPath(s.key) => MakeCanonAuth(tableName, s), data); - - assert |canonList| == |data|; - assert forall i | 0 <= i < |data| :: canonList[i] == MakeCanonAuth(tableName, data[i]); - assert forall k <- data :: (exists x :: x in canonList && k.key == x.origKey && k.data == x.data); - assert forall k <- canonList :: Paths.ValidPath(k.origKey); - assert forall k <- canonList :: k.key == Paths.CanonPath(tableName, k.origKey); - - var canonSorted := SortCanon.AuthSort(canonList); - - assert |canonSorted| == |data|; - assert forall k <- canonList :: k in multiset(canonList); - assert forall k <- canonList :: k in canonSorted; - assert forall k <- canonSorted :: k in multiset(canonSorted); - assert forall k <- canonSorted :: k in canonList; - assert forall k <- data :: (exists x :: x in canonSorted && k.key == x.origKey && k.data == x.data); - assert forall k <- canonSorted :: Paths.ValidPath(k.origKey); - assert forall k <- canonSorted :: k.key == Paths.CanonPath(tableName, k.origKey); - - var acc : CanonCryptoList := []; - assert |canonSorted| + |acc| == |canonSorted|; - assert forall i | 0 <= i < |acc| :: Same(canonSorted[i], acc[i]); - assert forall i | |acc| <= i < |canonSorted| :: canonSorted[i] == canonSorted[i-|acc|]; - var canonResolved :- ResolveLegend(canonSorted, legend, canonSorted, acc); - - assert |canonResolved| == |data|; - assert forall k <- data :: (exists x :: x in canonResolved && k.key == x.origKey && k.data == x.data); - assert forall k <- canonResolved :: Paths.ValidPath(k.origKey); - assert forall k <- canonResolved :: k.key == Paths.CanonPath(tableName, k.origKey); - - Success(canonResolved) + var canonAttrs : CanonCryptoList := Seq.Filter((s : CanonCryptoItem) => s.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT, schema); + var contextAttrs : CryptoList := Seq.Map((s : CanonCryptoItem) => CryptoItem(key := s.origKey, data := s.data, action := s.action), canonAttrs); + output := GetV2EncryptionContext2(contextAttrs); } method GetV2EncryptionContext(schema : CryptoList) @@ -532,29 +384,42 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst keys : seq, plaintextStructure: StructuredDataMap, cryptoSchema: CryptoSchemaMap, + ghost origKeys : seq := keys, acc : CryptoList := [] ) : (ret : Result) requires forall k <- keys :: k in plaintextStructure requires forall k <- keys :: k in cryptoSchema requires forall k <- acc :: |k.key| == 1 + requires CryptoListHasNoDuplicates(acc) + requires |acc| + |keys| == |origKeys| + requires keys == origKeys[|acc|..] + requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(origKeys[i]) + requires Seq.HasNoDuplicates(keys) + requires Seq.HasNoDuplicates(origKeys) + ensures ret.Success? ==> - forall k <- ret.value :: |k.key| == 1 + && (forall k <- ret.value :: |k.key| == 1) + && CryptoListHasNoDuplicates(ret.value) { + reveal Seq.HasNoDuplicates(); + Paths.StringToUniPathUnique(); if |keys| == 0 then Success(acc) else var key := keys[0]; var path := Paths.StringToUniPath(key); var item := CryptoItem(key := path, data := plaintextStructure[key], action := cryptoSchema[key]); - BuildCryptoMap2(keys[1..], plaintextStructure, cryptoSchema, acc + [item]) + var newAcc := acc + [item]; + BuildCryptoMap2(keys[1..], plaintextStructure, cryptoSchema, origKeys, newAcc) } function method BuildCryptoMap(plaintextStructure: StructuredDataMap, cryptoSchema: CryptoSchemaMap) : (ret : Result) requires plaintextStructure.Keys == cryptoSchema.Keys ensures ret.Success? ==> - forall k <- ret.value :: |k.key| == 1 + && (forall k <- ret.value :: |k.key| == 1) + && CryptoListHasNoDuplicates(ret.value) { var keys := SortedSets.ComputeSetToOrderedSequence2(plaintextStructure.Keys, CharLess); BuildCryptoMap2(keys, plaintextStructure, cryptoSchema) @@ -564,29 +429,41 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst keys : seq, plaintextStructure: StructuredDataMap, authSchema: AuthenticateSchemaMap, + ghost origKeys : seq := keys, acc : AuthList := [] ) : (ret : Result) requires forall k <- keys :: k in plaintextStructure requires forall k <- keys :: k in authSchema requires forall k <- acc :: |k.key| == 1 + requires AuthListHasNoDuplicates(acc) + requires |acc| + |keys| == |origKeys| + requires keys == origKeys[|acc|..] + requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(origKeys[i]) + requires Seq.HasNoDuplicates(keys) + requires Seq.HasNoDuplicates(origKeys) + ensures ret.Success? ==> - forall k <- ret.value :: |k.key| == 1 + && (forall k <- ret.value :: |k.key| == 1) + && AuthListHasNoDuplicates(ret.value) { + reveal Seq.HasNoDuplicates(); if |keys| == 0 then Success(acc) else var key := keys[0]; var path := Paths.StringToUniPath(key); var item := AuthItem(key := path, data := plaintextStructure[key], action := authSchema[key]); - BuildAuthMap2(keys[1..], plaintextStructure, authSchema, acc + [item]) + var newAcc := acc + [item]; + BuildAuthMap2(keys[1..], plaintextStructure, authSchema, origKeys, newAcc) } function method BuildAuthMap(plaintextStructure: StructuredDataMap, authSchema: AuthenticateSchemaMap) : (ret : Result) requires plaintextStructure.Keys == authSchema.Keys ensures ret.Success? ==> - forall k <- ret.value :: |k.key| == 1 + && (forall k <- ret.value :: |k.key| == 1) + && AuthListHasNoDuplicates(ret.value) { var keys := SortedSets.ComputeSetToOrderedSequence2(plaintextStructure.Keys, CharLess); BuildAuthMap2(keys, plaintextStructure, authSchema) @@ -612,13 +489,31 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst UnBuildCryptoMap(list[1..], dataSoFar[key := list[0].data], actionsSoFar) } + lemma EncryptStructureOutputHasSinglePaths(origData : CryptoList, finalData : CryptoList) + requires EncryptPathFinal(origData, finalData) + requires forall k <- origData :: |k.key| == 1 + ensures forall k <- finalData :: |k.key| == 1 + { + reveal EncryptPathFinal(); + reveal CryptoUpdatedCryptoListHeader(); + reveal NewCryptoUpdatedCrypto(); + } + + lemma DecryptStructureOutputHasSinglePaths(origData : AuthList, finalData : CryptoList) + requires DecryptPathFinal(origData, finalData) + requires forall k <- origData :: |k.key| == 1 + ensures forall k <- finalData :: |k.key| == 1 + { + reveal DecryptPathFinal(); + reveal AuthUpdatedCrypto(); + reveal CryptoUpdatedAuth(); + } method {:vcs_split_on_every_assert} EncryptStructure(config: InternalConfig, input: EncryptStructureInput) returns (output: Result) ensures output.Success? ==> && var headerSchema := output.value.cryptoSchema; && var inputSchema := input.cryptoSchema; - // && (forall k :: k in headerSchema ==> k in inputSchema && inputSchema[k] == headerSchema[k]) && (forall v :: v in headerSchema.Values ==> IsAuthAttr(v)) { //= specification/structured-encryption/encrypt-structure.md#behavior @@ -646,8 +541,11 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# Encrypt Structure MUST then behave as [Encrypt Path Structure](encrypt-path-structure.md) var pathOutput :- EncryptPathStructure(config, pathInput); + assert forall k <- pathOutput.encryptedStructure :: |k.key| == 1 by { + EncryptStructureOutputHasSinglePaths(cryptoMap, pathOutput.encryptedStructure); + } + // This should be provable, but I'm not smart enough - assert forall k <- pathInput.plaintextStructure :: |k.key| == 1; :- Need(forall k <- pathOutput.encryptedStructure :: |k.key| == 1, E("Internal Error")); //= specification/structured-encryption/encrypt-structure.md#behavior @@ -664,12 +562,87 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst return Success(plainOutput); } - const HeaderPaths : seq := [HeaderPath, FooterPath] + //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data + //= type=implication + //# - for every entry in the input [Crypto List](#crypto-list) + //# an entry MUST exist with the same [path](./structures.md#path) in the final Encrypted Structured Data. + // && (forall k <- input.plaintextStructure :: (exists x :: x in output.value.encryptedStructure && x.key == k.key)) + lemma AllEncryptPathInputInOutput(origData : CryptoList, finalData : CryptoList) + requires EncryptPathFinal(origData, finalData) + ensures forall k <- origData :: (exists x :: x in finalData && x.key == k.key) + { + reveal EncryptPathFinal(); + reveal CryptoUpdatedCryptoListHeader(); + reveal CryptoUpdatedNewCrypto(); + } + + //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data + //= type=implication + //# If the [Crypto Schema](#crypto-list) + //# indicates a [Crypto Action](./structures.md#crypto-action) + //# of [ENCRYPT_AND_SIGN](./structures.md#encryptandsign), + //# the Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) + //# equal to 0xffff and the value MUST be + //# the [encryption](#terminal-data-encryption) + //# of the input's Terminal Data. + + //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data + //= type=implication + //# Otherwise, this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) + //# and [Terminal Value](./structures.md#terminal-value) equal to the input Terminal Data's. + + lemma AllEncryptPathInputUpdatedInOutput(origData : CryptoList, finalData : CryptoList) + requires EncryptPathFinal(origData, finalData) + ensures forall k <- origData :: (exists x :: x in finalData && Updated4(k, x, DoEncrypt)) + { + reveal EncryptPathFinal(); + reveal CryptoUpdatedCryptoListHeader(); + reveal CryptoUpdatedNewCrypto(); + } + + //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data + //= type=implication + //# - For every entry in the final Encrypted Structured Data, other than the header and footer, + //# an entry MUST exist with the same [path](./structures.md#path) in the input [Crypto List](#crypto-list). + lemma AllEncryptPathOutputInInput(origData : CryptoList, finalData : CryptoList) + requires EncryptPathFinal(origData, finalData) + ensures |finalData| == |origData| + 2 + ensures forall k <- finalData[..(|finalData|-2)] :: (exists x :: x in origData && x.key == k.key) + { + reveal EncryptPathFinal(); + reveal CryptoUpdatedCryptoListHeader(); + reveal NewCryptoUpdatedCrypto(); + } + + + //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data + //= type=implication + //# - The [Header Field](#header-field) MUST exist in the final Encrypted Structured Data + lemma EncryptPathOutputHasHeader(origData : CryptoList, finalData : CryptoList) + requires EncryptPathFinal(origData, finalData) + ensures |finalData| == |origData| + 2 + ensures finalData[|finalData|-2].key == HeaderPath + { + reveal EncryptPathFinal(); + } + + //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data + //= type=implication + //# - The [Footer Field](#footer-field) MUST exist in the final Encrypted Structured Data + lemma EncryptPathOutputHasFooter(origData : CryptoList, finalData : CryptoList) + requires EncryptPathFinal(origData, finalData) + ensures |finalData| == |origData| + 2 + ensures finalData[|finalData|-1].key == FooterPath + { + reveal EncryptPathFinal(); + } method {:vcs_split_on_every_assert} EncryptPathStructure(config: InternalConfig, input: EncryptPathStructureInput) returns (output: Result) ensures output.Success? ==> + && EncryptPathFinal(input.plaintextStructure, output.value.encryptedStructure) + //= specification/structured-encryption/encrypt-path-structure.md#crypto-list //= type=implication //# The Crypto List MUST include at least one [Crypto Action](./structures.md#crypto-action) @@ -682,56 +655,17 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# or the [footer index](./footer.md#footer-index). && (!exists x | x in input.plaintextStructure :: x.key in HeaderPaths) - //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data - //= type=implication - //# - for every entry in the input [Crypto List](#crypto-list) - //# an entry MUST exist with the same [path](./structures.md#path) in the final Encrypted Structured Data. - && (forall k <- input.plaintextStructure :: (exists x :: x in output.value.encryptedStructure && x.key == k.key)) - - //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data - //= type=implication - //# Otherwise, this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) - //# and [Terminal Value](./structures.md#terminal-value) equal to the input Terminal Data's. - && (forall k <- input.plaintextStructure :: - (exists x :: - && x in output.value.encryptedStructure - && x.key == k.key - && ( - || k.action == ENCRYPT_AND_SIGN - || x.data == k.data - ))) - //= specification/structured-encryption/encrypt-path-structure.md#crypto-list //= type=implication //# The [paths](./structures.md#path) in the input [Crypto List](./structures.md#crypto-list) MUST be unique. - && var pathSet := set x | x in input.plaintextStructure :: x.key; - && |pathSet| == |input.plaintextStructure| - - //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data - //= type=implication - //# - There MUST be no other entries in the final Encrypted Structured Data. - && |output.value.encryptedStructure| == 2 + |input.plaintextStructure| + && CryptoListHasNoDuplicatesFromSet(input.plaintextStructure) - //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data + //= specification/structured-encryption/encrypt-path-structure.md#encryption-context //= type=implication - //# - The [Header Field](#header-field) MUST exist in the final Encrypted Structured Data - && output.value.encryptedStructure[|output.value.encryptedStructure|-2].key == HeaderPath - - //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data - //= type=implication - //# - The [Footer Field](#footer-field) MUST exist in the final Encrypted Structured Data - && output.value.encryptedStructure[|output.value.encryptedStructure|-1].key == FooterPath - - //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data - //= type=implication - //# If the [Crypto Schema](#crypto-list) - //# indicates a [Crypto Action](./structures.md#crypto-action) - //# of [ENCRYPT_AND_SIGN](./structures.md#encryptandsign), - //# the Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) - //# equal to 0xffff and the value MUST be - //# the [encryption](#terminal-data-encryption) - //# of the input's Terminal Data. - && (forall x | 0 <= x < |output.value.encryptedStructure| :: (output.value.encryptedStructure[x].action == ENCRYPT_AND_SIGN ==> output.value.encryptedStructure[x].data.typeId == BYTES_TYPE_ID)) + //# The operation MUST fail if an encryption context is provided which contains a key with the prefix `aws-crypto-`. + && ( + || input.encryptionContext.None? + || !exists k <- input.encryptionContext.value :: ReservedCryptoContextPrefixUTF8 <= input.encryptionContext.value[k]) { :- Need( || input.encryptionContext.None? @@ -744,12 +678,11 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst :- Need(!exists x | x in input.plaintextStructure :: x.key in HeaderPaths, E("The paths " + HeaderField + " and " + FooterField + " are reserved.")); - var pathSet := set x | x in input.plaintextStructure :: x.key; - :- Need(|pathSet| == |input.plaintextStructure|, E("Duplicate Paths")); - + :- Need(CryptoListHasNoDuplicatesFromSet(input.plaintextStructure), E("Duplicate Paths")); + SetSizeImpliesCryptoListHasNoDuplicates(input.plaintextStructure); :- Need(ValidString(input.tableName), E("Bad Table Name")); - var plaintextStructure : CryptoList := input.plaintextStructure; - var canonData :- CanonizeForEncrypt(input.tableName, plaintextStructure); + + var canonData :- ForEncrypt(input.tableName, input.plaintextStructure); //= specification/structured-encryption/encrypt-path-structure.md#calculate-intermediate-encrypted-structured-data //= type=implication @@ -757,12 +690,17 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# in the input [Crypto List](#crypto-list) //# there MUST be an entry with the same [canonical path](./header.md#canonical-path) //# in Intermediate Encrypted Structured Data. - assert forall k <- input.plaintextStructure :: (exists x :: x in canonData && x.origKey == k.key && x.data == k.data); + assert forall k <- input.plaintextStructure :: (exists x :: x in canonData && x.origKey == k.key && x.data == k.data) by { + reveal CanonCryptoMatchesCryptoList(); + reveal CryptoExistsInCanonCrypto(); + } //= specification/structured-encryption/encrypt-path-structure.md#calculate-intermediate-encrypted-structured-data //= type=implication //# There MUST be no other entries in the Intermediate Encrypted Structured Data. - assert |input.plaintextStructure| == |canonData|; + assert |input.plaintextStructure| == |canonData| by { + reveal CanonCryptoMatchesCryptoList(); + } //= specification/structured-encryption/encrypt-path-structure.md#retrieve-encryption-materials //# This operation MUST [calculate the appropriate CMM and encryption context](#create-new-encryption-context-and-cmm). @@ -773,9 +711,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# If no [Crypto Action](./structures.md#crypto-action) is configured to be //# [SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT Crypto Action](./structures.md#sign_and_include_in_encryption_context) //# then the input cmm and encryption context MUST be used unchanged. - if exists x <- plaintextStructure :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT { + if exists x <- input.plaintextStructure :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT { assume {:axiom} input.cmm.Modifies !! {config.materialProviders.History}; - var newEncryptionContext :- GetV2EncryptionContext(plaintextStructure); + var newEncryptionContext :- GetV2EncryptionContext(input.plaintextStructure); if |newEncryptionContext| != 0 { //= specification/structured-encryption/encrypt-path-structure.md#create-new-encryption-context-and-cmm //# An error MUST be returned if any of the entries added to the encryption context in this step @@ -842,77 +780,14 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst :- Need(|canonData| < (UINT32_LIMIT / 3), E("Too many encrypted fields")); // input canonData has all input fields, none encrypted // output canonData has all input fields, some encrypted - assert forall k <- input.plaintextStructure :: (exists x :: x in canonData && x.origKey == k.key); - var encryptedItems : CanonCryptoList :- Crypt.Encrypt(config.primitives, alg, key, head, canonData); - assert forall k <- input.plaintextStructure :: (exists x :: x in encryptedItems && x.origKey == k.key); - - // this assert can be an implication, because it is explicitly ensuring an intermediate state. - assert forall i | 0 <= i < |canonData| :: canonData[i].key == encryptedItems[i].key; + var encryptedItems : CanonCryptoList :- Crypt.Encrypt(config.primitives, alg, key, head, canonData, input.tableName, input.plaintextStructure); - // this assert can be an implication, because it is explicitly ensuring an intermediate state. - assert forall i | 0 <= i < |encryptedItems| :: encryptedItems[i].key == canonData[i].key; - - assert forall x | 0 <= x < |encryptedItems| :: (encryptedItems[x].action == ENCRYPT_AND_SIGN ==> encryptedItems[x].data.typeId == BYTES_TYPE_ID); - assert forall x | 0 <= x < |encryptedItems| :: (encryptedItems[x].action == ENCRYPT_AND_SIGN || encryptedItems[x].data == canonData[x].data); - - // verifies, but it takes too long - assume {:axiom} forall k <- input.plaintextStructure :: - (exists x :: - && x in encryptedItems - && x.origKey == k.key - && Crypt.Updated5(k, x, Crypt.DoEncrypt) - ); + var smallResult : CryptoList := UnCanonEncrypt(encryptedItems, input.tableName, input.plaintextStructure); var footer :- Footer.CreateFooter(config.primitives, mat, encryptedItems, headerSerialized); var footerAttribute := footer.makeTerminal(); - assert forall k <- input.plaintextStructure :: (exists x :: x in encryptedItems && x.origKey == k.key); - var smallResult : CryptoList := UnCanon(encryptedItems); - assert forall k <- input.plaintextStructure :: (exists x :: x in smallResult && x.key == k.key); - assert forall x | 0 <= x < |smallResult| :: (smallResult[x].action == ENCRYPT_AND_SIGN ==> smallResult[x].data.typeId == BYTES_TYPE_ID) by { - assert |smallResult| == |encryptedItems|; - assert forall x | 0 <= x < |smallResult| :: SameUnCanon(encryptedItems[x], smallResult[x]); - assert forall x | 0 <= x < |smallResult| :: (smallResult[x].action == encryptedItems[x].action && smallResult[x].data == encryptedItems[x].data); - assert forall x | 0 <= x < |encryptedItems| :: (encryptedItems[x].action == ENCRYPT_AND_SIGN || encryptedItems[x].data == canonData[x].data); - } - // verifies, but it takes too long - assume {:axiom} forall k <- input.plaintextStructure :: - (exists x :: - && x in smallResult - && x.key == k.key - && Crypt.Updated4(k, x, Crypt.DoEncrypt) - ); - - var headItem := CryptoItem(key := HeaderPath, data := headerAttribute, action := DO_NOTHING); - var footItem := CryptoItem(key := FooterPath, data := footerAttribute, action := DO_NOTHING); - var largeResult := smallResult + [headItem, footItem]; - assert |largeResult| == |smallResult| + 2; - assert largeResult[|largeResult|-2] == headItem; - assert largeResult[|largeResult|-2].key == HeaderPath; - assert largeResult[|largeResult|-1] == footItem; - assert largeResult[|largeResult|-1].key == FooterPath; - assert forall k <- input.plaintextStructure :: (exists x :: x in largeResult && x.key == k.key); - assert forall x | 0 <= x < |largeResult| :: (largeResult[x].action == ENCRYPT_AND_SIGN ==> largeResult[x].data.typeId == BYTES_TYPE_ID) by { - assert forall x | 0 <= x < |smallResult| :: (smallResult[x].action == ENCRYPT_AND_SIGN ==> smallResult[x].data.typeId == BYTES_TYPE_ID); - assert forall x | 0 <= x < |smallResult| :: smallResult[x] == largeResult[x]; - assert forall x | 0 <= x < |smallResult| :: (largeResult[x].action == ENCRYPT_AND_SIGN ==> largeResult[x].data.typeId == BYTES_TYPE_ID); - assert largeResult[|smallResult|] == headItem; - assert largeResult[|smallResult|].key == HeaderPath; - assert largeResult[|smallResult|+1] == footItem; - assert largeResult[|smallResult|+1].key == FooterPath; - assert largeResult[|smallResult|].action == DO_NOTHING; - assert largeResult[|smallResult|+1].action == DO_NOTHING; - assert |largeResult| == |smallResult| + 2; - // verifies, but it takes too long - assume {:axiom} forall x | |smallResult| <= x < |largeResult| :: largeResult[x].action == DO_NOTHING; - } - - assert forall k <- input.plaintextStructure :: - (exists x :: - && x in largeResult - && x.key == k.key - && Crypt.Updated4(k, x, Crypt.DoEncrypt) - ); + var largeResult := AddHeaders(smallResult, headerAttribute, footerAttribute, input.plaintextStructure); var headerAlgorithmSuite :- head.GetAlgorithmSuite(config.materialProviders); var parsedHeader := ParsedHeader ( @@ -926,8 +801,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst encryptedStructure := largeResult, parsedHeader := parsedHeader ); - assert encryptOutput.encryptedStructure[|encryptOutput.encryptedStructure|-1].key == FooterPath; - + assert EncryptPathFinal(input.plaintextStructure, encryptOutput.encryptedStructure); return Success(encryptOutput); } @@ -969,6 +843,41 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst Fail(E("Encryption Context Mismatch\n" + str)) } + method NewCmm(config: InternalConfig, cmm : CMP.ICryptographicMaterialsManager, context : CMP.EncryptionContext) + returns (ret : Result) + requires |context| != 0 + requires ValidInternalConfig?(config) + requires cmm.ValidState() + requires cmm.Modifies !! {config.materialProviders.History} + + modifies ModifiesInternalConfig(config) + modifies cmm.Modifies + + ensures ValidInternalConfig?(config) + ensures cmm.ValidState() + ensures ret.Success? ==> + && ret.value.ValidState() + && fresh(ret.value) + { + + var contextKeysX := SortedSets.ComputeSetToOrderedSequence2(context.Keys, ByteLess); + assert forall k <- contextKeysX :: ValidUTF8Seq(k) by { + assert forall k <- context.Keys :: ValidUTF8Seq(k); + assert forall k <- contextKeysX :: k in context.Keys; + } + var contextKeys : seq := contextKeysX; + + var cmmR := config.materialProviders.CreateRequiredEncryptionContextCMM( + CMP.CreateRequiredEncryptionContextCMMInput( + underlyingCMM := Some(cmm), + keyring := None, + requiredEncryptionContextKeys := contextKeys + ) + ); + var newCmm :- cmmR.MapFailure(e => AwsCryptographyMaterialProviders(e)); + return Success(newCmm); + } + method {:vcs_split_on_every_assert} DecryptStructure (config: InternalConfig, input: DecryptStructureInput) returns (output: Result) { @@ -996,9 +905,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# Decrypt Structure MUST then behave as [Decrypt Path Structure](decrypt-path-structure.md) var pathOutput :- DecryptPathStructure(config, pathInput); - // This should be provable, but I'm not smart enough - assert forall k <- pathInput.encryptedStructure :: |k.key| == 1; - :- Need(forall k <- pathOutput.plaintextStructure :: |k.key| == 1, E("Internal Error")); + assert forall k <- pathOutput.plaintextStructure :: |k.key| == 1 by { + DecryptStructureOutputHasSinglePaths(pathInput.encryptedStructure, pathOutput.plaintextStructure); + } //= specification/structured-encryption/decrypt-structure.md#behavior //= type=implication @@ -1014,10 +923,70 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst return Success(plainOutput); } + //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data + //= type=implication + //# - For every entry in the [input Auth List](#auth-list), other than the header and footer, + //# an entry MUST exist with the same key in the output Crypto List. + lemma AllDecryptPathInputInOutput(origData : AuthList, finalData : CryptoList) + requires DecryptPathFinal(origData, finalData) + ensures forall k <- origData :: (k.key in [HeaderPath, FooterPath]) || exists x :: x in finalData + { + reveal DecryptPathFinal(); + reveal AuthUpdatedCrypto(); + } + + //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data + //= type=implication + //# - For every entry in the output Crypto List + //# an entry MUST exist with the same key in the [input Auth List](#auth-list). + lemma AllDecryptPathOutputInInput(origData : AuthList, finalData : CryptoList) + requires DecryptPathFinal(origData, finalData) + ensures forall k <- finalData :: exists x :: x in origData + { + reveal DecryptPathFinal(); + reveal CryptoUpdatedAuth(); + } + + //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data + //= type=implication + //# If the action is [ENCRYPT_AND_SIGN](./structures.md#encryptandsign) + //# this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) + //# equal to the first two bytes of the input Terminal Data's value, + //# and a value equal to the [decryption](#terminal-data-decryption) of the input Terminal Data's value. + + //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data + //= type=implication + //# Otherwise, this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) and + //# [Terminal Value](./structures.md#terminal-value) equal to the input Terminal Data. + + lemma AllDecryptPathOutputUpdatesInput(origData : AuthList, finalData : CryptoList) + requires DecryptPathFinal(origData, finalData) + ensures forall k <- finalData :: exists x :: + && x in origData + && (k.action != ENCRYPT_AND_SIGN <==> x.data == k.data) + && (k.action == ENCRYPT_AND_SIGN <==> x.data != k.data) + && (k.action == ENCRYPT_AND_SIGN ==> |x.data.value| >= 2 && k.data.typeId == x.data.value[..2]) + { + reveal DecryptPathFinal(); + reveal CryptoUpdatedAuth(); + } + + //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data + //= type=implication + //# - An entry MUST NOT exist with the key "aws_dbe_head" or "aws_dbe_foot". + lemma DecryptPathRemovesHeaders(origData : AuthList, finalData : CryptoList) + requires DecryptPathFinal(origData, finalData) + ensures !exists x :: x in finalData && x.key == HeaderPath + ensures !exists x :: x in finalData && x.key == FooterPath + { + reveal DecryptPathFinal(); + } + method {:vcs_split_on_every_assert} DecryptPathStructure (config: InternalConfig, input: DecryptPathStructureInput) returns (output: Result) ensures output.Success? ==> + && DecryptPathFinal(input.encryptedStructure, output.value.plaintextStructure) && var encRecord : AuthList := input.encryptedStructure; //= specification/structured-encryption/decrypt-path-structure.md#parse-the-header @@ -1059,46 +1028,16 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //# according to the [header format](./header.md). && Header.PartialDeserialize(headerSerialized.value).Success? - //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data - //= type=implication - //# - An entry MUST NOT exist with the key "aws_dbe_head" or "aws_dbe_foot". - && (!exists x :: x in output.value.plaintextStructure && x.key == HeaderPath) - && (!exists x :: x in output.value.plaintextStructure && x.key == FooterPath) - - //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data - //= type=implication - //# - For every entry in the [input Auth List](#auth-list), other than the header and footer, - //# an entry MUST exist with the same key in the output Crypto List. - && (forall k <- input.encryptedStructure | k.key !in HeaderPaths :: - (exists x :: x in output.value.plaintextStructure && x.key == k.key)) - - //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data - //= type=implication - //# - The output Crypto List MUST NOT have any additional entries. - && |output.value.plaintextStructure| == |input.encryptedStructure| - 2 - - //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data - //= type=implication - //# If the action is [ENCRYPT_AND_SIGN](./structures.md#encryptandsign) - //# this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) - //# equal to the first two bytes of the input Terminal Data's value, - //# and a value equal to the [decryption](#terminal-data-decryption) of the input Terminal Data's value. - - //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data + //= specification/structured-encryption/decrypt-path-structure.md#auth-list //= type=implication - //# Otherwise, this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) and - //# [Terminal Value](./structures.md#terminal-value) equal to the input Terminal Data. - && (forall k <- input.encryptedStructure | k.key !in HeaderPaths :: - (exists x :: - && x in output.value.plaintextStructure - && x.key == k.key - && (x.action == ENCRYPT_AND_SIGN ==> |k.data.value| >= 2 && x.data.typeId == k.data.value[..2]) - && (x.action != ENCRYPT_AND_SIGN ==> k.data == x.data) - ) - ) + //# The Auth List MUST NOT contain duplicate Paths. + && AuthListHasNoDuplicatesFromSet(input.encryptedStructure) { :- Need(exists x :: (x in input.encryptedStructure && x.action == SIGN), E("At least one Authenticate Action must be SIGN")); + :- Need(AuthListHasNoDuplicatesFromSet(input.encryptedStructure), E("Duplicate Paths")); + SetSizeImpliesAuthListHasNoDuplicates(input.encryptedStructure); + var headerSerialized :- GetBinary(input.encryptedStructure, HeaderPath); var footerSerialized :- GetBinary(input.encryptedStructure, FooterPath); assert exists x :: x in input.encryptedStructure && x.key == HeaderPath; @@ -1111,11 +1050,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst var headerAlgorithmSuite :- head.GetAlgorithmSuite(config.materialProviders); :- Need(ValidString(input.tableName), E("Bad Table Name")); - var canonData :- CanonizeForDecrypt(input.tableName, input.encryptedStructure, head.legend); - assert forall k <- input.encryptedStructure :: (exists x :: x in canonData && k.key == x.origKey && k.data == x.data); - assert |canonData| == |input.encryptedStructure|; - assert exists x :: x in canonData && x.origKey == HeaderPath; - assert exists x :: x in canonData && x.origKey == FooterPath; + var canonData :- ForDecrypt(input.tableName, input.encryptedStructure, head.legend); assume {:axiom} input.cmm.Modifies !! {config.materialProviders.History}; @@ -1180,6 +1115,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst // parsed in the header. // - Encrypted Data Keys: The [Encrypted Data Keys parsed from the header](./header.md#encrypted-data-keys). + // assert (cmm == input.cmm) || fresh(cmm); var matR := cmm.DecryptMaterials( CMP.DecryptMaterialsInput ( algorithmSuiteId := headerAlgorithmSuite.id, @@ -1227,46 +1163,10 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst //= specification/structured-encryption/decrypt-path-structure.md#verify-signatures //# Decryption MUST fail immediately if verification fails. var _ :- footer.validate(config.primitives, mat, head.dataKeys, canonData, headerSerialized.value); - var decryptedItems : CanonCryptoList :- Crypt.Decrypt(config.primitives, postCMMAlg, key, head, canonData); - assert |decryptedItems| == |input.encryptedStructure|; - assert forall k <- input.encryptedStructure :: (exists x :: x in decryptedItems && x.origKey == k.key); - assert exists x :: x in decryptedItems && x.origKey == HeaderPath; - assert exists x :: x in decryptedItems && x.origKey == FooterPath; - - assert (forall k <- input.encryptedStructure :: - (exists x :: - && x in decryptedItems - && x.origKey == k.key - && Crypt.Updated2(k, x, Crypt.DoDecrypt) - )); - - var largeResult := UnCanon(decryptedItems); - assert |largeResult| == |input.encryptedStructure|; - assert forall k <- input.encryptedStructure :: (exists x :: x in largeResult && x.key == k.key); - assert (forall k <- input.encryptedStructure :: - (exists x :: - && x in largeResult - && x.key == k.key - && Crypt.Updated3(k, x, Crypt.DoDecrypt) - )); - - assert exists x :: x in largeResult && x.key == HeaderPath; - assert exists x :: x in largeResult && x.key == FooterPath; - var smallResult := Seq.Filter((x : CryptoItem) => x.key !in HeaderPaths, largeResult); - reveal Seq.Filter(); - assert !exists x :: x in smallResult && x.key == HeaderPath; - assert !exists x :: x in smallResult && x.key == FooterPath; - // verifies, but it takes too long - assume {:axiom} forall k <- largeResult | k.key !in HeaderPaths :: (exists x :: x in smallResult && x == k); - :- Need(|smallResult| == |input.encryptedStructure| - 2, E("Internal Error.")); - assert |smallResult| == |input.encryptedStructure| - 2; - - assert (forall k <- input.encryptedStructure | k.key !in HeaderPaths :: - (exists x :: - && x in smallResult - && x.key == k.key - && Crypt.Updated3(k, x, Crypt.DoDecrypt) - )); + var decryptedItems : CanonCryptoList :- Crypt.Decrypt(config.primitives, postCMMAlg, key, head, canonData, input.tableName, input.encryptedStructure); + + var largeResult := UnCanonDecrypt(decryptedItems, input.tableName, input.encryptedStructure); + var smallResult := RemoveHeaders(largeResult, input.encryptedStructure); //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data //= type=implication @@ -1284,15 +1184,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst parsedHeader := parsedHeader ); - assert (forall k <- input.encryptedStructure | k.key !in HeaderPaths :: - (exists x :: - && x in smallResult - && x.key == k.key - && (x.action == ENCRYPT_AND_SIGN ==> |k.data.value| >= 2 && x.data.typeId == k.data.value[..2]) - && (x.action != ENCRYPT_AND_SIGN ==> k.data == x.data) - ) - ); - + assert DecryptPathFinal(input.encryptedStructure, decryptOutput.plaintextStructure); output := Success(decryptOutput); } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy new file mode 100644 index 000000000..16c1f3771 --- /dev/null +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy @@ -0,0 +1,823 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy" +include "Util.dfy" +include "Header.dfy" +include "SortCanon.dfy" + +module {:options "/functionSyntax:4" } Canonize { + import opened StructuredEncryptionUtil + import opened Types = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes + import opened Wrappers + import opened StandardLibrary + import opened StandardLibrary.UInt + import Header = StructuredEncryptionHeader + import Paths = StructuredEncryptionPaths + import SortCanon + import Relations + + opaque ghost predicate IsValidPath(path : Path) + { + Paths.ValidPath(path) + } + + datatype EncryptionSelector = DoEncrypt | DoDecrypt + + // Updated return true if the given item has been updated properly for the given operation. + // Updated2..Update5 do exactly the same thing, but with different data types. + ghost predicate Updated(oldVal : CanonCryptoItem, newVal : CanonCryptoItem, mode : EncryptionSelector) + { + && oldVal.key == newVal.key + && oldVal.origKey == newVal.origKey + && oldVal.action == newVal.action + && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) + && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) + && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) + && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + } + + ghost predicate Updated2(oldVal : AuthItem, newVal : CanonCryptoItem, mode : EncryptionSelector) + { + && oldVal.key == newVal.origKey + && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) + && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) + && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) + && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + } + + ghost predicate Updated3(oldVal : AuthItem, newVal : CryptoItem, mode : EncryptionSelector) + { + && oldVal.key == newVal.key + && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) + && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) + && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) + && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + } + + ghost predicate Updated4(oldVal : CryptoItem, newVal : CryptoItem, mode : EncryptionSelector) + { + && oldVal.key == newVal.key + && oldVal.action == newVal.action + && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) + && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) + && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) + && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + } + + ghost predicate Updated5(oldVal : CryptoItem, newVal : CanonCryptoItem, mode : EncryptionSelector) + { + && oldVal.key == newVal.origKey + && oldVal.action == newVal.action + && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) + && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) + && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) + && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + } + + opaque predicate IsCanonPath(table : GoodString, origKey : Path, key : CanonicalPath) + requires IsValidPath(origKey) + { + reveal IsValidPath(); + key == Paths.CanonPath(table, origKey) + } + + opaque function MakeCanon(tableName : GoodString, data : CryptoItem) : (result : CanonCryptoItem) + requires Paths.ValidPath(data.key) + requires IsValidPath(data.key) + ensures result.origKey == data.key + ensures result.data == data.data + ensures result.action == data.action + ensures IsValidPath(result.origKey) + ensures result.key == Paths.CanonPath(tableName, data.key) + ensures IsCanonPath(tableName, data.key, result.key) + ensures IsCanonPath(tableName, result.origKey, result.key) + { + reveal IsValidPath(); + reveal IsCanonPath(); + CanonCryptoItem(Paths.CanonPath(tableName, data.key), data.key, data.data, data.action) + } + + opaque function MakeCanonAuth(tableName : GoodString, data : AuthItem) : (result : CanonAuthItem) + requires Paths.ValidPath(data.key) + requires IsValidPath(data.key) + ensures result.origKey == data.key + ensures result.data == data.data + ensures result.action == data.action + ensures IsValidPath(result.origKey) + ensures result.key == Paths.CanonPath(tableName, data.key) + ensures IsCanonPath(tableName, data.key, result.key) + ensures IsCanonPath(tableName, result.origKey, result.key) + { + reveal IsValidPath(); + reveal IsCanonPath(); + CanonAuthItem(Paths.CanonPath(tableName, data.key), data.key, data.data, data.action) + } + + predicate Same(x : CanonAuthItem, y : CanonCryptoItem) + { + && x.key == y.key + && x.origKey == y.origKey + && x.data == y.data + } + + function MakeCryptoItem(x : CanonAuthItem, action : CryptoAction) : (ret : CanonCryptoItem) + ensures Same(x, ret) + { + CanonCryptoItem(x.key, x.origKey, x.data, action) + } + + function LegendToAction(v : Header.LegendByte) : CryptoAction + { + if v == Header.ENCRYPT_AND_SIGN_LEGEND then + ENCRYPT_AND_SIGN + else if v == Header.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND then + SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT + else + SIGN_ONLY + } + + opaque function {:tailrecursion} ResolveLegend( + fields : CanonAuthList, + legend : Header.Legend, + ghost origFields : CanonAuthList, + acc : CanonCryptoList + ) + : (ret : Result) + requires |fields| + |acc| == |origFields| + requires forall i | 0 <= i < |acc| :: Same(origFields[i], acc[i]) + requires forall i | |acc| <= i < |origFields| :: origFields[i] == fields[i-|acc|] + ensures ret.Success? ==> + && |origFields| == |ret.value| + && forall i | 0 <= i < |origFields| :: Same(origFields[i], ret.value[i]) + { + if |fields| == 0 then + :- Need(|legend| == 0, E("Schema changed : something that was signed is now unsigned.")); + Success(acc) + else if fields[0].action == DO_NOT_SIGN then + ResolveLegend(fields[1..], legend, origFields, acc + [MakeCryptoItem(fields[0], DO_NOTHING)]) + else + :- Need(0 < |legend|, E("Schema changed : something that was unsigned is now signed.")); + ResolveLegend(fields[1..], legend[1..], origFields, acc + [MakeCryptoItem(fields[0], LegendToAction(legend[0]))]) + } + + opaque function ForEncrypt(tableName : GoodString, data : CryptoList) + : (ret : Result) + requires CryptoListHasNoDuplicates(data) + requires !exists x | x in data :: x.key in HeaderPaths + ensures ret.Success? ==> + && CanonCryptoMatchesCryptoList(tableName, data, ret.value) + && IsCryptoSorted(ret.value) + { + reveal IsValidPath(); + :- Need(forall k <- data :: Paths.ValidPath(k.key), E("Invalid Paths")); + var canonList := CryptoToCanonCrypto(tableName, data); + Success(CryptoSort(canonList, tableName, data)) + } + + opaque ghost predicate AuthExistsInCanonAuth(k : AuthItem, list : CanonAuthList) + { + exists x :: x in list && k.key == x.origKey && k.data == x.data && k.action == x.action + } + + opaque ghost predicate AuthExistsInCrypto(k : AuthItem, list : CryptoList) + { + exists x :: x in list && k.key == x.key // && k.data == x.data + } + + opaque ghost predicate CryptoExistsInAuth(k : CryptoItem, list : AuthList) + { + exists x :: x in list && k.key == x.key // && k.data == x.data + } + + opaque ghost predicate AuthExistsInCanonCrypto(k : AuthItem, list : CanonCryptoList) + { + exists x :: x in list && k.key == x.origKey && k.data == x.data + } + + ghost predicate SameStuff1(k : CryptoItem, x : CanonCryptoItem) + { + k.key == x.origKey && k.data == x.data && k.action == x.action + } + + opaque ghost predicate CryptoExistsInCanonCrypto(k : CryptoItem, list : CanonCryptoList) + { + exists x :: x in list && SameStuff1(k, x) + } + + opaque ghost predicate CanonAuthExistsInAuth(k : CanonAuthItem, list : AuthList) + { + exists x :: x in list && k.origKey == x.key && k.data == x.data && k.action == x.action + } + + opaque ghost predicate CanonCryptoExistsInAuth(k : CanonCryptoItem, list : AuthList) + { + exists x :: x in list && k.origKey == x.key && k.data == x.data + } + + opaque ghost predicate CanonCryptoExistsInCrypto(k : CanonCryptoItem, list : CryptoList) + { + exists x :: x in list && k.origKey == x.key && k.data == x.data && k.action == x.action + } + + opaque ghost predicate CanonAuthExistsInCanonAuth(k : CanonAuthItem, list : CanonAuthList) + { + exists x :: x in list && k.origKey == x.origKey && k.data == x.data && k.action == x.action + } + + opaque ghost predicate CanonAuthExistsInCanonCrypto(k : CanonAuthItem, list : CanonCryptoList) + { + exists x :: x in list && k.origKey == x.origKey && k.data == x.data + } + + opaque ghost predicate CanonCryptoExistsInCanonAuth(k : CanonCryptoItem, list : CanonAuthList) + { + exists x :: x in list && k.origKey == x.origKey && k.data == x.data + } + + opaque ghost predicate CanonCryptoExistsInCanonCrypto(k : CanonCryptoItem, list : CanonCryptoList) + { + exists x :: x in list && k.origKey == x.origKey && k.data == x.data && k.action == x.action + } + + opaque ghost predicate CanonAuthMatchesAuthList(tableName : GoodString, data : AuthList, canonList : CanonAuthList) + { + && (exists x :: x in data && x.key == HeaderPath) + && (exists x :: x in data && x.key == FooterPath) + && (forall k <- data :: AuthExistsInCanonAuth(k, canonList)) + && (forall k <- canonList :: CanonAuthExistsInAuth(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.origKey)) + && (forall k <- canonList :: IsCanonPath(tableName, k.origKey, k.key)) + && CanonAuthListHasNoDuplicates(canonList) + } + + opaque ghost predicate CanonCryptoMatchesAuthList(tableName : GoodString, data : AuthList, canonList : CanonCryptoList) + { + && (exists x :: x in data && x.key == HeaderPath) + && (exists x :: x in data && x.key == FooterPath) + && (forall k <- data :: AuthExistsInCanonCrypto(k, canonList)) + && (forall k <- canonList :: CanonCryptoExistsInAuth(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.origKey)) + && (forall k <- canonList :: IsCanonPath(tableName, k.origKey, k.key)) + && CanonCryptoListHasNoDuplicates(canonList) + } + + opaque ghost predicate CanonCryptoUpdatedAuth(k : CanonCryptoItem, list : AuthList) + { + exists x :: x in list && Updated2(x, k, DoDecrypt) + } + + opaque ghost predicate AuthUpdatedCanonCrypto(k : AuthItem, list : CanonCryptoList) + { + exists x :: x in list && Updated2(k, x, DoDecrypt) + } + + opaque ghost predicate CryptoUpdatedAuth(k : CryptoItem, list : AuthList) + { + exists x :: x in list && Updated3(x, k, DoDecrypt) + } + + opaque ghost predicate AuthUpdatedCrypto(k : AuthItem, list : CryptoList) + { + exists x :: x in list && Updated3(k, x, DoDecrypt) + } + + opaque ghost predicate CanonCryptoUpdatedCrypto(k : CanonCryptoItem, list : CryptoList) + { + exists x :: x in list && Updated5(x, k, DoEncrypt) + } + + opaque ghost predicate CryptoUpdatedCanonCrypto(k : CryptoItem, list : CanonCryptoList) + { + exists x :: x in list && Updated5(k, x, DoEncrypt) + } + + opaque ghost predicate NewCryptoUpdatedCrypto(k : CryptoItem, list : CryptoList) + { + exists x :: x in list && Updated4(x, k, DoEncrypt) + } + + opaque ghost predicate CryptoUpdatedNewCrypto(k : CryptoItem, list : CryptoList) + { + exists x :: x in list && Updated4(k, x, DoEncrypt) + } + + opaque ghost predicate CanonCryptoUpdatedAuthList(tableName : GoodString, data : AuthList, canonList : CanonCryptoList) + { + && (exists x :: x in data && x.key == HeaderPath) + && (exists x :: x in data && x.key == FooterPath) + && (forall k <- data :: AuthUpdatedCanonCrypto(k, canonList)) + && (forall k <- canonList :: CanonCryptoUpdatedAuth(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.origKey)) + && (forall k <- canonList :: IsCanonPath(tableName, k.origKey, k.key)) + && CanonCryptoListHasNoDuplicates(canonList) + } + + opaque ghost predicate CryptoUpdatedAuthList(data : AuthList, canonList : CryptoList) + { + && (exists x :: x in data && x.key == HeaderPath) + && (exists x :: x in data && x.key == FooterPath) + && (forall k <- data :: AuthUpdatedCrypto(k, canonList)) + && (forall k <- canonList :: CryptoUpdatedAuth(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.key)) + && CryptoListHasNoDuplicates(canonList) + } + + opaque ghost predicate CryptoMatchesAuthList(tableName : GoodString, data : AuthList, canonList : CryptoList) + { + && (forall k <- data :: AuthExistsInCrypto(k, canonList)) + && (forall k <- canonList :: CryptoExistsInAuth(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.key)) + && CryptoListHasNoDuplicates(canonList) + } + + opaque ghost predicate CanonCryptoMatchesCryptoList(tableName : GoodString, data : CryptoList, canonList : CanonCryptoList) + { + && (!exists x | x in data :: x.key in HeaderPaths) + && (forall k <- data :: CryptoExistsInCanonCrypto(k, canonList)) + && (forall k <- canonList :: CanonCryptoExistsInCrypto(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.origKey)) + && (forall k <- canonList :: IsCanonPath(tableName, k.origKey, k.key)) + && CanonCryptoListHasNoDuplicates(canonList) + } + + opaque ghost predicate CanonCryptoUpdatedCryptoList(tableName : GoodString, data : CryptoList, canonList : CanonCryptoList) + { + && (!exists x | x in data :: x.key in HeaderPaths) + && (forall k <- data :: CryptoUpdatedCanonCrypto(k, canonList)) + && (forall k <- canonList :: CanonCryptoUpdatedCrypto(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.origKey)) + && (forall k <- canonList :: IsCanonPath(tableName, k.origKey, k.key)) + && CanonCryptoListHasNoDuplicates(canonList) + } + + opaque ghost predicate CryptoUpdatedCryptoList(data : CryptoList, canonList : CryptoList) + { + && (!exists x | x in data :: x.key in HeaderPaths) + && (forall k <- data :: CryptoUpdatedNewCrypto(k, canonList)) + && (forall k <- canonList :: NewCryptoUpdatedCrypto(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.key)) + && CryptoListHasNoDuplicates(canonList) + } + + opaque ghost predicate CryptoUpdatedCryptoListHeader(data : CryptoList, canonList : CryptoList) + { + && (forall k <- data :: CryptoUpdatedNewCrypto(k, canonList)) + && (forall k <- canonList :: NewCryptoUpdatedCrypto(k, data)) + && |data| == |canonList| + && (forall k <- canonList :: IsValidPath(k.key)) + && CryptoListHasNoDuplicates(canonList) + } + + + opaque function AuthToCanonAuth(tableName : GoodString, data : AuthList) : (ret : CanonAuthList) + requires forall k <- data :: IsValidPath(k.key) + requires exists x :: x in data && x.key == HeaderPath + requires exists x :: x in data && x.key == FooterPath + requires AuthListHasNoDuplicates(data) + ensures CanonAuthMatchesAuthList(tableName, data, ret) + { + reveal CanonAuthMatchesAuthList(); + reveal Seq.Map(); + reveal IsValidPath(); + var canonList : CanonAuthList := Seq.Map((s : AuthItem) requires IsValidPath(s.key) => MakeCanonAuth(tableName, s), data); + + assert |data| == |canonList|; + assert forall i | 0 <= i < |data| :: canonList[i] == MakeCanonAuth(tableName, data[i]); + assert (forall k <- data :: AuthExistsInCanonAuth(k, canonList)) by { + reveal AuthExistsInCanonAuth(); + } + assert (forall k <- canonList :: CanonAuthExistsInAuth(k, data)) by { + reveal CanonAuthExistsInAuth(); + } + assert (forall k <- canonList :: IsValidPath(k.origKey)); + assert (forall k <- canonList :: IsCanonPath(tableName, k.origKey, k.key)); + assert CanonAuthListHasNoDuplicates(canonList) by { + assert forall i | 0 <= i < |canonList| :: data[i].key == canonList[i].origKey; + } + assert CanonAuthMatchesAuthList(tableName, data, canonList); + canonList + } + + opaque function CryptoToCanonCrypto(tableName : GoodString, data : CryptoList) : (ret : CanonCryptoList) + requires forall k <- data :: IsValidPath(k.key) + requires CryptoListHasNoDuplicates(data) + requires !exists x | x in data :: x.key in HeaderPaths + ensures CanonCryptoMatchesCryptoList(tableName, data, ret) + { + reveal CanonCryptoMatchesCryptoList(); + reveal Seq.Map(); + reveal IsValidPath(); + var canonList : CanonCryptoList := Seq.Map((s : CryptoItem) requires IsValidPath(s.key) => MakeCanon(tableName, s), data); + + assert |data| == |canonList|; + assert forall i | 0 <= i < |data| :: canonList[i] == MakeCanon(tableName, data[i]); + assert (forall k <- data :: CryptoExistsInCanonCrypto(k, canonList)) by { + reveal CryptoExistsInCanonCrypto(); + assert forall k <- data :: exists x :: x in canonList && k.key == x.origKey && k.data == x.data && k.action == x.action; + assert forall k <- data :: exists x :: x in canonList && SameStuff1(k, x); + } + assert (forall k <- canonList :: CanonCryptoExistsInCrypto(k, data)) by { + reveal CanonCryptoExistsInCrypto(); + } + assert (forall k <- canonList :: IsValidPath(k.origKey)); + assert (forall k <- canonList :: IsCanonPath(tableName, k.origKey, k.key)); + assert CanonCryptoListHasNoDuplicates(canonList) by { + assert forall i | 0 <= i < |canonList| :: data[i].key == canonList[i].origKey; + } + assert CanonCryptoMatchesCryptoList(tableName, data, canonList); + canonList + } + + lemma SameMultisetSameStuff(x : seq, y : seq) + requires multiset(x) == multiset(y) + ensures forall k <- x :: k in y + ensures forall k <- y :: k in x + { + assert forall k <- x :: k in multiset(x); + assert forall k <- y :: k in multiset(y); + assert multiset(y) == multiset(x); + } + + opaque function AuthSort(canonList : CanonAuthList, ghost tableName : GoodString, ghost data : AuthList) : (ret : CanonAuthList) + requires forall k <- data :: IsValidPath(k.key) + requires CanonAuthMatchesAuthList(tableName, data, canonList) + ensures CanonAuthMatchesAuthList(tableName, data, ret) + ensures Relations.SortedBy(ret, SortCanon.AuthBelow) + { + reveal CanonAuthMatchesAuthList(); + reveal IsCryptoSorted(); + var canonSorted := SortCanon.AuthSort(canonList); + + assert |data| == |canonSorted|; + + assert forall k <- canonList :: k in canonSorted by { + SameMultisetSameStuff(canonList, canonSorted); + } + + assert forall k <- canonSorted :: k in canonList by { + SameMultisetSameStuff(canonList, canonSorted); + } + + assert (forall k <- canonList :: CanonAuthExistsInCanonAuth(k, canonSorted)) by { + reveal CanonAuthExistsInCanonAuth(); + } + assert (forall k <- canonSorted :: CanonAuthExistsInCanonAuth(k, canonList)) by { + reveal CanonAuthExistsInCanonAuth(); + } + + assert (forall k <- data :: AuthExistsInCanonAuth(k, canonSorted)) by { + reveal AuthExistsInCanonAuth(); + } + assert (forall k <- canonSorted :: CanonAuthExistsInAuth(k, data)); + assert |data| == |canonSorted|; + assert (forall k <- canonSorted :: IsValidPath(k.origKey)); + assert (forall k <- canonSorted :: IsCanonPath(tableName, k.origKey, k.key)); + assert CanonAuthListHasNoDuplicates(canonSorted); + assert CanonAuthMatchesAuthList(tableName, data, canonSorted); + + canonSorted + } + + opaque function CryptoSort(canonList : CanonCryptoList, ghost tableName : GoodString, ghost data : CryptoList) : (ret : CanonCryptoList) + requires forall k <- data :: IsValidPath(k.key) + requires CanonCryptoMatchesCryptoList(tableName, data, canonList) + ensures CanonCryptoMatchesCryptoList(tableName, data, ret) + ensures IsCryptoSorted(ret) + { + reveal CanonCryptoMatchesCryptoList(); + reveal IsCryptoSorted(); + var canonSorted := SortCanon.CryptoSort(canonList); + + assert |data| == |canonSorted|; + + assert forall k <- canonList :: k in canonSorted by { + SameMultisetSameStuff(canonList, canonSorted); + } + + assert forall k <- canonSorted :: k in canonList by { + SameMultisetSameStuff(canonList, canonSorted); + } + + assert (forall k <- canonList :: CanonCryptoExistsInCanonCrypto(k, canonSorted)) by { + reveal CanonCryptoExistsInCanonCrypto(); + } + assert (forall k <- canonSorted :: CanonCryptoExistsInCanonCrypto(k, canonList)) by { + reveal CanonCryptoExistsInCanonCrypto(); + } + + assert (forall k <- data :: CryptoExistsInCanonCrypto(k, canonSorted)) by { + reveal CryptoExistsInCanonCrypto(); + } + assert (forall k <- canonSorted :: CanonCryptoExistsInCrypto(k, data)); + assert |data| == |canonSorted|; + assert (forall k <- canonSorted :: IsValidPath(k.origKey)); + assert (forall k <- canonSorted :: IsCanonPath(tableName, k.origKey, k.key)); + assert CanonCryptoListHasNoDuplicates(canonSorted); + assert CanonCryptoMatchesCryptoList(tableName, data, canonSorted); + + canonSorted + } + + lemma IsValidPathTransfers(canonSorted : CanonAuthList, canonResolved : CanonCryptoList) + requires forall k <- canonSorted :: IsValidPath(k.origKey) + requires |canonSorted| == |canonResolved| + requires forall i | 0 <= i < |canonSorted| :: Same(canonSorted[i], canonResolved[i]) + ensures forall k <- canonResolved :: IsValidPath(k.origKey) + {} + + lemma IsCanonPathTransfers(canonSorted : CanonAuthList, canonResolved : CanonCryptoList, tableName : GoodString) + requires forall k <- canonSorted :: IsValidPath(k.origKey) + requires forall k <- canonSorted :: IsCanonPath(tableName, k.origKey, k.key) + requires |canonSorted| == |canonResolved| + requires forall i | 0 <= i < |canonSorted| :: Same(canonSorted[i], canonResolved[i]) + ensures forall k <- canonResolved :: IsValidPath(k.origKey) + ensures forall k <- canonResolved :: IsCanonPath(tableName, k.origKey, k.key) + {} + + lemma NoDupsTransfers(canonSorted : CanonAuthList, canonResolved : CanonCryptoList) + requires CanonAuthListHasNoDuplicates(canonSorted) + requires |canonSorted| == |canonResolved| + requires forall i | 0 <= i < |canonSorted| :: Same(canonSorted[i], canonResolved[i]) + ensures CanonCryptoListHasNoDuplicates(canonResolved) + {} + + + // This says vcs_split_on_every_assert, because it has many many asserts, each of which is cheap + opaque function {:vcs_split_on_every_assert} + DoResolveLegend(canonSorted : CanonAuthList, legend: Header.Legend, ghost tableName : GoodString, ghost data : AuthList) : (ret : Result) + requires CanonAuthMatchesAuthList(tableName, data, canonSorted) + requires Relations.SortedBy(canonSorted, SortCanon.AuthBelow) + ensures ret.Success? ==> + && CanonCryptoMatchesAuthList(tableName, data, ret.value) + && IsCryptoSorted(ret.value) + { + reveal CanonAuthMatchesAuthList(); + reveal CanonCryptoMatchesAuthList(); + reveal IsCryptoSorted(); + var canonResolved :- ResolveLegend(canonSorted, legend, canonSorted, []); + + assert (forall k <- data :: AuthExistsInCanonCrypto(k, canonResolved)) by { + reveal AuthExistsInCanonCrypto(); + reveal AuthExistsInCanonAuth(); + } + assert (forall k <- canonResolved :: CanonCryptoExistsInAuth(k, data)) by { + reveal CanonCryptoExistsInAuth(); + reveal CanonAuthExistsInAuth(); + reveal AuthExistsInCanonAuth(); + assert forall k <- canonSorted :: CanonAuthExistsInAuth(k, data); + } + assert |data| == |canonResolved|; + assert (forall k <- canonResolved :: IsValidPath(k.origKey)) by { + IsValidPathTransfers(canonSorted, canonResolved); + } + assert (forall k <- canonResolved :: IsCanonPath(tableName, k.origKey, k.key)) by { + IsCanonPathTransfers(canonSorted, canonResolved, tableName); + } + assert CanonCryptoListHasNoDuplicates(canonResolved) by { + NoDupsTransfers(canonSorted, canonResolved); + } + + assert Relations.SortedBy(canonResolved, SortCanon.CryptoBelow) by { + assert Relations.SortedBy(canonSorted, SortCanon.AuthBelow); + SortCanon.AuthSortIsCryptoSort(canonSorted, canonResolved); + } + + assert CanonCryptoMatchesAuthList(tableName, data, canonResolved); + Success(canonResolved) + } + + opaque ghost predicate IsCryptoSorted(list : CanonCryptoList) + { + Relations.SortedBy(list, SortCanon.CryptoBelow) + } + + opaque function ForDecrypt(tableName : GoodString, data : AuthList, legend: Header.Legend) + : (ret : Result) + requires AuthListHasNoDuplicates(data) + requires exists x :: x in data && x.key == HeaderPath + requires exists x :: x in data && x.key == FooterPath + ensures ret.Success? ==> + && CanonCryptoMatchesAuthList(tableName, data, ret.value) + && IsCryptoSorted(ret.value) + { + reveal IsValidPath(); + :- Need(forall k <- data :: Paths.ValidPath(k.key), E("Invalid Paths")); + var canonList := AuthToCanonAuth(tableName, data); + var canonSorted := AuthSort(canonList, tableName, data); + DoResolveLegend(canonSorted, legend, tableName, data) + } + + predicate SameUnCanon(x : CanonCryptoItem, y : CryptoItem) + { + && x.origKey == y.key + && x.data == y.data + && x.action == y.action + } + + function UnCanon(input : CanonCryptoList) : (ret : CryptoList) + ensures + && |ret| == |input| + && (forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i])) + { + if |input| == 0 then + [] + else + var newItem := CryptoItem(key := input[0].origKey, data := input[0].data, action := input[0].action); + assert SameUnCanon(input[0], newItem); + [newItem] + UnCanon(input[1..]) + } + + lemma Update2ImpliesUpdate3() + ensures forall oldVal : AuthItem, x : CanonCryptoItem, y : CryptoItem :: + SameUnCanon(x, y) && Updated2(oldVal, x, DoDecrypt) ==> Updated3(oldVal, y, DoDecrypt) + {} + + lemma Update5ImpliesUpdate4() + ensures forall oldVal : CryptoItem, x : CanonCryptoItem, y : CryptoItem :: + SameUnCanon(x, y) && Updated5(oldVal, x, DoEncrypt) ==> Updated4(oldVal, y, DoEncrypt) + {} + + lemma AuthUpdatedCryptoMaps(origData : AuthList, input : CanonCryptoList, output : CryptoList) + requires |input| == |output| + requires forall k <- origData :: AuthUpdatedCanonCrypto(k, input) + requires forall i | 0 <= i < |input| :: SameUnCanon(input[i], output[i]) + ensures forall k <- origData :: AuthUpdatedCrypto(k, output) + { + reveal AuthUpdatedCanonCrypto(); + reveal AuthUpdatedCrypto(); + assert forall k <- origData :: exists x :: x in output && Updated3(k, x, DoDecrypt) by { + Update2ImpliesUpdate3(); + } + } + + // command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false} + lemma {:vcs_split_on_every_assert false} InputIsInput(origData : AuthList, input : CanonCryptoList) + requires forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt) + ensures forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt) + { + assert forall i | 0 <= i < |input| :: input[i] in input; + forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) { + var x :| x in origData && Updated2(x, input[i], DoDecrypt); + } + } + + // command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false} + lemma {:vcs_split_on_every_assert false} InputIsInput2(origData : CryptoList, input : CanonCryptoList) + requires forall val <- input :: exists x :: x in origData && Updated5(x, val, DoEncrypt) + ensures forall i | 0 <= i < |input| :: exists x :: x in origData && Updated5(x, input[i], DoEncrypt) + { + assert forall i | 0 <= i < |input| :: input[i] in input; + forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated5(x, input[i], DoEncrypt) { + var x :| x in origData && Updated5(x, input[i], DoEncrypt); + } + } + + lemma CryptoUpdatedAuthMaps(origData : AuthList, input : CanonCryptoList, output : CryptoList) + requires |input| == |output| + requires forall k <- input :: CanonCryptoUpdatedAuth(k, origData) + requires forall i | 0 <= i < |input| :: SameUnCanon(input[i], output[i]) + ensures forall k <- output :: CryptoUpdatedAuth(k, origData) + { + reveal CanonCryptoUpdatedAuth(); + reveal CryptoUpdatedAuth(); + assert forall k <- output :: exists x :: x in origData && Updated3(x, k, DoDecrypt) by { + Update2ImpliesUpdate3(); + assert forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt); + assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt) by { + InputIsInput(origData, input); + } + assert forall newVal <- output :: exists x :: x in origData && Updated3(x, newVal, DoDecrypt); + } + } + + function UnCanonDecrypt(input : CanonCryptoList, ghost tableName : GoodString, ghost origData : AuthList) + : (ret : CryptoList) + requires CanonCryptoUpdatedAuthList(tableName, origData, input) + ensures CryptoUpdatedAuthList(origData, ret) + { + reveal CanonCryptoUpdatedAuthList(); + reveal CryptoUpdatedAuthList(); + + var results := UnCanon(input); + assert (forall k <- origData :: AuthUpdatedCrypto(k, results)) by { + AuthUpdatedCryptoMaps(origData, input, results); + } + assert (forall k <- results :: CryptoUpdatedAuth(k, origData)) by { + CryptoUpdatedAuthMaps(origData, input, results); + } + results + } + + lemma CryptoUpdatedCryptoMaps(origData : CryptoList, input : CanonCryptoList, output : CryptoList) + requires |input| == |output| + requires forall k <- origData :: CryptoUpdatedCanonCrypto(k, input) + requires forall i | 0 <= i < |input| :: SameUnCanon(input[i], output[i]) + ensures forall k <- origData :: CryptoUpdatedNewCrypto(k, output) + { + reveal CryptoUpdatedCanonCrypto(); + reveal CryptoUpdatedNewCrypto(); + assert forall k <- origData :: exists x :: x in output && Updated4(k, x, DoEncrypt) by { + Update5ImpliesUpdate4(); + } + } + + lemma CryptoUpdatedCryptoMaps2(origData : CryptoList, input : CanonCryptoList, output : CryptoList) + requires |input| == |output| + requires forall k <- input :: CanonCryptoUpdatedCrypto(k, origData) + requires forall i | 0 <= i < |input| :: SameUnCanon(input[i], output[i]) + ensures forall k <- output :: NewCryptoUpdatedCrypto(k, origData) + { + assert forall i | 0 <= i < |input| :: input[i] in input; + assert forall i | 0 <= i < |output| :: output[i] in output; + forall i | 0 <= i < |output| ensures NewCryptoUpdatedCrypto(output[i], origData) { + reveal CanonCryptoUpdatedCrypto(); + reveal NewCryptoUpdatedCrypto(); + Update5ImpliesUpdate4(); + } + } + + function UnCanonEncrypt(input : CanonCryptoList, ghost tableName : GoodString, ghost origData : CryptoList) + : (ret : CryptoList) + requires CanonCryptoUpdatedCryptoList(tableName, origData, input) + ensures CryptoUpdatedCryptoList(origData, ret) + { + reveal CanonCryptoUpdatedCryptoList(); + reveal CryptoUpdatedCryptoList(); + + var results := UnCanon(input); + assert forall k <- origData :: CryptoUpdatedNewCrypto(k, results) by { + CryptoUpdatedCryptoMaps(origData, input, results); + } + assert forall k <- results :: NewCryptoUpdatedCrypto(k, origData) by { + CryptoUpdatedCryptoMaps2(origData, input, results); + } + results + } + + opaque ghost predicate EncryptPathFinal(origData : CryptoList, finalData : CryptoList) + { + && |finalData| == |origData| + 2 + && CryptoUpdatedCryptoListHeader(origData, finalData[..(|finalData|-2)]) + && finalData[|finalData|-2].key == HeaderPath + && finalData[|finalData|-1].key == FooterPath + } + + opaque function AddHeaders(input : CryptoList, headerData : StructuredDataTerminal, footerData : StructuredDataTerminal, ghost origData : CryptoList) + : (ret : CryptoList) + requires CryptoUpdatedCryptoList(origData, input) + ensures EncryptPathFinal(origData, ret) + { + reveal EncryptPathFinal(); + reveal CryptoUpdatedCryptoList(); + reveal CryptoUpdatedCryptoListHeader(); + var headItem := Types.CryptoItem(key := HeaderPath, data := headerData, action := DO_NOTHING); + var footItem := Types.CryptoItem(key := FooterPath, data := footerData, action := DO_NOTHING); + var largeResult := input + [headItem, footItem]; + largeResult + } + + opaque ghost predicate DecryptPathFinal(origData : AuthList, finalData : CryptoList) + { + && (!exists x :: x in finalData && x.key == HeaderPath) + && (!exists x :: x in finalData && x.key == FooterPath) + && (forall k <- origData :: (k.key in [HeaderPath, FooterPath]) || AuthUpdatedCrypto(k, finalData)) + && (forall k <- finalData :: CryptoUpdatedAuth(k, origData)) + && (forall k <- finalData :: IsValidPath(k.key)) + && CryptoListHasNoDuplicates(finalData) + } + + opaque function RemoveHeaderPaths(xs : CryptoList) : (ret : CryptoList) + requires CryptoListHasNoDuplicates(xs) + ensures !exists x :: x in ret && x.key in [HeaderPath, FooterPath] + ensures !exists x :: x in ret && x.key == HeaderPath + ensures !exists x :: x in ret && x.key == FooterPath + ensures forall x <- ret :: x in xs + ensures forall x <- xs :: x.key in [HeaderPath, FooterPath] || x in ret + ensures CryptoListHasNoDuplicates(ret) + { + if |xs| == 0 then [] + else (if xs[0].key in [HeaderPath, FooterPath] then [] else [xs[0]]) + RemoveHeaderPaths(xs[1..]) + } + + opaque function RemoveHeaders(input : CryptoList, ghost origData : AuthList) + : (ret : CryptoList) + requires CryptoUpdatedAuthList(origData, input) + + ensures DecryptPathFinal(origData, ret) + { + reveal CryptoUpdatedAuthList(); + reveal DecryptPathFinal(); + reveal AuthUpdatedCrypto(); + var finalData := RemoveHeaderPaths(input); + assert forall k <- origData :: (k.key in [HeaderPath, FooterPath]) || AuthUpdatedCrypto(k, finalData); + finalData + } +} diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy index 9a3690367..dca910df0 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy @@ -6,6 +6,8 @@ include "../../../../submodules/MaterialProviders/AwsCryptographyPrimitives/src/ include "Header.dfy" include "Util.dfy" +include "SortCanon.dfy" +include "Canonize.dfy" module StructuredEncryptionCrypt { import opened Wrappers @@ -23,6 +25,9 @@ module StructuredEncryptionCrypt { import HKDF import AesKdfCtr import Seq + import SortCanon + // import Relations + import opened Canonize function method FieldKey(HKDFOutput : Bytes, offset : uint32) : (ret : Result) @@ -125,57 +130,45 @@ module StructuredEncryptionCrypt { return commitKey.MapFailure(e => AwsCryptographyPrimitives(e)); } - datatype EncryptionSelector = DoEncrypt | DoDecrypt - - // Updated return true if the given item has been updated properly for the given operation. - // Updated2..Update5 do exactly the same thing, but with different data types. - predicate Updated(oldVal : CanonCryptoItem, newVal : CanonCryptoItem, mode : EncryptionSelector) + lemma EncryptDataUpdated(origData : CryptoList, data : CanonCryptoList, finalData : CanonCryptoList) + requires forall k <- origData :: CryptoExistsInCanonCrypto(k, data) + requires |finalData| == |origData| == |data| + requires (forall i | 0 <= i < |origData| :: Updated(data[i], finalData[i], DoEncrypt)) + ensures forall k <- origData :: CryptoUpdatedCanonCrypto(k, finalData) { - && oldVal.key == newVal.key - && oldVal.origKey == newVal.origKey - && oldVal.action == newVal.action - && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) - && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) - && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) - && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + reveal CryptoExistsInCanonCrypto(); + reveal CryptoUpdatedCanonCrypto(); + assert forall oldVal <- origData :: exists i :: 0 <= i < |finalData| && Updated5(oldVal, finalData[i], DoEncrypt); + assert forall oldVal <- origData :: exists x :: x in finalData && Updated5(oldVal, x, DoEncrypt); } - predicate Updated2(oldVal : AuthItem, newVal : CanonCryptoItem, mode : EncryptionSelector) + lemma EncryptFinalUpdated(origData : CryptoList, data : CanonCryptoList, finalData : CanonCryptoList) + requires forall k <- data :: CanonCryptoExistsInCrypto(k, origData) + requires |finalData| == |origData| == |data| + requires forall i | 0 <= i < |origData| :: Updated(data[i], finalData[i], DoEncrypt) + ensures forall k <- finalData :: CanonCryptoUpdatedCrypto(k, origData) { - && oldVal.key == newVal.origKey - && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) - && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) - && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) - && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + reveal CanonCryptoExistsInCrypto(); + reveal CanonCryptoUpdatedCrypto(); + assert forall val <- data :: exists x :: x in origData && x.key == val.origKey && x.data == val.data && x.action == val.action; + assert forall newVal <- finalData :: exists x :: x in origData && Updated5(x, newVal, DoEncrypt); } - predicate Updated3(oldVal : AuthItem, newVal : CryptoItem, mode : EncryptionSelector) + lemma EncryptMaintains(tableName : GoodString, origData : CryptoList, data : CanonCryptoList, finalData : CanonCryptoList) + requires CanonCryptoMatchesCryptoList(tableName, origData, data) + requires |finalData| == |data| + requires (forall i | 0 <= i < |data| :: Updated(data[i], finalData[i], DoEncrypt)) + ensures CanonCryptoUpdatedCryptoList(tableName, origData, finalData) { - && oldVal.key == newVal.key - && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) - && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) - && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) - && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) - } - - predicate Updated4(oldVal : CryptoItem, newVal : CryptoItem, mode : EncryptionSelector) - { - && oldVal.key == newVal.key - && oldVal.action == newVal.action - && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) - && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) - && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) - && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) - } + reveal CanonCryptoMatchesCryptoList(); + reveal CanonCryptoUpdatedCryptoList(); - predicate Updated5(oldVal : CryptoItem, newVal : CanonCryptoItem, mode : EncryptionSelector) - { - && oldVal.key == newVal.origKey - && oldVal.action == newVal.action - && (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data) - && (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data) - && (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID)) - && (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2])) + assert forall k <- origData :: CryptoUpdatedCanonCrypto(k, finalData) by { + EncryptDataUpdated(origData, data, finalData); + } + assert forall k <- finalData :: CanonCryptoUpdatedCrypto(k, origData) by { + EncryptFinalUpdated(origData, data, finalData); + } } // Encrypt a StructuredDataMap @@ -184,9 +177,13 @@ module StructuredEncryptionCrypt { alg : CMP.AlgorithmSuiteInfo, key : Key, head : Header.PartialHeader, - data : CanonCryptoList) + data : CanonCryptoList, + ghost tableName : GoodString, + ghost origData : CryptoList) returns (ret : Result) requires ValidSuite(alg) + requires IsCryptoSorted(data) + requires CanonCryptoMatchesCryptoList(tableName, origData, data) modifies client.Modifies requires client.ValidState() @@ -194,8 +191,57 @@ module StructuredEncryptionCrypt { ensures ret.Success? ==> && |ret.value| == |data| && (forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], DoEncrypt)) + && CanonCryptoListHasNoDuplicates(ret.value) + && IsCryptoSorted(ret.value) + && CanonCryptoUpdatedCryptoList(tableName, origData, ret.value) + { + reveal CanonCryptoMatchesCryptoList(); + var result :- Crypt(DoEncrypt, client, alg, key, head, data); + assert CanonCryptoUpdatedCryptoList(tableName, origData, result) by { + EncryptMaintains(tableName, origData, data, result); + } + return Success(result); + } + + lemma DecryptDataUpdated(origData : AuthList, data : CanonCryptoList, finalData : CanonCryptoList) + requires forall k <- origData :: AuthExistsInCanonCrypto(k, data) + requires |finalData| == |origData| == |data| + requires (forall i | 0 <= i < |origData| :: Updated(data[i], finalData[i], DoDecrypt)) + ensures forall k <- origData :: AuthUpdatedCanonCrypto(k, finalData) + { + reveal AuthExistsInCanonCrypto(); + reveal AuthUpdatedCanonCrypto(); + assert forall oldVal <- origData :: exists i :: 0 <= i < |finalData| && Updated2(oldVal, finalData[i], DoDecrypt); + assert forall oldVal <- origData :: exists x :: x in finalData && Updated2(oldVal, x, DoDecrypt); + } + + lemma DecryptFinalUpdated(origData : AuthList, data : CanonCryptoList, finalData : CanonCryptoList) + requires forall k <- data :: CanonCryptoExistsInAuth(k, origData) + requires |finalData| == |origData| == |data| + requires (forall i | 0 <= i < |origData| :: Updated(data[i], finalData[i], DoDecrypt)) + ensures forall k <- finalData :: CanonCryptoUpdatedAuth(k, origData) { - ret := Crypt(DoEncrypt, client, alg, key, head, data); + reveal CanonCryptoExistsInAuth(); + reveal CanonCryptoUpdatedAuth(); + assert forall val <- data :: exists x :: x in origData && x.key == val.origKey && x.data == val.data; + assert forall newVal <- finalData :: exists x :: x in origData && Updated2(x, newVal, DoDecrypt); + } + + lemma DecryptMaintains(tableName : GoodString, origData : AuthList, data : CanonCryptoList, finalData : CanonCryptoList) + requires CanonCryptoMatchesAuthList(tableName, origData, data) + requires |finalData| == |data| + requires (forall i | 0 <= i < |data| :: Updated(data[i], finalData[i], DoDecrypt)) + ensures CanonCryptoUpdatedAuthList(tableName, origData, finalData) + { + reveal CanonCryptoMatchesAuthList(); + reveal CanonCryptoUpdatedAuthList(); + + assert forall k <- origData :: AuthUpdatedCanonCrypto(k, finalData) by { + DecryptDataUpdated(origData, data, finalData); + } + assert forall k <- finalData :: CanonCryptoUpdatedAuth(k, origData) by { + DecryptFinalUpdated(origData, data, finalData); + } } // Decrypt a StructuredDataMap @@ -204,18 +250,40 @@ module StructuredEncryptionCrypt { alg : CMP.AlgorithmSuiteInfo, key : Key, head : Header.PartialHeader, - data : CanonCryptoList) + data : CanonCryptoList, + ghost tableName : GoodString, + ghost origData : AuthList) returns (ret : Result) requires ValidSuite(alg) + requires IsCryptoSorted(data) + requires CanonCryptoMatchesAuthList(tableName, origData, data) modifies client.Modifies requires client.ValidState() ensures client.ValidState() ensures ret.Success? ==> && |ret.value| == |data| - && forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], DoDecrypt) + && (forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], DoDecrypt)) + && IsCryptoSorted(ret.value) + && CanonCryptoUpdatedAuthList(tableName, origData, ret.value) + { + reveal CanonCryptoMatchesAuthList(); + var result :- Crypt(DoDecrypt, client, alg, key, head, data); + assert CanonCryptoUpdatedAuthList(tableName, origData, result) by { + DecryptMaintains(tableName, origData, data, result); + } + return Success(result); + } + + lemma MaintainSorted(data : CanonCryptoList, result : CanonCryptoList, mode : EncryptionSelector) + requires IsCryptoSorted(data) + requires |result| == |data| + requires forall i | 0 <= i < |data| :: Updated(data[i], result[i], mode) + ensures IsCryptoSorted(result) { - ret := Crypt(DoDecrypt, client, alg, key, head, data); + reveal IsCryptoSorted(); + assert forall i | 0 <= i < |data| :: data[i].key == result[i].key; + SortCanon.SortedIsSorted(data, result); } // Encrypt or Decrypt a StructuredDataMap @@ -228,6 +296,8 @@ module StructuredEncryptionCrypt { data : CanonCryptoList) returns (ret : Result) requires ValidSuite(alg) + requires CanonCryptoListHasNoDuplicates(data) + requires IsCryptoSorted(data) ensures ret.Success? ==> //= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce @@ -263,6 +333,8 @@ module StructuredEncryptionCrypt { ensures ret.Success? ==> && |ret.value| == |data| && (forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], mode)) + && CanonCryptoListHasNoDuplicates(ret.value) + && IsCryptoSorted(ret.value) { //= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce //# The `FieldRootKey` MUST be generated with the plaintext data key in the encryption materials @@ -283,8 +355,13 @@ module StructuredEncryptionCrypt { //# The calculated Field Root MUST have length equal to the //# [algorithm suite's encryption key length](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/algorithm-suites.md#algorithm-suites-encryption-settings). assert |fieldRootKey| == AlgorithmSuites.GetEncryptKeyLength(alg) as int; - var result := CryptList(mode, client, alg, fieldRootKey, data); - return result; + var result :- CryptList(mode, client, alg, fieldRootKey, data); + + assert IsCryptoSorted(result) by { + MaintainSorted(data, result, mode); + } + + return Success(result); } // Encrypt or Decrypt each entry in keys, putting results in output diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy index f7d5d33a0..f5b8bba4e 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy @@ -34,6 +34,12 @@ module StructuredEncryptionPaths { [member(StructureSegment(key := x))] } + lemma StringToUniPathUnique() + ensures forall x : string, y : string + :: x != y ==> StringToUniPath(x) != StringToUniPath(y) + { + } + function method UniPathToString(x : Path) : Result requires |x| == 1 { diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy index db2fb2797..1fb2832cb 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy @@ -5,13 +5,16 @@ include "../Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy" include "Util.dfy" module SortCanon { - export provides + export + provides AuthSort, CryptoSort, AuthBelow, CryptoBelow, StructuredEncryptionUtil, - Relations + Relations, + AuthSortIsCryptoSort, + SortedIsSorted import opened Wrappers import opened StandardLibrary @@ -28,6 +31,20 @@ module SortCanon { Below(x.key, y.key) } + lemma SameBelow2(x1 : CanonAuthItem, x2 : CanonAuthItem, y1 : CanonCryptoItem, y2 : CanonCryptoItem) + requires x1.key == y1.key + requires x2.key == y2.key + ensures AuthBelow(x1, x2) == CryptoBelow(y1, y2) + {} + + lemma SameBelow() + ensures forall x1 : CanonAuthItem, x2 : CanonAuthItem, y1 : CanonCryptoItem, y2 : CanonCryptoItem + | x1.key == y1.key && x2.key == y2.key + :: AuthBelow(x1, x2) == CryptoBelow(y1, y2) + { + + } + lemma AuthBelowIsReflexive(x: CanonAuthItem) ensures AuthBelow(x, x) { @@ -185,21 +202,109 @@ module SortCanon { { } - function method AuthSort(x : seq) : (result : seq) + lemma AuthSortIsCryptoSort(x : CanonAuthList, y : CanonCryptoList) + requires SortedBy(x, AuthBelow) + requires |x| == |y| + requires forall i | 0 <= i < |x| :: x[i].key == y[i].key + ensures SortedBy(y, CryptoBelow) + {} + + lemma SortedIsSorted(x : CanonCryptoList, y : CanonCryptoList) + requires SortedBy(x, CryptoBelow) + requires |x| == |y| + requires forall i | 0 <= i < |x| :: x[i].key == y[i].key + ensures SortedBy(y, CryptoBelow) + {} + + + function method AuthSort(x : CanonAuthList) : (result : CanonAuthList) + requires CanonAuthListHasNoDuplicates(x) ensures multiset(x) == multiset(result) ensures SortedBy(result, AuthBelow) + ensures CanonAuthListHasNoDuplicates(result) { AuthBelowIsTotal(); - MergeSortBy(x, AuthBelow) + var ret := MergeSortBy(x, AuthBelow); + CanonAuthListMultiNoDup(x, ret); + assert CanonAuthListHasNoDuplicates(ret); + ret } - function method CryptoSort(x : seq) : (result : seq) + function method CryptoSort(x : CanonCryptoList) : (result : CanonCryptoList) + requires CanonCryptoListHasNoDuplicates(x) ensures multiset(x) == multiset(result) + ensures multiset(result) == multiset(x) ensures SortedBy(result, CryptoBelow) + ensures CanonCryptoListHasNoDuplicates(result) { CryptoBelowIsTotal(); - MergeSortBy(x, CryptoBelow) + var ret := MergeSortBy(x, CryptoBelow); + CanonCryptoListMultiNoDup(x, ret); + assert CanonCryptoListHasNoDuplicates(ret); + ret } + lemma MultisetHasNoDuplicates(xs: CanonCryptoList) + requires CanonCryptoListHasNoDuplicates(xs) + ensures forall x | x in multiset(xs) :: multiset(xs)[x] == 1 + { + if |xs| == 0 { + } else { + assert xs == Seq.DropLast(xs) + [Seq.Last(xs)]; + assert Seq.Last(xs) !in Seq.DropLast(xs); + assert CanonCryptoListHasNoDuplicates(Seq.DropLast(xs)); + MultisetHasNoDuplicates(Seq.DropLast(xs)); + } + } + lemma MultisetHasNoDuplicates2(xs: CanonAuthList) + requires CanonAuthListHasNoDuplicates(xs) + ensures forall x | x in multiset(xs) :: multiset(xs)[x] == 1 + { + if |xs| == 0 { + } else { + assert xs == Seq.DropLast(xs) + [Seq.Last(xs)]; + assert Seq.Last(xs) !in Seq.DropLast(xs); + assert CanonAuthListHasNoDuplicates(Seq.DropLast(xs)); + MultisetHasNoDuplicates2(Seq.DropLast(xs)); + } + } + lemma CanonCryptoListMultiNoDup(a: CanonCryptoList, b: CanonCryptoList) + requires CanonCryptoListHasNoDuplicates(a) && multiset(a) == multiset(b) + ensures CanonCryptoListHasNoDuplicates(b) + { + forall i,j | 0 <= i < j < |b| + ensures b[i].origKey != b[j].origKey + { + assert b[i] in multiset(a); + assert b[j] in multiset(a); + if b[i] == b[j] { + assert b[i].origKey == b[j].origKey; + MultisetHasNoDuplicates(a); + assert multiset(b)[b[i]] == 1; + assert b == b[..i] + [b[i]] + b[i+1..j] + [b[j]] + b[j+1..]; + } else { + assert b[i].origKey != b[j].origKey; + } + } + } + lemma CanonAuthListMultiNoDup(a: CanonAuthList, b: CanonAuthList) + requires CanonAuthListHasNoDuplicates(a) && multiset(a) == multiset(b) + ensures CanonAuthListHasNoDuplicates(b) + { + forall i,j | 0 <= i < j < |b| + ensures b[i].origKey != b[j].origKey + { + assert b[i] in multiset(a); + assert b[j] in multiset(a); + if b[i] == b[j] { + assert b[i].origKey == b[j].origKey; + MultisetHasNoDuplicates2(a); + assert multiset(b)[b[i]] == 1; + assert b == b[..i] + [b[i]] + b[i+1..j] + [b[j]] + b[j+1..]; + } else { + assert b[i].origKey != b[j].origKey; + } + } + } } \ No newline at end of file diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy index 0d3a721f5..fecdcad0a 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy @@ -15,6 +15,7 @@ module StructuredEncryptionUtil { import AlgorithmSuites import SortedSets import Base64 + import opened Seq // all attributes with this prefix reserved for the implementation const ReservedPrefix := "aws_dbe_" @@ -23,6 +24,7 @@ module StructuredEncryptionUtil { const FooterField := ReservedPrefix + "foot" const HeaderPath : Path := [member(StructureSegment(key := HeaderField))] const FooterPath : Path := [member(StructureSegment(key := FooterField))] + const HeaderPaths : seq := [HeaderPath, FooterPath] const ReservedCryptoContextPrefixString := "aws-crypto-" const ReservedCryptoContextPrefixUTF8 := UTF8.EncodeAscii(ReservedCryptoContextPrefixString) @@ -57,6 +59,60 @@ module StructuredEncryptionUtil { type CanonCryptoList = seq type CanonAuthList = seq + function method CryptoListToSet(xs: CryptoList) : (ret : set) + ensures |xs| == 0 ==> |ret| == 0 + ensures |xs| == 1 ==> ret == {xs[0].key} + ensures |xs| == 1 ==> |ret| == 1 + { + set k <- xs :: k.key + } + + function method CanonCryptoListToSet(xs: CanonCryptoList) : (ret : set) + ensures |xs| == 0 ==> |ret| == 0 + ensures |xs| == 1 ==> ret == {xs[0].origKey} + ensures |xs| == 1 ==> |ret| == 1 + { + set k <- xs :: k.origKey + } + + function method AuthListToSet(xs: AuthList) : (ret : set) + ensures |xs| == 0 ==> |ret| == 0 + ensures |xs| == 1 ==> ret == {xs[0].key} + ensures |xs| == 1 ==> |ret| == 1 + { + set k <- xs :: k.key + } + + predicate method CryptoListHasNoDuplicatesFromSet(xs: CryptoList) + { + |CryptoListToSet(xs)| == |xs| + } + + predicate method AuthListHasNoDuplicatesFromSet(xs: AuthList) + { + |AuthListToSet(xs)| == |xs| + } + + predicate CryptoListHasNoDuplicates(xs: CryptoList) + { + forall i, j :: 0 <= i < j < |xs| ==> xs[i].key != xs[j].key + } + + predicate AuthListHasNoDuplicates(xs: AuthList) + { + forall i, j :: 0 <= i < j < |xs| ==> xs[i].key != xs[j].key + } + + predicate CanonCryptoListHasNoDuplicates(xs: CanonCryptoList) + { + forall i, j :: 0 <= i < j < |xs| ==> xs[i].origKey != xs[j].origKey + } + + predicate CanonAuthListHasNoDuplicates(xs: CanonAuthList) + { + forall i, j :: 0 <= i < j < |xs| ==> xs[i].origKey != xs[j].origKey + } + //= specification/structured-encryption/encrypt-path-structure.md#header-field //= type=implication //# The Header Field name MUST be `aws_dbe_head` @@ -249,4 +305,95 @@ module StructuredEncryptionUtil { Success(StructuredDataTerminal(value := serializedValue, typeId := typeId)) } + lemma CryptoListNoDupFromMap(xs: seq) + requires HasNoDuplicates(Map((x: CryptoItem) => x.key, xs)) + ensures CryptoListHasNoDuplicates(xs) + { + var ys := Map((x: CryptoItem) => x.key, xs); + assert forall i, j | 0 <= i < j < |xs| :: ys[i] != ys[j] by { + reveal HasNoDuplicates(); + } + assert forall i | 0 <= i < |xs| :: ys[i] == xs[i].key; + } + + lemma AuthListNoDupFromMap(xs: seq) + requires HasNoDuplicates(Map((x: AuthItem) => x.key, xs)) + ensures AuthListHasNoDuplicates(xs) + { + var ys := Map((x: AuthItem) => x.key, xs); + assert forall i, j | 0 <= i < j < |xs| :: ys[i] != ys[j] by { + reveal HasNoDuplicates(); + } + assert forall i | 0 <= i < |xs| :: ys[i] == xs[i].key; + } + + lemma CryptoListCard(xs: seq) + ensures |ToSet(Map((x: CryptoItem) => x.key, xs))| == |CryptoListToSet(xs)| + { + reveal ToSet(); + var ys := Map((x: CryptoItem) => x.key, xs); + forall x ensures x in ToSet(ys) <==> x in CryptoListToSet(xs) { + assert x in ToSet(ys) ==> x in CryptoListToSet(xs); + assert x in CryptoListToSet(xs) ==> x in ToSet(ys) by { + if x in CryptoListToSet(xs) { + var i :| 0 <= i < |xs| && xs[i].key == x; + assert ys[i] == x by { + calc == { + ys[i]; + Map((x: CryptoItem) => x.key, xs)[i]; + xs[i].key; + x; + } + } + } else {} + } + } + assert ToSet(ys) == CryptoListToSet(xs); + } + + lemma AuthListCard(xs: seq) + ensures |ToSet(Map((x: AuthItem) => x.key, xs))| == |AuthListToSet(xs)| + { + reveal ToSet(); + var ys := Map((x: AuthItem) => x.key, xs); + forall x ensures x in ToSet(ys) <==> x in AuthListToSet(xs) { + assert x in ToSet(ys) ==> x in AuthListToSet(xs); + assert x in AuthListToSet(xs) ==> x in ToSet(ys) by { + if x in AuthListToSet(xs) { + var i :| 0 <= i < |xs| && xs[i].key == x; + assert ys[i] == x by { + calc == { + ys[i]; + Map((x: AuthItem) => x.key, xs)[i]; + xs[i].key; + x; + } + } + } else {} + } + } + assert ToSet(ys) == AuthListToSet(xs); + } + + lemma SetSizeImpliesCryptoListHasNoDuplicates(xs: seq) + requires CryptoListHasNoDuplicatesFromSet(xs) + ensures CryptoListHasNoDuplicates(xs) + { + var ys := Map((x: CryptoItem) => x.key, xs); + CryptoListCard(xs); + LemmaNoDuplicatesCardinalityOfSet(ys); + CryptoListNoDupFromMap(xs); + } + + lemma SetSizeImpliesAuthListHasNoDuplicates(xs: seq) + requires AuthListHasNoDuplicatesFromSet(xs) + ensures AuthListHasNoDuplicates(xs) + { + var ys := Map((x: AuthItem) => x.key, xs); + AuthListCard(xs); + LemmaNoDuplicatesCardinalityOfSet(ys); + AuthListNoDupFromMap(xs); + } + + } diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy index 5533fa7e7..60242e1e1 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy @@ -19,6 +19,7 @@ module TestHeader { import opened UTF8 import Aws.Cryptography.Primitives import AlgorithmSuites + import Canonize method {:test} TestRoundTrip() { var head := PartialHeader ( @@ -136,7 +137,7 @@ module TestHeader { MakeCrypto("pqr", DO_NOTHING) ]; var tableName : GoodString := "name"; - var canonSchema :- expect OPS.CanonizeForEncrypt(tableName, schemaMap); + var canonSchema :- expect Canonize.ForEncrypt(tableName, schemaMap); var legend :- expect MakeLegend(canonSchema); //= specification/structured-encryption/header.md#encrypt-legend-bytes //= type=test @@ -158,7 +159,7 @@ module TestHeader { MakeCrypto("zzzz", DO_NOTHING) ]; var tableName : GoodString := "name"; - var canonSchema :- expect OPS.CanonizeForEncrypt(tableName, schemaMap); + var canonSchema :- expect Canonize.ForEncrypt(tableName, schemaMap); var legend :- expect MakeLegend(canonSchema); //= specification/structured-encryption/header.md#encrypt-legend-bytes //= type=test @@ -180,7 +181,7 @@ module TestHeader { MakeCrypto("aaaa", SIGN_ONLY) ]; var tableName : GoodString := "name"; - var canonSchema :- expect OPS.CanonizeForEncrypt(tableName, schemaMap); + var canonSchema :- expect Canonize.ForEncrypt(tableName, schemaMap); var legend :- expect MakeLegend(canonSchema); //= specification/structured-encryption/header.md#encrypt-legend-bytes //= type=test diff --git a/SharedMakefile.mk b/SharedMakefile.mk index 21e4627a7..d93ba5857 100644 --- a/SharedMakefile.mk +++ b/SharedMakefile.mk @@ -10,3 +10,5 @@ SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/submodules/smithy-dafny GRADLEW := ./runtimes/java/gradlew include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk + +VERIFY_TIMEOUT := 250 diff --git a/specification/structured-encryption/decrypt-path-structure.md b/specification/structured-encryption/decrypt-path-structure.md index f523b43a6..0518c61b0 100644 --- a/specification/structured-encryption/decrypt-path-structure.md +++ b/specification/structured-encryption/decrypt-path-structure.md @@ -58,6 +58,8 @@ The Auth List describes how each [Terminal Data](./structures.md#terminal-data) The Auth List MUST include at least one [SIGN Authenticate Action](./structures.md#sign); otherwise, this operation MUST yield an error. +The Auth List MUST NOT contain duplicate Paths. + ### CMM A CMM that implements the [CMM interface](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cmm-interface.md). @@ -207,11 +209,12 @@ The Cipherkey and Nonce must be calculated as for [encryption](encrypt-structure ### Construct Decrypted Structured Data -In the output a [Crypto List](./structures.md#crypto-list): +In the output [Crypto List](./structures.md#crypto-list): - An entry MUST NOT exist with the key "aws_dbe_head" or "aws_dbe_foot". - For every entry in the [input Auth List](#auth-list), other than the header and footer, an entry MUST exist with the same key in the output Crypto List. -- The output Crypto List MUST NOT have any additional entries. +- For every entry in the output Crypto List + an entry MUST exist with the same key in the [input Auth List](#auth-list). Put plainly, the output does not add or drop any entries during decryption, other than the header and footer. For each entry in the output Crypto List: diff --git a/specification/structured-encryption/encrypt-path-structure.md b/specification/structured-encryption/encrypt-path-structure.md index 97e01ed32..1e3cdf0ae 100644 --- a/specification/structured-encryption/encrypt-path-structure.md +++ b/specification/structured-encryption/encrypt-path-structure.md @@ -79,6 +79,7 @@ See [encryption context](./structures.md#encryption-context). The prefix `aws-crypto-` is reserved for internal use by the AWS Encryption SDK; see the [the Default CMM spec](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/default-cmm.md) for one such use. +The operation MUST fail if an encryption context is provided which contains a key with the prefix `aws-crypto-`. ## Output @@ -307,11 +308,12 @@ The Footer Field Value MUST be the serialized [footer](footer.md). #### Encrypted Structured Data -- for every entry in the input [Crypto List](#crypto-list) +- For every entry in the input [Crypto List](#crypto-list) an entry MUST exist with the same [path](./structures.md#path) in the final Encrypted Structured Data. - The [Header Field](#header-field) MUST exist in the final Encrypted Structured Data - The [Footer Field](#footer-field) MUST exist in the final Encrypted Structured Data -- There MUST be no other entries in the final Encrypted Structured Data. +- For every entry in the final Encrypted Structured Data, other than the header and footer, + an entry MUST exist with the same [path](./structures.md#path) in the input [Crypto List](#crypto-list). For each entry in the final Encrypted Structured Data: