in releases/go/mpl/AwsKmsEcdhKeyring/AwsKmsEcdhKeyring.go [756:998]
func (_this *DecryptSingleEncryptedDataKey) Invoke(edk interface{}) interface{} {
{
var edk m_AwsCryptographyMaterialProvidersTypes.EncryptedDataKey = edk.(m_AwsCryptographyMaterialProvidersTypes.EncryptedDataKey)
_ = edk
var res m_Wrappers.Result = m_Wrappers.Result{}
_ = res
var _0_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _0_valueOrError0
_0_valueOrError0 = m_Wrappers.Companion_Default___.Need(m_UTF8.Companion_Default___.ValidUTF8Seq((edk).Dtor_keyProviderId()), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Received invalid EDK provider id for AWS KMS ECDH Keyring")))
if (_0_valueOrError0).IsFailure() {
res = (_0_valueOrError0).PropagateFailure()
return res
}
var _1_suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo
_ = _1_suite
_1_suite = ((_this).Materials()).Dtor_algorithmSuite()
var _2_keyProviderId _dafny.Sequence
_ = _2_keyProviderId
_2_keyProviderId = (edk).Dtor_keyProviderId()
var _3_providerInfo _dafny.Sequence
_ = _3_providerInfo
_3_providerInfo = (edk).Dtor_keyProviderInfo()
var _4_ciphertext _dafny.Sequence
_ = _4_ciphertext
_4_ciphertext = (edk).Dtor_ciphertext()
var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _5_valueOrError1
_5_valueOrError1 = m_EdkWrapping.Companion_Default___.GetProviderWrappedMaterial(_4_ciphertext, _1_suite)
if (_5_valueOrError1).IsFailure() {
res = (_5_valueOrError1).PropagateFailure()
return res
}
var _6_providerWrappedMaterial _dafny.Sequence
_ = _6_providerWrappedMaterial
_6_providerWrappedMaterial = (_5_valueOrError1).Extract().(_dafny.Sequence)
var _7_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _7_valueOrError2
_7_valueOrError2 = m_Wrappers.Companion_Default___.Need(((_dafny.IntOfUint32((_3_providerInfo).Cardinality())).Cmp(_dafny.IntOfUint32(m_Constants.Companion_Default___.ECDH__PROVIDER__INFO__521__LEN())) <= 0) && (m_RawECDHKeyring.Companion_Default___.ValidProviderInfoLength(_3_providerInfo)), Companion_Default___.E(_dafny.SeqOfString("EDK ProviderInfo longer than expected")))
if (_7_valueOrError2).IsFailure() {
res = (_7_valueOrError2).PropagateFailure()
return res
}
var _8_keyringVersion uint8
_ = _8_keyringVersion
_8_keyringVersion = (_3_providerInfo).Select(0).(uint8)
var _9_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _9_valueOrError3
_9_valueOrError3 = m_Wrappers.Companion_Default___.Need(_dafny.Companion_Sequence_.Equal(_dafny.SeqOf(_8_keyringVersion), Companion_Default___.AWS__KMS__ECDH__KEYRING__VERSION()), Companion_Default___.E(_dafny.SeqOfString("Incorrect Keyring version found in provider info.")))
if (_9_valueOrError3).IsFailure() {
res = (_9_valueOrError3).PropagateFailure()
return res
}
var _10_recipientPublicKeyLength _dafny.Int
_ = _10_recipientPublicKeyLength
_10_recipientPublicKeyLength = _dafny.IntOfUint32(m_StandardLibrary_UInt.Companion_Default___.SeqToUInt32((_3_providerInfo).Subsequence(uint32(m_Constants.Companion_Default___.ECDH__PROVIDER__INFO__RPL__INDEX()), uint32(m_Constants.Companion_Default___.ECDH__PROVIDER__INFO__RPK__INDEX()))))
var _11_recipientPublicKeyLengthIndex _dafny.Int
_ = _11_recipientPublicKeyLengthIndex
_11_recipientPublicKeyLengthIndex = (_dafny.IntOfUint32(m_Constants.Companion_Default___.ECDH__PROVIDER__INFO__RPK__INDEX())).Plus(_10_recipientPublicKeyLength)
var _12_senderPublicKeyIndex _dafny.Int
_ = _12_senderPublicKeyIndex
_12_senderPublicKeyIndex = (_11_recipientPublicKeyLengthIndex).Plus(m_Constants.Companion_Default___.ECDH__PROVIDER__INFO__PUBLIC__KEY__LEN())
var _13_valueOrError4 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _13_valueOrError4
_13_valueOrError4 = m_Wrappers.Companion_Default___.Need(((_11_recipientPublicKeyLengthIndex).Plus(_dafny.IntOfInt64(4))).Cmp(_dafny.IntOfUint32((_3_providerInfo).Cardinality())) < 0, Companion_Default___.E(_dafny.SeqOfString("Key Provider Info Serialization Error. Serialized length less than expected.")))
if (_13_valueOrError4).IsFailure() {
res = (_13_valueOrError4).PropagateFailure()
return res
}
var _14_providerInfoRecipientPublicKey _dafny.Sequence
_ = _14_providerInfoRecipientPublicKey
_14_providerInfoRecipientPublicKey = (_3_providerInfo).Subsequence(uint32(m_Constants.Companion_Default___.ECDH__PROVIDER__INFO__RPK__INDEX()), (_11_recipientPublicKeyLengthIndex).Uint32())
var _15_providerInfoSenderPublicKey _dafny.Sequence
_ = _15_providerInfoSenderPublicKey
_15_providerInfoSenderPublicKey = (_3_providerInfo).Drop((_12_senderPublicKeyIndex).Uint32())
var _16_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _16_valueOrError5
var _out0 m_Wrappers.Result
_ = _out0
_out0 = m_RawECDHKeyring.Companion_Default___.DecompressPublicKey(_15_providerInfoSenderPublicKey, (_this).CurveSpec(), (_this).CryptoPrimitives())
_16_valueOrError5 = _out0
if (_16_valueOrError5).IsFailure() {
res = (_16_valueOrError5).PropagateFailure()
return res
}
var _17_senderPublicKey _dafny.Sequence
_ = _17_senderPublicKey
_17_senderPublicKey = (_16_valueOrError5).Extract().(_dafny.Sequence)
var _18_valueOrError6 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _18_valueOrError6
var _out1 m_Wrappers.Result
_ = _out1
_out1 = m_RawECDHKeyring.Companion_Default___.DecompressPublicKey(_14_providerInfoRecipientPublicKey, (_this).CurveSpec(), (_this).CryptoPrimitives())
_18_valueOrError6 = _out1
if (_18_valueOrError6).IsFailure() {
res = (_18_valueOrError6).PropagateFailure()
return res
}
var _19_recipientPublicKey _dafny.Sequence
_ = _19_recipientPublicKey
_19_recipientPublicKey = (_18_valueOrError6).Extract().(_dafny.Sequence)
var _20_valueOrError7 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _20_valueOrError7
var _out2 m_Wrappers.Result
_ = _out2
_out2 = m_RawECDHKeyring.Companion_Default___.ValidatePublicKey((_this).CryptoPrimitives(), (_this).CurveSpec(), _17_senderPublicKey)
_20_valueOrError7 = _out2
if (_20_valueOrError7).IsFailure() {
res = (_20_valueOrError7).PropagateFailure()
return res
}
var _21___v0 bool
_ = _21___v0
_21___v0 = (_20_valueOrError7).Extract().(bool)
var _22_valueOrError8 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _22_valueOrError8
var _out3 m_Wrappers.Result
_ = _out3
_out3 = m_RawECDHKeyring.Companion_Default___.ValidatePublicKey((_this).CryptoPrimitives(), (_this).CurveSpec(), _19_recipientPublicKey)
_22_valueOrError8 = _out3
if (_22_valueOrError8).IsFailure() {
res = (_22_valueOrError8).PropagateFailure()
return res
}
var _23___v1 bool
_ = _23___v1
_23___v1 = (_22_valueOrError8).Extract().(bool)
var _24_valueOrError9 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _24_valueOrError9
_24_valueOrError9 = m_Wrappers.Companion_Default___.Need((m_ComAmazonawsKmsTypes.Companion_Default___.IsValid__PublicKeyType(_17_senderPublicKey)) && (m_ComAmazonawsKmsTypes.Companion_Default___.IsValid__PublicKeyType((_this).RecipientPublicKey())), Companion_Default___.E(_dafny.SeqOfString("Received serialized sender public key of incorrect length")))
if (_24_valueOrError9).IsFailure() {
res = (_24_valueOrError9).PropagateFailure()
return res
}
var _25_sharedSecretPublicKey _dafny.Sequence = _dafny.EmptySeq
_ = _25_sharedSecretPublicKey
var _26_sharedSecretKmsKeyId _dafny.Sequence = _dafny.EmptySeq.SetString()
_ = _26_sharedSecretKmsKeyId
var _source0 m_AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations = (_this).KeyAgreementScheme()
_ = _source0
{
{
if _source0.Is_KmsPublicKeyDiscovery() {
var _27_kmsPublicKeyDiscovery m_AwsCryptographyMaterialProvidersTypes.KmsPublicKeyDiscoveryInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations_KmsPublicKeyDiscovery).KmsPublicKeyDiscovery
_ = _27_kmsPublicKeyDiscovery
{
var _28_valueOrError10 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _28_valueOrError10
_28_valueOrError10 = m_AwsKmsUtils.Companion_Default___.ValidateKmsKeyId((_27_kmsPublicKeyDiscovery).Dtor_recipientKmsIdentifier())
if (_28_valueOrError10).IsFailure() {
res = (_28_valueOrError10).PropagateFailure()
return res
}
var _29___v2 _dafny.Tuple
_ = _29___v2
_29___v2 = (_28_valueOrError10).Extract().(_dafny.Tuple)
_25_sharedSecretPublicKey = _17_senderPublicKey
_26_sharedSecretKmsKeyId = (_27_kmsPublicKeyDiscovery).Dtor_recipientKmsIdentifier()
}
goto Lmatch0
}
}
{
var _30_kmsPrivateKeyToStaticPublicKey m_AwsCryptographyMaterialProvidersTypes.KmsPrivateKeyToStaticPublicKeyInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations_KmsPrivateKeyToStaticPublicKey).KmsPrivateKeyToStaticPublicKey
_ = _30_kmsPrivateKeyToStaticPublicKey
{
var _31_valueOrError11 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _31_valueOrError11
_31_valueOrError11 = m_AwsKmsUtils.Companion_Default___.ValidateKmsKeyId((_30_kmsPrivateKeyToStaticPublicKey).Dtor_senderKmsIdentifier())
if (_31_valueOrError11).IsFailure() {
res = (_31_valueOrError11).PropagateFailure()
return res
}
var _32___v3 _dafny.Tuple
_ = _32___v3
_32___v3 = (_31_valueOrError11).Extract().(_dafny.Tuple)
_26_sharedSecretKmsKeyId = (_30_kmsPrivateKeyToStaticPublicKey).Dtor_senderKmsIdentifier()
if _dafny.Companion_Sequence_.Equal((_30_kmsPrivateKeyToStaticPublicKey).Dtor_recipientPublicKey(), _19_recipientPublicKey) {
_25_sharedSecretPublicKey = _19_recipientPublicKey
} else {
_25_sharedSecretPublicKey = _17_senderPublicKey
}
}
}
goto Lmatch0
}
Lmatch0:
var _33_valueOrError12 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _33_valueOrError12
_33_valueOrError12 = m_Wrappers.Companion_Default___.Need(m_ComAmazonawsKmsTypes.Companion_Default___.IsValid__PublicKeyType(_25_sharedSecretPublicKey), Companion_Default___.E(_dafny.SeqOfString("Received Recipient Public Key of incorrect expected length")))
if (_33_valueOrError12).IsFailure() {
res = (_33_valueOrError12).PropagateFailure()
return res
}
var _34_valueOrError13 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _34_valueOrError13
var _out4 m_Wrappers.Result
_ = _out4
_out4 = Companion_Default___.DeriveSharedSecret((_this).Client(), _26_sharedSecretKmsKeyId, _25_sharedSecretPublicKey, (_this).GrantTokens())
_34_valueOrError13 = _out4
if (_34_valueOrError13).IsFailure() {
res = (_34_valueOrError13).PropagateFailure()
return res
}
var _35_sharedSecret _dafny.Sequence
_ = _35_sharedSecret
_35_sharedSecret = (_34_valueOrError13).Extract().(_dafny.Sequence)
var _36_ecdhUnwrap *m_EcdhEdkWrapping.EcdhUnwrap
_ = _36_ecdhUnwrap
var _nw0 *m_EcdhEdkWrapping.EcdhUnwrap = m_EcdhEdkWrapping.New_EcdhUnwrap_()
_ = _nw0
_nw0.Ctor__(_15_providerInfoSenderPublicKey, _14_providerInfoRecipientPublicKey, _35_sharedSecret, Companion_Default___.AWS__KMS__ECDH__KEYRING__VERSION(), (_this).CurveSpec(), (_this).CryptoPrimitives())
_36_ecdhUnwrap = _nw0
var _37_unwrapOutputRes m_Wrappers.Result
_ = _37_unwrapOutputRes
var _out5 m_Wrappers.Result
_ = _out5
_out5 = m_EdkWrapping.Companion_Default___.UnwrapEdkMaterial((edk).Dtor_ciphertext(), (_this).Materials(), _36_ecdhUnwrap)
_37_unwrapOutputRes = _out5
var _38_valueOrError14 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_EdkWrapping.Companion_UnwrapEdkMaterialOutput_.Default(m_EcdhEdkWrapping.Companion_EcdhUnwrapInfo_.Default()))
_ = _38_valueOrError14
_38_valueOrError14 = _37_unwrapOutputRes
if (_38_valueOrError14).IsFailure() {
res = (_38_valueOrError14).PropagateFailure()
return res
}
var _39_unwrapOutput m_EdkWrapping.UnwrapEdkMaterialOutput
_ = _39_unwrapOutput
_39_unwrapOutput = (_38_valueOrError14).Extract().(m_EdkWrapping.UnwrapEdkMaterialOutput)
var _40_valueOrError15 m_Wrappers.Result = m_Wrappers.Result{}
_ = _40_valueOrError15
_40_valueOrError15 = m_Materials.Companion_Default___.DecryptionMaterialsAddDataKey((_this).Materials(), (_39_unwrapOutput).Dtor_plaintextDataKey(), (_39_unwrapOutput).Dtor_symmetricSigningKey())
if (_40_valueOrError15).IsFailure() {
res = (_40_valueOrError15).PropagateFailure()
return res
}
var _41_result m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials
_ = _41_result
_41_result = (_40_valueOrError15).Extract().(m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials)
res = m_Wrappers.Companion_Result_.Create_Success_(_41_result)
return res
return res
}
}