feat: improve verification

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);
   }

DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

@@ -101,6 +101,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     assert AuthListHasNoDuplicates(input.authActions);
     var head :- Header.PartialDeserialize(input.headerBytes);
     :- Need(ValidString(input.tableName), E("Bad Table Name"));
+    :- 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)));
@@ -493,7 +495,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     ensures forall k <- finalData :: |k.key| == 1
   {
     reveal EncryptPathFinal();
-    reveal CryptoUpdatedCryptoList();
+    reveal CryptoUpdatedCryptoListHeader();
     reveal NewCryptoUpdatedCrypto();
   }
 
@@ -560,8 +562,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     return Success(plainOutput);
   }
 
-  const HeaderPaths : seq<Path> := [HeaderPath, FooterPath]
-
   //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data
   //= type=implication
   //# - for every entry in the input [Crypto List](#crypto-list)
@@ -572,7 +572,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     ensures forall k <- origData :: (exists x :: x in finalData && x.key == k.key)
   {
     reveal EncryptPathFinal();
-    reveal CryptoUpdatedCryptoList();
+    reveal CryptoUpdatedCryptoListHeader();
     reveal CryptoUpdatedNewCrypto();
   }
 
@@ -593,23 +593,24 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
 
   lemma AllEncryptPathInputUpdatedInOutput(origData : CryptoList, finalData : CryptoList)
     requires EncryptPathFinal(origData, finalData)
-    ensures forall k <- origData :: (exists x :: x in finalData && Updated4(k, x, DoDecrypt))
+    ensures forall k <- origData :: (exists x :: x in finalData && Updated4(k, x, DoEncrypt))
   {
     reveal EncryptPathFinal();
-    reveal CryptoUpdatedCryptoList();
+    reveal CryptoUpdatedCryptoListHeader();
     reveal CryptoUpdatedNewCrypto();
   }
 
   //= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data
   //= type=implication
-  //# - 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) int 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 CryptoUpdatedCryptoList();
+    reveal CryptoUpdatedCryptoListHeader();
     reveal NewCryptoUpdatedCrypto();
   }
 
@@ -658,6 +659,13 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
         //= type=implication
         //# The [paths](./structures.md#path) in the input [Crypto List](./structures.md#crypto-list) MUST be unique.
         && CryptoListHasNoDuplicatesFromSet(input.plaintextStructure)
+
+        //= specification/structured-encryption/encrypt-path-structure.md#encryption-context
+        //= type=implication
+        //# 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?
@@ -929,7 +937,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
 
   //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
   //= type=implication
-  //# - 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).
   lemma AllDecryptPathOutputInInput(origData : AuthList, finalData : CryptoList)
     requires DecryptPathFinal(origData, finalData)
     ensures forall k <- finalData :: exists x :: x in origData
@@ -1013,6 +1022,12 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
               //# - 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#auth-list
+              //= type=implication
+              //# 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"));