in releases/go/mpl/RawECDHKeyring/RawECDHKeyring.go [1044:1274]
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) && (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___.RAW__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 = 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 = 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 = 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 = 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_sharedSecretPublicKey _dafny.Sequence = _dafny.EmptySeq
_ = _24_sharedSecretPublicKey
var _25_sharedSecretPrivateKey _dafny.Sequence = _dafny.EmptySeq
_ = _25_sharedSecretPrivateKey
var _source0 m_AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations = (_this).KeyAgreementScheme()
_ = _source0
{
{
if _source0.Is_PublicKeyDiscovery() {
var _26_publicKeyDiscovery m_AwsCryptographyMaterialProvidersTypes.PublicKeyDiscoveryInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations_PublicKeyDiscovery).PublicKeyDiscovery
_ = _26_publicKeyDiscovery
{
_24_sharedSecretPublicKey = _17_senderPublicKey
_25_sharedSecretPrivateKey = (_26_publicKeyDiscovery).Dtor_recipientStaticPrivateKey()
}
goto Lmatch0
}
}
{
if _source0.Is_RawPrivateKeyToStaticPublicKey() {
var _27_rawPrivateKeyToStaticPublicKey m_AwsCryptographyMaterialProvidersTypes.RawPrivateKeyToStaticPublicKeyInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations_RawPrivateKeyToStaticPublicKey).RawPrivateKeyToStaticPublicKey
_ = _27_rawPrivateKeyToStaticPublicKey
{
_25_sharedSecretPrivateKey = (_27_rawPrivateKeyToStaticPublicKey).Dtor_senderStaticPrivateKey()
if _dafny.Companion_Sequence_.Equal((_27_rawPrivateKeyToStaticPublicKey).Dtor_recipientPublicKey(), _19_recipientPublicKey) {
_24_sharedSecretPublicKey = _19_recipientPublicKey
} else {
_24_sharedSecretPublicKey = _17_senderPublicKey
}
}
goto Lmatch0
}
}
{
{
res = m_Wrappers.Companion_Result_.Create_Failure_(Companion_Default___.E(_dafny.SeqOfString("EphemeralPrivateKeyToStaticPublicKey Not allowed on decrypt")))
return res
}
}
goto Lmatch0
}
Lmatch0:
var _28_valueOrError9 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _28_valueOrError9
var _out4 m_Wrappers.Result
_ = _out4
_out4 = Companion_Default___.ValidatePublicKey((_this).CryptoPrimitives(), (_this).CurveSpec(), _24_sharedSecretPublicKey)
_28_valueOrError9 = _out4
if (_28_valueOrError9).IsFailure() {
res = (_28_valueOrError9).PropagateFailure()
return res
}
var _29___v3 bool
_ = _29___v3
_29___v3 = (_28_valueOrError9).Extract().(bool)
var _30_valueOrError10 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _30_valueOrError10
var _out5 m_Wrappers.Result
_ = _out5
_out5 = Companion_Default___.LocalDeriveSharedSecret(m_AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Create_ECCPrivateKey_(_25_sharedSecretPrivateKey), m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(_24_sharedSecretPublicKey), (_this).CurveSpec(), (_this).CryptoPrimitives())
_30_valueOrError10 = _out5
if (_30_valueOrError10).IsFailure() {
res = (_30_valueOrError10).PropagateFailure()
return res
}
var _31_sharedSecret _dafny.Sequence
_ = _31_sharedSecret
_31_sharedSecret = (_30_valueOrError10).Extract().(_dafny.Sequence)
var _32_ecdhUnwrap *m_EcdhEdkWrapping.EcdhUnwrap
_ = _32_ecdhUnwrap
var _nw0 *m_EcdhEdkWrapping.EcdhUnwrap = m_EcdhEdkWrapping.New_EcdhUnwrap_()
_ = _nw0
_nw0.Ctor__(_15_providerInfoSenderPublicKey, _14_providerInfoRecipientPublicKey, _31_sharedSecret, Companion_Default___.RAW__ECDH__KEYRING__VERSION(), (_this).CurveSpec(), (_this).CryptoPrimitives())
_32_ecdhUnwrap = _nw0
var _33_unwrapOutputRes m_Wrappers.Result
_ = _33_unwrapOutputRes
var _out6 m_Wrappers.Result
_ = _out6
_out6 = m_EdkWrapping.Companion_Default___.UnwrapEdkMaterial((edk).Dtor_ciphertext(), (_this).Materials(), _32_ecdhUnwrap)
_33_unwrapOutputRes = _out6
var _34_valueOrError11 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_EdkWrapping.Companion_UnwrapEdkMaterialOutput_.Default(m_EcdhEdkWrapping.Companion_EcdhUnwrapInfo_.Default()))
_ = _34_valueOrError11
_34_valueOrError11 = _33_unwrapOutputRes
if (_34_valueOrError11).IsFailure() {
res = (_34_valueOrError11).PropagateFailure()
return res
}
var _35_unwrapOutput m_EdkWrapping.UnwrapEdkMaterialOutput
_ = _35_unwrapOutput
_35_unwrapOutput = (_34_valueOrError11).Extract().(m_EdkWrapping.UnwrapEdkMaterialOutput)
var _36_valueOrError12 m_Wrappers.Result = m_Wrappers.Result{}
_ = _36_valueOrError12
_36_valueOrError12 = m_Materials.Companion_Default___.DecryptionMaterialsAddDataKey((_this).Materials(), (_35_unwrapOutput).Dtor_plaintextDataKey(), (_35_unwrapOutput).Dtor_symmetricSigningKey())
if (_36_valueOrError12).IsFailure() {
res = (_36_valueOrError12).PropagateFailure()
return res
}
var _37_result m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials
_ = _37_result
_37_result = (_36_valueOrError12).Extract().(m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials)
res = m_Wrappers.Companion_Result_.Create_Success_(_37_result)
return res
return res
}
}