From 4a636fe98910b62f1b7ba1672e6165f415c38c1b Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Thu, 3 Oct 2019 09:01:36 -0700 Subject: [PATCH 01/17] Refactoring AES crypto code --- Makefile | 3 +- src/Crypto/AESEncryption.dfy | 111 ++++++++++++-------------- src/Crypto/AESUtils.dfy | 21 +++++ src/Crypto/Cipher.dfy | 57 ------------- src/Crypto/EncryptionExtern.cs | 5 +- src/Crypto/GenBytes.dfy | 1 + src/Crypto/RSAEncryption.dfy | 3 +- src/Crypto/WrappingAlgorithmSuite.dfy | 28 +++++++ src/SDK/AlgorithmSuite.dfy | 28 ++++--- src/SDK/Keyring/AESKeyring.dfy | 34 ++++---- src/SDK/ToyClient.dfy | 16 ++-- 11 files changed, 150 insertions(+), 157 deletions(-) create mode 100644 src/Crypto/AESUtils.dfy delete mode 100644 src/Crypto/Cipher.dfy create mode 100644 src/Crypto/WrappingAlgorithmSuite.dfy diff --git a/Makefile b/Makefile index d60d307e6..f85175acf 100644 --- a/Makefile +++ b/Makefile @@ -10,11 +10,12 @@ endif # SRCS = $(foreach dir, $(SRCDIRS), $(wildcard $(dir)/*.dfy)) SRCS = \ src/Crypto/AESEncryption.dfy \ - src/Crypto/Cipher.dfy \ + src/Crypto/AESUtils.dfy \ src/Crypto/Digests.dfy \ src/Crypto/GenBytes.dfy \ src/Crypto/RSAEncryption.dfy \ src/Crypto/Signature.dfy \ + src/Crypto/WrappingAlgorithmSuite.dfy \ src/Main.dfy \ src/SDK/AlgorithmSuite.dfy \ src/SDK/CMM/DefaultCMM.dfy \ diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index 5d1dc0121..f8ca658ad 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -1,66 +1,53 @@ +include "../SDK/AlgorithmSuite.dfy" include "../StandardLibrary/StandardLibrary.dfy" -include "Cipher.dfy" +include "AESUtils.dfy" +include "WrappingAlgorithmSuite.dfy" +include "GenBytes.dfy" module {:extern "AESEncryption"} AESEncryption { - //TODO This code has yet to be reviewed. See issue #36 - import C = Cipher - import opened StandardLibrary - import opened UInt = StandardLibrary.UInt - - class {:extern "AES_GCM"} AES { - - static predicate method AESWfCtx(cipher : C.CipherParams, ctx : seq) { - |ctx| > (cipher.ivLen) as int - } - - static predicate method AESWfKey (cipher : C.CipherParams, k : seq) { - |k| == C.KeyLengthOfCipher(cipher) as int - } - - // TODO: make below return an option if anything throws. - static method AESKeygen(cipher : C.CipherParams) returns (k : seq) - ensures AESWfKey(cipher, k) { - k := C.GenKey(cipher); - } - - static function method {:extern "aes_decrypt"} aes_decrypt(cipher: C.CipherParams, - key: seq, - ctxt: seq, - iv: seq, - aad: seq): Result> - requires |key| == C.KeyLengthOfCipher(cipher) as int - - static function method AESDecrypt(cipher: C.CipherParams, k: seq, md: seq, c: seq): Result> - requires AESWfKey(cipher, k) - requires AESWfCtx(cipher, c) { - match aes_decrypt(cipher, k, c[cipher.ivLen ..], c[0 .. cipher.ivLen], md) - case Failure(e) => Failure(e) - case Success(m) => Success(m) - } - - static method {:extern "aes_encrypt"} aes_encrypt (cipher : C.CipherParams, - iv : seq, - key : seq, - msg : seq, - aad : seq) - returns (ctx : Result>) - - requires |iv| == cipher.ivLen as int - requires |key| == C.KeyLengthOfCipher(cipher) as int - ensures ctx.Success? ==> |ctx.value| > (cipher.tagLen) as int - ensures ctx.Success? ==> aes_decrypt(cipher, key, ctx.value, iv, aad) == Success((msg)) - - static method AESEncrypt(cipher : C.CipherParams, k : seq, msg : seq, md : seq) returns (c : Result>) - requires AESWfKey(cipher, k) - ensures c.Success? ==> AESWfCtx(cipher, c.value) - ensures c.Success? ==> AESDecrypt(cipher, k, md, c.value) == Success(msg) - { - var iv := C.GenIV(cipher); - var ctx := aes_encrypt(cipher, iv, k, msg, md); - match ctx { - case Failure(e) => return Failure(e); - case Success(ct) => return Success(iv + ct); - } - } - } + import AESUtils + import WrappingAlgorithmSuite + import RNG + import opened StandardLibrary + import opened UInt = StandardLibrary.UInt + + export + provides AESDecrypt, AESEncrypt, AESUtils, StandardLibrary, UInt + + //FIXME: Ensure that these methods correctly handle authenticaition tags, see #36 + method AESDecrypt(params: AESUtils.Params, key: seq, ctxt: seq, iv: seq, aad: seq) + returns (res: Result>) + requires |key| == params.keyLen as int + { + res := AES.AESDecrypt(params, key, ctxt, iv, aad); + } + + method AESEncrypt(params: AESUtils.Params, iv : seq, key : seq, msg : seq, aad : seq) + returns (res : Result>) + requires |iv| == params.ivLen as int + requires |key| == params.keyLen as int + ensures res.Success? ==> |res.value| > params.tagLen as int + { + res := AES.AESEncrypt(params, iv, key, msg, aad); + } + + class {:extern "AES_GCM"} AES { + static method {:extern "AESDecrypt"} AESDecrypt(params: AESUtils.Params, + key: seq, + ctxt: seq, + iv: seq, + aad: seq) + returns (res: Result>) + requires |key| == params.keyLen as int + + static method {:extern "AESEncrypt"} AESEncrypt (params: AESUtils.Params, + iv : seq, + key : seq, + msg : seq, + aad : seq) + returns (res : Result>) + requires |iv| == params.ivLen as int + requires |key| == params.keyLen as int + ensures res.Success? ==> |res.value| > params.tagLen as int + } } diff --git a/src/Crypto/AESUtils.dfy b/src/Crypto/AESUtils.dfy new file mode 100644 index 000000000..91c7ac669 --- /dev/null +++ b/src/Crypto/AESUtils.dfy @@ -0,0 +1,21 @@ +include "../StandardLibrary/StandardLibrary.dfy" + +module {:extern "AESUtils"} AESUtils { + import opened StandardLibrary + import opened UInt = StandardLibrary.UInt + + datatype Mode = AES256 | AES128 | AES192 + datatype Params = Params(mode: Mode, keyLen: uint8, tagLen: uint8, ivLen: uint8) + + const MAX_KEY_LEN := 32 + const CIPHER_KEY_LENGTHS := {32, 24, 16}; + const TAG_LEN := 16 as uint8; + const IV_LEN := 12 as uint8; + + function method KeyLengthOfCipher(m: Mode): uint8 { + match m + case AES256 => 32 as uint8 + case AES192 => 24 as uint8 + case AES128 => 16 as uint8 + } +} diff --git a/src/Crypto/Cipher.dfy b/src/Crypto/Cipher.dfy deleted file mode 100644 index 43049c919..000000000 --- a/src/Crypto/Cipher.dfy +++ /dev/null @@ -1,57 +0,0 @@ -include "../StandardLibrary/StandardLibrary.dfy" -include "GenBytes.dfy" - -// Information about the ciphers in the Encryption SDK, as well as information common to all algorithms which use ciphers (both encryption and KDF). -module {:extern "Cipher"} Cipher { - import opened StandardLibrary - import opened UInt = StandardLibrary.UInt - import opened RNG - - datatype AESMode = AES256 | AES128 | AES192 - datatype {:extern "CipherParams"} CipherParams = CipherParams(mode: AESMode, keyLen: uint8, tagLen: uint8, ivLen: uint8) - - const MAX_KEY_LEN := 32 - const CIPHER_KEY_LENGTHS := {32, 24, 16}; - const TAG_LEN := 16 as uint8; - const IV_LEN := 12 as uint8; - - const AES_GCM_128 := CipherParams(AES128, 16, TAG_LEN, IV_LEN); - const AES_GCM_192 := CipherParams(AES192, 24, TAG_LEN, IV_LEN); - const AES_GCM_256 := CipherParams(AES256, 32, TAG_LEN, IV_LEN); - - function method CipherOfKeyLength(n : int) : CipherParams - requires n in CIPHER_KEY_LENGTHS { - if n == 32 then AES_GCM_256 - else if n == 24 then AES_GCM_192 - else AES_GCM_128 - } - - function method KeyLengthOfCipher (c : CipherParams) : int { - match c.mode - case AES256 => 32 - case AES192 => 24 - case AES128 => 16 - } - - /* - lemma Cipher_KeyLengthK (c : CipherParams) - requires c.tagLen == TAG_LEN - requires c.ivLen == IV_LEN - ensures CipherOfKeyLength(KeyLengthOfCipher(c)) == c { - match c.mode - case AES256 => - case AES192 => - case AES128 => - } - */ - - method GenIV(m : CipherParams) returns (s : seq) ensures |s| == m.ivLen as int { - s := GenBytes(m.ivLen as uint16); - } - - method GenKey(m : CipherParams) returns (s : seq) ensures |s| == KeyLengthOfCipher(m) as int { - s := GenBytes(KeyLengthOfCipher(m) as uint16); - } - - -} diff --git a/src/Crypto/EncryptionExtern.cs b/src/Crypto/EncryptionExtern.cs index 3a7b359e7..caf9ec99d 100644 --- a/src/Crypto/EncryptionExtern.cs +++ b/src/Crypto/EncryptionExtern.cs @@ -23,7 +23,8 @@ namespace AESEncryption { //TODO This code has yet to be reviewed. See issue #36 public partial class AES_GCM { - public static STL.Result aes_encrypt(Cipher.CipherParams p, + //FIXME: Ensure that these methods correctly handle authenticaition tags, see #36 + public static STL.Result AESEncrypt(AESUtils.Params p, byteseq iv, byteseq key, byteseq msg, @@ -43,7 +44,7 @@ public static STL.Result aes_encrypt(Cipher.CipherParams p, } } - public static STL.Result aes_decrypt(Cipher.CipherParams p, byteseq key, byteseq ctx, byteseq iv, byteseq aad) { + public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, byteseq ctx, byteseq iv, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); var param = new AeadParameters(new KeyParameter(key.Elements), p.tagLen * 8, iv.Elements, aad.Elements); diff --git a/src/Crypto/GenBytes.dfy b/src/Crypto/GenBytes.dfy index ebffcbc84..5cf7d65f5 100644 --- a/src/Crypto/GenBytes.dfy +++ b/src/Crypto/GenBytes.dfy @@ -1,5 +1,6 @@ include "../StandardLibrary/StandardLibrary.dfy" +//TODO This module should be renamed, see #55. module {:extern "RNGWrap"} RNG { import opened StandardLibrary import opened UInt = StandardLibrary.UInt diff --git a/src/Crypto/RSAEncryption.dfy b/src/Crypto/RSAEncryption.dfy index e276ea034..a166c725b 100644 --- a/src/Crypto/RSAEncryption.dfy +++ b/src/Crypto/RSAEncryption.dfy @@ -1,8 +1,7 @@ include "../StandardLibrary/StandardLibrary.dfy" -include "Cipher.dfy" +//This code must be reviewed, see #18 module {:extern "RSAEncryption"} RSAEncryption { - import C = Cipher import opened StandardLibrary import opened UInt = StandardLibrary.UInt diff --git a/src/Crypto/WrappingAlgorithmSuite.dfy b/src/Crypto/WrappingAlgorithmSuite.dfy new file mode 100644 index 000000000..3c7a95db9 --- /dev/null +++ b/src/Crypto/WrappingAlgorithmSuite.dfy @@ -0,0 +1,28 @@ +include "../Crypto/AESUtils.dfy" +include "../StandardLibrary/StandardLibrary.dfy" +include "GenBytes.dfy" + +module WrappingAlgorithmSuite { + import opened StandardLibrary + import opened UInt = StandardLibrary.UInt + import AES = AESUtils + import RNG + + const AES_GCM_128 := AES.Params(AES.AES128, AES.KeyLengthOfCipher(AES.AES128), AES.TAG_LEN, AES.IV_LEN) + const AES_GCM_192 := AES.Params(AES.AES192, AES.KeyLengthOfCipher(AES.AES192), AES.TAG_LEN, AES.IV_LEN) + const AES_GCM_256 := AES.Params(AES.AES256, AES.KeyLengthOfCipher(AES.AES256), AES.TAG_LEN, AES.IV_LEN) + + const VALID_ALGORITHMS := {AES_GCM_128, AES_GCM_192, AES_GCM_256} + + method GenIV(p: AES.Params) returns (s : seq) + ensures |s| == p.ivLen as int + { + s := RNG.GenBytes(p.ivLen as uint16); + } + + method GenKey(p: AES.Params) returns (s : seq) + ensures |s| == p.keyLen as int + { + s := RNG.GenBytes(p.keyLen as uint16); + } +} diff --git a/src/SDK/AlgorithmSuite.dfy b/src/SDK/AlgorithmSuite.dfy index 4aeff1559..df8153be3 100644 --- a/src/SDK/AlgorithmSuite.dfy +++ b/src/SDK/AlgorithmSuite.dfy @@ -1,4 +1,4 @@ -include "../Crypto/Cipher.dfy" +include "../Crypto/AESUtils.dfy" include "../Crypto/Digests.dfy" include "../Crypto/Signature.dfy" include "../StandardLibrary/StandardLibrary.dfy" @@ -6,8 +6,8 @@ include "../StandardLibrary/StandardLibrary.dfy" module AlgorithmSuite { import opened StandardLibrary import opened UInt = StandardLibrary.UInt + import AES = AESUtils import S = Signature - import C = Cipher import Digests const validIDs: set := {0x0378, 0x0346, 0x0214, 0x0178, 0x0146, 0x0114, 0x0078, 0x0046, 0x0014}; @@ -33,17 +33,21 @@ module AlgorithmSuite { const AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0046 const AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0014 - datatype AlgSuite = AlgSuite(params: C.CipherParams, hkdf: Digests.HMAC_ALGORITHM, sign: Option) + const AES_GCM_128 := AES.Params(AES.AES128, 16, AES.TAG_LEN, AES.IV_LEN) + const AES_GCM_192 := AES.Params(AES.AES192, 24, AES.TAG_LEN, AES.IV_LEN) + const AES_GCM_256 := AES.Params(AES.AES256, 32, AES.TAG_LEN, AES.IV_LEN) + + datatype AlgSuite = AlgSuite(params: AES.Params, hkdf: Digests.HMAC_ALGORITHM, sign: Option) const Suite := map [ - AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(C.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(C.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(C.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), - AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(C.AES_GCM_256, Digests.HmacSHA256, None), - AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(C.AES_GCM_192, Digests.HmacSHA256, None), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(C.AES_GCM_128, Digests.HmacSHA256, None), - AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(C.AES_GCM_256, Digests.HmacNOSHA, None), - AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(C.AES_GCM_192, Digests.HmacNOSHA, None), - AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(C.AES_GCM_128, Digests.HmacNOSHA, None) + AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), + AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES_GCM_256, Digests.HmacSHA256, None), + AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES_GCM_192, Digests.HmacSHA256, None), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES_GCM_128, Digests.HmacSHA256, None), + AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES_GCM_256, Digests.HmacNOSHA, None), + AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES_GCM_192, Digests.HmacNOSHA, None), + AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES_GCM_128, Digests.HmacNOSHA, None) ] } diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index c00d54637..a910d9703 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -3,7 +3,8 @@ include "../../StandardLibrary/StandardLibrary.dfy" include "../../StandardLibrary/UInt.dfy" include "../AlgorithmSuite.dfy" include "./Defs.dfy" -include "../../Crypto/Cipher.dfy" +include "../../Crypto/AESUtils.dfy" +include "../../Crypto/WrappingAlgorithmSuite.dfy" include "../../Crypto/GenBytes.dfy" include "../../Crypto/AESEncryption.dfy" include "../Materials.dfy" @@ -11,9 +12,10 @@ include "../Materials.dfy" module AESKeyringDef { import opened StandardLibrary import opened UInt = StandardLibrary.UInt + import AESUtils import AlgorithmSuite - import Cipher - import GenBytes = RNG + import WrappingSuite = WrappingAlgorithmSuite + import RNG import KeyringDefs import AESEncryption import Mat = Materials @@ -25,19 +27,19 @@ module AESKeyringDef { const keyNamespace: string const keyName: string const wrappingKey: seq - const wrappingAlgorithm: Cipher.CipherParams + const wrappingAlgorithm: AESUtils.Params predicate Valid() reads this { Repr == {this} && - (|wrappingKey| == Cipher.KeyLengthOfCipher(wrappingAlgorithm)) && - (wrappingAlgorithm in {Cipher.AES_GCM_128, Cipher.AES_GCM_192, Cipher.AES_GCM_256}) && + (|wrappingKey| == wrappingAlgorithm.keyLen as int) && + (wrappingAlgorithm in WrappingSuite.VALID_ALGORITHMS) && StringIs8Bit(keyNamespace) && StringIs8Bit(keyName) } - constructor(namespace: string, name: string, key: seq, wrappingAlg: Cipher.CipherParams) + constructor(namespace: string, name: string, key: seq, wrappingAlg: AESUtils.Params) requires StringIs8Bit(namespace) && StringIs8Bit(name) - requires wrappingAlg in {Cipher.AES_GCM_128, Cipher.AES_GCM_192, Cipher.AES_GCM_256} - requires |key| == Cipher.KeyLengthOfCipher(wrappingAlg) + requires wrappingAlg in WrappingSuite.VALID_ALGORITHMS + requires |key| == wrappingAlg.keyLen as int ensures keyNamespace == namespace ensures keyName == name ensures wrappingKey == key @@ -74,12 +76,12 @@ module AESKeyringDef { { var dataKey := encMat.plaintextDataKey; if dataKey.None? { - var k := Cipher.RNG.GenBytes(encMat.algorithmSuiteID.KeyLength() as uint16); + var k := RNG.GenBytes(encMat.algorithmSuiteID.KeyLength() as uint16); dataKey := Some(k); } - var iv := Cipher.RNG.GenBytes(wrappingAlgorithm.ivLen as uint16); + var iv := RNG.GenBytes(wrappingAlgorithm.ivLen as uint16); var aad := Mat.FlattenSortEncCtx(encMat.encryptionContext); - var encryptResult := AESEncryption.AES.aes_encrypt(wrappingAlgorithm, iv, wrappingKey, dataKey.get, aad); + var encryptResult := AESEncryption.AESEncrypt(wrappingAlgorithm, iv, wrappingKey, dataKey.get, aad); if encryptResult.Failure? { return Failure("Error on encrypt!"); } var providerInfo := SerializeProviderInto(iv); var edk := Mat.EncryptedDataKey(keyNamespace, providerInfo, encryptResult.value); @@ -117,17 +119,19 @@ module AESKeyringDef { return Success(decMat); } var i := 0; - while i < |edks| { + while i < |edks| + invariant unchanged(decMat) + { if edks[i].providerID == keyNamespace && ValidProviderInfo(edks[i].providerInfo) { var iv := GetIvFromProvInfo(edks[i].providerInfo); var flatEncCtx: seq := Mat.FlattenSortEncCtx(decMat.encryptionContext); - var decryptResult := AESEncryption.AES.aes_decrypt(wrappingAlgorithm, wrappingKey, edks[i].ciphertext, iv, flatEncCtx); + var decryptResult := AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, edks[i].ciphertext, iv, flatEncCtx); if decryptResult.Success? { var ptKey := decryptResult.value; if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length decMat.plaintextDataKey := Some(ptKey); return Success(decMat); - } + } // Should we fail if the key length is incorrect? } else { return Failure("Decryption failed"); } diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index a14a62887..121a042e8 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -1,11 +1,12 @@ include "../StandardLibrary/StandardLibrary.dfy" include "../StandardLibrary/UInt.dfy" -include "Materials.dfy" +include "AlgorithmSuite.dfy" include "CMM/Defs.dfy" include "CMM/DefaultCMM.dfy" include "Keyring/Defs.dfy" -include "AlgorithmSuite.dfy" +include "Materials.dfy" include "../Crypto/AESEncryption.dfy" +include "../Crypto/WrappingAlgorithmSuite.dfy" module ToyClientDef { import opened StandardLibrary @@ -16,7 +17,7 @@ module ToyClientDef { import KeyringDefs import AlgorithmSuite import AESEncryption - import Cipher + import WrappingAlgorithmSuite datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, ctxt: seq) @@ -69,8 +70,9 @@ module ToyClientDef { if |em.plaintextDataKey.get| != 32 { return Failure("bad data key length"); } - var ciphertext :- AESEncryption.AES.AESEncrypt(Cipher.AES_GCM_256, em.plaintextDataKey.get, pt, []); - return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, ciphertext)); + var iv := WrappingAlgorithmSuite.GenIV(WrappingAlgorithmSuite.AES_GCM_256); + var ciphertext :- AESEncryption.AESEncrypt(WrappingAlgorithmSuite.AES_GCM_256, iv ,em.plaintextDataKey.get, pt, []); + return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, iv + ciphertext)); } method Decrypt(e: Encryption) returns (res: Result>) @@ -84,7 +86,9 @@ module ToyClientDef { match decmat.plaintextDataKey case Some(dk) => if |dk| == 32 && |e.ctxt| > 12 { - var msg := AESEncryption.AES.AESDecrypt(Cipher.AES_GCM_256, dk, [], e.ctxt); + var cipherText := e.ctxt[WrappingAlgorithmSuite.AES_GCM_256.ivLen ..]; + var iv := e.ctxt[0 .. WrappingAlgorithmSuite.AES_GCM_256.ivLen]; + var msg := AESEncryption.AESDecrypt(WrappingAlgorithmSuite.AES_GCM_256, dk, cipherText, iv, []); return msg; } else { return Failure("bad dk"); From e00db9fc74b1165d1ae0385320168b262a56e0aa Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Thu, 3 Oct 2019 11:41:43 -0700 Subject: [PATCH 02/17] Addressing PR comments --- src/Crypto/AESEncryption.dfy | 4 ++-- src/Crypto/AESUtils.dfy | 6 +++--- src/Crypto/WrappingAlgorithmSuite.dfy | 8 ++++---- src/SDK/Keyring/AESKeyring.dfy | 4 ++-- src/SDK/ToyClient.dfy | 2 +- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index f8ca658ad..086823dd7 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -22,11 +22,11 @@ module {:extern "AESEncryption"} AESEncryption { res := AES.AESDecrypt(params, key, ctxt, iv, aad); } - method AESEncrypt(params: AESUtils.Params, iv : seq, key : seq, msg : seq, aad : seq) + method AESEncrypt(params: AESUtils.Params, iv: seq, key: seq, msg: seq, aad: seq) returns (res : Result>) requires |iv| == params.ivLen as int requires |key| == params.keyLen as int - ensures res.Success? ==> |res.value| > params.tagLen as int + ensures res.Success? ==> params.tagLen as int < |res.value| { res := AES.AESEncrypt(params, iv, key, msg, aad); } diff --git a/src/Crypto/AESUtils.dfy b/src/Crypto/AESUtils.dfy index 91c7ac669..880bbebda 100644 --- a/src/Crypto/AESUtils.dfy +++ b/src/Crypto/AESUtils.dfy @@ -14,8 +14,8 @@ module {:extern "AESUtils"} AESUtils { function method KeyLengthOfCipher(m: Mode): uint8 { match m - case AES256 => 32 as uint8 - case AES192 => 24 as uint8 - case AES128 => 16 as uint8 + case AES256 => 32 as uint8 + case AES192 => 24 as uint8 + case AES128 => 16 as uint8 } } diff --git a/src/Crypto/WrappingAlgorithmSuite.dfy b/src/Crypto/WrappingAlgorithmSuite.dfy index 3c7a95db9..9b169e13f 100644 --- a/src/Crypto/WrappingAlgorithmSuite.dfy +++ b/src/Crypto/WrappingAlgorithmSuite.dfy @@ -14,14 +14,14 @@ module WrappingAlgorithmSuite { const VALID_ALGORITHMS := {AES_GCM_128, AES_GCM_192, AES_GCM_256} - method GenIV(p: AES.Params) returns (s : seq) - ensures |s| == p.ivLen as int + method GenIV(p: AES.Params) returns (s: seq) + ensures |s| == p.ivLen as int { s := RNG.GenBytes(p.ivLen as uint16); } - method GenKey(p: AES.Params) returns (s : seq) - ensures |s| == p.keyLen as int + method GenKey(p: AES.Params) returns (s: seq) + ensures |s| == p.keyLen as int { s := RNG.GenBytes(p.keyLen as uint16); } diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index a910d9703..012f11161 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -31,8 +31,8 @@ module AESKeyringDef { predicate Valid() reads this { Repr == {this} && - (|wrappingKey| == wrappingAlgorithm.keyLen as int) && - (wrappingAlgorithm in WrappingSuite.VALID_ALGORITHMS) && + |wrappingKey| == wrappingAlgorithm.keyLen as int && + wrappingAlgorithm in WrappingSuite.VALID_ALGORITHMS && StringIs8Bit(keyNamespace) && StringIs8Bit(keyName) } diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index aeba2f7de..a440da4a5 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -87,7 +87,7 @@ module ToyClientDef { case Some(dk) => if |dk| == 32 && |e.ctxt| > 12 { var cipherText := e.ctxt[WrappingAlgorithmSuite.AES_GCM_256.ivLen ..]; - var iv := e.ctxt[0 .. WrappingAlgorithmSuite.AES_GCM_256.ivLen]; + var iv := e.ctxt[.. WrappingAlgorithmSuite.AES_GCM_256.ivLen]; var msg := AESEncryption.AESDecrypt(WrappingAlgorithmSuite.AES_GCM_256, dk, cipherText, iv, []); return msg; } else { From c3a39bb5757ec0ec009281ff612f5c4251b5ca9f Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Fri, 4 Oct 2019 11:59:35 -0700 Subject: [PATCH 03/17] Addressing PR comments, and adding explainations for AESEncryption handles authentication tags --- src/Crypto/AESEncryption.dfy | 4 +++- src/Crypto/AESUtils.dfy | 6 +++--- src/Crypto/EncryptionExtern.cs | 5 ++--- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index 086823dd7..f4ded51e4 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -14,7 +14,8 @@ module {:extern "AESEncryption"} AESEncryption { export provides AESDecrypt, AESEncrypt, AESUtils, StandardLibrary, UInt - //FIXME: Ensure that these methods correctly handle authenticaition tags, see #36 + //Note: AESDecrypt expects the message authentication tag (also known as MAC) to be present as the last n bytes of ctxt. + // n = params.tagLen method AESDecrypt(params: AESUtils.Params, key: seq, ctxt: seq, iv: seq, aad: seq) returns (res: Result>) requires |key| == params.keyLen as int @@ -22,6 +23,7 @@ module {:extern "AESEncryption"} AESEncryption { res := AES.AESDecrypt(params, key, ctxt, iv, aad); } + //Note: The return value of AESEncrypt is the encrypted message, concatenated with the authentication tag. method AESEncrypt(params: AESUtils.Params, iv: seq, key: seq, msg: seq, aad: seq) returns (res : Result>) requires |iv| == params.ivLen as int diff --git a/src/Crypto/AESUtils.dfy b/src/Crypto/AESUtils.dfy index 880bbebda..5c8cb3103 100644 --- a/src/Crypto/AESUtils.dfy +++ b/src/Crypto/AESUtils.dfy @@ -14,8 +14,8 @@ module {:extern "AESUtils"} AESUtils { function method KeyLengthOfCipher(m: Mode): uint8 { match m - case AES256 => 32 as uint8 - case AES192 => 24 as uint8 - case AES128 => 16 as uint8 + case AES256 => 32 + case AES192 => 24 + case AES128 => 16 } } diff --git a/src/Crypto/EncryptionExtern.cs b/src/Crypto/EncryptionExtern.cs index caf9ec99d..92c015875 100644 --- a/src/Crypto/EncryptionExtern.cs +++ b/src/Crypto/EncryptionExtern.cs @@ -23,7 +23,6 @@ namespace AESEncryption { //TODO This code has yet to be reviewed. See issue #36 public partial class AES_GCM { - //FIXME: Ensure that these methods correctly handle authenticaition tags, see #36 public static STL.Result AESEncrypt(AESUtils.Params p, byteseq iv, byteseq key, @@ -36,7 +35,7 @@ public static STL.Result AESEncrypt(AESUtils.Params p, byte[] c = new byte[cipher.GetOutputSize(msg.Elements.Length)]; var len = cipher.ProcessBytes(msg.Elements, 0, msg.Elements.Length, c, 0); - cipher.DoFinal(c, len); + cipher.DoFinal(c, len); //Append authentication tag to `c` return new STL.Result_Success(new byteseq(c)); } catch { @@ -51,7 +50,7 @@ public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, byt cipher.Init(false, param); var pt = new byte[cipher.GetOutputSize(ctx.Elements.Length)]; var len = cipher.ProcessBytes(ctx.Elements, 0, ctx.Elements.Length, pt, 0); - cipher.DoFinal(pt, len); + cipher.DoFinal(pt, len); //Check message authentication tag return new STL.Result_Success(new byteseq(pt)); } catch { From b400edde21426b39d7ae204eac63fc669a5547f8 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Mon, 7 Oct 2019 08:12:45 -0700 Subject: [PATCH 04/17] Addressing PR comments. Mostly to seperate the ciphertext and authtag returned by AES. --- Makefile | 1 - src/Crypto/AESEncryption.dfy | 36 ++++++++++++++++++++++------------ src/Crypto/EncryptionExtern.cs | 11 +++++++---- src/SDK/Keyring/AESKeyring.dfy | 13 +++++++----- src/SDK/ToyClient.dfy | 5 +++-- 5 files changed, 41 insertions(+), 25 deletions(-) diff --git a/Makefile b/Makefile index f85175acf..20259dc6a 100644 --- a/Makefile +++ b/Makefile @@ -16,7 +16,6 @@ SRCS = \ src/Crypto/RSAEncryption.dfy \ src/Crypto/Signature.dfy \ src/Crypto/WrappingAlgorithmSuite.dfy \ - src/Main.dfy \ src/SDK/AlgorithmSuite.dfy \ src/SDK/CMM/DefaultCMM.dfy \ src/SDK/CMM/Defs.dfy \ diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index f4ded51e4..01ca10b16 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -1,34 +1,44 @@ include "../SDK/AlgorithmSuite.dfy" include "../StandardLibrary/StandardLibrary.dfy" include "AESUtils.dfy" -include "WrappingAlgorithmSuite.dfy" include "GenBytes.dfy" module {:extern "AESEncryption"} AESEncryption { import AESUtils - import WrappingAlgorithmSuite import RNG import opened StandardLibrary import opened UInt = StandardLibrary.UInt export provides AESDecrypt, AESEncrypt, AESUtils, StandardLibrary, UInt + reveals EncryptionArtifacts, EncryptionArtifactFromByteSeq - //Note: AESDecrypt expects the message authentication tag (also known as MAC) to be present as the last n bytes of ctxt. - // n = params.tagLen - method AESDecrypt(params: AESUtils.Params, key: seq, ctxt: seq, iv: seq, aad: seq) - returns (res: Result>) + // Is there a better name/location for this? + datatype EncryptionArtifacts = EncryptionArtifacts(cipherText: seq, authTag: seq) + + function method EncryptionArtifactFromByteSeq(s: seq, p: AESUtils.Params): (encArt: EncryptionArtifacts) + requires p.tagLen > 0 + requires |s| > p.tagLen as int + ensures |encArt.cipherText + encArt.authTag| <= |s| + ensures |encArt.authTag| == p.tagLen as int + { + EncryptionArtifacts(s[.. |s| - p.tagLen as int], s[|s| - p.tagLen as int ..]) + } + + method AESDecrypt(params: AESUtils.Params, key: seq, encryptionArtifacts: EncryptionArtifacts, iv: seq, aad: seq) + returns (res: Result>) requires |key| == params.keyLen as int + requires |encryptionArtifacts.authTag| == params.tagLen as int { - res := AES.AESDecrypt(params, key, ctxt, iv, aad); + var cipherText := encryptionArtifacts.cipherText + encryptionArtifacts.authTag; + res := AES.AESDecrypt(params, key, cipherText, iv, aad); } - //Note: The return value of AESEncrypt is the encrypted message, concatenated with the authentication tag. method AESEncrypt(params: AESUtils.Params, iv: seq, key: seq, msg: seq, aad: seq) - returns (res : Result>) + returns (res : Result) requires |iv| == params.ivLen as int requires |key| == params.keyLen as int - ensures res.Success? ==> params.tagLen as int < |res.value| + ensures res.Success? ==> |res.value.authTag| == params.tagLen as int { res := AES.AESEncrypt(params, iv, key, msg, aad); } @@ -39,7 +49,7 @@ module {:extern "AESEncryption"} AESEncryption { ctxt: seq, iv: seq, aad: seq) - returns (res: Result>) + returns (res: Result>) requires |key| == params.keyLen as int static method {:extern "AESEncrypt"} AESEncrypt (params: AESUtils.Params, @@ -47,9 +57,9 @@ module {:extern "AESEncryption"} AESEncryption { key : seq, msg : seq, aad : seq) - returns (res : Result>) + returns (res : Result) requires |iv| == params.ivLen as int requires |key| == params.keyLen as int - ensures res.Success? ==> |res.value| > params.tagLen as int + ensures res.Success? ==> |res.value.authTag| == params.tagLen as int } } diff --git a/src/Crypto/EncryptionExtern.cs b/src/Crypto/EncryptionExtern.cs index 92c015875..df32dca6e 100644 --- a/src/Crypto/EncryptionExtern.cs +++ b/src/Crypto/EncryptionExtern.cs @@ -1,6 +1,7 @@ using System; -using System.Text; +using System.Linq; using System.IO; +using System.Text; using Org.BouncyCastle.Crypto; using Org.BouncyCastle.Crypto.Digests; using Org.BouncyCastle.Crypto.EC; @@ -23,7 +24,7 @@ namespace AESEncryption { //TODO This code has yet to be reviewed. See issue #36 public partial class AES_GCM { - public static STL.Result AESEncrypt(AESUtils.Params p, + public static STL.Result AESEncrypt(AESUtils.Params p, byteseq iv, byteseq key, byteseq msg, @@ -36,10 +37,12 @@ public static STL.Result AESEncrypt(AESUtils.Params p, byte[] c = new byte[cipher.GetOutputSize(msg.Elements.Length)]; var len = cipher.ProcessBytes(msg.Elements, 0, msg.Elements.Length, c, 0); cipher.DoFinal(c, len); //Append authentication tag to `c` - return new STL.Result_Success(new byteseq(c)); + return new STL.Result_Success( + new EncryptionArtifacts(new byteseq(c.Take(len - 1).ToArray()), new byteseq(c.Skip(len - 1).ToArray())) + ); } catch { - return new STL.Result_Failure(new Dafny.Sequence("aes encrypt err".ToCharArray())); + return new STL.Result_Failure(new Dafny.Sequence("aes encrypt err".ToCharArray())); } } diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index 012f11161..895168f10 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -81,10 +81,9 @@ module AESKeyringDef { } var iv := RNG.GenBytes(wrappingAlgorithm.ivLen as uint16); var aad := Mat.FlattenSortEncCtx(encMat.encryptionContext); - var encryptResult := AESEncryption.AESEncrypt(wrappingAlgorithm, iv, wrappingKey, dataKey.get, aad); - if encryptResult.Failure? { return Failure("Error on encrypt!"); } + var encryptResult :- AESEncryption.AESEncrypt(wrappingAlgorithm, iv, wrappingKey, dataKey.get, aad); var providerInfo := SerializeProviderInto(iv); - var edk := Mat.EncryptedDataKey(keyNamespace, providerInfo, encryptResult.value); + var edk := Mat.EncryptedDataKey(keyNamespace, providerInfo, encryptResult.cipherText + encryptResult.authTag); encMat.plaintextDataKey := dataKey; encMat.encryptedDataKeys := encMat.encryptedDataKeys + [edk]; return Success(encMat); @@ -122,10 +121,14 @@ module AESKeyringDef { while i < |edks| invariant unchanged(decMat) { - if edks[i].providerID == keyNamespace && ValidProviderInfo(edks[i].providerInfo) { + if edks[i].providerID == keyNamespace && ValidProviderInfo(edks[i].providerInfo) && wrappingAlgorithm.tagLen as int <= |edks[i].ciphertext| { var iv := GetIvFromProvInfo(edks[i].providerInfo); var flatEncCtx: seq := Mat.FlattenSortEncCtx(decMat.encryptionContext); - var decryptResult := AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, edks[i].ciphertext, iv, flatEncCtx); + var encArt := AESEncryption.EncryptionArtifacts( + edks[i].ciphertext[wrappingAlgorithm.tagLen ..], + edks[i].ciphertext[.. wrappingAlgorithm.tagLen] + ); + var decryptResult := AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, encArt, iv, flatEncCtx); if decryptResult.Success? { var ptKey := decryptResult.value; if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index a440da4a5..282eadeaa 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -72,11 +72,12 @@ module ToyClientDef { } var iv := WrappingAlgorithmSuite.GenIV(WrappingAlgorithmSuite.AES_GCM_256); var ciphertext :- AESEncryption.AESEncrypt(WrappingAlgorithmSuite.AES_GCM_256, iv ,em.plaintextDataKey.get, pt, []); - return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, iv + ciphertext)); + return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, iv + ciphertext.cipherText + ciphertext.authTag)); } method Decrypt(e: Encryption) returns (res: Result>) requires Valid() + requires (WrappingAlgorithmSuite.AES_GCM_256.ivLen + WrappingAlgorithmSuite.AES_GCM_256.tagLen) as int < |e.ctxt| ensures Valid() { if |e.edks| == 0 { @@ -86,7 +87,7 @@ module ToyClientDef { match decmat.plaintextDataKey case Some(dk) => if |dk| == 32 && |e.ctxt| > 12 { - var cipherText := e.ctxt[WrappingAlgorithmSuite.AES_GCM_256.ivLen ..]; + var cipherText := AESEncryption.EncryptionArtifactFromByteSeq(e.ctxt[WrappingAlgorithmSuite.AES_GCM_256.ivLen ..], WrappingAlgorithmSuite.AES_GCM_256); var iv := e.ctxt[.. WrappingAlgorithmSuite.AES_GCM_256.ivLen]; var msg := AESEncryption.AESDecrypt(WrappingAlgorithmSuite.AES_GCM_256, dk, cipherText, iv, []); return msg; From bf84edee21548828efd1ca47917c59fa97dbecce Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Mon, 7 Oct 2019 11:15:38 -0700 Subject: [PATCH 05/17] Addressing PR comments. Mostly moving and refactoring WrappingAlgorithmSuite -> AESWrappingSuite --- Makefile | 2 +- src/Crypto/AESUtils.dfy | 4 ++++ src/Crypto/WrappingAlgorithmSuite.dfy | 28 --------------------------- src/SDK/AlgorithmSuite.dfy | 22 +++++++++------------ src/SDK/Keyring/AESKeyring.dfy | 10 +++++----- src/SDK/Keyring/AESWrappingSuite.dfy | 24 +++++++++++++++++++++++ src/SDK/ToyClient.dfy | 27 +++++++++++++++----------- 7 files changed, 59 insertions(+), 58 deletions(-) delete mode 100644 src/Crypto/WrappingAlgorithmSuite.dfy create mode 100644 src/SDK/Keyring/AESWrappingSuite.dfy diff --git a/Makefile b/Makefile index 20259dc6a..1fcc4c6dc 100644 --- a/Makefile +++ b/Makefile @@ -15,11 +15,11 @@ SRCS = \ src/Crypto/GenBytes.dfy \ src/Crypto/RSAEncryption.dfy \ src/Crypto/Signature.dfy \ - src/Crypto/WrappingAlgorithmSuite.dfy \ src/SDK/AlgorithmSuite.dfy \ src/SDK/CMM/DefaultCMM.dfy \ src/SDK/CMM/Defs.dfy \ src/SDK/Keyring/AESKeyring.dfy \ + src/SDK/Keyring/AESWrappingSuite.dfy \ src/SDK/Keyring/Defs.dfy \ src/SDK/Keyring/RSAKeyring.dfy \ src/SDK/Materials.dfy \ diff --git a/src/Crypto/AESUtils.dfy b/src/Crypto/AESUtils.dfy index 5c8cb3103..26109c7f5 100644 --- a/src/Crypto/AESUtils.dfy +++ b/src/Crypto/AESUtils.dfy @@ -12,6 +12,10 @@ module {:extern "AESUtils"} AESUtils { const TAG_LEN := 16 as uint8; const IV_LEN := 12 as uint8; + const AES_GCM_128 := Params(AES128, 16, TAG_LEN, IV_LEN) + const AES_GCM_192 := Params(AES192, 24, TAG_LEN, IV_LEN) + const AES_GCM_256 := Params(AES256, 32, TAG_LEN, IV_LEN) + function method KeyLengthOfCipher(m: Mode): uint8 { match m case AES256 => 32 diff --git a/src/Crypto/WrappingAlgorithmSuite.dfy b/src/Crypto/WrappingAlgorithmSuite.dfy deleted file mode 100644 index 9b169e13f..000000000 --- a/src/Crypto/WrappingAlgorithmSuite.dfy +++ /dev/null @@ -1,28 +0,0 @@ -include "../Crypto/AESUtils.dfy" -include "../StandardLibrary/StandardLibrary.dfy" -include "GenBytes.dfy" - -module WrappingAlgorithmSuite { - import opened StandardLibrary - import opened UInt = StandardLibrary.UInt - import AES = AESUtils - import RNG - - const AES_GCM_128 := AES.Params(AES.AES128, AES.KeyLengthOfCipher(AES.AES128), AES.TAG_LEN, AES.IV_LEN) - const AES_GCM_192 := AES.Params(AES.AES192, AES.KeyLengthOfCipher(AES.AES192), AES.TAG_LEN, AES.IV_LEN) - const AES_GCM_256 := AES.Params(AES.AES256, AES.KeyLengthOfCipher(AES.AES256), AES.TAG_LEN, AES.IV_LEN) - - const VALID_ALGORITHMS := {AES_GCM_128, AES_GCM_192, AES_GCM_256} - - method GenIV(p: AES.Params) returns (s: seq) - ensures |s| == p.ivLen as int - { - s := RNG.GenBytes(p.ivLen as uint16); - } - - method GenKey(p: AES.Params) returns (s: seq) - ensures |s| == p.keyLen as int - { - s := RNG.GenBytes(p.keyLen as uint16); - } -} diff --git a/src/SDK/AlgorithmSuite.dfy b/src/SDK/AlgorithmSuite.dfy index df8153be3..41ed6eabe 100644 --- a/src/SDK/AlgorithmSuite.dfy +++ b/src/SDK/AlgorithmSuite.dfy @@ -33,21 +33,17 @@ module AlgorithmSuite { const AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0046 const AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0014 - const AES_GCM_128 := AES.Params(AES.AES128, 16, AES.TAG_LEN, AES.IV_LEN) - const AES_GCM_192 := AES.Params(AES.AES192, 24, AES.TAG_LEN, AES.IV_LEN) - const AES_GCM_256 := AES.Params(AES.AES256, 32, AES.TAG_LEN, AES.IV_LEN) - datatype AlgSuite = AlgSuite(params: AES.Params, hkdf: Digests.HMAC_ALGORITHM, sign: Option) const Suite := map [ - AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), - AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES_GCM_256, Digests.HmacSHA256, None), - AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES_GCM_192, Digests.HmacSHA256, None), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES_GCM_128, Digests.HmacSHA256, None), - AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES_GCM_256, Digests.HmacNOSHA, None), - AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES_GCM_192, Digests.HmacNOSHA, None), - AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES_GCM_128, Digests.HmacNOSHA, None) + AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(AES.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), + AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES.AES_GCM_256, Digests.HmacSHA256, None), + AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES.AES_GCM_192, Digests.HmacSHA256, None), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES.AES_GCM_128, Digests.HmacSHA256, None), + AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES.AES_GCM_256, Digests.HmacNOSHA, None), + AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES.AES_GCM_192, Digests.HmacNOSHA, None), + AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES.AES_GCM_128, Digests.HmacNOSHA, None) ] } diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index 895168f10..a368ad844 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -4,21 +4,21 @@ include "../../StandardLibrary/UInt.dfy" include "../AlgorithmSuite.dfy" include "./Defs.dfy" include "../../Crypto/AESUtils.dfy" -include "../../Crypto/WrappingAlgorithmSuite.dfy" +include "./AESWrappingSuite.dfy" include "../../Crypto/GenBytes.dfy" include "../../Crypto/AESEncryption.dfy" include "../Materials.dfy" -module AESKeyringDef { +module AESKeyring{ import opened StandardLibrary import opened UInt = StandardLibrary.UInt + import AESEncryption import AESUtils import AlgorithmSuite - import WrappingSuite = WrappingAlgorithmSuite - import RNG import KeyringDefs - import AESEncryption import Mat = Materials + import RNG + import WrappingSuite = AESWrappingSuite const AUTH_TAG_LEN_LEN := 4; const IV_LEN_LEN := 4; diff --git a/src/SDK/Keyring/AESWrappingSuite.dfy b/src/SDK/Keyring/AESWrappingSuite.dfy new file mode 100644 index 000000000..921a97dfe --- /dev/null +++ b/src/SDK/Keyring/AESWrappingSuite.dfy @@ -0,0 +1,24 @@ +include "../../Crypto/AESUtils.dfy" +include "../../StandardLibrary/StandardLibrary.dfy" +include "../../Crypto/GenBytes.dfy" + +module AESKeyring.AESWrappingSuite { + import opened StandardLibrary + import opened UInt = StandardLibrary.UInt + import AES = AESUtils + import RNG + + const VALID_ALGORITHMS := {AES.AES_GCM_128, AES.AES_GCM_192, AES.AES_GCM_256} + + method GenIV(p: AES.Params) returns (s: seq) + ensures |s| == p.ivLen as int + { + s := RNG.GenBytes(p.ivLen as uint16); + } + + method GenKey(p: AES.Params) returns (s: seq) + ensures |s| == p.keyLen as int + { + s := RNG.GenBytes(p.keyLen as uint16); + } +} diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index 282eadeaa..23d6a127f 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -4,9 +4,11 @@ include "AlgorithmSuite.dfy" include "CMM/Defs.dfy" include "CMM/DefaultCMM.dfy" include "Keyring/Defs.dfy" +include "./Keyring/AESWrappingSuite.dfy" include "Materials.dfy" include "../Crypto/AESEncryption.dfy" -include "../Crypto/WrappingAlgorithmSuite.dfy" +include "../Crypto/AESUtils.dfy" +include "../Crypto/GenBytes.dfy" module ToyClientDef { import opened StandardLibrary @@ -15,11 +17,15 @@ module ToyClientDef { import CMMDefs import DefaultCMMDef import KeyringDefs + import RNG import AlgorithmSuite import AESEncryption - import WrappingAlgorithmSuite + import AESKeyring + import AESUtils - datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, ctxt: seq) + datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, iv: seq, ctxt: AESEncryption.EncryptionArtifacts) + + const ALGORITHM := AESUtils.AES_GCM_256 class Client { var cmm: CMMDefs.CMM @@ -70,14 +76,15 @@ module ToyClientDef { if |em.plaintextDataKey.get| != 32 { return Failure("bad data key length"); } - var iv := WrappingAlgorithmSuite.GenIV(WrappingAlgorithmSuite.AES_GCM_256); - var ciphertext :- AESEncryption.AESEncrypt(WrappingAlgorithmSuite.AES_GCM_256, iv ,em.plaintextDataKey.get, pt, []); - return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, iv + ciphertext.cipherText + ciphertext.authTag)); + var iv := RNG.GenBytes(ALGORITHM.ivLen as uint16); + var ciphertext :- AESEncryption.AESEncrypt(ALGORITHM, iv ,em.plaintextDataKey.get, pt, []); + return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, iv, ciphertext)); } method Decrypt(e: Encryption) returns (res: Result>) requires Valid() - requires (WrappingAlgorithmSuite.AES_GCM_256.ivLen + WrappingAlgorithmSuite.AES_GCM_256.tagLen) as int < |e.ctxt| + requires ALGORITHM.tagLen as int == |e.ctxt.authTag| + requires ALGORITHM.ivLen as int == |e.iv| ensures Valid() { if |e.edks| == 0 { @@ -86,10 +93,8 @@ module ToyClientDef { var decmat :- cmm.DecryptMaterials(AlgorithmSuite.AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384, e.edks, e.ec); match decmat.plaintextDataKey case Some(dk) => - if |dk| == 32 && |e.ctxt| > 12 { - var cipherText := AESEncryption.EncryptionArtifactFromByteSeq(e.ctxt[WrappingAlgorithmSuite.AES_GCM_256.ivLen ..], WrappingAlgorithmSuite.AES_GCM_256); - var iv := e.ctxt[.. WrappingAlgorithmSuite.AES_GCM_256.ivLen]; - var msg := AESEncryption.AESDecrypt(WrappingAlgorithmSuite.AES_GCM_256, dk, cipherText, iv, []); + if |dk| == 32 { + var msg := AESEncryption.AESDecrypt(ALGORITHM, dk, e.ctxt, e.iv, []); return msg; } else { return Failure("bad dk"); From 1711ca58d4300f14a5f89edf86a29755aeae5058 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Mon, 7 Oct 2019 14:15:31 -0700 Subject: [PATCH 06/17] Removing AESWrappingSuite --- Makefile | 1 - src/SDK/Keyring/AESKeyring.dfy | 7 +++---- src/SDK/Keyring/AESWrappingSuite.dfy | 24 ------------------------ src/SDK/ToyClient.dfy | 2 -- 4 files changed, 3 insertions(+), 31 deletions(-) delete mode 100644 src/SDK/Keyring/AESWrappingSuite.dfy diff --git a/Makefile b/Makefile index 1fcc4c6dc..a21f88ab7 100644 --- a/Makefile +++ b/Makefile @@ -19,7 +19,6 @@ SRCS = \ src/SDK/CMM/DefaultCMM.dfy \ src/SDK/CMM/Defs.dfy \ src/SDK/Keyring/AESKeyring.dfy \ - src/SDK/Keyring/AESWrappingSuite.dfy \ src/SDK/Keyring/Defs.dfy \ src/SDK/Keyring/RSAKeyring.dfy \ src/SDK/Materials.dfy \ diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index a368ad844..544ebb612 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -4,7 +4,6 @@ include "../../StandardLibrary/UInt.dfy" include "../AlgorithmSuite.dfy" include "./Defs.dfy" include "../../Crypto/AESUtils.dfy" -include "./AESWrappingSuite.dfy" include "../../Crypto/GenBytes.dfy" include "../../Crypto/AESEncryption.dfy" include "../Materials.dfy" @@ -18,10 +17,10 @@ module AESKeyring{ import KeyringDefs import Mat = Materials import RNG - import WrappingSuite = AESWrappingSuite const AUTH_TAG_LEN_LEN := 4; const IV_LEN_LEN := 4; + const VALID_ALGORITHMS := {AESUtils.AES_GCM_128, AESUtils.AES_GCM_192, AESUtils.AES_GCM_256} class AESKeyring extends KeyringDefs.Keyring { const keyNamespace: string @@ -32,13 +31,13 @@ module AESKeyring{ predicate Valid() reads this { Repr == {this} && |wrappingKey| == wrappingAlgorithm.keyLen as int && - wrappingAlgorithm in WrappingSuite.VALID_ALGORITHMS && + wrappingAlgorithm in VALID_ALGORITHMS && StringIs8Bit(keyNamespace) && StringIs8Bit(keyName) } constructor(namespace: string, name: string, key: seq, wrappingAlg: AESUtils.Params) requires StringIs8Bit(namespace) && StringIs8Bit(name) - requires wrappingAlg in WrappingSuite.VALID_ALGORITHMS + requires wrappingAlg in VALID_ALGORITHMS requires |key| == wrappingAlg.keyLen as int ensures keyNamespace == namespace ensures keyName == name diff --git a/src/SDK/Keyring/AESWrappingSuite.dfy b/src/SDK/Keyring/AESWrappingSuite.dfy deleted file mode 100644 index 921a97dfe..000000000 --- a/src/SDK/Keyring/AESWrappingSuite.dfy +++ /dev/null @@ -1,24 +0,0 @@ -include "../../Crypto/AESUtils.dfy" -include "../../StandardLibrary/StandardLibrary.dfy" -include "../../Crypto/GenBytes.dfy" - -module AESKeyring.AESWrappingSuite { - import opened StandardLibrary - import opened UInt = StandardLibrary.UInt - import AES = AESUtils - import RNG - - const VALID_ALGORITHMS := {AES.AES_GCM_128, AES.AES_GCM_192, AES.AES_GCM_256} - - method GenIV(p: AES.Params) returns (s: seq) - ensures |s| == p.ivLen as int - { - s := RNG.GenBytes(p.ivLen as uint16); - } - - method GenKey(p: AES.Params) returns (s: seq) - ensures |s| == p.keyLen as int - { - s := RNG.GenBytes(p.keyLen as uint16); - } -} diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index 23d6a127f..11d5760e9 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -4,7 +4,6 @@ include "AlgorithmSuite.dfy" include "CMM/Defs.dfy" include "CMM/DefaultCMM.dfy" include "Keyring/Defs.dfy" -include "./Keyring/AESWrappingSuite.dfy" include "Materials.dfy" include "../Crypto/AESEncryption.dfy" include "../Crypto/AESUtils.dfy" @@ -20,7 +19,6 @@ module ToyClientDef { import RNG import AlgorithmSuite import AESEncryption - import AESKeyring import AESUtils datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, iv: seq, ctxt: AESEncryption.EncryptionArtifacts) From 6601113162ab2d281a77bd52e4c414e247016b7f Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Wed, 9 Oct 2019 10:51:05 -0700 Subject: [PATCH 07/17] Removing Dafny class from AESEncryption, misc fixes to AESKeyring --- src/Crypto/AESEncryption.dfy | 43 ++++++---------------------------- src/Crypto/EncryptionExtern.cs | 14 +++++------ src/SDK/Keyring/AESKeyring.dfy | 28 +++++++++++----------- 3 files changed, 27 insertions(+), 58 deletions(-) diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index 01ca10b16..a03ddd852 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -5,61 +5,32 @@ include "GenBytes.dfy" module {:extern "AESEncryption"} AESEncryption { import AESUtils - import RNG import opened StandardLibrary import opened UInt = StandardLibrary.UInt export provides AESDecrypt, AESEncrypt, AESUtils, StandardLibrary, UInt - reveals EncryptionArtifacts, EncryptionArtifactFromByteSeq + reveals EncryptionArtifacts // Is there a better name/location for this? datatype EncryptionArtifacts = EncryptionArtifacts(cipherText: seq, authTag: seq) function method EncryptionArtifactFromByteSeq(s: seq, p: AESUtils.Params): (encArt: EncryptionArtifacts) - requires p.tagLen > 0 - requires |s| > p.tagLen as int + requires |s| >= p.tagLen as int ensures |encArt.cipherText + encArt.authTag| <= |s| ensures |encArt.authTag| == p.tagLen as int { EncryptionArtifacts(s[.. |s| - p.tagLen as int], s[|s| - p.tagLen as int ..]) } - method AESDecrypt(params: AESUtils.Params, key: seq, encryptionArtifacts: EncryptionArtifacts, iv: seq, aad: seq) - returns (res: Result>) - requires |key| == params.keyLen as int - requires |encryptionArtifacts.authTag| == params.tagLen as int - { - var cipherText := encryptionArtifacts.cipherText + encryptionArtifacts.authTag; - res := AES.AESDecrypt(params, key, cipherText, iv, aad); - } - - method AESEncrypt(params: AESUtils.Params, iv: seq, key: seq, msg: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(params: AESUtils.Params, iv: seq, key: seq, msg: seq, aad: seq) returns (res : Result) requires |iv| == params.ivLen as int requires |key| == params.keyLen as int ensures res.Success? ==> |res.value.authTag| == params.tagLen as int - { - res := AES.AESEncrypt(params, iv, key, msg, aad); - } - - class {:extern "AES_GCM"} AES { - static method {:extern "AESDecrypt"} AESDecrypt(params: AESUtils.Params, - key: seq, - ctxt: seq, - iv: seq, - aad: seq) - returns (res: Result>) - requires |key| == params.keyLen as int - static method {:extern "AESEncrypt"} AESEncrypt (params: AESUtils.Params, - iv : seq, - key : seq, - msg : seq, - aad : seq) - returns (res : Result) - requires |iv| == params.ivLen as int - requires |key| == params.keyLen as int - ensures res.Success? ==> |res.value.authTag| == params.tagLen as int - } + method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: AESUtils.Params, key: seq, encryptionArtifacts: EncryptionArtifacts, iv: seq, aad: seq) + returns (res: Result>) + requires |key| == params.keyLen as int + requires |encryptionArtifacts.authTag| == params.tagLen as int } diff --git a/src/Crypto/EncryptionExtern.cs b/src/Crypto/EncryptionExtern.cs index df32dca6e..2e06624a8 100644 --- a/src/Crypto/EncryptionExtern.cs +++ b/src/Crypto/EncryptionExtern.cs @@ -37,29 +37,27 @@ public static STL.Result AESEncrypt(AESUtils.Params p, byte[] c = new byte[cipher.GetOutputSize(msg.Elements.Length)]; var len = cipher.ProcessBytes(msg.Elements, 0, msg.Elements.Length, c, 0); cipher.DoFinal(c, len); //Append authentication tag to `c` - return new STL.Result_Success( - new EncryptionArtifacts(new byteseq(c.Take(len - 1).ToArray()), new byteseq(c.Skip(len - 1).ToArray())) - ); + return new STL.Result_Success(__default.EncryptionArtifactFromByteSeq(byteseq.FromElements(c), p)); } catch { return new STL.Result_Failure(new Dafny.Sequence("aes encrypt err".ToCharArray())); } } - public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, byteseq ctx, byteseq iv, byteseq aad) { + public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, EncryptionArtifacts encArt, byteseq iv, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); var param = new AeadParameters(new KeyParameter(key.Elements), p.tagLen * 8, iv.Elements, aad.Elements); cipher.Init(false, param); + var ctx = encArt.cipherText.Concat(encArt.authTag); var pt = new byte[cipher.GetOutputSize(ctx.Elements.Length)]; var len = cipher.ProcessBytes(ctx.Elements, 0, ctx.Elements.Length, pt, 0); cipher.DoFinal(pt, len); //Check message authentication tag return new STL.Result_Success(new byteseq(pt)); - } - catch { - // TODO: distinguish BC error from unsuccessful decrypt + } catch(InvalidCipherTextException macEx) { + return new STL.Result_Failure(new Dafny.Sequence(macEx.ToString().ToCharArray())); + } catch { return new STL.Result_Failure(new Dafny.Sequence("aes decrypt err".ToCharArray())); - } } } diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index 544ebb612..cfc9ce508 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -73,17 +73,20 @@ module AESKeyring{ ensures res.Success? && old(encMat.plaintextDataKey.Some?) ==> res.value.plaintextDataKey == old(encMat.plaintextDataKey) ensures res.Failure? ==> unchanged(encMat) { - var dataKey := encMat.plaintextDataKey; - if dataKey.None? { - var k := RNG.GenBytes(encMat.algorithmSuiteID.KeyLength() as uint16); - dataKey := Some(k); + var dataKey: seq; + if encMat.plaintextDataKey.Some? { + dataKey := encMat.plaintextDataKey.get; + } else { + dataKey := RNG.GenBytes(encMat.algorithmSuiteID.KeyLength() as uint16); } var iv := RNG.GenBytes(wrappingAlgorithm.ivLen as uint16); var aad := Mat.FlattenSortEncCtx(encMat.encryptionContext); - var encryptResult :- AESEncryption.AESEncrypt(wrappingAlgorithm, iv, wrappingKey, dataKey.get, aad); + var encryptResult :- AESEncryption.AESEncrypt(wrappingAlgorithm, iv, wrappingKey, dataKey, aad); var providerInfo := SerializeProviderInto(iv); var edk := Mat.EncryptedDataKey(keyNamespace, providerInfo, encryptResult.cipherText + encryptResult.authTag); - encMat.plaintextDataKey := dataKey; + if encMat.plaintextDataKey.None? { + encMat.SetPlaintextDataKey(dataKey); + } encMat.encryptedDataKeys := encMat.encryptedDataKeys + [edk]; return Success(encMat); } @@ -127,15 +130,12 @@ module AESKeyring{ edks[i].ciphertext[wrappingAlgorithm.tagLen ..], edks[i].ciphertext[.. wrappingAlgorithm.tagLen] ); - var decryptResult := AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, encArt, iv, flatEncCtx); - if decryptResult.Success? { - var ptKey := decryptResult.value; - if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length - decMat.plaintextDataKey := Some(ptKey); - return Success(decMat); - } // Should we fail if the key length is incorrect? + var ptKey :- AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, encArt, iv, flatEncCtx); + if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length + decMat.setPlaintextDataKey(ptKey); + return Success(decMat); } else { - return Failure("Decryption failed"); + return Failure("Decryption failed: bad datakey length."); } } i := i + 1; From 29e3ed3ab6edc8f1c04e511aa9e545d7d45ed5b6 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Fri, 11 Oct 2019 14:46:44 -0700 Subject: [PATCH 08/17] Removing uses of except for the output of AESEncrypt --- src/Crypto/AESEncryption.dfy | 4 ++-- src/Crypto/EncryptionExtern.cs | 4 ++-- src/SDK/Keyring/AESKeyring.dfy | 7 ++----- src/SDK/ToyClient.dfy | 8 ++++---- 4 files changed, 10 insertions(+), 13 deletions(-) diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index a03ddd852..f8a1e928c 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -29,8 +29,8 @@ module {:extern "AESEncryption"} AESEncryption { requires |key| == params.keyLen as int ensures res.Success? ==> |res.value.authTag| == params.tagLen as int - method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: AESUtils.Params, key: seq, encryptionArtifacts: EncryptionArtifacts, iv: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: AESUtils.Params, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) returns (res: Result>) requires |key| == params.keyLen as int - requires |encryptionArtifacts.authTag| == params.tagLen as int + requires |authTag| == params.tagLen as int } diff --git a/src/Crypto/EncryptionExtern.cs b/src/Crypto/EncryptionExtern.cs index 2e06624a8..71597004b 100644 --- a/src/Crypto/EncryptionExtern.cs +++ b/src/Crypto/EncryptionExtern.cs @@ -44,12 +44,12 @@ public static STL.Result AESEncrypt(AESUtils.Params p, } } - public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, EncryptionArtifacts encArt, byteseq iv, byteseq aad) { + public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); var param = new AeadParameters(new KeyParameter(key.Elements), p.tagLen * 8, iv.Elements, aad.Elements); cipher.Init(false, param); - var ctx = encArt.cipherText.Concat(encArt.authTag); + var ctx = cipherText.Concat(authTag); var pt = new byte[cipher.GetOutputSize(ctx.Elements.Length)]; var len = cipher.ProcessBytes(ctx.Elements, 0, ctx.Elements.Length, pt, 0); cipher.DoFinal(pt, len); //Check message authentication tag diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index cfc9ce508..e28467dae 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -126,11 +126,8 @@ module AESKeyring{ if edks[i].providerID == keyNamespace && ValidProviderInfo(edks[i].providerInfo) && wrappingAlgorithm.tagLen as int <= |edks[i].ciphertext| { var iv := GetIvFromProvInfo(edks[i].providerInfo); var flatEncCtx: seq := Mat.FlattenSortEncCtx(decMat.encryptionContext); - var encArt := AESEncryption.EncryptionArtifacts( - edks[i].ciphertext[wrappingAlgorithm.tagLen ..], - edks[i].ciphertext[.. wrappingAlgorithm.tagLen] - ); - var ptKey :- AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, encArt, iv, flatEncCtx); + var cipherText, authTag := edks[i].ciphertext[wrappingAlgorithm.tagLen ..], edks[i].ciphertext[.. wrappingAlgorithm.tagLen]; + var ptKey :- AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, cipherText, authTag, iv, flatEncCtx); if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length decMat.setPlaintextDataKey(ptKey); return Success(decMat); diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index 11d5760e9..09819af87 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -21,7 +21,7 @@ module ToyClientDef { import AESEncryption import AESUtils - datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, iv: seq, ctxt: AESEncryption.EncryptionArtifacts) + datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, iv: seq, ctxt: seq, authTag: seq) const ALGORITHM := AESUtils.AES_GCM_256 @@ -76,12 +76,12 @@ module ToyClientDef { } var iv := RNG.GenBytes(ALGORITHM.ivLen as uint16); var ciphertext :- AESEncryption.AESEncrypt(ALGORITHM, iv ,em.plaintextDataKey.get, pt, []); - return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, iv, ciphertext)); + return Success(Encryption(em.encryptionContext, em.encryptedDataKeys, iv, ciphertext.cipherText, ciphertext.authTag)); } method Decrypt(e: Encryption) returns (res: Result>) requires Valid() - requires ALGORITHM.tagLen as int == |e.ctxt.authTag| + requires ALGORITHM.tagLen as int == |e.authTag| requires ALGORITHM.ivLen as int == |e.iv| ensures Valid() { @@ -92,7 +92,7 @@ module ToyClientDef { match decmat.plaintextDataKey case Some(dk) => if |dk| == 32 { - var msg := AESEncryption.AESDecrypt(ALGORITHM, dk, e.ctxt, e.iv, []); + var msg := AESEncryption.AESDecrypt(ALGORITHM, dk, e.ctxt, e.authTag, e.iv, []); return msg; } else { return Failure("bad dk"); From cc652088637fc9eb1ef2a6307894a21d6cf41cf2 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Tue, 15 Oct 2019 11:47:26 -0700 Subject: [PATCH 09/17] Remove AES Mode datatype --- src/Crypto/AESUtils.dfy | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/src/Crypto/AESUtils.dfy b/src/Crypto/AESUtils.dfy index 26109c7f5..5feb28ec7 100644 --- a/src/Crypto/AESUtils.dfy +++ b/src/Crypto/AESUtils.dfy @@ -4,22 +4,14 @@ module {:extern "AESUtils"} AESUtils { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - datatype Mode = AES256 | AES128 | AES192 - datatype Params = Params(mode: Mode, keyLen: uint8, tagLen: uint8, ivLen: uint8) + datatype Params = Params(keyLen: uint8, tagLen: uint8, ivLen: uint8) const MAX_KEY_LEN := 32 const CIPHER_KEY_LENGTHS := {32, 24, 16}; const TAG_LEN := 16 as uint8; const IV_LEN := 12 as uint8; - const AES_GCM_128 := Params(AES128, 16, TAG_LEN, IV_LEN) - const AES_GCM_192 := Params(AES192, 24, TAG_LEN, IV_LEN) - const AES_GCM_256 := Params(AES256, 32, TAG_LEN, IV_LEN) - - function method KeyLengthOfCipher(m: Mode): uint8 { - match m - case AES256 => 32 - case AES192 => 24 - case AES128 => 16 - } + const AES_GCM_128 := Params(16, TAG_LEN, IV_LEN) + const AES_GCM_192 := Params(24, TAG_LEN, IV_LEN) + const AES_GCM_256 := Params(32, TAG_LEN, IV_LEN) } From 5de67bf5b488be8d230fba6182c213c0f05f63a8 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Thu, 17 Oct 2019 14:52:22 -0700 Subject: [PATCH 10/17] Generalizing AESUtils --- Makefile | 2 +- src/Crypto/AESEncryption.dfy | 12 +- src/Crypto/AESUtils.dfy | 17 -- src/Crypto/EncryptionExtern.cs | 233 ---------------------------- src/Crypto/EncryptionParameters.dfy | 27 ++++ src/SDK/AlgorithmSuite.dfy | 24 +-- src/SDK/Keyring/AESKeyring.dfy | 10 +- src/SDK/ToyClient.dfy | 6 +- src/extern/dotnet/AESEncryption.cs | 4 +- 9 files changed, 56 insertions(+), 279 deletions(-) delete mode 100644 src/Crypto/AESUtils.dfy delete mode 100644 src/Crypto/EncryptionExtern.cs create mode 100644 src/Crypto/EncryptionParameters.dfy diff --git a/Makefile b/Makefile index 9539e78ed..cf2583ba5 100644 --- a/Makefile +++ b/Makefile @@ -10,7 +10,7 @@ endif # SRCS = $(foreach dir, $(SRCDIRS), $(wildcard $(dir)/*.dfy)) SRCS = \ src/Crypto/AESEncryption.dfy \ - src/Crypto/AESUtils.dfy \ + src/Crypto/EncryptionParameters.dfy \ src/Crypto/Digests.dfy \ src/Crypto/Random.dfy \ src/Crypto/RSAEncryption.dfy \ diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index f8a1e928c..b95b25870 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -1,21 +1,21 @@ include "../SDK/AlgorithmSuite.dfy" include "../StandardLibrary/StandardLibrary.dfy" -include "AESUtils.dfy" +include "EncryptionParameters.dfy" include "GenBytes.dfy" module {:extern "AESEncryption"} AESEncryption { - import AESUtils + import EncryptionParameters import opened StandardLibrary import opened UInt = StandardLibrary.UInt export - provides AESDecrypt, AESEncrypt, AESUtils, StandardLibrary, UInt + provides AESDecrypt, AESEncrypt, EncryptionParameters, StandardLibrary, UInt reveals EncryptionArtifacts // Is there a better name/location for this? datatype EncryptionArtifacts = EncryptionArtifacts(cipherText: seq, authTag: seq) - function method EncryptionArtifactFromByteSeq(s: seq, p: AESUtils.Params): (encArt: EncryptionArtifacts) + function method EncryptionArtifactFromByteSeq(s: seq, p: EncryptionParameters.Params): (encArt: EncryptionArtifacts) requires |s| >= p.tagLen as int ensures |encArt.cipherText + encArt.authTag| <= |s| ensures |encArt.authTag| == p.tagLen as int @@ -23,13 +23,13 @@ module {:extern "AESEncryption"} AESEncryption { EncryptionArtifacts(s[.. |s| - p.tagLen as int], s[|s| - p.tagLen as int ..]) } - method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(params: AESUtils.Params, iv: seq, key: seq, msg: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(params: EncryptionParameters.Params, iv: seq, key: seq, msg: seq, aad: seq) returns (res : Result) requires |iv| == params.ivLen as int requires |key| == params.keyLen as int ensures res.Success? ==> |res.value.authTag| == params.tagLen as int - method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: AESUtils.Params, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: EncryptionParameters.Params, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) returns (res: Result>) requires |key| == params.keyLen as int requires |authTag| == params.tagLen as int diff --git a/src/Crypto/AESUtils.dfy b/src/Crypto/AESUtils.dfy deleted file mode 100644 index 5feb28ec7..000000000 --- a/src/Crypto/AESUtils.dfy +++ /dev/null @@ -1,17 +0,0 @@ -include "../StandardLibrary/StandardLibrary.dfy" - -module {:extern "AESUtils"} AESUtils { - import opened StandardLibrary - import opened UInt = StandardLibrary.UInt - - datatype Params = Params(keyLen: uint8, tagLen: uint8, ivLen: uint8) - - const MAX_KEY_LEN := 32 - const CIPHER_KEY_LENGTHS := {32, 24, 16}; - const TAG_LEN := 16 as uint8; - const IV_LEN := 12 as uint8; - - const AES_GCM_128 := Params(16, TAG_LEN, IV_LEN) - const AES_GCM_192 := Params(24, TAG_LEN, IV_LEN) - const AES_GCM_256 := Params(32, TAG_LEN, IV_LEN) -} diff --git a/src/Crypto/EncryptionExtern.cs b/src/Crypto/EncryptionExtern.cs deleted file mode 100644 index 71597004b..000000000 --- a/src/Crypto/EncryptionExtern.cs +++ /dev/null @@ -1,233 +0,0 @@ -using System; -using System.Linq; -using System.IO; -using System.Text; -using Org.BouncyCastle.Crypto; -using Org.BouncyCastle.Crypto.Digests; -using Org.BouncyCastle.Crypto.EC; -using Org.BouncyCastle.Crypto.Engines; -using Org.BouncyCastle.Crypto.Encodings; -using Org.BouncyCastle.Crypto.Generators; -using Org.BouncyCastle.Crypto.Modes; -using Org.BouncyCastle.Crypto.Parameters; -using Org.BouncyCastle.Crypto.Prng; -using Org.BouncyCastle.Crypto.Signers; -using Org.BouncyCastle.Math; -using Org.BouncyCastle.Math.EC; -using Org.BouncyCastle.OpenSsl; -using Org.BouncyCastle.Security; -using Org.BouncyCastle.Asn1.X9; - -using byteseq = Dafny.Sequence; - -namespace AESEncryption { - //TODO This code has yet to be reviewed. See issue #36 - public partial class AES_GCM { - - public static STL.Result AESEncrypt(AESUtils.Params p, - byteseq iv, - byteseq key, - byteseq msg, - byteseq aad) { - try { - var cipher = new GcmBlockCipher(new AesEngine()); - var param = new AeadParameters(new KeyParameter(key.Elements), (int)p.tagLen * 8, iv.Elements, aad.Elements); - cipher.Init(true, param); - - byte[] c = new byte[cipher.GetOutputSize(msg.Elements.Length)]; - var len = cipher.ProcessBytes(msg.Elements, 0, msg.Elements.Length, c, 0); - cipher.DoFinal(c, len); //Append authentication tag to `c` - return new STL.Result_Success(__default.EncryptionArtifactFromByteSeq(byteseq.FromElements(c), p)); - } - catch { - return new STL.Result_Failure(new Dafny.Sequence("aes encrypt err".ToCharArray())); - } - } - - public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { - try { - var cipher = new GcmBlockCipher(new AesEngine()); - var param = new AeadParameters(new KeyParameter(key.Elements), p.tagLen * 8, iv.Elements, aad.Elements); - cipher.Init(false, param); - var ctx = cipherText.Concat(authTag); - var pt = new byte[cipher.GetOutputSize(ctx.Elements.Length)]; - var len = cipher.ProcessBytes(ctx.Elements, 0, ctx.Elements.Length, pt, 0); - cipher.DoFinal(pt, len); //Check message authentication tag - return new STL.Result_Success(new byteseq(pt)); - } catch(InvalidCipherTextException macEx) { - return new STL.Result_Failure(new Dafny.Sequence(macEx.ToString().ToCharArray())); - } catch { - return new STL.Result_Failure(new Dafny.Sequence("aes decrypt err".ToCharArray())); - } - } - } -} - // https://stackoverflow.com/questions/23056347/creating-rsa-public-private-key-pair-with-bouncy-castle-or-net-rsacryptoservice - -namespace RSAEncryption { - - public partial class RSA { - - public static void get_pem(AsymmetricCipherKeyPair kp, out byte[] pk, out byte[] sk) { - using (var stringWriter = new StringWriter()) { - var pemWriter = new PemWriter(stringWriter); - pemWriter.WriteObject(kp.Public); - pk = Encoding.UTF8.GetBytes(stringWriter.ToString()); - } - - using (var stringWriter = new StringWriter()) { - var pemWriter = new PemWriter(stringWriter); - pemWriter.WriteObject(kp.Private); - sk = Encoding.UTF8.GetBytes(stringWriter.ToString()); - } - } - - const int RSA_PUBLIC_EXPONENT = (65537); - const int RSA_CERTAINTY = 256; - - public static void RSAKeygen(int bits, RSAPaddingMode padding, out byteseq ek, out byteseq dk) { - RsaKeyPairGenerator gen = new RsaKeyPairGenerator(); - SecureRandom rng = new SecureRandom(); - gen.Init(new RsaKeyGenerationParameters(BigInteger.ValueOf(RSA_PUBLIC_EXPONENT), rng, bits, RSA_CERTAINTY)); - AsymmetricCipherKeyPair kp = gen.GenerateKeyPair(); - byte[] e; - byte[] d; - get_pem(kp, out e, out d); - ek = new byteseq(e); - dk = new byteseq(d); - } - - public static STL.Option RSAEncrypt(int bits, RSAPaddingMode padding, byteseq ek, byteseq msg) { - try { - AsymmetricKeyParameter pub; - using (var stringReader = new StringReader(Encoding.UTF8.GetString(ek.Elements))) - { - var pemReader = new PemReader(stringReader); - var pemObject = pemReader.ReadObject(); - pub = ((AsymmetricKeyParameter)pemObject); - } - - IAsymmetricBlockCipher engine; - - if (padding.is_PKCS1) { - engine = new Pkcs1Encoding(new RsaEngine()); - } else if (padding.is_OAEP__SHA1) { - engine = new OaepEncoding(new RsaEngine(), new Sha1Digest()); - } - else { // paddingi_is_OAEP__SHA256 - engine = new OaepEncoding(new RsaEngine(), new Sha256Digest()); - } - - engine.Init(true, pub); - return new STL.Option_Some(new byteseq(engine.ProcessBlock(msg.Elements, 0, msg.Elements.Length))); - } - catch { - return new STL.Option_None(); - } - - } - - // https://stackoverflow.com/questions/28086321/c-sharp-bouncycastle-rsa-encryption-with-public-private-keys - - public static STL.Option RSADecrypt(int bits, RSAPaddingMode padding, byteseq dk, byteseq ctx) { - try { - AsymmetricCipherKeyPair keyPair; - - IAsymmetricBlockCipher engine; - - if (padding.is_PKCS1) { - engine = new Pkcs1Encoding(new RsaEngine()); - } else if (padding.is_OAEP__SHA1) { - engine = new OaepEncoding(new RsaEngine(), new Sha1Digest(), null); - } - else { // paddingi_is_OAEP__SHA256 - engine = new OaepEncoding(new RsaEngine(), new Sha256Digest(), null); - } - - using ( var txtreader = new StringReader(Encoding.UTF8.GetString(dk.Elements))) { - keyPair = (AsymmetricCipherKeyPair) new PemReader(txtreader).ReadObject(); - engine.Init(false, keyPair.Private); - } - return new STL.Option_Some(new byteseq(engine.ProcessBlock(ctx.Elements, 0, ctx.Elements.Length))); - } - catch { - return new STL.Option_None(); - } - } - } -} - -namespace Signature { - public partial class ECDSA { - public static STL.Option<_System.Tuple2> KeyGen(ECDSAParams x) { - try { - ECKeyPairGenerator g = new ECKeyPairGenerator(); - SecureRandom rng = new SecureRandom(); - X9ECParameters p; - if (x.is_ECDSA__P384) { - p = ECNamedCurveTable.GetByName("secp384r1"); - g.Init(new ECKeyGenerationParameters(new ECDomainParameters(p.Curve, p.G, p.N, p.H), rng)); - } - else { // x is ECDSA__P256 - p = ECNamedCurveTable.GetByName("secp256r1"); - g.Init(new ECKeyGenerationParameters(new ECDomainParameters(p.Curve, p.G, p.N, p.H), rng)); - } - AsymmetricCipherKeyPair kp = g.GenerateKeyPair(); - ECPoint pt = ((ECPublicKeyParameters)kp.Public).Q; - byteseq vk = new byteseq(pt.GetEncoded()); - byteseq sk = new byteseq(((ECPrivateKeyParameters)kp.Private).D.ToByteArray()); - return new STL.Option_Some<_System.Tuple2>(new _System.Tuple2(vk, sk)); - } - catch { - return new STL.Option_None<_System.Tuple2>(); - } - } - - public static bool Verify(ECDSAParams x, byteseq vk, byteseq msg, _System.Tuple2 sig) { - try { - X9ECParameters p; - if (x.is_ECDSA__P384) { - p = ECNamedCurveTable.GetByName("secp384r1"); - } - else { - p = ECNamedCurveTable.GetByName("secp256r1"); - } - ECDomainParameters dp = new ECDomainParameters(p.Curve, p.G, p.N, p.H); - ECPoint pt = p.Curve.DecodePoint(vk.Elements); - ECPublicKeyParameters vkp = new ECPublicKeyParameters(pt, dp); - ECDsaSigner sign = new ECDsaSigner(); - sign.Init(false, vkp); - BigInteger r = new BigInteger(sig._0.Elements); - BigInteger s = new BigInteger(sig._1.Elements); - return sign.VerifySignature(msg.Elements, r, s); - } - catch { - return false; - } - } - - public static STL.Option<_System.Tuple2> Sign(ECDSAParams x, byteseq sk, byteseq msg) { - try { - X9ECParameters p; - if (x.is_ECDSA__P384) { - p = ECNamedCurveTable.GetByName("secp384r1"); - } - else { - p = ECNamedCurveTable.GetByName("secp256r1"); - } - ECDomainParameters dp = new ECDomainParameters(p.Curve, p.G, p.N, p.H); - ECPrivateKeyParameters skp = new ECPrivateKeyParameters(new BigInteger(sk.Elements), dp); - ECDsaSigner sign = new ECDsaSigner(); - sign.Init(true, skp); - BigInteger[] sig = sign.GenerateSignature(msg.Elements); - byte[] r = sig[0].ToByteArray(); - byte[] s = sig[1].ToByteArray(); - return new STL.Option_Some<_System.Tuple2>(new _System.Tuple2(new byteseq(r), new byteseq(s))); - } - catch { - return new STL.Option_None<_System.Tuple2>(); - } - } - - } -} diff --git a/src/Crypto/EncryptionParameters.dfy b/src/Crypto/EncryptionParameters.dfy new file mode 100644 index 000000000..eb48e7b39 --- /dev/null +++ b/src/Crypto/EncryptionParameters.dfy @@ -0,0 +1,27 @@ +include "../StandardLibrary/StandardLibrary.dfy" + +module EncryptionParameters { + import opened StandardLibrary + import opened UInt = StandardLibrary.UInt + + datatype Algorithm = AES + datatype Mode = GCM + + datatype Params = Params(alg: Algorithm, mode: Mode, keyLen: uint8, tagLen: uint8, ivLen: uint8) + { + predicate Valid() { + // mmtj: Should we include GCM in this match/Is there any further validation reasoning to do? + match alg + case AES => keyLen as int in AES_CIPHER_KEY_LENGTHS && tagLen == AES_TAG_LEN && ivLen == AES_IV_LEN + } + } + + const AES_MAX_KEY_LEN := 32 + const AES_CIPHER_KEY_LENGTHS := {32, 24, 16}; + const AES_TAG_LEN := 16 as uint8; + const AES_IV_LEN := 12 as uint8; + + const AES_GCM_128 := Params(AES, GCM, 16, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_192 := Params(AES, GCM, 24, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_256 := Params(AES, GCM, 32, AES_TAG_LEN, AES_IV_LEN) +} diff --git a/src/SDK/AlgorithmSuite.dfy b/src/SDK/AlgorithmSuite.dfy index aed697417..8f8a07abe 100644 --- a/src/SDK/AlgorithmSuite.dfy +++ b/src/SDK/AlgorithmSuite.dfy @@ -1,4 +1,4 @@ -include "../Crypto/AESUtils.dfy" +include "../Crypto/EncryptionParameters.dfy" include "../Crypto/Digests.dfy" include "../Crypto/Signature.dfy" include "../StandardLibrary/StandardLibrary.dfy" @@ -6,7 +6,7 @@ include "../StandardLibrary/StandardLibrary.dfy" module AlgorithmSuite { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - import AES = AESUtils + import P = EncryptionParameters import S = Signature import Digests @@ -41,18 +41,18 @@ module AlgorithmSuite { const AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0046 const AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0014 - datatype AlgSuite = AlgSuite(params: AES.Params, hkdf: Digests.HMAC_ALGORITHM, sign: Option) + datatype AlgSuite = AlgSuite(params: P.Params, hkdf: Digests.HMAC_ALGORITHM, sign: Option) const Suite := map [ - AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(AES.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(AES.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), - AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES.AES_GCM_256, Digests.HmacSHA256, None), - AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES.AES_GCM_192, Digests.HmacSHA256, None), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(AES.AES_GCM_128, Digests.HmacSHA256, None), - AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES.AES_GCM_256, Digests.HmacNOSHA, None), - AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES.AES_GCM_192, Digests.HmacNOSHA, None), - AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(AES.AES_GCM_128, Digests.HmacNOSHA, None) + AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(P.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(P.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(P.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), + AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(P.AES_GCM_256, Digests.HmacSHA256, None), + AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(P.AES_GCM_192, Digests.HmacSHA256, None), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(P.AES_GCM_128, Digests.HmacSHA256, None), + AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(P.AES_GCM_256, Digests.HmacNOSHA, None), + AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(P.AES_GCM_192, Digests.HmacNOSHA, None), + AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(P.AES_GCM_128, Digests.HmacNOSHA, None) ] /* Suite is intended to have an entry for each possible value of ID. This is stated and checked in three ways. diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index 188266dd0..521f6f1a8 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -2,7 +2,7 @@ include "../../StandardLibrary/StandardLibrary.dfy" include "../../StandardLibrary/UInt.dfy" include "../AlgorithmSuite.dfy" include "./Defs.dfy" -include "../../Crypto/AESUtils.dfy" +include "../../Crypto/EncryptionParameters.dfy" include "../../Crypto/Random.dfy" include "../../Crypto/AESEncryption.dfy" include "../Materials.dfy" @@ -11,7 +11,7 @@ module AESKeyring{ import opened StandardLibrary import opened UInt = StandardLibrary.UInt import AESEncryption - import AESUtils + import EncryptionParameters import AlgorithmSuite import Random import KeyringDefs @@ -19,13 +19,13 @@ module AESKeyring{ const AUTH_TAG_LEN_LEN := 4; const IV_LEN_LEN := 4; - const VALID_ALGORITHMS := {AESUtils.AES_GCM_128, AESUtils.AES_GCM_192, AESUtils.AES_GCM_256} + const VALID_ALGORITHMS := {EncryptionParameters.AES_GCM_128, EncryptionParameters.AES_GCM_192, EncryptionParameters.AES_GCM_256} class AESKeyring extends KeyringDefs.Keyring { const keyNamespace: string const keyName: string const wrappingKey: seq - const wrappingAlgorithm: AESUtils.Params + const wrappingAlgorithm: EncryptionParameters.Params predicate Valid() reads this { Repr == {this} && @@ -34,7 +34,7 @@ module AESKeyring{ StringIs8Bit(keyNamespace) && StringIs8Bit(keyName) } - constructor(namespace: string, name: string, key: seq, wrappingAlg: AESUtils.Params) + constructor(namespace: string, name: string, key: seq, wrappingAlg: EncryptionParameters.Params) requires StringIs8Bit(namespace) && StringIs8Bit(name) requires wrappingAlg in VALID_ALGORITHMS requires |key| == wrappingAlg.keyLen as int diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index 97c59c1e2..3f11397b3 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -6,7 +6,7 @@ include "CMM/DefaultCMM.dfy" include "Keyring/Defs.dfy" include "Materials.dfy" include "../Crypto/AESEncryption.dfy" -include "../Crypto/AESUtils.dfy" +include "../Crypto/EncryptionParameters.dfy" include "../Crypto/Random.dfy" module ToyClientDef { @@ -19,11 +19,11 @@ module ToyClientDef { import Random import AlgorithmSuite import AESEncryption - import AESUtils + import EncryptionParameters datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, iv: seq, ctxt: seq, authTag: seq) - const ALGORITHM := AESUtils.AES_GCM_256 + const ALGORITHM := EncryptionParameters.AES_GCM_256 class Client { var cmm: CMMDefs.CMM diff --git a/src/extern/dotnet/AESEncryption.cs b/src/extern/dotnet/AESEncryption.cs index d9a580b25..20ab79e0c 100644 --- a/src/extern/dotnet/AESEncryption.cs +++ b/src/extern/dotnet/AESEncryption.cs @@ -12,7 +12,7 @@ namespace AESEncryption { //TODO This code has yet to be reviewed. See issue #36 public partial class AES_GCM { - public static STL.Result AESEncrypt(AESUtils.Params p, + public static STL.Result AESEncrypt(EncryptionParameters.Params p, byteseq iv, byteseq key, byteseq msg, @@ -32,7 +32,7 @@ public static STL.Result AESEncrypt(AESUtils.Params p, } } - public static STL.Result AESDecrypt(AESUtils.Params p, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { + public static STL.Result AESDecrypt(EncryptionParameters.Params p, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); var param = new AeadParameters(new KeyParameter(key.Elements), p.tagLen * 8, iv.Elements, aad.Elements); From 33c7dcf53e1dc5069488b663761f7abef0474845 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Thu, 17 Oct 2019 15:13:13 -0700 Subject: [PATCH 11/17] Fix make build --- src/Crypto/EncryptionParameters.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Crypto/EncryptionParameters.dfy b/src/Crypto/EncryptionParameters.dfy index eb48e7b39..adf6ffa6b 100644 --- a/src/Crypto/EncryptionParameters.dfy +++ b/src/Crypto/EncryptionParameters.dfy @@ -1,6 +1,6 @@ include "../StandardLibrary/StandardLibrary.dfy" -module EncryptionParameters { +module {:extern "EncryptionParameters"} EncryptionParameters { import opened StandardLibrary import opened UInt = StandardLibrary.UInt From ad8be28f25eb31f9859d14142239b3b8bce5d34b Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Fri, 18 Oct 2019 13:37:15 -0700 Subject: [PATCH 12/17] Address PR comments, propagate Params.Valid() predicate. --- Makefile | 2 +- src/Crypto/AESEncryption.dfy | 30 ++++++++++++------- ...arameters.dfy => EncryptionAlgorithms.dfy} | 2 +- src/SDK/AlgorithmSuite.dfy | 4 +-- src/SDK/Keyring/AESKeyring.dfy | 13 ++++---- src/SDK/ToyClient.dfy | 6 ++-- src/extern/dotnet/AESEncryption.cs | 8 ++--- 7 files changed, 38 insertions(+), 27 deletions(-) rename src/Crypto/{EncryptionParameters.dfy => EncryptionAlgorithms.dfy} (93%) diff --git a/Makefile b/Makefile index cf2583ba5..0cf4a756e 100644 --- a/Makefile +++ b/Makefile @@ -10,7 +10,7 @@ endif # SRCS = $(foreach dir, $(SRCDIRS), $(wildcard $(dir)/*.dfy)) SRCS = \ src/Crypto/AESEncryption.dfy \ - src/Crypto/EncryptionParameters.dfy \ + src/Crypto/EncryptionAlgorithms.dfy \ src/Crypto/Digests.dfy \ src/Crypto/Random.dfy \ src/Crypto/RSAEncryption.dfy \ diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index b95b25870..6a2fe904c 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -1,36 +1,44 @@ include "../SDK/AlgorithmSuite.dfy" include "../StandardLibrary/StandardLibrary.dfy" -include "EncryptionParameters.dfy" +include "EncryptionAlgorithms.dfy" include "GenBytes.dfy" module {:extern "AESEncryption"} AESEncryption { - import EncryptionParameters + import EncryptionAlgorithms import opened StandardLibrary import opened UInt = StandardLibrary.UInt export - provides AESDecrypt, AESEncrypt, EncryptionParameters, StandardLibrary, UInt - reveals EncryptionArtifacts + provides AESDecrypt, AESEncrypt, EncryptionAlgorithms, StandardLibrary, UInt + reveals EncryptionOutput // Is there a better name/location for this? - datatype EncryptionArtifacts = EncryptionArtifacts(cipherText: seq, authTag: seq) + datatype EncryptionOutput = EncryptionOutput(cipherText: seq, authTag: seq) - function method EncryptionArtifactFromByteSeq(s: seq, p: EncryptionParameters.Params): (encArt: EncryptionArtifacts) + function method EncryptionArtifactFromByteSeq(s: seq, p: EncryptionAlgorithms.Params): (encArt: EncryptionOutput) + requires p.Valid() requires |s| >= p.tagLen as int - ensures |encArt.cipherText + encArt.authTag| <= |s| + ensures |encArt.cipherText + encArt.authTag| == |s| ensures |encArt.authTag| == p.tagLen as int { - EncryptionArtifacts(s[.. |s| - p.tagLen as int], s[|s| - p.tagLen as int ..]) + EncryptionOutput(s[.. |s| - p.tagLen as int], s[|s| - p.tagLen as int ..]) } - method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(params: EncryptionParameters.Params, iv: seq, key: seq, msg: seq, aad: seq) - returns (res : Result) + method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(params: EncryptionAlgorithms.Params, iv: seq, key: seq, msg: seq, aad: seq) + returns (res : Result) + requires params.Valid() + requires params.alg.AES? + requires params.mode.GCM? requires |iv| == params.ivLen as int requires |key| == params.keyLen as int ensures res.Success? ==> |res.value.authTag| == params.tagLen as int - method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: EncryptionParameters.Params, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: EncryptionAlgorithms.Params, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) returns (res: Result>) + requires params.Valid() + requires params.alg.AES? + requires params.mode.GCM? requires |key| == params.keyLen as int + requires |iv| == params.ivLen as int requires |authTag| == params.tagLen as int } diff --git a/src/Crypto/EncryptionParameters.dfy b/src/Crypto/EncryptionAlgorithms.dfy similarity index 93% rename from src/Crypto/EncryptionParameters.dfy rename to src/Crypto/EncryptionAlgorithms.dfy index adf6ffa6b..bdeca2470 100644 --- a/src/Crypto/EncryptionParameters.dfy +++ b/src/Crypto/EncryptionAlgorithms.dfy @@ -1,6 +1,6 @@ include "../StandardLibrary/StandardLibrary.dfy" -module {:extern "EncryptionParameters"} EncryptionParameters { +module {:extern "EncryptionAlgorithms"} EncryptionAlgorithms { import opened StandardLibrary import opened UInt = StandardLibrary.UInt diff --git a/src/SDK/AlgorithmSuite.dfy b/src/SDK/AlgorithmSuite.dfy index 8f8a07abe..d04ddeea2 100644 --- a/src/SDK/AlgorithmSuite.dfy +++ b/src/SDK/AlgorithmSuite.dfy @@ -1,4 +1,4 @@ -include "../Crypto/EncryptionParameters.dfy" +include "../Crypto/EncryptionAlgorithms.dfy" include "../Crypto/Digests.dfy" include "../Crypto/Signature.dfy" include "../StandardLibrary/StandardLibrary.dfy" @@ -6,7 +6,7 @@ include "../StandardLibrary/StandardLibrary.dfy" module AlgorithmSuite { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - import P = EncryptionParameters + import P = EncryptionAlgorithms import S = Signature import Digests diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index 521f6f1a8..b95ebe7c0 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -2,7 +2,7 @@ include "../../StandardLibrary/StandardLibrary.dfy" include "../../StandardLibrary/UInt.dfy" include "../AlgorithmSuite.dfy" include "./Defs.dfy" -include "../../Crypto/EncryptionParameters.dfy" +include "../../Crypto/EncryptionAlgorithms.dfy" include "../../Crypto/Random.dfy" include "../../Crypto/AESEncryption.dfy" include "../Materials.dfy" @@ -11,7 +11,7 @@ module AESKeyring{ import opened StandardLibrary import opened UInt = StandardLibrary.UInt import AESEncryption - import EncryptionParameters + import EncryptionAlgorithms import AlgorithmSuite import Random import KeyringDefs @@ -19,24 +19,26 @@ module AESKeyring{ const AUTH_TAG_LEN_LEN := 4; const IV_LEN_LEN := 4; - const VALID_ALGORITHMS := {EncryptionParameters.AES_GCM_128, EncryptionParameters.AES_GCM_192, EncryptionParameters.AES_GCM_256} + const VALID_ALGORITHMS := {EncryptionAlgorithms.AES_GCM_128, EncryptionAlgorithms.AES_GCM_192, EncryptionAlgorithms.AES_GCM_256} class AESKeyring extends KeyringDefs.Keyring { const keyNamespace: string const keyName: string const wrappingKey: seq - const wrappingAlgorithm: EncryptionParameters.Params + const wrappingAlgorithm: EncryptionAlgorithms.Params predicate Valid() reads this { Repr == {this} && |wrappingKey| == wrappingAlgorithm.keyLen as int && wrappingAlgorithm in VALID_ALGORITHMS && + wrappingAlgorithm.Valid() && StringIs8Bit(keyNamespace) && StringIs8Bit(keyName) } - constructor(namespace: string, name: string, key: seq, wrappingAlg: EncryptionParameters.Params) + constructor(namespace: string, name: string, key: seq, wrappingAlg: EncryptionAlgorithms.Params) requires StringIs8Bit(namespace) && StringIs8Bit(name) requires wrappingAlg in VALID_ALGORITHMS + requires wrappingAlg.Valid() requires |key| == wrappingAlg.keyLen as int ensures keyNamespace == namespace ensures keyName == name @@ -125,6 +127,7 @@ module AESKeyring{ if edks[i].providerID == keyNamespace && ValidProviderInfo(edks[i].providerInfo) && wrappingAlgorithm.tagLen as int <= |edks[i].ciphertext| { var iv := GetIvFromProvInfo(edks[i].providerInfo); var flatEncCtx: seq := Mat.FlattenSortEncCtx(decMat.encryptionContext); + //TODO: #68 var cipherText, authTag := edks[i].ciphertext[wrappingAlgorithm.tagLen ..], edks[i].ciphertext[.. wrappingAlgorithm.tagLen]; var ptKey :- AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, cipherText, authTag, iv, flatEncCtx); if |ptKey| == decMat.algorithmSuiteID.KeyLength() { // check for correct key length diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index 3f11397b3..73f2fc561 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -6,7 +6,7 @@ include "CMM/DefaultCMM.dfy" include "Keyring/Defs.dfy" include "Materials.dfy" include "../Crypto/AESEncryption.dfy" -include "../Crypto/EncryptionParameters.dfy" +include "../Crypto/EncryptionAlgorithms.dfy" include "../Crypto/Random.dfy" module ToyClientDef { @@ -19,11 +19,11 @@ module ToyClientDef { import Random import AlgorithmSuite import AESEncryption - import EncryptionParameters + import EncryptionAlgorithms datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, iv: seq, ctxt: seq, authTag: seq) - const ALGORITHM := EncryptionParameters.AES_GCM_256 + const ALGORITHM := EncryptionAlgorithms.AES_GCM_256 class Client { var cmm: CMMDefs.CMM diff --git a/src/extern/dotnet/AESEncryption.cs b/src/extern/dotnet/AESEncryption.cs index 20ab79e0c..22b078c92 100644 --- a/src/extern/dotnet/AESEncryption.cs +++ b/src/extern/dotnet/AESEncryption.cs @@ -12,7 +12,7 @@ namespace AESEncryption { //TODO This code has yet to be reviewed. See issue #36 public partial class AES_GCM { - public static STL.Result AESEncrypt(EncryptionParameters.Params p, + public static STL.Result AESEncrypt(EncryptionAlgorithms.Params p, byteseq iv, byteseq key, byteseq msg, @@ -25,14 +25,14 @@ public static STL.Result AESEncrypt(EncryptionParameters.Pa byte[] c = new byte[cipher.GetOutputSize(msg.Elements.Length)]; var len = cipher.ProcessBytes(msg.Elements, 0, msg.Elements.Length, c, 0); cipher.DoFinal(c, len); //Append authentication tag to `c` - return new STL.Result_Success(__default.EncryptionArtifactFromByteSeq(byteseq.FromElements(c), p)); + return new STL.Result_Success(__default.EncryptionArtifactFromByteSeq(byteseq.FromElements(c), p)); } catch { - return new STL.Result_Failure(new Dafny.Sequence("aes encrypt err".ToCharArray())); + return new STL.Result_Failure(new Dafny.Sequence("aes encrypt err".ToCharArray())); } } - public static STL.Result AESDecrypt(EncryptionParameters.Params p, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { + public static STL.Result AESDecrypt(EncryptionAlgorithms.Params p, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); var param = new AeadParameters(new KeyParameter(key.Elements), p.tagLen * 8, iv.Elements, aad.Elements); From f82cbceed9f1fe0f9b2c2b620c691cfdac33feb2 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Mon, 21 Oct 2019 10:46:12 -0700 Subject: [PATCH 13/17] Remove the `mode` field from EncryptionAlgorithms.Params. The field now resides inside the AES datatype. --- src/Crypto/AESEncryption.dfy | 4 ++-- src/Crypto/EncryptionAlgorithms.dfy | 15 +++++++-------- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index 6a2fe904c..4f6489ca6 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -28,7 +28,7 @@ module {:extern "AESEncryption"} AESEncryption { returns (res : Result) requires params.Valid() requires params.alg.AES? - requires params.mode.GCM? + requires params.alg.mode.GCM? requires |iv| == params.ivLen as int requires |key| == params.keyLen as int ensures res.Success? ==> |res.value.authTag| == params.tagLen as int @@ -37,7 +37,7 @@ module {:extern "AESEncryption"} AESEncryption { returns (res: Result>) requires params.Valid() requires params.alg.AES? - requires params.mode.GCM? + requires params.alg.mode.GCM? requires |key| == params.keyLen as int requires |iv| == params.ivLen as int requires |authTag| == params.tagLen as int diff --git a/src/Crypto/EncryptionAlgorithms.dfy b/src/Crypto/EncryptionAlgorithms.dfy index bdeca2470..c9c2b12bc 100644 --- a/src/Crypto/EncryptionAlgorithms.dfy +++ b/src/Crypto/EncryptionAlgorithms.dfy @@ -4,15 +4,14 @@ module {:extern "EncryptionAlgorithms"} EncryptionAlgorithms { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - datatype Algorithm = AES - datatype Mode = GCM + datatype Algorithm = AES(mode: AESMode) + datatype AESMode = GCM - datatype Params = Params(alg: Algorithm, mode: Mode, keyLen: uint8, tagLen: uint8, ivLen: uint8) + datatype Params = Params(alg: Algorithm, keyLen: uint8, tagLen: uint8, ivLen: uint8) { predicate Valid() { - // mmtj: Should we include GCM in this match/Is there any further validation reasoning to do? match alg - case AES => keyLen as int in AES_CIPHER_KEY_LENGTHS && tagLen == AES_TAG_LEN && ivLen == AES_IV_LEN + case AES(mode) => keyLen as int in AES_CIPHER_KEY_LENGTHS && tagLen == AES_TAG_LEN && ivLen == AES_IV_LEN && mode == GCM } } @@ -21,7 +20,7 @@ module {:extern "EncryptionAlgorithms"} EncryptionAlgorithms { const AES_TAG_LEN := 16 as uint8; const AES_IV_LEN := 12 as uint8; - const AES_GCM_128 := Params(AES, GCM, 16, AES_TAG_LEN, AES_IV_LEN) - const AES_GCM_192 := Params(AES, GCM, 24, AES_TAG_LEN, AES_IV_LEN) - const AES_GCM_256 := Params(AES, GCM, 32, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_128 := Params(AES(GCM), 16, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_192 := Params(AES(GCM), 24, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_256 := Params(AES(GCM), 32, AES_TAG_LEN, AES_IV_LEN) } From 52f55a977b02f0e2cf299634eed92c235c47da0e Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Mon, 21 Oct 2019 14:53:38 -0700 Subject: [PATCH 14/17] Remove old comment --- src/Crypto/AESEncryption.dfy | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index 4f6489ca6..d2ff3388f 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -12,7 +12,6 @@ module {:extern "AESEncryption"} AESEncryption { provides AESDecrypt, AESEncrypt, EncryptionAlgorithms, StandardLibrary, UInt reveals EncryptionOutput - // Is there a better name/location for this? datatype EncryptionOutput = EncryptionOutput(cipherText: seq, authTag: seq) function method EncryptionArtifactFromByteSeq(s: seq, p: EncryptionAlgorithms.Params): (encArt: EncryptionOutput) From f57321c52bc72fda95e25eae8d98015ffefba034 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Mon, 21 Oct 2019 15:52:17 -0700 Subject: [PATCH 15/17] Rename `Params` to `EncryptionAlgorithm`. --- src/Crypto/AESEncryption.dfy | 38 ++++++++++++++--------------- src/Crypto/EncryptionAlgorithms.dfy | 8 +++--- src/SDK/AlgorithmSuite.dfy | 28 ++++++++++----------- src/SDK/Keyring/AESKeyring.dfy | 4 +-- src/extern/dotnet/AESEncryption.cs | 10 ++++---- 5 files changed, 44 insertions(+), 44 deletions(-) diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index d2ff3388f..04d7904af 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -14,30 +14,30 @@ module {:extern "AESEncryption"} AESEncryption { datatype EncryptionOutput = EncryptionOutput(cipherText: seq, authTag: seq) - function method EncryptionArtifactFromByteSeq(s: seq, p: EncryptionAlgorithms.Params): (encArt: EncryptionOutput) - requires p.Valid() - requires |s| >= p.tagLen as int + function method EncryptionArtifactFromByteSeq(s: seq, encAlg: EncryptionAlgorithms.EncryptionAlgorithm): (encArt: EncryptionOutput) + requires encAlg.Valid() + requires |s| >= encAlg.tagLen as int ensures |encArt.cipherText + encArt.authTag| == |s| - ensures |encArt.authTag| == p.tagLen as int + ensures |encArt.authTag| == encAlg.tagLen as int { - EncryptionOutput(s[.. |s| - p.tagLen as int], s[|s| - p.tagLen as int ..]) + EncryptionOutput(s[.. |s| - encAlg.tagLen as int], s[|s| - encAlg.tagLen as int ..]) } - method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(params: EncryptionAlgorithms.Params, iv: seq, key: seq, msg: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(encAlg: EncryptionAlgorithms.EncryptionAlgorithm, iv: seq, key: seq, msg: seq, aad: seq) returns (res : Result) - requires params.Valid() - requires params.alg.AES? - requires params.alg.mode.GCM? - requires |iv| == params.ivLen as int - requires |key| == params.keyLen as int - ensures res.Success? ==> |res.value.authTag| == params.tagLen as int + requires encAlg.Valid() + requires encAlg.alg.AES? + requires encAlg.alg.mode.GCM? + requires |iv| == encAlg.ivLen as int + requires |key| == encAlg.keyLen as int + ensures res.Success? ==> |res.value.authTag| == encAlg.tagLen as int - method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(params: EncryptionAlgorithms.Params, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(encAlg: EncryptionAlgorithms.EncryptionAlgorithm, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) returns (res: Result>) - requires params.Valid() - requires params.alg.AES? - requires params.alg.mode.GCM? - requires |key| == params.keyLen as int - requires |iv| == params.ivLen as int - requires |authTag| == params.tagLen as int + requires encAlg.Valid() + requires encAlg.alg.AES? + requires encAlg.alg.mode.GCM? + requires |key| == encAlg.keyLen as int + requires |iv| == encAlg.ivLen as int + requires |authTag| == encAlg.tagLen as int } diff --git a/src/Crypto/EncryptionAlgorithms.dfy b/src/Crypto/EncryptionAlgorithms.dfy index c9c2b12bc..da1a7146f 100644 --- a/src/Crypto/EncryptionAlgorithms.dfy +++ b/src/Crypto/EncryptionAlgorithms.dfy @@ -7,7 +7,7 @@ module {:extern "EncryptionAlgorithms"} EncryptionAlgorithms { datatype Algorithm = AES(mode: AESMode) datatype AESMode = GCM - datatype Params = Params(alg: Algorithm, keyLen: uint8, tagLen: uint8, ivLen: uint8) + datatype EncryptionAlgorithm = EncryptionAlgorithm(alg: Algorithm, keyLen: uint8, tagLen: uint8, ivLen: uint8) { predicate Valid() { match alg @@ -20,7 +20,7 @@ module {:extern "EncryptionAlgorithms"} EncryptionAlgorithms { const AES_TAG_LEN := 16 as uint8; const AES_IV_LEN := 12 as uint8; - const AES_GCM_128 := Params(AES(GCM), 16, AES_TAG_LEN, AES_IV_LEN) - const AES_GCM_192 := Params(AES(GCM), 24, AES_TAG_LEN, AES_IV_LEN) - const AES_GCM_256 := Params(AES(GCM), 32, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_128 := EncryptionAlgorithm(AES(GCM), 16, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_192 := EncryptionAlgorithm(AES(GCM), 24, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_256 := EncryptionAlgorithm(AES(GCM), 32, AES_TAG_LEN, AES_IV_LEN) } diff --git a/src/SDK/AlgorithmSuite.dfy b/src/SDK/AlgorithmSuite.dfy index d04ddeea2..2daa981ae 100644 --- a/src/SDK/AlgorithmSuite.dfy +++ b/src/SDK/AlgorithmSuite.dfy @@ -6,7 +6,7 @@ include "../StandardLibrary/StandardLibrary.dfy" module AlgorithmSuite { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - import P = EncryptionAlgorithms + import EncryptionAlgorithms import S = Signature import Digests @@ -15,15 +15,15 @@ module AlgorithmSuite { newtype ID = x | x in VALID_IDS witness 0x0014 { function method KeyLength(): nat { - Suite[this].params.keyLen as nat + Suite[this].algorithm.keyLen as nat } function method IVLength(): nat { - Suite[this].params.ivLen as nat + Suite[this].algorithm.ivLen as nat } function method TagLength(): nat { - Suite[this].params.tagLen as nat + Suite[this].algorithm.tagLen as nat } function method SignatureType(): Option { @@ -41,18 +41,18 @@ module AlgorithmSuite { const AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0046 const AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0014 - datatype AlgSuite = AlgSuite(params: P.Params, hkdf: Digests.HMAC_ALGORITHM, sign: Option) + datatype AlgSuite = AlgSuite(algorithm: EncryptionAlgorithms.EncryptionAlgorithm, hkdf: Digests.HMAC_ALGORITHM, sign: Option) const Suite := map [ - AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(P.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(P.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(P.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), - AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(P.AES_GCM_256, Digests.HmacSHA256, None), - AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(P.AES_GCM_192, Digests.HmacSHA256, None), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(P.AES_GCM_128, Digests.HmacSHA256, None), - AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(P.AES_GCM_256, Digests.HmacNOSHA, None), - AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(P.AES_GCM_192, Digests.HmacNOSHA, None), - AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(P.AES_GCM_128, Digests.HmacNOSHA, None) + AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionAlgorithms.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionAlgorithms.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(EncryptionAlgorithms.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), + AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_256, Digests.HmacSHA256, None), + AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_192, Digests.HmacSHA256, None), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_128, Digests.HmacSHA256, None), + AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_256, Digests.HmacNOSHA, None), + AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_192, Digests.HmacNOSHA, None), + AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_128, Digests.HmacNOSHA, None) ] /* Suite is intended to have an entry for each possible value of ID. This is stated and checked in three ways. diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index b95ebe7c0..8e28ca9db 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -25,7 +25,7 @@ module AESKeyring{ const keyNamespace: string const keyName: string const wrappingKey: seq - const wrappingAlgorithm: EncryptionAlgorithms.Params + const wrappingAlgorithm: EncryptionAlgorithms.EncryptionAlgorithm predicate Valid() reads this { Repr == {this} && @@ -35,7 +35,7 @@ module AESKeyring{ StringIs8Bit(keyNamespace) && StringIs8Bit(keyName) } - constructor(namespace: string, name: string, key: seq, wrappingAlg: EncryptionAlgorithms.Params) + constructor(namespace: string, name: string, key: seq, wrappingAlg: EncryptionAlgorithms.EncryptionAlgorithm) requires StringIs8Bit(namespace) && StringIs8Bit(name) requires wrappingAlg in VALID_ALGORITHMS requires wrappingAlg.Valid() diff --git a/src/extern/dotnet/AESEncryption.cs b/src/extern/dotnet/AESEncryption.cs index 22b078c92..66284e55d 100644 --- a/src/extern/dotnet/AESEncryption.cs +++ b/src/extern/dotnet/AESEncryption.cs @@ -12,30 +12,30 @@ namespace AESEncryption { //TODO This code has yet to be reviewed. See issue #36 public partial class AES_GCM { - public static STL.Result AESEncrypt(EncryptionAlgorithms.Params p, + public static STL.Result AESEncrypt(EncryptionAlgorithms.EncryptionAlgorithm encAlg, byteseq iv, byteseq key, byteseq msg, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); - var param = new AeadParameters(new KeyParameter(key.Elements), (int)p.tagLen * 8, iv.Elements, aad.Elements); + var param = new AeadParameters(new KeyParameter(key.Elements), (int)encAlg.tagLen * 8, iv.Elements, aad.Elements); cipher.Init(true, param); byte[] c = new byte[cipher.GetOutputSize(msg.Elements.Length)]; var len = cipher.ProcessBytes(msg.Elements, 0, msg.Elements.Length, c, 0); cipher.DoFinal(c, len); //Append authentication tag to `c` - return new STL.Result_Success(__default.EncryptionArtifactFromByteSeq(byteseq.FromElements(c), p)); + return new STL.Result_Success(__default.EncryptionArtifactFromByteSeq(byteseq.FromElements(c), encAlg)); } catch { return new STL.Result_Failure(new Dafny.Sequence("aes encrypt err".ToCharArray())); } } - public static STL.Result AESDecrypt(EncryptionAlgorithms.Params p, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { + public static STL.Result AESDecrypt(EncryptionAlgorithms.EncryptionAlgorithm encAlg, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); - var param = new AeadParameters(new KeyParameter(key.Elements), p.tagLen * 8, iv.Elements, aad.Elements); + var param = new AeadParameters(new KeyParameter(key.Elements), encAlg.tagLen * 8, iv.Elements, aad.Elements); cipher.Init(false, param); var ctx = cipherText.Concat(authTag); var pt = new byte[cipher.GetOutputSize(ctx.Elements.Length)]; From 313f647acf327b797009d33fb94cf548f8c66629 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Wed, 23 Oct 2019 16:14:38 -0700 Subject: [PATCH 16/17] EncryptionAlgorithm(s) -> EncryptionSuite(s) --- Makefile | 2 +- src/Crypto/AESEncryption.dfy | 12 +++++----- ...ionAlgorithms.dfy => EncryptionSuites.dfy} | 12 +++++----- src/SDK/AlgorithmSuite.dfy | 24 +++++++++---------- src/SDK/Keyring/AESKeyring.dfy | 10 ++++---- src/SDK/ToyClient.dfy | 6 ++--- src/extern/dotnet/AESEncryption.cs | 4 ++-- 7 files changed, 35 insertions(+), 35 deletions(-) rename src/Crypto/{EncryptionAlgorithms.dfy => EncryptionSuites.dfy} (51%) diff --git a/Makefile b/Makefile index 0cf4a756e..8db0b9986 100644 --- a/Makefile +++ b/Makefile @@ -10,7 +10,7 @@ endif # SRCS = $(foreach dir, $(SRCDIRS), $(wildcard $(dir)/*.dfy)) SRCS = \ src/Crypto/AESEncryption.dfy \ - src/Crypto/EncryptionAlgorithms.dfy \ + src/Crypto/EncryptionSuites.dfy \ src/Crypto/Digests.dfy \ src/Crypto/Random.dfy \ src/Crypto/RSAEncryption.dfy \ diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy index 04d7904af..8b42da0f9 100644 --- a/src/Crypto/AESEncryption.dfy +++ b/src/Crypto/AESEncryption.dfy @@ -1,20 +1,20 @@ include "../SDK/AlgorithmSuite.dfy" include "../StandardLibrary/StandardLibrary.dfy" -include "EncryptionAlgorithms.dfy" +include "EncryptionSuites.dfy" include "GenBytes.dfy" module {:extern "AESEncryption"} AESEncryption { - import EncryptionAlgorithms + import EncryptionSuites import opened StandardLibrary import opened UInt = StandardLibrary.UInt export - provides AESDecrypt, AESEncrypt, EncryptionAlgorithms, StandardLibrary, UInt + provides AESDecrypt, AESEncrypt, EncryptionSuites, StandardLibrary, UInt reveals EncryptionOutput datatype EncryptionOutput = EncryptionOutput(cipherText: seq, authTag: seq) - function method EncryptionArtifactFromByteSeq(s: seq, encAlg: EncryptionAlgorithms.EncryptionAlgorithm): (encArt: EncryptionOutput) + function method EncryptionArtifactFromByteSeq(s: seq, encAlg: EncryptionSuites.EncryptionSuite): (encArt: EncryptionOutput) requires encAlg.Valid() requires |s| >= encAlg.tagLen as int ensures |encArt.cipherText + encArt.authTag| == |s| @@ -23,7 +23,7 @@ module {:extern "AESEncryption"} AESEncryption { EncryptionOutput(s[.. |s| - encAlg.tagLen as int], s[|s| - encAlg.tagLen as int ..]) } - method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(encAlg: EncryptionAlgorithms.EncryptionAlgorithm, iv: seq, key: seq, msg: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(encAlg: EncryptionSuites.EncryptionSuite, iv: seq, key: seq, msg: seq, aad: seq) returns (res : Result) requires encAlg.Valid() requires encAlg.alg.AES? @@ -32,7 +32,7 @@ module {:extern "AESEncryption"} AESEncryption { requires |key| == encAlg.keyLen as int ensures res.Success? ==> |res.value.authTag| == encAlg.tagLen as int - method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(encAlg: EncryptionAlgorithms.EncryptionAlgorithm, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) + method {:extern "AESEncryption.AES_GCM", "AESDecrypt"} AESDecrypt(encAlg: EncryptionSuites.EncryptionSuite, key: seq, cipherTxt: seq, authTag: seq, iv: seq, aad: seq) returns (res: Result>) requires encAlg.Valid() requires encAlg.alg.AES? diff --git a/src/Crypto/EncryptionAlgorithms.dfy b/src/Crypto/EncryptionSuites.dfy similarity index 51% rename from src/Crypto/EncryptionAlgorithms.dfy rename to src/Crypto/EncryptionSuites.dfy index da1a7146f..d6e928ad3 100644 --- a/src/Crypto/EncryptionAlgorithms.dfy +++ b/src/Crypto/EncryptionSuites.dfy @@ -1,13 +1,13 @@ include "../StandardLibrary/StandardLibrary.dfy" -module {:extern "EncryptionAlgorithms"} EncryptionAlgorithms { +module {:extern "EncryptionSuites"} EncryptionSuites { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - datatype Algorithm = AES(mode: AESMode) + datatype EncryptionAlgorithm = AES(mode: AESMode) datatype AESMode = GCM - datatype EncryptionAlgorithm = EncryptionAlgorithm(alg: Algorithm, keyLen: uint8, tagLen: uint8, ivLen: uint8) + datatype EncryptionSuite = EncryptionSuite(alg: EncryptionAlgorithm, keyLen: uint8, tagLen: uint8, ivLen: uint8) { predicate Valid() { match alg @@ -20,7 +20,7 @@ module {:extern "EncryptionAlgorithms"} EncryptionAlgorithms { const AES_TAG_LEN := 16 as uint8; const AES_IV_LEN := 12 as uint8; - const AES_GCM_128 := EncryptionAlgorithm(AES(GCM), 16, AES_TAG_LEN, AES_IV_LEN) - const AES_GCM_192 := EncryptionAlgorithm(AES(GCM), 24, AES_TAG_LEN, AES_IV_LEN) - const AES_GCM_256 := EncryptionAlgorithm(AES(GCM), 32, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_128 := EncryptionSuite(AES(GCM), 16, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_192 := EncryptionSuite(AES(GCM), 24, AES_TAG_LEN, AES_IV_LEN) + const AES_GCM_256 := EncryptionSuite(AES(GCM), 32, AES_TAG_LEN, AES_IV_LEN) } diff --git a/src/SDK/AlgorithmSuite.dfy b/src/SDK/AlgorithmSuite.dfy index 2daa981ae..6050ec540 100644 --- a/src/SDK/AlgorithmSuite.dfy +++ b/src/SDK/AlgorithmSuite.dfy @@ -1,4 +1,4 @@ -include "../Crypto/EncryptionAlgorithms.dfy" +include "../Crypto/EncryptionSuites.dfy" include "../Crypto/Digests.dfy" include "../Crypto/Signature.dfy" include "../StandardLibrary/StandardLibrary.dfy" @@ -6,7 +6,7 @@ include "../StandardLibrary/StandardLibrary.dfy" module AlgorithmSuite { import opened StandardLibrary import opened UInt = StandardLibrary.UInt - import EncryptionAlgorithms + import EncryptionSuites import S = Signature import Digests @@ -41,18 +41,18 @@ module AlgorithmSuite { const AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0046 const AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE: ID := 0x0014 - datatype AlgSuite = AlgSuite(algorithm: EncryptionAlgorithms.EncryptionAlgorithm, hkdf: Digests.HMAC_ALGORITHM, sign: Option) + datatype AlgSuite = AlgSuite(algorithm: EncryptionSuites.EncryptionSuite, hkdf: Digests.HMAC_ALGORITHM, sign: Option) const Suite := map [ - AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionAlgorithms.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionAlgorithms.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(EncryptionAlgorithms.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), - AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_256, Digests.HmacSHA256, None), - AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_192, Digests.HmacSHA256, None), - AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_128, Digests.HmacSHA256, None), - AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_256, Digests.HmacNOSHA, None), - AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_192, Digests.HmacNOSHA, None), - AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionAlgorithms.AES_GCM_128, Digests.HmacNOSHA, None) + AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionSuites.AES_GCM_256, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384 := AlgSuite(EncryptionSuites.AES_GCM_192, Digests.HmacSHA384, Some(S.ECDSA_P384)), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256 := AlgSuite(EncryptionSuites.AES_GCM_128, Digests.HmacSHA256, Some(S.ECDSA_P256)), + AES_256_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionSuites.AES_GCM_256, Digests.HmacSHA256, None), + AES_192_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionSuites.AES_GCM_192, Digests.HmacSHA256, None), + AES_128_GCM_IV12_TAG16_HKDF_SHA256_SIGNONE := AlgSuite(EncryptionSuites.AES_GCM_128, Digests.HmacSHA256, None), + AES_256_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionSuites.AES_GCM_256, Digests.HmacNOSHA, None), + AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionSuites.AES_GCM_192, Digests.HmacNOSHA, None), + AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE := AlgSuite(EncryptionSuites.AES_GCM_128, Digests.HmacNOSHA, None) ] /* Suite is intended to have an entry for each possible value of ID. This is stated and checked in three ways. diff --git a/src/SDK/Keyring/AESKeyring.dfy b/src/SDK/Keyring/AESKeyring.dfy index 8e28ca9db..314b802a5 100644 --- a/src/SDK/Keyring/AESKeyring.dfy +++ b/src/SDK/Keyring/AESKeyring.dfy @@ -2,7 +2,7 @@ include "../../StandardLibrary/StandardLibrary.dfy" include "../../StandardLibrary/UInt.dfy" include "../AlgorithmSuite.dfy" include "./Defs.dfy" -include "../../Crypto/EncryptionAlgorithms.dfy" +include "../../Crypto/EncryptionSuites.dfy" include "../../Crypto/Random.dfy" include "../../Crypto/AESEncryption.dfy" include "../Materials.dfy" @@ -11,7 +11,7 @@ module AESKeyring{ import opened StandardLibrary import opened UInt = StandardLibrary.UInt import AESEncryption - import EncryptionAlgorithms + import EncryptionSuites import AlgorithmSuite import Random import KeyringDefs @@ -19,13 +19,13 @@ module AESKeyring{ const AUTH_TAG_LEN_LEN := 4; const IV_LEN_LEN := 4; - const VALID_ALGORITHMS := {EncryptionAlgorithms.AES_GCM_128, EncryptionAlgorithms.AES_GCM_192, EncryptionAlgorithms.AES_GCM_256} + const VALID_ALGORITHMS := {EncryptionSuites.AES_GCM_128, EncryptionSuites.AES_GCM_192, EncryptionSuites.AES_GCM_256} class AESKeyring extends KeyringDefs.Keyring { const keyNamespace: string const keyName: string const wrappingKey: seq - const wrappingAlgorithm: EncryptionAlgorithms.EncryptionAlgorithm + const wrappingAlgorithm: EncryptionSuites.EncryptionSuite predicate Valid() reads this { Repr == {this} && @@ -35,7 +35,7 @@ module AESKeyring{ StringIs8Bit(keyNamespace) && StringIs8Bit(keyName) } - constructor(namespace: string, name: string, key: seq, wrappingAlg: EncryptionAlgorithms.EncryptionAlgorithm) + constructor(namespace: string, name: string, key: seq, wrappingAlg: EncryptionSuites.EncryptionSuite) requires StringIs8Bit(namespace) && StringIs8Bit(name) requires wrappingAlg in VALID_ALGORITHMS requires wrappingAlg.Valid() diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index 73f2fc561..eb0796417 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -6,7 +6,7 @@ include "CMM/DefaultCMM.dfy" include "Keyring/Defs.dfy" include "Materials.dfy" include "../Crypto/AESEncryption.dfy" -include "../Crypto/EncryptionAlgorithms.dfy" +include "../Crypto/EncryptionSuites.dfy" include "../Crypto/Random.dfy" module ToyClientDef { @@ -19,11 +19,11 @@ module ToyClientDef { import Random import AlgorithmSuite import AESEncryption - import EncryptionAlgorithms + import EncryptionSuites datatype Encryption = Encryption(ec: Materials.EncryptionContext, edks: seq, iv: seq, ctxt: seq, authTag: seq) - const ALGORITHM := EncryptionAlgorithms.AES_GCM_256 + const ALGORITHM := EncryptionSuites.AES_GCM_256 class Client { var cmm: CMMDefs.CMM diff --git a/src/extern/dotnet/AESEncryption.cs b/src/extern/dotnet/AESEncryption.cs index 66284e55d..c3d74f2cf 100644 --- a/src/extern/dotnet/AESEncryption.cs +++ b/src/extern/dotnet/AESEncryption.cs @@ -12,7 +12,7 @@ namespace AESEncryption { //TODO This code has yet to be reviewed. See issue #36 public partial class AES_GCM { - public static STL.Result AESEncrypt(EncryptionAlgorithms.EncryptionAlgorithm encAlg, + public static STL.Result AESEncrypt(EncryptionSuites.EncryptionSuite encAlg, byteseq iv, byteseq key, byteseq msg, @@ -32,7 +32,7 @@ public static STL.Result AESEncrypt(EncryptionAlgorithms.Encry } } - public static STL.Result AESDecrypt(EncryptionAlgorithms.EncryptionAlgorithm encAlg, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { + public static STL.Result AESDecrypt(EncryptionSuites.EncryptionSuite encAlg, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) { try { var cipher = new GcmBlockCipher(new AesEngine()); var param = new AeadParameters(new KeyParameter(key.Elements), encAlg.tagLen * 8, iv.Elements, aad.Elements); From 70c164329565c7cf47fd2b78d385dcdeca64b396 Mon Sep 17 00:00:00 2001 From: Matthew Jones Date: Thu, 24 Oct 2019 15:23:56 -0700 Subject: [PATCH 17/17] Make Main.dfy verify --- Makefile | 1 + src/SDK/ToyClient.dfy | 2 ++ 2 files changed, 3 insertions(+) diff --git a/Makefile b/Makefile index 8db0b9986..91ec80285 100644 --- a/Makefile +++ b/Makefile @@ -15,6 +15,7 @@ SRCS = \ src/Crypto/Random.dfy \ src/Crypto/RSAEncryption.dfy \ src/Crypto/Signature.dfy \ + src/Main.dfy \ src/SDK/AlgorithmSuite.dfy \ src/SDK/CMM/DefaultCMM.dfy \ src/SDK/CMM/Defs.dfy \ diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy index eb0796417..26ad8f955 100644 --- a/src/SDK/ToyClient.dfy +++ b/src/SDK/ToyClient.dfy @@ -69,6 +69,8 @@ module ToyClientDef { method Encrypt(pt: seq, ec: Materials.EncryptionContext) returns (res: Result) requires Valid() ensures Valid() + ensures res.Success? ==> |res.value.authTag| == ALGORITHM.tagLen as int + ensures res.Success? ==> |res.value.iv| == ALGORITHM.ivLen as int { var em :- GetEncMaterials(ec); if |em.plaintextDataKey.get| != 32 {