Create request types for CMM interface (#209)

* Create request types for CMM interface
aws · Feb 28, 2020 · 7cc10af · 7cc10af
1 parent 9a91689
commit 7cc10af
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 23 deletions.
diff --git a/src/SDK/CMM/DefaultCMM.dfy b/src/SDK/CMM/DefaultCMM.dfy
@@ -41,9 +41,11 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
       Repr := {this, kr} + k.Repr;
     }
 
-    method GetEncryptionMaterials(ec: Materials.EncryptionContext, alg_id: Option<AlgorithmSuite.ID>, pt_len: Option<nat>) returns (res: Result<Materials.ValidEncryptionMaterials>)
+    method GetEncryptionMaterials(materialsRequest: Materials.EncryptionMaterialsRequest)
+                                  returns (res: Result<Materials.ValidEncryptionMaterials>)
       requires Valid()
-      requires ValidAAD(ec) && ec.Keys !! Materials.ReservedKeyValues
+      requires ValidAAD(materialsRequest.encryptionContext)
+      requires materialsRequest.encryptionContext.Keys !! Materials.ReservedKeyValues
       ensures Valid()
       ensures res.Success? ==> res.value.plaintextDataKey.Some? && res.value.algorithmSuiteID.ValidPlaintextDataKey(res.value.plaintextDataKey.get)
       ensures res.Success? ==> |res.value.encryptedDataKeys| > 0
@@ -54,9 +56,12 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
           case Some(sigType) =>
             res.value.signingKey.Some?
     {
-      var id := if alg_id.Some? then alg_id.get else AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
+      var id := if materialsRequest.algorithmSuiteID.Some? then
+        materialsRequest.algorithmSuiteID.get
+      else
+        AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384;
       var enc_sk := None;
-      var enc_ctx := ec;
+      var enc_ctx := materialsRequest.encryptionContext;
 
       match id.SignatureType() {
         case None =>
@@ -66,7 +71,7 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
           var enc_vk :- UTF8.Encode(Base64.Encode(signatureKeys.verificationKey));
           var reservedField := Materials.EC_PUBLIC_KEY_FIELD;
           assert reservedField in Materials.ReservedKeyValues;
-          assert forall i :: i in ec.Keys ==> i != reservedField;
+          assert forall i :: i in materialsRequest.encryptionContext.Keys ==> i != reservedField;
           enc_ctx := enc_ctx[reservedField := enc_vk];
       }
 
@@ -82,29 +87,31 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
       return Success(materials);
     }
 
-    method DecryptMaterials(alg_id: AlgorithmSuite.ID, edks: seq<Materials.EncryptedDataKey>, enc_ctx: Materials.EncryptionContext) 
-      returns (res: Result<Materials.ValidDecryptionMaterials>)
-      requires |edks| > 0
+    method DecryptMaterials(materialsRequest: Materials.ValidDecryptionMaterialsRequest)
+                            returns (res: Result<Materials.ValidDecryptionMaterials>)
       requires Valid()
       ensures Valid()
       ensures res.Success? ==> res.value.plaintextDataKey.Some? && res.value.algorithmSuiteID.ValidPlaintextDataKey(res.value.plaintextDataKey.get)
       ensures res.Success? && res.value.algorithmSuiteID.SignatureType().Some? ==> res.value.verificationKey.Some?
     {
       // Retrieve and decode verification key from encryption context if using signing algorithm
       var vkey := None;
-      if alg_id.SignatureType().Some? {
+      var algID := materialsRequest.algorithmSuiteID;
+      var encCtx := materialsRequest.encryptionContext;
+
+      if algID.SignatureType().Some? {
         var reservedField := Materials.EC_PUBLIC_KEY_FIELD;
-        if reservedField !in enc_ctx {
+        if reservedField !in encCtx {
           return Failure("Could not get materials required for decryption.");
         }
-        var encodedVKey := enc_ctx[reservedField];
+        var encodedVKey := encCtx[reservedField];
         var utf8Decoded :- UTF8.Decode(encodedVKey);
         var base64Decoded :- Base64.Decode(utf8Decoded);
         vkey := Some(base64Decoded);
       }
 
-      var materials := Materials.DecryptionMaterials.WithoutPlaintextDataKey(enc_ctx, alg_id, vkey);
-      materials :- kr.OnDecrypt(materials, edks);
+      var materials := Materials.DecryptionMaterials.WithoutPlaintextDataKey(encCtx, algID, vkey);
+      materials :- kr.OnDecrypt(materials, materialsRequest.encryptedDataKeys);
       if materials.plaintextDataKey.None? {
         return Failure("Keyring.OnDecrypt failed to decrypt the plaintext data key.");
       }

diff --git a/src/SDK/CMM/Defs.dfy b/src/SDK/CMM/Defs.dfy
@@ -16,12 +16,11 @@ module {:extern "CMMDefs"} CMMDefs {
     ghost var Repr : set<object>
     predicate Valid() reads this, Repr
 
-    method GetEncryptionMaterials(encCtx: Materials.EncryptionContext,
-                                  algSuiteID: Option<AlgorithmSuite.ID>,
-                                  plaintextLen: Option<nat>)
+    method GetEncryptionMaterials(materialsRequest: Materials.EncryptionMaterialsRequest)
                                   returns (res: Result<Materials.ValidEncryptionMaterials>)
       requires Valid()
-      requires ValidAAD(encCtx) && encCtx.Keys !! Materials.ReservedKeyValues
+      requires ValidAAD(materialsRequest.encryptionContext)
+      requires materialsRequest.encryptionContext.Keys !! Materials.ReservedKeyValues
       ensures Valid()
       ensures res.Success? ==> res.value.plaintextDataKey.Some? && res.value.algorithmSuiteID.ValidPlaintextDataKey(res.value.plaintextDataKey.get)
       ensures res.Success? ==> |res.value.encryptedDataKeys| > 0
@@ -38,11 +37,8 @@ module {:extern "CMMDefs"} CMMDefs {
       MessageHeader.ValidAAD(encryptionContext)
     }
 
-    method DecryptMaterials(algSuiteID: AlgorithmSuite.ID,
-                            edks: seq<Materials.EncryptedDataKey>,
-                            encCtx: Materials.EncryptionContext)
+    method DecryptMaterials(materialsRequest: Materials.ValidDecryptionMaterialsRequest)
                             returns (res: Result<Materials.ValidDecryptionMaterials>)
-      requires |edks| > 0
       requires Valid()
       ensures Valid()
       ensures res.Success? ==> res.value.plaintextDataKey.Some? && res.value.algorithmSuiteID.ValidPlaintextDataKey(res.value.plaintextDataKey.get)

diff --git a/src/SDK/Client.dfy b/src/SDK/Client.dfy
@@ -46,7 +46,9 @@ module {:extern "ESDKClient"} ESDKClient {
       assert Msg.ValidAAD(encryptionContext);
     }
     var frameLength := if optFrameLength.Some? then optFrameLength.get else DEFAULT_FRAME_LENGTH;
-    var encMat :- cmm.GetEncryptionMaterials(encryptionContext, algorithmSuiteID, Some(|plaintext|));
+
+    var encMatRequest := Materials.EncryptionMaterialsRequest(encryptionContext, algorithmSuiteID, Some(|plaintext|));
+    var encMat :- cmm.GetEncryptionMaterials(encMatRequest);
     if UINT16_LIMIT <= |encMat.encryptedDataKeys| {
       return Failure("Number of EDKs exceeds the allowed maximum.");
     }
@@ -117,7 +119,8 @@ module {:extern "ESDKClient"} ESDKClient {
   {
     var rd := new Streams.ByteReader(message);
     var header :- Deserialize.DeserializeHeader(rd);
-    var decMat :- cmm.DecryptMaterials(header.body.algorithmSuiteID, header.body.encryptedDataKeys.entries, header.body.aad);
+    var decMatRequest := Materials.DecryptionMaterialsRequest(header.body.algorithmSuiteID, header.body.encryptedDataKeys.entries, header.body.aad);
+    var decMat :- cmm.DecryptMaterials(decMatRequest);
 
     var decryptionKey := DeriveKey(decMat.plaintextDataKey.get, decMat.algorithmSuiteID, header.body.messageID);
 

diff --git a/src/SDK/Materials.dfy b/src/SDK/Materials.dfy
@@ -178,4 +178,25 @@ module {:extern "Materials"} Materials {
   }
 
   type ValidDecryptionMaterials = i: DecryptionMaterials | i.Valid() witness DecryptionMaterials.ValidWitness()
+
+  datatype EncryptionMaterialsRequest = EncryptionMaterialsRequest(encryptionContext: EncryptionContext,
+                                                                   algorithmSuiteID: Option<AlgorithmSuite.ID>,
+                                                                   plaintextLength: Option<nat>)
+
+  datatype DecryptionMaterialsRequest = DecryptionMaterialsRequest(algorithmSuiteID: AlgorithmSuite.ID,
+                                                                   encryptedDataKeys: seq<ValidEncryptedDataKey>,
+                                                                   encryptionContext: EncryptionContext)
+  {
+    predicate Valid() {
+      |encryptedDataKeys| > 0
+    }
+
+    static function method ValidWitness(): DecryptionMaterialsRequest {
+      DecryptionMaterialsRequest(AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384,
+                                 [EncryptedDataKey.ValidWitness()],
+                                 map[])
+    }
+  }
+
+  type ValidDecryptionMaterialsRequest = i: DecryptionMaterialsRequest | i.Valid() witness DecryptionMaterialsRequest.ValidWitness()
 }