diff --git a/src/SDK/AlgorithmSuite.dfy b/src/SDK/AlgorithmSuite.dfy index 4d35d24e5..9d297e195 100644 --- a/src/SDK/AlgorithmSuite.dfy +++ b/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 := {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) const Suite := map [ @@ -39,7 +36,6 @@ 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) } @@ -47,6 +43,6 @@ module AlgorithmSuite { function method signature_type_of_id(x : ID) : Option { Suite[x].sign } - + */ -} \ No newline at end of file +} diff --git a/src/SDK/Common.dfy b/src/SDK/Common.dfy index 803a65568..f90e2a45f 100644 --- a/src/SDK/Common.dfy +++ b/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, seq)> - - - const EC_PUBLIC_KEY_FIELD: seq := byteseq_of_string("aws-crypto-public-key"); - - datatype EDK = EDK(provider_id : seq, - provider_info : seq, - ciphertext : seq) - - datatype EncMaterials = EncMat(alg_id : AlgorithmSuite.ID, - edks : seq, - enc_ctx : EncCtx, - data_key : Option>, - signing_key : Option>) +module Materials { + import opened StandardLibrary + import opened UInt = StandardLibrary.UInt + import AlgorithmSuite + + type EncryptionContext = seq<(seq, seq)> + + datatype EncryptedDataKey = EncryptedDataKey(providerID : string, + providerInfo : seq, + ciphertext : seq) + + // TODO: Add keyring trace + class EncryptionMaterials { + var algorithmSuiteID: AlgorithmSuite.ID + var encryptedDataKeys: seq + var encryptionContext: Option + var plaintextDataKey: Option> + var signingKey: Option> + + 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, + encryptionContext: Option, + plaintextDataKey: Option>, + signingKey: Option>) + 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>, verif_key : Option>) + method SetPlaintextDataKey(dataKey: seq) + 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 + var plaintextDataKey: Option> + var verificationKey: Option> + + // TODO add Valid() + + constructor(algorithmSuiteID: AlgorithmSuite.ID, + encryptionContext: Option, + plaintextDataKey: Option>, + verificationKey: Option>) { + this.algorithmSuiteID := algorithmSuiteID; + this.encryptionContext := encryptionContext; + this.plaintextDataKey := plaintextDataKey; + this.verificationKey := verificationKey; + } + method setPlaintextDataKey(dataKey: seq) + requires plaintextDataKey.None? + modifies `plaintextDataKey + ensures plaintextDataKey == Some(dataKey) + { + plaintextDataKey := Some(dataKey); + } + } + /* function method naive_merge (x : seq, y : seq, lt : (T, T) -> bool) : seq { 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..]) } + */ } diff --git a/src/SDK/Keyring/Defs.dfy b/src/SDK/Keyring/Defs.dfy index 7ee319636..191070473 100644 --- a/src/SDK/Keyring/Defs.dfy +++ b/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 - predicate Valid() reads this, Repr + trait {:termination false} Keyring { + ghost var Repr : set + predicate Valid() reads this, Repr - method OnEncrypt(x : EncMaterials) returns (res : Result) - 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) returns (res : Result) - 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) + 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) returns (res: Result) + 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 + } } diff --git a/src/StandardLibrary/StandardLibrary.dfy b/src/StandardLibrary/StandardLibrary.dfy index d4febb395..f46b0cd5e 100644 --- a/src/StandardLibrary/StandardLibrary.dfy +++ b/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 = Ok(get : T) | Err(err : string) + datatype {:extern} Result = Success(value : T) | Failure(error : string) function Fill(value: T, n: nat): seq 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 (s : seq, s' : seq) requires multiset(s) == multiset(s') ensures |s| == |s'| ->>>>>>> d86c7da4676e9cfc8609dd5cb492177e18867845 } diff --git a/src/StandardLibrary/UInt.dfy b/src/StandardLibrary/UInt.dfy index 9998d822e..a8a3a3f6f 100644 --- a/src/StandardLibrary/UInt.dfy +++ b/src/StandardLibrary/UInt.dfy @@ -139,4 +139,3 @@ module {:extern "STLUINT"} StandardLibrary.UInt { x as uint32 } } ->>>>>>> d86c7da4676e9cfc8609dd5cb492177e18867845