From 8e7f318e17ce103e1ff7669f94809a473d5accc6 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Mon, 12 Aug 2024 16:01:39 -0700 Subject: [PATCH 1/2] chore: Rename AtomicPrimitives Dafny module name --- ...ryptographyMaterialProvidersOperations.dfy | 4 +- .../src/CMMs/DefaultCMM.dfy | 6 +-- .../src/Index.dfy | 12 ++--- .../src/KeyWrapping/EcdhEdkWrapping.dfy | 16 +++--- .../src/KeyWrapping/EdkWrapping.dfy | 2 +- .../KeyWrapping/IntermediateKeyWrapping.dfy | 18 +++---- .../src/KeyWrapping/MaterialWrapping.dfy | 2 +- .../src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy | 10 ++-- .../AwsKms/AwsKmsHierarchicalKeyring.dfy | 34 ++++++------- .../src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy | 16 +++--- .../src/Keyrings/RawAESKeyring.dfy | 14 +++--- .../src/Keyrings/RawECDHKeyring.dfy | 20 ++++---- .../src/Keyrings/RawRSAKeyring.dfy | 18 +++---- .../src/Utils.dfy | 4 +- .../TestAwsKmsEncryptedDataKeyFilter.dfy | 2 +- .../TestAwsKmsHierarchicalKeyring.dfy | 2 +- .../Keyrings/AwsKms/TestAwsKmsEcdhKeyring.dfy | 4 +- .../test/Keyrings/TesRawECDHKeyring.dfy | 16 +++--- .../test/Keyrings/TestMultiKeyring.dfy | 2 +- .../test/Keyrings/TestRawAESKeyring.dfy | 2 +- .../test/Keyrings/TestRawRSAKeyring.dfy | 4 +- .../test/TestEcdhCalculation.dfy | 8 +-- .../AwsCryptographyKeyStore/src/Index.dfy | 3 +- AwsCryptographyPrimitives/src/Index.dfy | 4 +- AwsCryptographyPrimitives/test/TestAES.dfy | 20 ++++---- .../test/TestAesKdfCtr.dfy | 2 +- .../TestAwsCryptographyPrimitivesHKDF.dfy | 22 ++++---- .../TestAwsCryptographyPrimitivesHMAC.dfy | 14 +++--- AwsCryptographyPrimitives/test/TestDigest.dfy | 14 +++--- AwsCryptographyPrimitives/test/TestECDH.dfy | 4 +- .../test/TestGenerateRandomBytes.dfy | 6 +-- .../test/TestHKDF_Rfc5869TestVectors.dfy | 18 +++---- AwsCryptographyPrimitives/test/TestHMAC.dfy | 4 +- AwsCryptographyPrimitives/test/TestKDF.dfy | 18 +++---- .../test/TestKDF_TestVectors.dfy | 48 +++++++++--------- AwsCryptographyPrimitives/test/TestRSA.dfy | 50 +++++++++---------- .../test/TestSignature.dfy | 4 +- .../dafny/CombinedSrc.dfy | 2 + .../src/KeyringFromKeyDescription.dfy | 4 +- .../src/LibraryIndex.dfy | 4 +- .../src/TestManifests.dfy | 2 +- .../src/TestVectorsUtils.dfy | 4 +- 42 files changed, 231 insertions(+), 232 deletions(-) create mode 100644 TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy index 4cc747bac..af517f032 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy @@ -55,7 +55,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph import StormTracker import StormTrackingCMC import Crypto = AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened AwsKmsUtils import DefaultClientSupplier import Materials @@ -68,7 +68,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph import RequiredEncryptionContextCMM datatype Config = Config( - nameonly crypto: Primitives.AtomicPrimitivesClient + nameonly crypto: AtomicPrimitives.AtomicPrimitivesClient ) type InternalConfig = Config diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy index 7b40aa215..8eb180ddf 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy @@ -19,7 +19,7 @@ module DefaultCMM { import UTF8 import Types = AwsCryptographyMaterialProvidersTypes import Crypto = AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Defaults import Commitment import Seq @@ -27,7 +27,7 @@ module DefaultCMM { class DefaultCMM extends CMM.VerifiableInterface { - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient predicate ValidState() ensures ValidState() ==> History in Modifies @@ -50,7 +50,7 @@ module DefaultCMM { //# the caller MUST provide the following value: //# - [Keyring](#keyring) k: Types.IKeyring, - c: Primitives.AtomicPrimitivesClient + c: AtomicPrimitives.AtomicPrimitivesClient ) requires k.ValidState() && c.ValidState() ensures keyring == k && cryptoPrimitives == c diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy index db4e0df6c..12517b8fb 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy @@ -3,13 +3,11 @@ include "AwsCryptographyMaterialProvidersOperations.dfy" -module - {:extern "software.amazon.cryptography.materialproviders.internaldafny" } - MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService +module {:extern "software.amazon.cryptography.materialproviders.internaldafny" } MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService { import Operations = AwsCryptographyMaterialProvidersOperations - import Aws.Cryptography.Primitives + import AtomicPrimitives import Crypto = AwsCryptographyPrimitivesTypes function method DefaultMaterialProvidersConfig(): MaterialProvidersConfig @@ -22,11 +20,11 @@ module ensures res.Success? ==> && res.value is MaterialProvidersClient { - var maybeCrypto := Primitives.AtomicPrimitives(); + var maybeCrypto := AtomicPrimitives.AtomicPrimitives(); var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto .MapFailure(e => Types.AwsCryptographyPrimitives(e)); - assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient; - var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient; + assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient; + var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient; var client := new MaterialProvidersClient(Operations.Config( crypto := cryptoPrimitives )); return Success(client); diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy index 6443b0d09..2d96c8fe5 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy @@ -20,7 +20,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping { import opened AlgorithmSuites import PrimitiveTypes = AwsCryptographyPrimitivesTypes import Types = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Materials datatype EcdhUnwrapInfo = EcdhUnwrapInfo() @@ -34,7 +34,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping { const sharedSecret: seq const keyringVersion: seq const curveSpec: PrimitiveTypes.ECDHCurveSpec - const crypto: Primitives.AtomicPrimitivesClient + const crypto: AtomicPrimitives.AtomicPrimitivesClient constructor( senderPublicKey: seq, @@ -42,7 +42,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping { sharedSecret: seq, keyringVersion: seq, curveSpec: PrimitiveTypes.ECDHCurveSpec, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) requires crypto.ValidState() ensures @@ -228,12 +228,12 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping { { const sharedSecret: seq const fixedInfo: seq - const crypto: Primitives.AtomicPrimitivesClient + const crypto: AtomicPrimitives.AtomicPrimitivesClient constructor( sharedSecret: seq, fixedInfo: seq, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) requires crypto.ValidState() ensures @@ -316,12 +316,12 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping { { const sharedSecret: seq const fixedInfo: seq - const crypto: Primitives.AtomicPrimitivesClient + const crypto: AtomicPrimitives.AtomicPrimitivesClient constructor( sharedSecret: seq, fixedInfo: seq, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) requires crypto.ValidState() ensures @@ -461,7 +461,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping { sharedSecret: seq, fixedInfo: seq, salt: seq, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) returns (res :Result, Types.Error>) requires crypto.ValidState() modifies crypto.Modifies diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy index bba73f9d7..f064f4754 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy @@ -20,7 +20,7 @@ module EdkWrapping { import opened IntermediateKeyWrapping import Crypto = AwsCryptographyPrimitivesTypes import Types = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Materials import AlgorithmSuites diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy index 6ce682dde..6da1f5b43 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy @@ -15,7 +15,7 @@ module IntermediateKeyWrapping { import opened AlgorithmSuites import Crypto = AwsCryptographyPrimitivesTypes import Types = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Materials import UTF8 import HKDF @@ -74,11 +74,11 @@ module IntermediateKeyWrapping { []) { - var maybeCrypto := Primitives.AtomicPrimitives(); + var maybeCrypto := AtomicPrimitives.AtomicPrimitives(); var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto .MapFailure(e => Types.AwsCryptographyPrimitives(e)); - assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient; - var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient; + assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient; + var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient; // Deserialize the Intermediate-Wrapped material var deserializedWrapped :- DeserializeIntermediateWrappedMaterial(wrappedMaterial, algorithmSuite); var DeserializedIntermediateWrappedMaterial(encryptedPdk, providerWrappedIkm) := deserializedWrapped; @@ -168,12 +168,12 @@ module IntermediateKeyWrapping { && |maybeIntermediateWrappedMat.value.encryptedPdk| == (AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat { - var maybeCrypto := Primitives.AtomicPrimitives(); + var maybeCrypto := AtomicPrimitives.AtomicPrimitives(); var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto .MapFailure(e => Types.AwsCryptographyPrimitives(e)); - assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient; - var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient; + assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient; + var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient; // Use the provider to get the intermediate key material, and wrapped intermediate key material @@ -252,7 +252,7 @@ module IntermediateKeyWrapping { wrapInfo := res.value.wrapInfo)), []) { - var maybeCrypto := Primitives.AtomicPrimitives(); + var maybeCrypto := AtomicPrimitives.AtomicPrimitives(); var cryptoPrimitives :- maybeCrypto .MapFailure(e => Types.AwsCryptographyPrimitives(e)); @@ -305,7 +305,7 @@ module IntermediateKeyWrapping { intermediateMaterial: seq, algorithmSuite: Types.AlgorithmSuiteInfo, encryptionContext: Types.EncryptionContext, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) returns (res: Result) requires cryptoPrimitives.ValidState() diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy index a73d67015..123762822 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy @@ -13,7 +13,7 @@ module MaterialWrapping { import opened Actions import opened Wrappers import Types = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Materials import AlgorithmSuites diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy index af838cbd4..b5680ef21 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy @@ -38,7 +38,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { import MaterialWrapping import EcdhEdkWrapping import ErrorMessages - import Aws.Cryptography.Primitives + import AtomicPrimitives import CanonicalEncryptionContext const AWS_KMS_ECDH_KEYRING_VERSION := RawECDHKeyring.RAW_ECDH_KEYRING_VERSION @@ -58,7 +58,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { const keyAgreementScheme: Types.KmsEcdhStaticConfigurations const curveSpec: PrimitiveTypes.ECDHCurveSpec const grantTokens: KMS.GrantTokenList - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ghost predicate ValidState() ensures ValidState() ==> History in Modifies @@ -95,7 +95,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { recipientPublicKey: KMS.PublicKeyType, compressedSenderPublicKey: Option>, compressedRecipientPublicKey: seq, - cryptoPrimitives : Primitives.AtomicPrimitivesClient + cryptoPrimitives : AtomicPrimitives.AtomicPrimitivesClient ) requires client.ValidState() requires cryptoPrimitives.ValidState() @@ -438,7 +438,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { Types.Error> { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const recipientPublicKey: seq const client: KMS.IKMSClient const grantTokens: KMS.GrantTokenList @@ -447,7 +447,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring { constructor( materials: Materials.DecryptionMaterialsPendingPlaintextDataKey, - cryptoPrimitives: Primitives.AtomicPrimitivesClient, + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient, recipientPublicKey: seq, client: KMS.IKMSClient, grantTokens: KMS.GrantTokenList, diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy index f87125982..93f33dfe6 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy @@ -50,7 +50,7 @@ module AwsKmsHierarchicalKeyring { import HKDF import HMAC import opened AESEncryption - import Aws.Cryptography.Primitives + import AtomicPrimitives import ErrorMessages const BRANCH_KEY_STORE_GSI := "Active-Keys" @@ -127,7 +127,7 @@ module AwsKmsHierarchicalKeyring { const branchKeyIdSupplier: Option const keyStore: KeyStore.IKeyStoreClient const ttlSeconds: Types.PositiveLong - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const cache: Types.ICryptographicMaterialsCache predicate ValidState() @@ -163,7 +163,7 @@ module AwsKmsHierarchicalKeyring { ttlSeconds: Types.PositiveLong, cmc: Types.ICryptographicMaterialsCache, - cryptoPrimitives : Primitives.AtomicPrimitivesClient + cryptoPrimitives : AtomicPrimitives.AtomicPrimitivesClient ) requires ttlSeconds >= 0 requires keyStore.ValidState() && cryptoPrimitives.ValidState() @@ -384,7 +384,7 @@ module AwsKmsHierarchicalKeyring { method GetActiveCacheId( branchKeyId: string, branchKeyIdUtf8: seq, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) returns (cacheId: Result, Types.Error>) @@ -490,7 +490,7 @@ module AwsKmsHierarchicalKeyring { branchKey: seq, salt: seq, purpose: Option>, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) returns (output: Result, Types.Error>) @@ -605,7 +605,7 @@ module AwsKmsHierarchicalKeyring { { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey const keyStore: KeyStore.IKeyStoreClient - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const branchKeyId: string const ttlSeconds: Types.PositiveLong const cache: Types.ICryptographicMaterialsCache @@ -613,7 +613,7 @@ module AwsKmsHierarchicalKeyring { constructor( materials: Materials.DecryptionMaterialsPendingPlaintextDataKey, keyStore: KeyStore.IKeyStoreClient, - cryptoPrimitives: Primitives.AtomicPrimitivesClient, + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient, branchKeyId: string, ttlSeconds: Types.PositiveLong, cache: Types.ICryptographicMaterialsCache @@ -697,11 +697,11 @@ module AwsKmsHierarchicalKeyring { // We need to create a new client here so that we can reason about the state of the client // down the line. This is ok because the only state tracked is the client's history. - var maybeCrypto := Primitives.AtomicPrimitives(); + var maybeCrypto := AtomicPrimitives.AtomicPrimitives(); var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto .MapFailure(e => Types.AwsCryptographyPrimitives(e)); - assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient; - var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient; + assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient; + var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient; var kmsHierarchyUnwrap := new KmsHierarchyUnwrapKeyMaterial( branchKey, @@ -725,7 +725,7 @@ module AwsKmsHierarchicalKeyring { method GetVersionCacheId( branchKeyIdUtf8: seq, // The branch key as Bytes branchKeyVersion: string, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) returns (cacheId: Result, Types.Error>) ensures cacheId.Success? ==> |cacheId.value| == 32 @@ -824,13 +824,13 @@ module AwsKmsHierarchicalKeyring { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq - const crypto: Primitives.AtomicPrimitivesClient + const crypto: AtomicPrimitives.AtomicPrimitivesClient constructor( branchKey: seq, branchKeyIdUtf8: UTF8.ValidUTF8Bytes, branchKeyVersionAsBytes: seq, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) requires crypto.ValidState() ensures @@ -963,13 +963,13 @@ module AwsKmsHierarchicalKeyring { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq - const crypto: Primitives.AtomicPrimitivesClient + const crypto: AtomicPrimitives.AtomicPrimitivesClient constructor( branchKey: seq, branchKeyIdUtf8 : UTF8.ValidUTF8Bytes, branchKeyVersionAsBytes: seq, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) requires crypto.ValidState() ensures @@ -1053,13 +1053,13 @@ module AwsKmsHierarchicalKeyring { const branchKey: seq const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes const branchKeyVersionAsBytes: seq - const crypto: Primitives.AtomicPrimitivesClient + const crypto: AtomicPrimitives.AtomicPrimitivesClient constructor( branchKey: seq, branchKeyIdUtf8 : UTF8.ValidUTF8Bytes, branchKeyVersionAsBytes: seq, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) requires crypto.ValidState() ensures diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy index 3dfacb8c7..44374aa23 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy @@ -21,7 +21,7 @@ module AwsKmsRsaKeyring { import opened Actions import UTF8 import UUID - import Aws.Cryptography.Primitives + import AtomicPrimitives import Crypto = AwsCryptographyPrimitivesTypes import Keyring import Materials @@ -48,7 +48,7 @@ module AwsKmsRsaKeyring { const awsKmsArn: AwsArnParsing.AwsKmsIdentifier const paddingScheme: KMS.EncryptionAlgorithmSpec const publicKey: Option> - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient predicate ValidState() ensures ValidState() ==> History in Modifies @@ -78,7 +78,7 @@ module AwsKmsRsaKeyring { awsKmsKey: AwsArnParsing.AwsKmsIdentifierString, paddingScheme: KMS.EncryptionAlgorithmSpec, client: Option, - cryptoPrimitives: Primitives.AtomicPrimitivesClient, + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient, grantTokens: KMS.GrantTokenList ) requires cryptoPrimitives.ValidState() @@ -272,7 +272,7 @@ module AwsKmsRsaKeyring { } } - method EncryptionContextDigest(cryptoPrimitives: Primitives.AtomicPrimitivesClient, encryptionContext: Types.EncryptionContext) + method EncryptionContextDigest(cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient, encryptionContext: Types.EncryptionContext) returns (output: Result, Types.Error>) requires cryptoPrimitives.ValidState() modifies cryptoPrimitives.Modifies @@ -417,12 +417,12 @@ module AwsKmsRsaKeyring { { const publicKey: seq const paddingScheme: KMS.EncryptionAlgorithmSpec - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient constructor( publicKey: seq, paddingScheme: KMS.EncryptionAlgorithmSpec, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() requires (paddingScheme.RSAES_OAEP_SHA_1? || paddingScheme.RSAES_OAEP_SHA_256?) @@ -498,12 +498,12 @@ module AwsKmsRsaKeyring { { const publicKey: seq const paddingScheme: KMS.EncryptionAlgorithmSpec - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient constructor( publicKey: seq, paddingScheme: KMS.EncryptionAlgorithmSpec, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() requires (paddingScheme.RSAES_OAEP_SHA_1? || paddingScheme.RSAES_OAEP_SHA_256?) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy index 0d8969ea6..477d4942c 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy @@ -29,7 +29,7 @@ module RawAESKeyring { import EdkWrapping import ErrorMessages - import Aws.Cryptography.Primitives + import AtomicPrimitives const AUTH_TAG_LEN_LEN := 4 const IV_LEN_LEN := 4 @@ -39,7 +39,7 @@ module RawAESKeyring { Keyring.VerifiableInterface, Types.IKeyring { - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient predicate ValidState() ensures ValidState() ==> History in Modifies @@ -81,7 +81,7 @@ module RawAESKeyring { name: UTF8.ValidUTF8Bytes, key: seq, wrappingAlgorithm: Crypto.AES_GCM, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires |namespace| < UINT16_LIMIT requires |name| < UINT16_LIMIT @@ -531,12 +531,12 @@ module RawAESKeyring { { const wrappingKey: seq const wrappingAlgorithm: Crypto.AES_GCM - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient constructor( wrappingKey: seq, wrappingAlgorithm: Crypto.AES_GCM, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() ensures @@ -632,13 +632,13 @@ module RawAESKeyring { const wrappingKey: seq const wrappingAlgorithm: Crypto.AES_GCM const iv: seq - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient constructor( wrappingKey: seq, wrappingAlgorithm: Crypto.AES_GCM, iv: seq, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() requires |iv| == wrappingAlgorithm.ivLength as nat diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy index fdaede43f..55435c4e6 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy @@ -22,7 +22,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { import opened Constants import Types = AwsCryptographyMaterialProvidersTypes import PrimitiveTypes = AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Keyring import Materials import opened AlgorithmSuites @@ -73,7 +73,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { const compressedRecipientPublicKey: seq const keyAgreementScheme: Types.RawEcdhStaticConfigurations const curveSpec: PrimitiveTypes.ECDHCurveSpec - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ghost predicate ValidState() ensures ValidState() ==> History in Modifies @@ -99,7 +99,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { recipientPublicKey: seq, compressedSenderPublicKey: Option>, compressedRecipientPublicKey: seq, - cryptoPrimitives : Primitives.AtomicPrimitivesClient + cryptoPrimitives : AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() requires senderPublicKey.Some? ==> ValidPublicKeyLength(senderPublicKey.value) @@ -482,7 +482,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { Types.Error> { const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient const senderPublicKey: seq const recipientPublicKey: seq const keyAgreementScheme: Types.RawEcdhStaticConfigurations @@ -490,7 +490,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { constructor( materials: Materials.DecryptionMaterialsPendingPlaintextDataKey, - cryptoPrimitives: Primitives.AtomicPrimitivesClient, + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient, senderPublicKey: seq, recipientPublicKey: seq, keyAgreementScheme: Types.RawEcdhStaticConfigurations, @@ -672,7 +672,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { senderPrivateKey: PrimitiveTypes.ECCPrivateKey, recipientPublicKey: PrimitiveTypes.ECCPublicKey, curveSpec: PrimitiveTypes.ECDHCurveSpec, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) returns (res: Result, Types.Error>) requires crypto.ValidState() modifies crypto.Modifies @@ -705,7 +705,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { method {:vcs_split_on_every_assert} CompressPublicKey( publicKey: PrimitiveTypes.ECCPublicKey, curveSpec: PrimitiveTypes.ECDHCurveSpec, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) returns (res: Result, Types.Error>) requires crypto.ValidState() modifies crypto.Modifies @@ -736,7 +736,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { method {:vcs_split_on_every_assert} DecompressPublicKey( publicKey: seq, curveSpec: PrimitiveTypes.ECDHCurveSpec, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) returns (res: Result, Types.Error>) requires crypto.ValidState() modifies crypto.Modifies @@ -786,7 +786,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { method {:vcs_split_on_every_assert} GenerateEphemeralEccKeyPair( curveSpec: PrimitiveTypes.ECDHCurveSpec, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) returns (res: Result) requires crypto.ValidState() modifies crypto.Modifies @@ -810,7 +810,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring { } method ValidatePublicKey( - crypto: Primitives.AtomicPrimitivesClient, + crypto: AtomicPrimitives.AtomicPrimitivesClient, curveSpec: PrimitiveTypes.ECDHCurveSpec, publicKey: seq ) returns (res: Result) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy index 7fa6f0f04..c20a98b8f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy @@ -18,7 +18,7 @@ module RawRSAKeyring { import opened Wrappers import Types = AwsCryptographyMaterialProvidersTypes import Crypto = AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Keyring import Materials import opened AlgorithmSuites @@ -40,7 +40,7 @@ module RawRSAKeyring { class RawRSAKeyring extends Keyring.VerifiableInterface, Types.IKeyring { - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient predicate ValidState() ensures ValidState() ==> History in Modifies @@ -98,7 +98,7 @@ module RawRSAKeyring { //# This value MUST correspond with one of the [supported padding schemes] //# (#supported-padding-schemes). paddingScheme: Crypto.RSAPaddingMode, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires |namespace| < UINT16_LIMIT requires |name| < UINT16_LIMIT @@ -413,12 +413,12 @@ module RawRSAKeyring { { const publicKey: seq const paddingScheme: Crypto.RSAPaddingMode - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient constructor( publicKey: seq, paddingScheme: Crypto.RSAPaddingMode, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() ensures @@ -507,12 +507,12 @@ module RawRSAKeyring { { const publicKey: seq const paddingScheme: Crypto.RSAPaddingMode - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient constructor( publicKey: seq, paddingScheme: Crypto.RSAPaddingMode, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() ensures @@ -603,12 +603,12 @@ module RawRSAKeyring { { const privateKey: seq const paddingScheme: Crypto.RSAPaddingMode - const cryptoPrimitives: Primitives.AtomicPrimitivesClient + const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient constructor( privateKey: seq, paddingScheme: Crypto.RSAPaddingMode, - cryptoPrimitives: Primitives.AtomicPrimitivesClient + cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient ) requires cryptoPrimitives.ValidState() ensures diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Utils.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Utils.dfy index 70c1c20ad..3f6edce3b 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Utils.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Utils.dfy @@ -4,7 +4,7 @@ include "../Model/AwsCryptographyMaterialProvidersTypes.dfy" module {:options "/functionSyntax:4" } Utils { import Crypto = AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Types = AwsCryptographyMaterialProvidersTypes import opened StandardLibrary import opened UInt = StandardLibrary.UInt @@ -14,7 +14,7 @@ module {:options "/functionSyntax:4" } Utils { method {:vcs_split_on_every_assert} GetPublicKey( curveSpec: Crypto.ECDHCurveSpec, privateKey: Crypto.ECCPrivateKey, - crypto: Primitives.AtomicPrimitivesClient + crypto: AtomicPrimitives.AtomicPrimitivesClient ) returns (res: Result, Types.Error>) requires crypto.ValidState() modifies crypto.Modifies diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsDiscoveryKeryring/TestAwsKmsEncryptedDataKeyFilter.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsDiscoveryKeryring/TestAwsKmsEncryptedDataKeyFilter.dfy index c260f1129..aba8550b1 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsDiscoveryKeryring/TestAwsKmsEncryptedDataKeyFilter.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsDiscoveryKeryring/TestAwsKmsEncryptedDataKeyFilter.dfy @@ -9,7 +9,7 @@ module TestAwsKmsEncryptedDataKeyFilter { import opened Wrappers import TestUtils import UTF8 - import Aws.Cryptography.Primitives + import AtomicPrimitives import AwsCryptographyPrimitivesTypes import MaterialProviders import Types = AwsCryptographyMaterialProvidersTypes diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy index 772bc3af9..61a65826f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy @@ -19,7 +19,7 @@ module TestAwsKmsHierarchicalKeyring { import KeyStore = KeyStore import KeyStoreTypes = AwsCryptographyKeyStoreTypes import Crypto = AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import MaterialProviders import StormTracker import StormTrackingCMC diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/TestAwsKmsEcdhKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/TestAwsKmsEcdhKeyring.dfy index 16f953db4..5f6f6b361 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/TestAwsKmsEcdhKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/TestAwsKmsEcdhKeyring.dfy @@ -11,7 +11,7 @@ module {:options "/functionSyntax:4" } TestAwsKmsEcdhKeyring { import opened UInt = StandardLibrary.UInt import MaterialProviders import Types = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import PrimitiveTypes = AwsCryptographyPrimitivesTypes import Com.Amazonaws.Kms import AwsKmsRsaKeyring @@ -341,7 +341,7 @@ module {:options "/functionSyntax:4" } TestAwsKmsEcdhKeyring { method {:test} TestKmsEcdhKeyringRecipientRawKeyEncryptDecryptSuccessSetSenderPublicKey() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var recipientKeypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TesRawECDHKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TesRawECDHKeyring.dfy index 66f9055d5..5222e613b 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TesRawECDHKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TesRawECDHKeyring.dfy @@ -11,7 +11,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { import UTF8 import ComAmazonawsKmsTypes import Com.Amazonaws.Kms - import Aws.Cryptography.Primitives + import AtomicPrimitives import AwsCryptographyPrimitivesTypes import MaterialProviders import Types = AwsCryptographyMaterialProvidersTypes @@ -28,7 +28,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { method {:test} TestRawEcdhDiscoveryOnEncryptFailure() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var keypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( @@ -71,7 +71,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { method {:test} TestRawEcdhEphemeralOnDecryptFailure() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var keypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( @@ -115,7 +115,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { method {:test} TestRawEcdhKeyringEphemeralDecryptOwnMessageFailure() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var keypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( @@ -179,7 +179,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { method {:test} TestRawEcdhKeyringStaticSuccess() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var senderKeypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( @@ -248,7 +248,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { method {:test} TestTwoRawEcdhKeyringStaticSuccess() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var senderKeypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( @@ -329,7 +329,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { method {:test} TestTwoEcdhKeyringStaticSuccess() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var senderKeypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( @@ -418,7 +418,7 @@ module {:options "/functionSyntax:4" } TestRawECDHKeyring { method {:test} TestRawEcdhKeyringEncryptDecryptSuccessDBESDKSuite() { var mpl :- expect MaterialProviders.MaterialProviders(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var senderKeypair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy index 7e353fd76..36df31146 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy @@ -8,7 +8,7 @@ module TestMultiKeyring { import opened Wrappers import TestUtils import UTF8 - import Aws.Cryptography.Primitives + import AtomicPrimitives import AwsCryptographyPrimitivesTypes import MaterialProviders import Types = AwsCryptographyMaterialProvidersTypes diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawAESKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawAESKeyring.dfy index 17364fbc2..300111edc 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawAESKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawAESKeyring.dfy @@ -9,7 +9,7 @@ module TestRawAESKeyring { import opened Wrappers import TestUtils import UTF8 - import Aws.Cryptography.Primitives + import AtomicPrimitives import AwsCryptographyPrimitivesTypes import MaterialProviders import Types = AwsCryptographyMaterialProvidersTypes diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawRSAKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawRSAKeyring.dfy index c2204fecc..77af020d8 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawRSAKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestRawRSAKeyring.dfy @@ -8,7 +8,7 @@ include "../../src/ErrorMessages.dfy" module TestRawRSAKeying { import opened Wrappers import TestUtils - import Aws.Cryptography.Primitives + import AtomicPrimitives import AwsCryptographyPrimitivesTypes import MaterialProviders import Types = AwsCryptographyMaterialProvidersTypes @@ -283,7 +283,7 @@ module TestRawRSAKeying { method GenerateKeyPair( keyModulusLength: AwsCryptographyPrimitivesTypes.RSAModulusLengthBitsToGenerate ) returns (keys: AwsCryptographyPrimitivesTypes.GenerateRSAKeyPairOutput) { - var crypto :- expect Primitives.AtomicPrimitives(); + var crypto :- expect AtomicPrimitives.AtomicPrimitives(); keys :- expect crypto.GenerateRSAKeyPair( AwsCryptographyPrimitivesTypes.GenerateRSAKeyPairInput( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/TestEcdhCalculation.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/TestEcdhCalculation.dfy index 3bf194e58..a36bc4f3e 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/TestEcdhCalculation.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/TestEcdhCalculation.dfy @@ -11,7 +11,7 @@ module TestEcdhCalculation { import opened UInt = StandardLibrary.UInt import MaterialProviders import Types = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Com.Amazonaws.Kms import TestUtils import PrimitiveTypes = AwsCryptographyPrimitivesTypes @@ -30,7 +30,7 @@ module TestEcdhCalculation { method {:test} TestKmsDeriveSharedSecretOfflineCalculation() { var kmsClient :- expect Kms.KMSClient(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); var keyPair :- expect primitives.GenerateECCKeyPair( PrimitiveTypes.GenerateECCKeyPairInput( @@ -75,7 +75,7 @@ module TestEcdhCalculation { method {:test} TestKmsDeriveSharedSecretOfflineCalculationCurves() { var kmsClient :- expect Kms.KMSClient(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); for i := 0 to |senderArns| { @@ -123,7 +123,7 @@ module TestEcdhCalculation { method {:test} TestOfflineDeriveSharedSecretStaticKeys() { var kmsClient :- expect Kms.KMSClient(); - var primitives :- expect Primitives.AtomicPrimitives(); + var primitives :- expect AtomicPrimitives.AtomicPrimitives(); for i := 0 to |curveSpecs| { diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy index 688831b19..550b8c9be 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy @@ -6,8 +6,7 @@ include "AwsCryptographyKeyStoreOperations.dfy" include "ErrorMessages.dfy" include "KmsArn.dfy" -module {:extern "software.amazon.cryptography.keystore.internaldafny"} - KeyStore refines AbstractAwsCryptographyKeyStoreService +module {:extern "software.amazon.cryptography.keystore.internaldafny"} KeyStore refines AbstractAwsCryptographyKeyStoreService { import opened AwsKmsUtils import Operations = AwsCryptographyKeyStoreOperations diff --git a/AwsCryptographyPrimitives/src/Index.dfy b/AwsCryptographyPrimitives/src/Index.dfy index 40a672ece..65c7de54e 100644 --- a/AwsCryptographyPrimitives/src/Index.dfy +++ b/AwsCryptographyPrimitives/src/Index.dfy @@ -4,7 +4,9 @@ include "../Model/AwsCryptographyPrimitivesTypes.dfy" include "AwsCryptographyPrimitivesOperations.dfy" -module {:extern "software.amazon.cryptography.primitives.internaldafny" } Aws.Cryptography.Primitives refines AbstractAwsCryptographyPrimitivesService { +// Note: This module name SHOULD be `AtomicPrimitives` +// to align with this project's Smithy-Model localService's `sdkId` trait. +module {:extern "software.amazon.cryptography.primitives.internaldafny" } AtomicPrimitives refines AbstractAwsCryptographyPrimitivesService { import Operations = AwsCryptographyPrimitivesOperations function method DefaultCryptoConfig(): CryptoConfig { diff --git a/AwsCryptographyPrimitives/test/TestAES.dfy b/AwsCryptographyPrimitives/test/TestAES.dfy index 708e8bc9d..978751ca9 100644 --- a/AwsCryptographyPrimitives/test/TestAES.dfy +++ b/AwsCryptographyPrimitives/test/TestAES.dfy @@ -5,7 +5,7 @@ include "../src/Index.dfy" include "../src/Digest.dfy" module TestAwsCryptographyPrimitivesAES { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened Wrappers import opened StandardLibrary.UInt import Digest @@ -33,8 +33,8 @@ module TestAwsCryptographyPrimitivesAES { // d.final() BasicAESDecryptTest( - Primitives.Types.AESDecryptInput( - encAlg := Primitives.Types.AES_GCM( + AtomicPrimitives.Types.AESDecryptInput( + encAlg := AtomicPrimitives.Types.AES_GCM( keyLength := 32 as int32, tagLength := 16 as int32, ivLength := 12 as int32 @@ -67,8 +67,8 @@ module TestAwsCryptographyPrimitivesAES { method {:test} AESEncryptTests() { BasicAESEncryptTest( - Primitives.Types.AESEncryptInput( - encAlg := Primitives.Types.AES_GCM( + AtomicPrimitives.Types.AESEncryptInput( + encAlg := AtomicPrimitives.Types.AES_GCM( keyLength := 32 as int32, tagLength := 16 as int32, ivLength := 12 as int32 @@ -92,23 +92,23 @@ module TestAwsCryptographyPrimitivesAES { } method BasicAESDecryptTest( - input: Primitives.Types.AESDecryptInput, + input: AtomicPrimitives.Types.AESDecryptInput, expectedOutput: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.AESDecrypt(input); expect output == expectedOutput; } method BasicAESEncryptTest( - input: Primitives.Types.AESEncryptInput + input: AtomicPrimitives.Types.AESEncryptInput ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.AESEncrypt(input); - var decryptInput := Primitives.Types.AESDecryptInput( + var decryptInput := AtomicPrimitives.Types.AESDecryptInput( encAlg := input.encAlg, key := input.key, cipherTxt := output.cipherText, diff --git a/AwsCryptographyPrimitives/test/TestAesKdfCtr.dfy b/AwsCryptographyPrimitives/test/TestAesKdfCtr.dfy index 3a62c49d3..60c6a6c0b 100644 --- a/AwsCryptographyPrimitives/test/TestAesKdfCtr.dfy +++ b/AwsCryptographyPrimitives/test/TestAesKdfCtr.dfy @@ -5,7 +5,7 @@ include "../src/Index.dfy" include "../src/AesKdfCtr.dfy" module TestAwsCryptographyPrimitivesAesKdfCtr { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened Wrappers import opened StandardLibrary.UInt import opened AesKdfCtr diff --git a/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHKDF.dfy b/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHKDF.dfy index ea092fbcc..eee553e9f 100644 --- a/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHKDF.dfy +++ b/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHKDF.dfy @@ -5,7 +5,7 @@ include "../src/Index.dfy" include "../src/Digest.dfy" module TestAwsCryptographyPrimitivesHKDF { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened Wrappers import opened StandardLibrary.UInt import Digest @@ -14,7 +14,7 @@ module TestAwsCryptographyPrimitivesHKDF { // https://tools.ietf.org/html/rfc5869#appendix-A // A.1. Test Case 1 Basic test case with SHA-256 - var hash := Primitives.Types.SHA_256; + var hash := AtomicPrimitives.Types.SHA_256; var IKM := [ 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, @@ -48,7 +48,7 @@ module TestAwsCryptographyPrimitivesHKDF { ]; BasicExtractTest( - Primitives.Types.HkdfExtractInput( + AtomicPrimitives.Types.HkdfExtractInput( digestAlgorithm := hash, salt := Some(salt), ikm := IKM @@ -57,7 +57,7 @@ module TestAwsCryptographyPrimitivesHKDF { ); BasicExpandTest( - Primitives.Types.HkdfExpandInput( + AtomicPrimitives.Types.HkdfExpandInput( digestAlgorithm := hash, prk := PRK, info := info, @@ -67,7 +67,7 @@ module TestAwsCryptographyPrimitivesHKDF { ); BasicHkdfTest( - Primitives.Types.HkdfInput( + AtomicPrimitives.Types.HkdfInput( digestAlgorithm := hash, salt := Some(salt), ikm := IKM, @@ -79,11 +79,11 @@ module TestAwsCryptographyPrimitivesHKDF { } method BasicExtractTest( - input: Primitives.Types.HkdfExtractInput, + input: AtomicPrimitives.Types.HkdfExtractInput, expectedPRK: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.HkdfExtract(input); expect |output| == Digest.Length(input.digestAlgorithm); @@ -91,11 +91,11 @@ module TestAwsCryptographyPrimitivesHKDF { } method BasicExpandTest( - input: Primitives.Types.HkdfExpandInput, + input: AtomicPrimitives.Types.HkdfExpandInput, expectedOKM: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.HkdfExpand(input); expect |output| == input.expectedLength as nat; @@ -103,11 +103,11 @@ module TestAwsCryptographyPrimitivesHKDF { } method BasicHkdfTest( - input: Primitives.Types.HkdfInput, + input: AtomicPrimitives.Types.HkdfInput, expectedOKM: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.Hkdf(input); expect |output| == input.expectedLength as nat; diff --git a/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHMAC.dfy b/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHMAC.dfy index 4e3fe1fce..a90159328 100644 --- a/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHMAC.dfy +++ b/AwsCryptographyPrimitives/test/TestAwsCryptographyPrimitivesHMAC.dfy @@ -5,14 +5,14 @@ include "../src/Index.dfy" include "../src/Digest.dfy" module TestAwsCryptographyPrimitivesHMAC { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened StandardLibrary.UInt import Digest method {:test} HMACTests() { BasicHMACTest( - digestAlgorithm := Primitives.Types.SHA_256, + digestAlgorithm := AtomicPrimitives.Types.SHA_256, key := [1,2,3,4], // The string "asdf" as bytes message := [ 97, 115, 100, 102 ], @@ -26,7 +26,7 @@ module TestAwsCryptographyPrimitivesHMAC { ); BasicHMACTest( - digestAlgorithm := Primitives.Types.SHA_384, + digestAlgorithm := AtomicPrimitives.Types.SHA_384, key := [1,2,3,4], // The string "asdf" as bytes message := [ 97, 115, 100, 102 ], @@ -40,7 +40,7 @@ module TestAwsCryptographyPrimitivesHMAC { ); BasicHMACTest( - digestAlgorithm := Primitives.Types.SHA_512, + digestAlgorithm := AtomicPrimitives.Types.SHA_512, key := [1,2,3,4], // The string "asdf" as bytes message := [ 97, 115, 100, 102 ], @@ -57,15 +57,15 @@ module TestAwsCryptographyPrimitivesHMAC { } method BasicHMACTest( - nameonly digestAlgorithm: Primitives.Types.DigestAlgorithm, + nameonly digestAlgorithm: AtomicPrimitives.Types.DigestAlgorithm, nameonly key: seq, nameonly message: seq, nameonly expectedDigest: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); - var input := Primitives.Types.HMacInput( + var input := AtomicPrimitives.Types.HMacInput( digestAlgorithm := digestAlgorithm, key := key, message := message diff --git a/AwsCryptographyPrimitives/test/TestDigest.dfy b/AwsCryptographyPrimitives/test/TestDigest.dfy index 03b7c1599..a2172f850 100644 --- a/AwsCryptographyPrimitives/test/TestDigest.dfy +++ b/AwsCryptographyPrimitives/test/TestDigest.dfy @@ -5,13 +5,13 @@ include "../src/Index.dfy" include "../src/Digest.dfy" module TestAwsCryptographyPrimitivesDigest { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened StandardLibrary.UInt import Digest method {:test} DigestTests() { BasicDigestTest( - digestAlgorithm := Primitives.Types.SHA_256, + digestAlgorithm := AtomicPrimitives.Types.SHA_256, // The string "asdf" as bytes message := [ 97, 115, 100, 102 ], expectedDigest := [ @@ -23,7 +23,7 @@ module TestAwsCryptographyPrimitivesDigest { ); BasicDigestTest( - digestAlgorithm := Primitives.Types.SHA_384, + digestAlgorithm := AtomicPrimitives.Types.SHA_384, // The string "asdf" as bytes message := [ 97, 115, 100, 102 ], expectedDigest := [ @@ -37,7 +37,7 @@ module TestAwsCryptographyPrimitivesDigest { ); BasicDigestTest( - digestAlgorithm := Primitives.Types.SHA_512, + digestAlgorithm := AtomicPrimitives.Types.SHA_512, // The string "asdf" as bytes message := [ 97, 115, 100, 102 ], expectedDigest := [ @@ -53,14 +53,14 @@ module TestAwsCryptographyPrimitivesDigest { } method BasicDigestTest( - nameonly digestAlgorithm: Primitives.Types.DigestAlgorithm, + nameonly digestAlgorithm: AtomicPrimitives.Types.DigestAlgorithm, nameonly message: seq, nameonly expectedDigest: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); - var input := Primitives.Types.DigestInput( + var input := AtomicPrimitives.Types.DigestInput( digestAlgorithm := digestAlgorithm, message := message ); diff --git a/AwsCryptographyPrimitives/test/TestECDH.dfy b/AwsCryptographyPrimitives/test/TestECDH.dfy index b1ad68033..c95ee5308 100644 --- a/AwsCryptographyPrimitives/test/TestECDH.dfy +++ b/AwsCryptographyPrimitives/test/TestECDH.dfy @@ -5,9 +5,9 @@ include "../src/Index.dfy" include "../src/ECDH.dfy" module TestECDH { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened StandardLibrary.UInt - import Types = Aws.Cryptography.Primitives.Types + import Types = AwsCryptographyPrimitivesTypes import UTF8 import HexStrings import Base64 diff --git a/AwsCryptographyPrimitives/test/TestGenerateRandomBytes.dfy b/AwsCryptographyPrimitives/test/TestGenerateRandomBytes.dfy index 728b55626..519bf44e7 100644 --- a/AwsCryptographyPrimitives/test/TestGenerateRandomBytes.dfy +++ b/AwsCryptographyPrimitives/test/TestGenerateRandomBytes.dfy @@ -4,14 +4,14 @@ include "../src/Index.dfy" module TestAwsCryptographyPrimitivesGenerateRandomBytes { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened StandardLibrary.UInt method {:test} BasicGenerateRandomBytes() { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var length := 5 as int32; - var input := Primitives.Types.GenerateRandomBytesInput( + var input := AtomicPrimitives.Types.GenerateRandomBytesInput( length := length ); diff --git a/AwsCryptographyPrimitives/test/TestHKDF_Rfc5869TestVectors.dfy b/AwsCryptographyPrimitives/test/TestHKDF_Rfc5869TestVectors.dfy index a4f0b7bc3..39a3881fd 100644 --- a/AwsCryptographyPrimitives/test/TestHKDF_Rfc5869TestVectors.dfy +++ b/AwsCryptographyPrimitives/test/TestHKDF_Rfc5869TestVectors.dfy @@ -6,7 +6,7 @@ include "../src/Digest.dfy" include "TestAwsCryptographyPrimitivesHKDF.dfy" module TestHKDF_Rfc5869TestVectors { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened Wrappers import opened StandardLibrary.UInt import opened TestAwsCryptographyPrimitivesHKDF @@ -31,7 +31,7 @@ module TestHKDF_Rfc5869TestVectors { // 34007208d5b887185865 (42 octets) const a1 := RFCTestVector( name := "A.1. Test Case 1", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, @@ -96,7 +96,7 @@ module TestHKDF_Rfc5869TestVectors { // 1d87 (82 octets) const {:vcs_split_on_every_assert} a2 := RFCTestVector( name := "A.2. Test Case 2", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, @@ -161,7 +161,7 @@ module TestHKDF_Rfc5869TestVectors { // 9d201395faa4b61a96c8 (42 octets) const a3 := RFCTestVector( name := "A.3. Test Case 3", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, @@ -203,7 +203,7 @@ module TestHKDF_Rfc5869TestVectors { print name + "\n"; BasicExtractTest( - Primitives.Types.HkdfExtractInput( + AtomicPrimitives.Types.HkdfExtractInput( digestAlgorithm := hash, salt := if |salt| > 0 then Some(salt) else None, ikm := IKM @@ -212,7 +212,7 @@ module TestHKDF_Rfc5869TestVectors { ); BasicExpandTest( - Primitives.Types.HkdfExpandInput( + AtomicPrimitives.Types.HkdfExpandInput( digestAlgorithm := hash, prk := PRK, info := info, @@ -222,7 +222,7 @@ module TestHKDF_Rfc5869TestVectors { ); BasicHkdfTest( - Primitives.Types.HkdfInput( + AtomicPrimitives.Types.HkdfInput( digestAlgorithm := hash, salt := if |salt| > 0 then Some(salt) else None, ikm := IKM, @@ -235,11 +235,11 @@ module TestHKDF_Rfc5869TestVectors { datatype RFCTestVector = RFCTestVector( nameonly name: string, - nameonly hash: Primitives.Types.DigestAlgorithm, + nameonly hash: AtomicPrimitives.Types.DigestAlgorithm, nameonly IKM: seq, nameonly salt: seq, nameonly info: seq, - nameonly L: Primitives.Types.PositiveInteger, + nameonly L: AtomicPrimitives.Types.PositiveInteger, nameonly PRK: seq, nameonly OKM: seq ) diff --git a/AwsCryptographyPrimitives/test/TestHMAC.dfy b/AwsCryptographyPrimitives/test/TestHMAC.dfy index 1a15d1ab7..d259b3bd1 100644 --- a/AwsCryptographyPrimitives/test/TestHMAC.dfy +++ b/AwsCryptographyPrimitives/test/TestHMAC.dfy @@ -4,14 +4,14 @@ include "../src/Index.dfy" module TestAwsCryptographyPrimitivesHMacDigest { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened StandardLibrary.UInt import Types = AwsCryptographyPrimitivesTypes import Digest import opened Wrappers method {:test} DigestTests() { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); HmacSHA_256(client); HmacSHA_384(client); diff --git a/AwsCryptographyPrimitives/test/TestKDF.dfy b/AwsCryptographyPrimitives/test/TestKDF.dfy index c00ad7732..66be2f4d5 100644 --- a/AwsCryptographyPrimitives/test/TestKDF.dfy +++ b/AwsCryptographyPrimitives/test/TestKDF.dfy @@ -6,7 +6,7 @@ include "../src/Digest.dfy" include "../src/KDF/KdfCtr.dfy" module TestKDF { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened Wrappers import opened StandardLibrary.UInt import Digest @@ -15,18 +15,18 @@ module TestKDF { method KdfRawDeriveTest( ikm: seq, info: seq, - L: Primitives.Types.PositiveInteger, + L: AtomicPrimitives.Types.PositiveInteger, expectedOKM: seq, - digestAlgorithm: Primitives.Types.DigestAlgorithm + digestAlgorithm: AtomicPrimitives.Types.DigestAlgorithm ) requires && |ikm| >= 32 && L > 0 && 4 + |info| < INT32_MAX_LIMIT - && L as int + Digest.Length(Primitives.Types.DigestAlgorithm.SHA_256) < INT32_MAX_LIMIT - 1 - && L as int + Digest.Length(Primitives.Types.DigestAlgorithm.SHA_384) < INT32_MAX_LIMIT - 1 - && (digestAlgorithm == Primitives.Types.DigestAlgorithm.SHA_256 - || digestAlgorithm == Primitives.Types.DigestAlgorithm.SHA_384) + && L as int + Digest.Length(AtomicPrimitives.Types.DigestAlgorithm.SHA_256) < INT32_MAX_LIMIT - 1 + && L as int + Digest.Length(AtomicPrimitives.Types.DigestAlgorithm.SHA_384) < INT32_MAX_LIMIT - 1 + && (digestAlgorithm == AtomicPrimitives.Types.DigestAlgorithm.SHA_256 + || digestAlgorithm == AtomicPrimitives.Types.DigestAlgorithm.SHA_384) { var output := KdfCtr.RawDerive(ikm, info, L, 0, digestAlgorithm); @@ -38,11 +38,11 @@ module TestKDF { } method KdfTest( - input: Primitives.Types.KdfCtrInput, + input: AtomicPrimitives.Types.KdfCtrInput, expectedOKM: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.KdfCounterMode(input); expect |output| == input.expectedLength as nat; diff --git a/AwsCryptographyPrimitives/test/TestKDF_TestVectors.dfy b/AwsCryptographyPrimitives/test/TestKDF_TestVectors.dfy index b0cb916f0..f8c54b926 100644 --- a/AwsCryptographyPrimitives/test/TestKDF_TestVectors.dfy +++ b/AwsCryptographyPrimitives/test/TestKDF_TestVectors.dfy @@ -6,7 +6,7 @@ include "../src/Digest.dfy" include "TestKDF.dfy" module TestKDFK_TestVectors { - import Aws.Cryptography.Primitives + import AtomicPrimitives import UTF8 import opened Wrappers import opened StandardLibrary.UInt @@ -22,7 +22,7 @@ module TestKDFK_TestVectors { // Internal Test Vectors SHOULD only call RawDerive const b1 := InternalTestVector( name := "B.1 Test Case 1", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 226, 4, 214, 212, 102, 170, 213, 7, 255, 175, 109, 109, 171, 10, 91, 38, @@ -49,7 +49,7 @@ module TestKDFK_TestVectors { const b2 := InternalTestVector( name := "B.2 Test Case 2", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 174, 238, 202, 96, 246, 137, 164, 65, 177, 59, 12, 188, 212, 65, 216, 45, @@ -75,7 +75,7 @@ module TestKDFK_TestVectors { const b3 := InternalTestVector( name := "B.3 Test Case 3", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 149, 200, 247, 110, 17, 54, 126, 181, 85, 38, 162, 179, 147, 174, @@ -102,7 +102,7 @@ module TestKDFK_TestVectors { const b4 := InternalTestVector( name := "B.4 Test Case 4", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 77, 5, 57, 31, 214, 251, 30, 41, 46, 120, 171, 150, 25, 177, 183, 42, @@ -128,7 +128,7 @@ module TestKDFK_TestVectors { const b5 := InternalTestVector( name := "B.5 Test Case 5", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 15, 104, 168, 47, 241, 103, 22, 52, 204, 145, 54, 197, 100, 169, 224, 42, @@ -154,7 +154,7 @@ module TestKDFK_TestVectors { const b6 := InternalTestVector( name := "B.6 Test Case 6", - hash := Primitives.Types.SHA_384, + hash := AtomicPrimitives.Types.SHA_384, IKM := [ 130,44,118,74,27,17,112,133,193, 15,14,104,152,20,210,191,189,155, @@ -183,7 +183,7 @@ module TestKDFK_TestVectors { const b7 := InternalTestVector( name := "B.7 Test Case 7", - hash := Primitives.Types.SHA_384, + hash := AtomicPrimitives.Types.SHA_384, IKM := [52,14,33,45,117,142,131,204,91,137,228,181,106,134,238,140,150,49,174,78,75,186,236,21,172,9,94,164,64,123,199,182,52,173,99,13,208,190,133,169,28,8,168,199,225,225,3,11], info := [60,213,86,26,209,47,173,252,228,8,224,65,128,175,206,227,139,131,21,107,158,75,224,119,156,79,13,185,226,107,254,92,205,67,225,89,33,151,124,210,107,29,184,40,139,128,8,158,183,209,187,215,245,158,16,17,179,225,139,81], L := 32, @@ -194,7 +194,7 @@ module TestKDFK_TestVectors { const b8 := InternalTestVector( name := "B.8 Test Case 8", - hash := Primitives.Types.SHA_384, + hash := AtomicPrimitives.Types.SHA_384, IKM := [0,161,45,60,228,255,117,166,227,15,65,243,85,124,130,106,241,50,107,99,2,244,206,136,123,173,61,51,23,165,72,200,192,58,5,114,132,220,195,141,139,198,144,189,74,86,95,71], info := [36,197,192,178,200,16,223,160,142,53,215,254,235,184,199,142,12,215,38,201,46,205,66,217,23,16,19,115,140,162,83,26,148,127,82,60,55,246,76,219,4,48,91,217,105,209,214,249,236,212,100,5,210,130,128,249,104,80,11,167], L := 32, @@ -203,7 +203,7 @@ module TestKDFK_TestVectors { const b9 := InternalTestVector( name := "B.9 Test Case 9", - hash := Primitives.Types.SHA_384, + hash := AtomicPrimitives.Types.SHA_384, IKM := [0,0,217,183,236,111,190,253,242,86,253,104,34,11,82,5,172,101,162,0,17,69,17,140,80,186,107,101,112,50,25,139,139,124,227,178,247,6,138,120,13,193,124,34,69,154,242,183], info := [216,87,84,28,98,184,87,86,220,115,222,125,194,216,111,93,94,139,40,51,139,176,169,69,181,196,253,124,129,247,25,97,185,112,93,61,21,59,25,25,93,0,59,116,33,32,104,237,16,249,108,83,67,134,83,8,122,1,82,207], L := 20, @@ -212,7 +212,7 @@ module TestKDFK_TestVectors { const b10 := InternalTestVector( name := "B.10 Test Case 10", - hash := Primitives.Types.SHA_384, + hash := AtomicPrimitives.Types.SHA_384, IKM := [79,61,116,77,62,68,158,6,39,191,68,152,116,56,40,248,110,99,143,96,98,10,126,212,167,201,181,176,115,105,28,158,201,71,40,197,136,34,232,39,240,246,204,248,109,188,28,174], info := [48,31,238,178,94,108,168,80,62,205,130,31,29,55,135,174,191,179,208,236,81,139,179,17,116,245,32,155,42,193,242,142,211,230,152,115,107,173,16,161,142,60,189,181,220,39,187,209,45,5,139,54,219,8,146,249,207,208,131,0], L := 20, @@ -222,7 +222,7 @@ module TestKDFK_TestVectors { // Generated Test Vectors CAN call KdfCounterMode const c1 := TestVector( name := "C.1 Test Case 1", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 125, 201, 189, 252, 37, 52, 4, 124, 254, 99, 233, 235, 41, 123, 119, 82, @@ -247,7 +247,7 @@ module TestKDFK_TestVectors { const c2 := TestVector( name := "C.2 Test Case 2", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 80, 22, 113, 23, 118, 68, 10, 32, 75, 169, 199, 192, 255, 220, 214, 60, @@ -272,7 +272,7 @@ module TestKDFK_TestVectors { const c3 := TestVector( name := "C.3 Test Case 3", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 57, 90, 16, 46, 83, 54, 189, 241, 27, 242, 237, 236, 246, 66, 54, 226, @@ -298,7 +298,7 @@ module TestKDFK_TestVectors { const c4 := TestVector( name := "C.4 Test Case 4", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 152, 192, 25, 223, 239, 154, 175, 67, 237, 250, 184, 146, 228, 243, @@ -324,7 +324,7 @@ module TestKDFK_TestVectors { const c5 := TestVector( name := "C.5 Test Case 5", - hash := Primitives.Types.SHA_256, + hash := AtomicPrimitives.Types.SHA_256, IKM := [ 166, 236, 116, 51, 140, 189, 192, 175, 42, 154, 51, 26, 208, 149, 76, 159, @@ -361,10 +361,10 @@ module TestKDFK_TestVectors { { var InternalTestVector(name, hash, IKM, info, L, OKM) := vector; print name + "\n"; - expect (|IKM| == 32 || |IKM| == 48) && L > 0 && 4 + |info| < INT32_MAX_LIMIT && (hash == Primitives.Types.SHA_256 || hash == Primitives.Types.SHA_384); + expect (|IKM| == 32 || |IKM| == 48) && L > 0 && 4 + |info| < INT32_MAX_LIMIT && (hash == AtomicPrimitives.Types.SHA_256 || hash == AtomicPrimitives.Types.SHA_384); expect - L as int + Digest.Length(Primitives.Types.DigestAlgorithm.SHA_256) < INT32_MAX_LIMIT - 1 - && L as int + Digest.Length(Primitives.Types.DigestAlgorithm.SHA_384) < INT32_MAX_LIMIT - 1; + L as int + Digest.Length(AtomicPrimitives.Types.DigestAlgorithm.SHA_256) < INT32_MAX_LIMIT - 1 + && L as int + Digest.Length(AtomicPrimitives.Types.DigestAlgorithm.SHA_384) < INT32_MAX_LIMIT - 1; TestKDF.KdfRawDeriveTest(IKM, info, L, OKM, hash); } @@ -375,7 +375,7 @@ module TestKDFK_TestVectors { print name + "\n"; TestKDF.KdfTest( - Primitives.Types.KdfCtrInput( + AtomicPrimitives.Types.KdfCtrInput( digestAlgorithm := hash, ikm := IKM, expectedLength := L, @@ -388,20 +388,20 @@ module TestKDFK_TestVectors { datatype InternalTestVector = InternalTestVector( nameonly name: string, - nameonly hash: Primitives.Types.DigestAlgorithm, + nameonly hash: AtomicPrimitives.Types.DigestAlgorithm, nameonly IKM: seq, nameonly info: seq, - nameonly L: Primitives.Types.PositiveInteger, + nameonly L: AtomicPrimitives.Types.PositiveInteger, nameonly OKM: seq ) datatype TestVector = TestVector( nameonly name: string, - nameonly hash: Primitives.Types.DigestAlgorithm, + nameonly hash: AtomicPrimitives.Types.DigestAlgorithm, nameonly IKM: seq, nameonly info: seq, nameonly purpose: seq, - nameonly L: Primitives.Types.PositiveInteger, + nameonly L: AtomicPrimitives.Types.PositiveInteger, nameonly OKM: seq ) } diff --git a/AwsCryptographyPrimitives/test/TestRSA.dfy b/AwsCryptographyPrimitives/test/TestRSA.dfy index 2aafde804..9ae953fc2 100644 --- a/AwsCryptographyPrimitives/test/TestRSA.dfy +++ b/AwsCryptographyPrimitives/test/TestRSA.dfy @@ -5,7 +5,7 @@ include "../src/Index.dfy" include "../src/Digest.dfy" module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened Wrappers import opened StandardLibrary.UInt import UTF8 @@ -48,13 +48,13 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { + "-----END PUBLIC KEY-----" method {:test} RSAEncryptTests() { - var client :- expect Primitives.AtomicPrimitives(); - var keys := client.GenerateRSAKeyPair(input := Primitives.Types.GenerateRSAKeyPairInput(lengthBits := 2048 as Primitives.Types.RSAModulusLengthBits)); + var client :- expect AtomicPrimitives.AtomicPrimitives(); + var keys := client.GenerateRSAKeyPair(input := AtomicPrimitives.Types.GenerateRSAKeyPairInput(lengthBits := 2048 as AtomicPrimitives.Types.RSAModulusLengthBits)); expect keys.Success?; BasicRSAEncryptTest( - Primitives.Types.RSAEncryptInput( - padding := Primitives.Types.RSAPaddingMode.OAEP_SHA256, + AtomicPrimitives.Types.RSAEncryptInput( + padding := AtomicPrimitives.Types.RSAPaddingMode.OAEP_SHA256, publicKey := keys.value.publicKey.pem, // The string "asdf" as bytes plaintext := [ 97, 115, 100, 102 ] @@ -64,34 +64,34 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { } method {:test} GetRSAKeyModulusLength() { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); // 2048 var publicKey2048 :- expect UTF8.Encode(RSA_PUBLIC_2048); var length2048 :- expect client.GetRSAKeyModulusLength( - Primitives.Types.GetRSAKeyModulusLengthInput(publicKey := publicKey2048)); + AtomicPrimitives.Types.GetRSAKeyModulusLengthInput(publicKey := publicKey2048)); expect length2048.length == 2048; // 3072 var publicKey3072 :- expect UTF8.Encode(RSA_PUBLIC_3072); var length3072 :- expect client.GetRSAKeyModulusLength( - Primitives.Types.GetRSAKeyModulusLengthInput(publicKey := publicKey3072)); + AtomicPrimitives.Types.GetRSAKeyModulusLengthInput(publicKey := publicKey3072)); expect length3072.length == 3072; // 4096 var publicKey4096 :- expect UTF8.Encode(RSA_PUBLIC_4096); var length4096 :- expect client.GetRSAKeyModulusLength( - Primitives.Types.GetRSAKeyModulusLengthInput(publicKey := publicKey4096)); + AtomicPrimitives.Types.GetRSAKeyModulusLengthInput(publicKey := publicKey4096)); expect length4096.length == 4096; } method BasicRSADecryptTests( - input: Primitives.Types.RSADecryptInput, + input: AtomicPrimitives.Types.RSADecryptInput, expectedOutput: seq ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.RSADecrypt(input); expect output == expectedOutput; @@ -99,14 +99,14 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { } method BasicRSAEncryptTest( - input: Primitives.Types.RSAEncryptInput, - keypair: Primitives.Types.GenerateRSAKeyPairOutput + input: AtomicPrimitives.Types.RSAEncryptInput, + keypair: AtomicPrimitives.Types.GenerateRSAKeyPairOutput ) { - var client :- expect Primitives.AtomicPrimitives(); + var client :- expect AtomicPrimitives.AtomicPrimitives(); var output :- expect client.RSAEncrypt(input); - var decryptInput := Primitives.Types.RSADecryptInput( + var decryptInput := AtomicPrimitives.Types.RSADecryptInput( padding := input.padding, privateKey := keypair.privateKey.pem, cipherText := output @@ -116,17 +116,17 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { } method {:test} TestingPemParsingInRSAEncryptionForRSAKeyPairStoredInPEM() { - var allPadding := set p: Primitives.Types.RSAPaddingMode | true :: p; + var allPadding := set p: AtomicPrimitives.Types.RSAPaddingMode | true :: p; var PublicKeyFromGenerateRSAKeyPairPemBytes :- expect UTF8.Encode(StaticPublicKeyFromGenerateRSAKeyPair()); var PrivateKeyFromGenerateRSAKeyPairPemBytes :- expect UTF8.Encode(StaticPrivateKeyFromGenerateRSAKeyPair()); - var KeyFromGenerateRSAKeyPair := Primitives.Types.GenerateRSAKeyPairOutput( - publicKey := Primitives.Types.RSAPublicKey( + var KeyFromGenerateRSAKeyPair := AtomicPrimitives.Types.GenerateRSAKeyPairOutput( + publicKey := AtomicPrimitives.Types.RSAPublicKey( lengthBits := 2048, pem := PublicKeyFromGenerateRSAKeyPairPemBytes ), - privateKey := Primitives.Types.RSAPrivateKey( + privateKey := AtomicPrimitives.Types.RSAPrivateKey( lengthBits := 2048, pem := PrivateKeyFromGenerateRSAKeyPairPemBytes )); @@ -135,7 +135,7 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { { var padding :| padding in allPadding; BasicRSAEncryptTest( - Primitives.Types.RSAEncryptInput( + AtomicPrimitives.Types.RSAEncryptInput( padding := padding, publicKey := KeyFromGenerateRSAKeyPair.publicKey.pem, // The string "asdf" as bytes @@ -149,17 +149,17 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { } method {:test} TestingPemParsingInRSAEncryptionForOnlyRSAPrivateKeyStoredInPEM() { - var allPadding := set p: Primitives.Types.RSAPaddingMode | true :: p; + var allPadding := set p: AtomicPrimitives.Types.RSAPaddingMode | true :: p; var PublicKeyFromTestVectorsPemBytes :- expect UTF8.Encode(StaticPublicKeyFromTestVectors()); var PrivateKeyFromTestVectorsPemBytes :- expect UTF8.Encode(StaticPrivateKeyFromTestVectors()); - var KeyFromTestVectorsPair := Primitives.Types.GenerateRSAKeyPairOutput( - publicKey := Primitives.Types.RSAPublicKey( + var KeyFromTestVectorsPair := AtomicPrimitives.Types.GenerateRSAKeyPairOutput( + publicKey := AtomicPrimitives.Types.RSAPublicKey( lengthBits := 4096, pem := PublicKeyFromTestVectorsPemBytes ), - privateKey := Primitives.Types.RSAPrivateKey( + privateKey := AtomicPrimitives.Types.RSAPrivateKey( lengthBits := 4096, pem := PrivateKeyFromTestVectorsPemBytes )); @@ -169,7 +169,7 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { var padding :| padding in allPadding; BasicRSAEncryptTest( - Primitives.Types.RSAEncryptInput( + AtomicPrimitives.Types.RSAEncryptInput( padding := padding, publicKey := KeyFromTestVectorsPair.publicKey.pem, // The string "asdf" as bytes diff --git a/AwsCryptographyPrimitives/test/TestSignature.dfy b/AwsCryptographyPrimitives/test/TestSignature.dfy index afbce0c26..0ecb376bf 100644 --- a/AwsCryptographyPrimitives/test/TestSignature.dfy +++ b/AwsCryptographyPrimitives/test/TestSignature.dfy @@ -5,9 +5,9 @@ include "../src/Index.dfy" include "../src/Signature.dfy" module TestSignature { - import Aws.Cryptography.Primitives + import AtomicPrimitives import opened StandardLibrary.UInt - import Types = Aws.Cryptography.Primitives.Types + import Types = AwsCryptographyPrimitivesTypes import UTF8 import opened Wrappers import Signature diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy new file mode 100644 index 000000000..c7fa3cb9b --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy @@ -0,0 +1,2 @@ +include "./KeyVectors/src/Index.dfy" +include "./TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy" \ No newline at end of file diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy index fd2f26828..cca3ffeca 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy @@ -13,7 +13,7 @@ module {:options "-functionSyntax:4"} KeyringFromKeyDescription { import MPL = AwsCryptographyMaterialProvidersTypes import opened Wrappers import AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import AtomicPrimitives import Com.Amazonaws.Kms import ComAmazonawsKmsTypes import KeyMaterial @@ -281,7 +281,7 @@ module {:options "-functionSyntax:4"} KeyringFromKeyDescription { case ECDH(RawEcdh(senderKeyId: string, recipientKeyId: string, senderPublicKey: string, recipientPublicKey: string, providerId: string, curveSpec: string, keyAgreementScheme: string)) => { :- Need(curveSpec in KeyDescription.Curve2EccAlgorithmSpec, KeyVectorException(message := "Unknown curve spec")); var curveType := KeyDescription.Curve2EccAlgorithmSpec[curveSpec]; - var primitives? := Primitives.AtomicPrimitives(); + var primitives? := AtomicPrimitives.AtomicPrimitives(); var primitives :- primitives?.MapFailure(e => KeyVectorException( message := "Unable to create primitives client")); match keyAgreementScheme case "static" => { diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy index a91efcc6d..4b5021e9b 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy @@ -3,9 +3,7 @@ include "../Model/AwsCryptographyMaterialProvidersTypesWrapped.dfy" -module - {:extern "software.amazon.cryptography.materialproviders.internaldafny.wrapped" } - WrappedMaterialProviders refines WrappedAbstractAwsCryptographyMaterialProvidersService +module {:extern "software.amazon.cryptography.materialproviders.internaldafny.wrapped" } WrappedMaterialProviders refines WrappedAbstractAwsCryptographyMaterialProvidersService { import WrappedService = MaterialProviders diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy index 3674c06a9..16901ff14 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy @@ -10,7 +10,7 @@ include "../../KeyVectors/src/Index.dfy" module {:options "-functionSyntax:4"} TestManifests { import Types = AwsCryptographyMaterialProvidersTypes import opened Wrappers - import Aws.Cryptography.Primitives + import AtomicPrimitives import TestVectors import FileIO import JSON.API diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectorsUtils.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectorsUtils.dfy index 1ac48ec39..9a3df64a1 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectorsUtils.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectorsUtils.dfy @@ -14,7 +14,7 @@ module TestVectorsUtils { // This is cheating, // I know that this MUST be here // because this is required for MPL - import Aws.Cryptography.Primitives + import AtomicPrimitives import Crypto = AwsCryptographyPrimitivesTypes @@ -136,7 +136,7 @@ module TestVectorsUtils { { // This is copied from the Default CMM - var crypto :- expect Primitives.AtomicPrimitives(); + var crypto :- expect AtomicPrimitives.AtomicPrimitives(); var suite := AlgorithmSuites.GetSuite(algorithmSuiteId); var signingKey: Option>; var verificationKey: Option>; From c4a6ca98e1c0b0d32e0f183aaa69b973d0ab4374 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Mon, 12 Aug 2024 16:05:15 -0700 Subject: [PATCH 2/2] clean --- AwsCryptographyPrimitives/src/Index.dfy | 2 -- .../dafny/CombinedSrc.dfy | 2 -- 2 files changed, 4 deletions(-) delete mode 100644 TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy diff --git a/AwsCryptographyPrimitives/src/Index.dfy b/AwsCryptographyPrimitives/src/Index.dfy index 65c7de54e..0e49b3150 100644 --- a/AwsCryptographyPrimitives/src/Index.dfy +++ b/AwsCryptographyPrimitives/src/Index.dfy @@ -4,8 +4,6 @@ include "../Model/AwsCryptographyPrimitivesTypes.dfy" include "AwsCryptographyPrimitivesOperations.dfy" -// Note: This module name SHOULD be `AtomicPrimitives` -// to align with this project's Smithy-Model localService's `sdkId` trait. module {:extern "software.amazon.cryptography.primitives.internaldafny" } AtomicPrimitives refines AbstractAwsCryptographyPrimitivesService { import Operations = AwsCryptographyPrimitivesOperations diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy deleted file mode 100644 index c7fa3cb9b..000000000 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/CombinedSrc.dfy +++ /dev/null @@ -1,2 +0,0 @@ -include "./KeyVectors/src/Index.dfy" -include "./TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy" \ No newline at end of file