Update with new keyring trait and materials

src/SDK/AlgorithmSuite.dfy

@@ -1,30 +1,27 @@
-include "../Crypto/All.dfy"
-include "../Crypto/Cipher.dfy"
-include "../Crypto/Digests.dfy"
-include "../Crypto/Signature.dfy"
+//include "../Crypto/All.dfy"
+//include "../Crypto/Cipher.dfy"
+//include "../Crypto/Digests.dfy"
+//include "../Crypto/Signature.dfy"
 include "../StandardLibrary/StandardLibrary.dfy"
 
 module AlgorithmSuite {
-
-  import opened Cipher
-  import Digests
-  import S = Signature
-  import opened StandardLibrary
+  import StandardLibrary
   import opened UInt = StandardLibrary.UInt
 
   const validIDs: set<uint16> := {0x0378, 0x0346, 0x0214, 0x0178, 0x0146, 0x0114, 0x0078, 0x0046, 0x0014};
 
   newtype ID = x | x in validIDs witness 0x0014
-  const AES_256_GCM_IV12_AUTH16_KDSHA384_SIGEC384 : ID := 0x0378
-  const AES_192_GCM_IV12_AUTH16_KDSHA384_SIGEC384 : ID := 0x0346
-  const AES_128_GCM_IV12_AUTH16_KDSHA256_SIGEC256 : ID := 0x0214
-  const AES_256_GCM_IV12_AUTH16_KDSHA256_SIGNONE  : ID := 0x0178
-  const AES_192_GCM_IV12_AUTH16_KDSHA256_SIGNONE  : ID := 0x0146
-  const AES_128_GCM_IV12_AUTH16_KDSHA256_SIGNONE  : ID := 0x0114
-  const AES_256_GCM_IV12_AUTH16_KDNONE_SIGNONE    : ID := 0x0078
-  const AES_192_GCM_IV12_AUTH16_KDNONE_SIGNONE    : ID := 0x0046
-  const AES_128_GCM_IV12_AUTH16_KDNONE_SIGNONE    : ID := 0x0014
-
+  const AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384: ID := 0x0378
+  const AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384: ID := 0x0346
+  const AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_PZ256: ID := 0x0214
+  const AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE: ID := 0x0178
+  const AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE: ID := 0x0146
+  const AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE: ID := 0x0114
+  const AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0078
+  const AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0046
+  const AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0014
+
+  /*
   datatype AlgSuite = AlgSuite(params : Cipher.CipherParams, hkdf : Digests.HMAC_ALGORITHM, sign : Option<S.ECDSAParams>)
 
   const Suite := map [
@@ -39,14 +36,13 @@ module AlgorithmSuite {
     AES_128_GCM_IV12_AUTH16_KDNONE_SIGNONE    := AlgSuite(CipherParams(AES128, 16, 12), Digests.HmacNOSHA,  None)
   ]
 
-
   function method input_key_length(x : ID) : nat {
       KeyLengthOfCipher(Suite[x].params)
   }
 
   function method signature_type_of_id(x : ID) : Option<S.ECDSAParams> {
     Suite[x].sign
   }
-
+  */
 
-}
+}

src/SDK/Common.dfy

@@ -3,39 +3,97 @@ include "../StandardLibrary/UInt.dfy"
 include "./AlgorithmSuite.dfy"
 
 
-module SDKDefs {
-    import opened StandardLibrary
-    import opened UInt = StandardLibrary.UInt
-    import AlgorithmSuite
-
-    type EncCtx = seq<(seq<uint8>, seq<uint8>)>
-
-
-    const EC_PUBLIC_KEY_FIELD: seq<uint8> := byteseq_of_string("aws-crypto-public-key");
-
-    datatype EDK = EDK(provider_id : seq<uint8>, 
-                       provider_info : seq<uint8>, 
-                       ciphertext : seq<uint8>)
-
-    datatype EncMaterials = EncMat(alg_id : AlgorithmSuite.ID, 
-                                   edks : seq<EDK>, 
-                                   enc_ctx : EncCtx, 
-                                   data_key : Option<seq<uint8>>, 
-                                   signing_key : Option<seq<uint8>>)
+module Materials {
+  import opened StandardLibrary
+  import opened UInt = StandardLibrary.UInt
+  import AlgorithmSuite
+
+  type EncryptionContext = seq<(seq<uint8>, seq<uint8>)>
+
+  datatype EncryptedDataKey = EncryptedDataKey(providerID : string, 
+                                               providerInfo : seq<uint8>,
+                                               ciphertext : seq<uint8>)
+
+  // TODO: Add keyring trace
+  class EncryptionMaterials {
+    var algorithmSuiteID: AlgorithmSuite.ID
+    var encryptedDataKeys: seq<EncryptedDataKey>
+    var encryptionContext: Option<EncryptionContext>
+    var plaintextDataKey: Option<seq<uint8>>
+    var signingKey: Option<seq<uint8>>
+
+    predicate Valid() 
+      reads this
+    {
+      |encryptedDataKeys| > 0 ==> plaintextDataKey.Some?
+      // TODO data key length assurance
+    }
 
-    predicate WFEncMaterials(x : EncMaterials) {
-        x.data_key.Some? ==> |x.data_key.get| == AlgorithmSuite.input_key_length(x.alg_id)
-        // TODO: wf signature
+    constructor(algorithmSuiteID: AlgorithmSuite.ID,
+                encryptedDataKeys: seq<EncryptedDataKey>, 
+                encryptionContext: Option<EncryptionContext>, 
+                plaintextDataKey: Option<seq<uint8>>,
+                signingKey: Option<seq<uint8>>)
+      requires |encryptedDataKeys| > 0 ==> plaintextDataKey.Some?
+      ensures Valid()
+    {
+      this.algorithmSuiteID := algorithmSuiteID;
+      this.encryptedDataKeys := encryptedDataKeys;
+      this.encryptionContext := encryptionContext;
+      this.plaintextDataKey := plaintextDataKey;
+      this.signingKey := signingKey;
     }
 
-    datatype DecMaterials = DecMat(alg_id : AlgorithmSuite.ID, enc_ctx : EncCtx, data_key : Option<seq<uint8>>, verif_key : Option<seq<uint8>>)
+    method SetPlaintextDataKey(dataKey: seq<uint8>)
+      requires Valid()
+      requires plaintextDataKey.None?
+      modifies `plaintextDataKey
+      ensures Valid()
+      ensures plaintextDataKey == Some(dataKey)
+    {
+      plaintextDataKey := Some(dataKey);
+    }
 
-    predicate WFDecMaterials(x : DecMaterials) {
-        x.data_key.Some? ==> |x.data_key.get| == AlgorithmSuite.input_key_length(x.alg_id)
+    method AppendEncryptedDataKey(edk: EncryptedDataKey)
+      requires Valid()
+      requires plaintextDataKey.Some?
+      modifies `encryptedDataKeys
+      ensures Valid()
+      ensures encryptedDataKeys == old(encryptedDataKeys) + [edk]
+    {
+      encryptedDataKeys := encryptedDataKeys + [edk]; // TODO: Determine if this is a performance issue
     }
+  }
 
+  // TODO: Add keyring trace
+  class DecryptionMaterials {
+    var algorithmSuiteID: AlgorithmSuite.ID
+    var encryptionContext: Option<EncryptionContext>
+    var plaintextDataKey: Option<seq<uint8>>
+    var verificationKey: Option<seq<uint8>>
+
+    // TODO add Valid()
+
+    constructor(algorithmSuiteID: AlgorithmSuite.ID,
+                encryptionContext: Option<EncryptionContext>,
+                plaintextDataKey: Option<seq<uint8>>,
+                verificationKey: Option<seq<uint8>>) {
+      this.algorithmSuiteID := algorithmSuiteID;
+      this.encryptionContext := encryptionContext;
+      this.plaintextDataKey := plaintextDataKey;
+      this.verificationKey := verificationKey;
+    }
 
+    method setPlaintextDataKey(dataKey: seq<uint8>)
+      requires plaintextDataKey.None?
+      modifies `plaintextDataKey
+      ensures plaintextDataKey == Some(dataKey)
+    {
+      plaintextDataKey := Some(dataKey);
+    }
+  }
 
+    /*
     function method naive_merge<T> (x : seq<T>, y : seq<T>, lt : (T, T) -> bool) : seq<T>
     {
         if |x| == 0 then y
@@ -89,4 +147,5 @@ module SDKDefs {
         if x == [] then [] else
         [(byteseq_of_string_lossy(x[0].0), byteseq_of_string_lossy(x[0].1))] + enc_ctx_of_strings(x[1..])
     }
+    */
 }

src/SDK/Keyring/Defs.dfy

@@ -1,32 +1,33 @@
 include "../../StandardLibrary/StandardLibrary.dfy"
 include "../../StandardLibrary/UInt.dfy"
-include "../AlgorithmSuite.dfy"
 include "../Common.dfy"
 
 module KeyringDefs {
-    import opened StandardLibrary
-    import opened UInt = StandardLibrary.UInt
-    import AlgorithmSuite
-    import opened SDKDefs
+  import opened StandardLibrary
+  import Materials
 
-    trait {:termination false} Keyring {
-        ghost var Repr : set<object>
-        predicate Valid() reads this, Repr
+  trait {:termination false} Keyring {
+    ghost var Repr : set<object>
+    predicate Valid() reads this, Repr
 
-        method OnEncrypt(x : EncMaterials) returns (res : Result<EncMaterials>)
-            requires WFEncMaterials(x)
-            requires Valid()
-            ensures Valid()
-            ensures res.Ok? ==> WFEncMaterials(res.get)
-            ensures res.Ok? ==> res.get.alg_id == x.alg_id
-
-        method OnDecrypt(x : DecMaterials, edks : seq<EDK>) returns (res : Result<DecMaterials>)
-            requires Valid()
-            requires WFDecMaterials(x)
-            ensures Valid()
-            ensures res.Ok? ==> WFDecMaterials(res.get)
-            ensures res.Ok? ==> res.get.alg_id == x.alg_id
-
-    }
+    method OnEncrypt(encMat: Materials.EncryptionMaterials) returns (res: Result<Materials.EncryptionMaterials>)
+      requires Valid()
+      requires encMat.Valid()
+      modifies encMat`plaintextDataKey
+      modifies encMat`encryptedDataKeys
+      ensures Valid()
+      ensures res.Success? ==> res.value.Valid()
+      ensures res.Success? && old(encMat.plaintextDataKey.Some?) ==> res.value.plaintextDataKey == old(encMat.plaintextDataKey)
+      // TODO: keyring trace GENERATED_DATA_KEY flag assurance
+      // TODO: keyring trace ENCRYPTED_DATA_KEY flag assurance
 
+    method OnDecrypt(decMat: Materials.DecryptionMaterials, edks: seq<Materials.EncryptedDataKey>) returns (res: Result<Materials.DecryptionMaterials>)
+      requires Valid()
+      // TODO: Valid input DecMaterials
+      modifies decMat`plaintextDataKey
+      ensures Valid()
+      // TODO: Valid output DecMaterials
+      ensures decMat.plaintextDataKey.Some? ==> res.Success? && res.value == decMat
+      // TODO: keyring trace DECRYPTED_DATA_KEY flag assurance
+  }
 }

src/StandardLibrary/StandardLibrary.dfy

@@ -9,7 +9,7 @@ module {:extern "STL"} StandardLibrary {
 
   datatype Error = IOError(msg: string) | DeserializationError(msg: string) | SerializationError(msg: string) | Error(msg : string)
 
-  datatype {:extern} Result<T> = Ok(get : T) | Err(err : string)
+  datatype {:extern} Result<T> = Success(value : T) | Failure(error : string)
 
   function Fill<T>(value: T, n: nat): seq<T>
     ensures |Fill(value, n)| == n
@@ -327,11 +327,9 @@ module {:extern "STL"} StandardLibrary {
                   then false
                   else true // i+1 == a.Length && i+1 == b.Length, i.e. a == b
   }
-
 
   lemma {:axiom} eq_multiset_eq_len<T> (s : seq<T>, s' : seq<T>)
       requires multiset(s) == multiset(s')
       ensures |s| == |s'| 
 
->>>>>>> d86c7da4676e9cfc8609dd5cb492177e18867845
 }

src/StandardLibrary/UInt.dfy

@@ -139,4 +139,3 @@ module {:extern "STLUINT"} StandardLibrary.UInt {
         x as uint32
     }
 }
->>>>>>> d86c7da4676e9cfc8609dd5cb492177e18867845