in releases/go/mpl/RawECDHKeyring/RawECDHKeyring.go [518:684]
func (_this *RawEcdhKeyring) OnEncrypt_k(input m_AwsCryptographyMaterialProvidersTypes.OnEncryptInput) m_Wrappers.Result {
{
var res m_Wrappers.Result = m_Wrappers.Result{}
_ = res
if ((_this).KeyAgreementScheme()).Is_PublicKeyDiscovery() {
res = m_Wrappers.Companion_Result_.Create_Failure_(m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("PublicKeyDiscovery Key Agreement Scheme is forbidden on encrypt.")))
return res
}
var _0_operationSenderPrivateKey m_AwsCryptographyPrimitivesTypes.ECCPrivateKey = m_AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Default()
_ = _0_operationSenderPrivateKey
var _1_operationSenderPublicKey m_AwsCryptographyPrimitivesTypes.ECCPublicKey = m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Default()
_ = _1_operationSenderPublicKey
var _2_operationCompressedSenderPublicKey _dafny.Sequence = _dafny.EmptySeq
_ = _2_operationCompressedSenderPublicKey
if ((_this).KeyAgreementScheme()).Is_EphemeralPrivateKeyToStaticPublicKey() {
var _3_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyPrimitivesTypes.Companion_GenerateECCKeyPairOutput_.Default())
_ = _3_valueOrError0
var _out0 m_Wrappers.Result
_ = _out0
_out0 = Companion_Default___.GenerateEphemeralEccKeyPair((_this).CurveSpec(), (_this).CryptoPrimitives())
_3_valueOrError0 = _out0
if (_3_valueOrError0).IsFailure() {
res = (_3_valueOrError0).PropagateFailure()
return res
}
var _4_ephemeralKeyPair m_AwsCryptographyPrimitivesTypes.GenerateECCKeyPairOutput
_ = _4_ephemeralKeyPair
_4_ephemeralKeyPair = (_3_valueOrError0).Extract().(m_AwsCryptographyPrimitivesTypes.GenerateECCKeyPairOutput)
_0_operationSenderPrivateKey = (_4_ephemeralKeyPair).Dtor_privateKey()
_1_operationSenderPublicKey = (_4_ephemeralKeyPair).Dtor_publicKey()
var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _5_valueOrError1
var _out1 m_Wrappers.Result
_ = _out1
_out1 = Companion_Default___.CompressPublicKey(m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_((_1_operationSenderPublicKey).Dtor_der()), (_this).CurveSpec(), (_this).CryptoPrimitives())
_5_valueOrError1 = _out1
if (_5_valueOrError1).IsFailure() {
res = (_5_valueOrError1).PropagateFailure()
return res
}
var _6_operationCompressedSenderPublicKey_q _dafny.Sequence
_ = _6_operationCompressedSenderPublicKey_q
_6_operationCompressedSenderPublicKey_q = (_5_valueOrError1).Extract().(_dafny.Sequence)
_2_operationCompressedSenderPublicKey = _6_operationCompressedSenderPublicKey_q
} else {
_0_operationSenderPrivateKey = (_this).SenderPrivateKey()
_1_operationSenderPublicKey = (_this).SenderPublicKey()
_2_operationCompressedSenderPublicKey = (_this).CompressedSenderPublicKey()
}
var _7_materials m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials
_ = _7_materials
_7_materials = (input).Dtor_materials()
var _8_suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo
_ = _8_suite
_8_suite = ((input).Dtor_materials()).Dtor_algorithmSuite()
var _9_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _9_valueOrError2
var _out2 m_Wrappers.Result
_ = _out2
_out2 = Companion_Default___.LocalDeriveSharedSecret(_0_operationSenderPrivateKey, (_this).RecipientPublicKey(), (_this).CurveSpec(), (_this).CryptoPrimitives())
_9_valueOrError2 = _out2
if (_9_valueOrError2).IsFailure() {
res = (_9_valueOrError2).PropagateFailure()
return res
}
var _10_sharedSecret _dafny.Sequence
_ = _10_sharedSecret
_10_sharedSecret = (_9_valueOrError2).Extract().(_dafny.Sequence)
var _11_valueOrError3 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_UTF8.Companion_ValidUTF8Bytes_.Witness())
_ = _11_valueOrError3
_11_valueOrError3 = (m_UTF8.Encode(Companion_Default___.CurveSpecTypeToString((_this).CurveSpec()))).MapFailure(func(coer115 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg116 interface{}) interface{} {
return coer115(arg116.(_dafny.Sequence))
}
}(Companion_Default___.E))
if (_11_valueOrError3).IsFailure() {
res = (_11_valueOrError3).PropagateFailure()
return res
}
var _12_curveSpecUtf8 _dafny.Sequence
_ = _12_curveSpecUtf8
_12_curveSpecUtf8 = (_11_valueOrError3).Extract().(_dafny.Sequence)
var _13_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _13_valueOrError4
_13_valueOrError4 = m_CanonicalEncryptionContext.Companion_Default___.EncryptionContextToAAD(((input).Dtor_materials()).Dtor_encryptionContext())
if (_13_valueOrError4).IsFailure() {
res = (_13_valueOrError4).PropagateFailure()
return res
}
var _14_canonicalizedEC _dafny.Sequence
_ = _14_canonicalizedEC
_14_canonicalizedEC = (_13_valueOrError4).Extract().(_dafny.Sequence)
var _15_fixedInfo _dafny.Sequence
_ = _15_fixedInfo
_15_fixedInfo = m_EcdhEdkWrapping.Companion_Default___.SerializeFixedInfo(m_Constants.Companion_Default___.ECDH__KDF__UTF8(), _12_curveSpecUtf8, _2_operationCompressedSenderPublicKey, (_this).CompressedRecipientPublicKey(), _14_canonicalizedEC, Companion_Default___.RAW__ECDH__KEYRING__VERSION())
var _16_ecdhGenerateAndWrap *m_EcdhEdkWrapping.EcdhGenerateAndWrapKeyMaterial
_ = _16_ecdhGenerateAndWrap
var _nw0 *m_EcdhEdkWrapping.EcdhGenerateAndWrapKeyMaterial = m_EcdhEdkWrapping.New_EcdhGenerateAndWrapKeyMaterial_()
_ = _nw0
_nw0.Ctor__(_10_sharedSecret, _15_fixedInfo, (_this).CryptoPrimitives())
_16_ecdhGenerateAndWrap = _nw0
var _17_ecdhWrap *m_EcdhEdkWrapping.EcdhWrapKeyMaterial
_ = _17_ecdhWrap
var _nw1 *m_EcdhEdkWrapping.EcdhWrapKeyMaterial = m_EcdhEdkWrapping.New_EcdhWrapKeyMaterial_()
_ = _nw1
_nw1.Ctor__(_10_sharedSecret, _15_fixedInfo, (_this).CryptoPrimitives())
_17_ecdhWrap = _nw1
var _18_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_EdkWrapping.Companion_WrapEdkMaterialOutput_.Default(m_EcdhEdkWrapping.Companion_EcdhWrapInfo_.Default()))
_ = _18_valueOrError5
var _out3 m_Wrappers.Result
_ = _out3
_out3 = m_EdkWrapping.Companion_Default___.WrapEdkMaterial(_7_materials, _17_ecdhWrap, _16_ecdhGenerateAndWrap)
_18_valueOrError5 = _out3
if (_18_valueOrError5).IsFailure() {
res = (_18_valueOrError5).PropagateFailure()
return res
}
var _19_wrapOutput m_EdkWrapping.WrapEdkMaterialOutput
_ = _19_wrapOutput
_19_wrapOutput = (_18_valueOrError5).Extract().(m_EdkWrapping.WrapEdkMaterialOutput)
var _20_symmetricSigningKeyList m_Wrappers.Option
_ = _20_symmetricSigningKeyList
if ((_19_wrapOutput).Dtor_symmetricSigningKey()).Is_Some() {
_20_symmetricSigningKeyList = m_Wrappers.Companion_Option_.Create_Some_(_dafny.SeqOf(((_19_wrapOutput).Dtor_symmetricSigningKey()).Dtor_value().(_dafny.Sequence)))
} else {
_20_symmetricSigningKeyList = m_Wrappers.Companion_Option_.Create_None_()
}
var _21_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _21_valueOrError6
_21_valueOrError6 = m_Wrappers.Companion_Default___.Need((Companion_Default___.ValidCompressedPublicKeyLength(_2_operationCompressedSenderPublicKey)) && (Companion_Default___.ValidCompressedPublicKeyLength((_this).CompressedRecipientPublicKey())), Companion_Default___.E(_dafny.SeqOfString("Invalid compressed public key length.")))
if (_21_valueOrError6).IsFailure() {
res = (_21_valueOrError6).PropagateFailure()
return res
}
var _22_edk m_AwsCryptographyMaterialProvidersTypes.EncryptedDataKey
_ = _22_edk
_22_edk = m_AwsCryptographyMaterialProvidersTypes.Companion_EncryptedDataKey_.Create_EncryptedDataKey_(m_Constants.Companion_Default___.RAW__ECDH__PROVIDER__ID(), Companion_Default___.SerializeProviderInfo(_2_operationCompressedSenderPublicKey, (_this).CompressedRecipientPublicKey()), (_19_wrapOutput).Dtor_wrappedMaterial())
if (_19_wrapOutput).Is_GenerateAndWrapEdkMaterialOutput() {
var _23_valueOrError7 m_Wrappers.Result = m_Wrappers.Result{}
_ = _23_valueOrError7
_23_valueOrError7 = m_Materials.Companion_Default___.EncryptionMaterialAddDataKey(_7_materials, (_19_wrapOutput).Dtor_plaintextDataKey(), _dafny.SeqOf(_22_edk), _20_symmetricSigningKeyList)
if (_23_valueOrError7).IsFailure() {
res = (_23_valueOrError7).PropagateFailure()
return res
}
var _24_result m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials
_ = _24_result
_24_result = (_23_valueOrError7).Extract().(m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials)
res = m_Wrappers.Companion_Result_.Create_Success_(m_AwsCryptographyMaterialProvidersTypes.Companion_OnEncryptOutput_.Create_OnEncryptOutput_(_24_result))
return res
} else if (_19_wrapOutput).Is_WrapOnlyEdkMaterialOutput() {
var _25_valueOrError8 m_Wrappers.Result = m_Wrappers.Result{}
_ = _25_valueOrError8
_25_valueOrError8 = m_Materials.Companion_Default___.EncryptionMaterialAddEncryptedDataKeys(_7_materials, _dafny.SeqOf(_22_edk), _20_symmetricSigningKeyList)
if (_25_valueOrError8).IsFailure() {
res = (_25_valueOrError8).PropagateFailure()
return res
}
var _26_result m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials
_ = _26_result
_26_result = (_25_valueOrError8).Extract().(m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials)
res = m_Wrappers.Companion_Result_.Create_Success_(m_AwsCryptographyMaterialProvidersTypes.Companion_OnEncryptOutput_.Create_OnEncryptOutput_(_26_result))
return res
}
return res
}
}