Skip to content

Commit

Permalink
chore: Remove a few more case-based if statements (#639)
Browse files Browse the repository at this point in the history
  • Loading branch information
@atomb @lucasmcdonald3
atomb authored and lucasmcdonald3 committed Aug 29, 2024
1 parent 8e0c9a3 commit f1ac82f
Show file tree
Hide file tree
Showing 3 changed files with 40 additions and 33 deletions.
45 changes: 25 additions & 20 deletions ...afny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -303,52 +303,54 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
var senderPublicKey: Option<KMS.PublicKeyType>;
var compressedSenderPublicKey: Option<seq<uint8>>;

if {
case input.KeyAgreementScheme.KmsPublicKeyDiscovery? =>
match input.KeyAgreementScheme {
case KmsPublicKeyDiscovery(kmsPublicKeyDiscovery) => {
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#kmspublickeydiscovery
//# - MUST provide the recipient's AWS KMS key identifier
var _ :- ValidateKmsKeyId(input.KeyAgreementScheme.KmsPublicKeyDiscovery.recipientKmsIdentifier);
var _ :- ValidateKmsKeyId(kmsPublicKeyDiscovery.recipientKmsIdentifier);
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#kmspublickeydiscovery
//# the keyring MUST call
//# `kms:GetPublicKey` on the recipient's configured KMS key ID.
// (blank line for duvet)
//# If the keyring fails to retrieve the public key, the keyring MUST fail.
recipientPublicKey :- GetEcdhPublicKey(input.kmsClient, input.KeyAgreementScheme.KmsPublicKeyDiscovery.recipientKmsIdentifier);
recipientPublicKey :- GetEcdhPublicKey(input.kmsClient, kmsPublicKeyDiscovery.recipientKmsIdentifier);
senderPublicKey := Option.None();
compressedSenderPublicKey := Option.None();
case input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey? =>
if input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey.senderPublicKey.Some? {
}
case KmsPrivateKeyToStaticPublicKey(kmsPrivateKeyToStaticPublicKey) => {
if kmsPrivateKeyToStaticPublicKey.senderPublicKey.Some? {
:- Need(
KMS.IsValid_PublicKeyType(
input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey.senderPublicKey.value
kmsPrivateKeyToStaticPublicKey.senderPublicKey.value
),
Types.AwsCryptographicMaterialProvidersException(message := "Invalid SenderPublicKey length."));
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#kmsprivatekeytostaticpublickey
//# - MAY provide the sender's public key
//# - Public key MUST be DER-encoded [X.509 SubjectPublicKeyInfo](https://datatracker.ietf.org/doc/html/rfc5280#section-4.1)
senderPublicKey := Some(input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey.senderPublicKey.value);
senderPublicKey := Some(kmsPrivateKeyToStaticPublicKey.senderPublicKey.value);
var compressedPKU :- RawECDHKeyring.CompressPublicKey(Crypto.ECCPublicKey(der := senderPublicKey.value), input.curveSpec, config.crypto);
compressedSenderPublicKey := Some(compressedPKU);
} else {
var _ :- ValidateKmsKeyId(input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey.senderKmsIdentifier);
var _ :- ValidateKmsKeyId(kmsPrivateKeyToStaticPublicKey.senderKmsIdentifier);
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#kmsprivatekeytostaticpublickey
//# On initialization, if the keyring is not configured with
//# a sender public key, the keyring MUST call
//# `kms:GetPublicKey` on the sender's configured KMS key ID.
// (blank line for duvet)
//# If the keyring fails to retrieve the public key, the keyring MUST fail.
var senderPublicKeyResponse :- GetEcdhPublicKey(input.kmsClient, input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey.senderKmsIdentifier);
var senderPublicKeyResponse :- GetEcdhPublicKey(input.kmsClient, kmsPrivateKeyToStaticPublicKey.senderKmsIdentifier);
var compressedPKU :- RawECDHKeyring.CompressPublicKey(Crypto.ECCPublicKey(der := senderPublicKeyResponse), input.curveSpec, config.crypto);
senderPublicKey := Some(senderPublicKeyResponse);
compressedSenderPublicKey := Some(compressedPKU);
}

:- Need(
KMS.IsValid_PublicKeyType(
input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey.recipientPublicKey
kmsPrivateKeyToStaticPublicKey.recipientPublicKey
),
Types.AwsCryptographicMaterialProvidersException(message := "Invalid RecipientPublicKey length."));
recipientPublicKey := input.KeyAgreementScheme.KmsPrivateKeyToStaticPublicKey.recipientPublicKey;
recipientPublicKey := kmsPrivateKeyToStaticPublicKey.recipientPublicKey;
}
}

var _ :- RawECDHKeyring.ValidatePublicKey(
Expand Down Expand Up @@ -521,14 +523,14 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
var senderPublicKey: Option<seq<uint8>>;
var compressedSenderPublicKey: Option<seq<uint8>>;

if {
case input.KeyAgreementScheme.RawPrivateKeyToStaticPublicKey? =>
match input.KeyAgreementScheme {
case RawPrivateKeyToStaticPublicKey(rawPrivateKeyToStaticPublicKey) => {
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#rawprivatekeytostaticpublickey
//# - MUST provide the recipient's public key
recipientPublicKey := input.KeyAgreementScheme.RawPrivateKeyToStaticPublicKey.recipientPublicKey;
recipientPublicKey := rawPrivateKeyToStaticPublicKey.recipientPublicKey;
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#rawprivatekeytostaticpublickey
//# - MUST provide the sender's static private key
senderPrivateKey := Option.Some(input.KeyAgreementScheme.RawPrivateKeyToStaticPublicKey.senderStaticPrivateKey);
senderPrivateKey := Option.Some(rawPrivateKeyToStaticPublicKey.senderStaticPrivateKey);
var reproducedPublicKey :- GetPublicKey(input.curveSpec, Crypto.ECCPrivateKey(pem := senderPrivateKey.value), config.crypto);
var _ :- RawECDHKeyring.ValidatePublicKey(
config.crypto,
Expand All @@ -542,21 +544,24 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
config.crypto
);
compressedSenderPublicKey := Some(compressedSenderPublicKey?);
case input.KeyAgreementScheme.EphemeralPrivateKeyToStaticPublicKey? =>
}
case EphemeralPrivateKeyToStaticPublicKey(ephemeralPrivateKeyToStaticPublicKey) => {
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#ephemeralprivatekeytostaticpublickey
//# - MUST provide the recipient's public key
recipientPublicKey := input.KeyAgreementScheme.EphemeralPrivateKeyToStaticPublicKey.recipientPublicKey;
recipientPublicKey := ephemeralPrivateKeyToStaticPublicKey.recipientPublicKey;
senderPrivateKey := Option.None();
senderPublicKey := Option.None();
compressedSenderPublicKey := Option.None();
case input.KeyAgreementScheme.PublicKeyDiscovery? =>
}
case PublicKeyDiscovery(publicKeyDiscovery) => {
//= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#publickeydiscovery
//# - MUST provide the recipient's static private key
var reproducedPublicKey :- GetPublicKey(input.curveSpec, Crypto.ECCPrivateKey(pem := input.KeyAgreementScheme.PublicKeyDiscovery.recipientStaticPrivateKey), config.crypto);
var reproducedPublicKey :- GetPublicKey(input.curveSpec, Crypto.ECCPrivateKey(pem := publicKeyDiscovery.recipientStaticPrivateKey), config.crypto);
recipientPublicKey := reproducedPublicKey;
senderPrivateKey := Option.None();
senderPublicKey := Option.None();
compressedSenderPublicKey := Option.None();
}
}

var compressedRecipientPublicKey :- RawECDHKeyring.CompressPublicKey(
Expand Down
20 changes: 11 additions & 9 deletions ...oviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -566,19 +566,21 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {

var sharedSecretPublicKey: seq<uint8>;
var sharedSecretKmsKeyId;
if {
case this.keyAgreementScheme.KmsPublicKeyDiscovery? =>
var _ :- ValidateKmsKeyId(this.keyAgreementScheme.KmsPublicKeyDiscovery.recipientKmsIdentifier);
match this.keyAgreementScheme {
case KmsPublicKeyDiscovery(kmsPublicKeyDiscovery) => {
var _ :- ValidateKmsKeyId(kmsPublicKeyDiscovery.recipientKmsIdentifier);
sharedSecretPublicKey := senderPublicKey;
sharedSecretKmsKeyId := this.keyAgreementScheme.KmsPublicKeyDiscovery.recipientKmsIdentifier;
case this.keyAgreementScheme.KmsPrivateKeyToStaticPublicKey? =>
var _ :- ValidateKmsKeyId(this.keyAgreementScheme.KmsPrivateKeyToStaticPublicKey.senderKmsIdentifier);
sharedSecretKmsKeyId := this.keyAgreementScheme.KmsPrivateKeyToStaticPublicKey.senderKmsIdentifier;
if this.keyAgreementScheme.KmsPrivateKeyToStaticPublicKey.recipientPublicKey == recipientPublicKey {
sharedSecretKmsKeyId := kmsPublicKeyDiscovery.recipientKmsIdentifier;
}
case KmsPrivateKeyToStaticPublicKey(kmsPrivateKeyToStaticPublicKey) => {
var _ :- ValidateKmsKeyId(kmsPrivateKeyToStaticPublicKey.senderKmsIdentifier);
sharedSecretKmsKeyId := kmsPrivateKeyToStaticPublicKey.senderKmsIdentifier;
if kmsPrivateKeyToStaticPublicKey.recipientPublicKey == recipientPublicKey {
sharedSecretPublicKey := recipientPublicKey;
} else {
sharedSecretPublicKey := senderPublicKey;
}
}
}

:- Need(
Expand Down Expand Up @@ -705,4 +707,4 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
function E(s : string) : Types.Error {
Types.AwsCryptographicMaterialProvidersException(message := s)
}
}
}
8 changes: 4 additions & 4 deletions ...graphicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,20 +43,20 @@ module {:options "-functionSyntax:4"} WrappedMaterialProvidersMain {

if op?.Success? {
var op := op?.value;
if
case op.Decrypt? =>
match op
case Decrypt(_, _) =>
var result := TestManifests.StartDecrypt(op);
if result.Failure? {
print result.error;
}
expect result.Success?;
case op.Encrypt? =>
case Encrypt(_, _, _) =>
var result := TestManifests.StartEncrypt(op);
if result.Failure? {
print result.error;
}
expect result.Success?;
case op.EncryptManifest? =>
case EncryptManifest(_) =>
var result := CompleteVectors.WriteStuff(op);
if result.Failure? {
print result.error;
Expand Down

0 comments on commit f1ac82f

Please sign in to comment.