docs: Fix minor spec bugs (#176)

Author: lavaleri

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

@@ -497,7 +497,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   //= specification/dynamodb-encryption-client/decrypt-item.md#determining-plaintext-items
   //= type=implication
   //# An item MUST be determined to be plaintext if it does not contain
-  //# attributes with the names "aws_dbe_header" and "aws_dbe_footer".
+  //# attributes with the names "aws_dbe_head" and "aws_dbe_foot".
   predicate method IsPlaintextItem(ddbItem: ComAmazonawsDynamodbTypes.AttributeMap) {
     && StructuredEncryptionUtil.HeaderField !in ddbItem.Keys
     && StructuredEncryptionUtil.FooterField !in ddbItem.Keys

DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

@@ -62,8 +62,8 @@ module StructuredEncryptionHeader {
   //# [DBE supported algorithm suite](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/algorithm-suites.md#supported-algorithm-suites-enum).
   // | Value | Algorithm Suite ID | Algorithm Suite Enum |
   // |---|---|---|
-  // | 0x01 | 0x67 0x01 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384 |
-  // | 0x00 | 0x67 0x00 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384 |
+  // | 0x00 | 0x67 0x00 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384 |
+  // | 0x01 | 0x67 0x01 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384 |
   predicate method ValidFlavor(x : uint8) {
     x in [0, 1]
   }

specification/dynamodb-encryption-client/decrypt-item.md

@@ -155,7 +155,7 @@ although the DynamoDbEncryptor allows callers to configure custom names for thes
 ### Determining Plaintext Items
 
 An item MUST be determined to be plaintext if it does not contain
-attributes with the names "aws_dbe_header" and "aws_dbe_footer".
+attributes with the names "aws_dbe_head" and "aws_dbe_foot".
 
 Note that this does not conflict with the [legacy item](#determining-legacy-items) definition,
 as there is no configuration state which needs to be able to distinguish

specification/structured-encryption/header.md

@@ -50,8 +50,8 @@ The algorithm suite indicated by the flavor MUST be a
 
 | Value | Algorithm Suite ID | Algorithm Suite Enum |
 |---|---|---|
-| 0x01 | 0x67 0x01 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384 |
-| 0x00 | 0x67 0x00 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384 |
+| 0x00 | 0x67 0x00 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384 |
+| 0x01 | 0x67 0x01 | ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384 |
 
 ### Message ID