in releases/go/mpl/EcdhEdkWrapping/EcdhEdkWrapping.go [576:731]
func (_this *EcdhUnwrap) Invoke(input interface{}) interface{} {
{
var input m_MaterialWrapping.UnwrapInput = input.(m_MaterialWrapping.UnwrapInput)
_ = input
var res m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_MaterialWrapping.Companion_UnwrapOutput_.Default(Companion_EcdhUnwrapInfo_.Default()))
_ = res
var _0_suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo
_ = _0_suite
_0_suite = (input).Dtor_algorithmSuite()
var _1_wrappedMaterial _dafny.Sequence
_ = _1_wrappedMaterial
_1_wrappedMaterial = (input).Dtor_wrappedMaterial()
var _2_aad _dafny.Map
_ = _2_aad
_2_aad = (input).Dtor_encryptionContext()
var _3_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _3_valueOrError0
_3_valueOrError0 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_1_wrappedMaterial).Cardinality())).Cmp(m_Constants.Companion_Default___.CIPHERTEXT__WRAPPED__MATERIAL__INDEX()) > 0, Companion_Default___.E(_dafny.SeqOfString("Recieved ciphertext is shorter than expected.")))
if (_3_valueOrError0).IsFailure() {
res = (_3_valueOrError0).PropagateFailure()
return res
}
var _4_KeyLength _dafny.Int
_ = _4_KeyLength
_4_KeyLength = _dafny.IntOfInt32(m_AlgorithmSuites.Companion_Default___.GetEncryptKeyLength(_0_suite))
var _5_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _5_valueOrError1
_5_valueOrError1 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_1_wrappedMaterial).Cardinality())).Cmp((m_Constants.Companion_Default___.ECDH__WRAPPED__KEY__MATERIAL__INDEX()).Plus(_4_KeyLength)) > 0, m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Received EDK Ciphertext of incorrect length.")))
if (_5_valueOrError1).IsFailure() {
res = (_5_valueOrError1).PropagateFailure()
return res
}
var _6_kdfNonce _dafny.Sequence
_ = _6_kdfNonce
_6_kdfNonce = (_1_wrappedMaterial).Subsequence(0, (m_Constants.Companion_Default___.ECDH__COMMITMENT__KEY__INDEX()).Uint32())
var _7_iv _dafny.Sequence
_ = _7_iv
_7_iv = _dafny.SeqCreate((_dafny.IntOfInt32((m_Constants.Companion_Default___.ECDH__AES__256__ENC__ALG()).Dtor_ivLength())).Uint32(), func(coer103 func(_dafny.Int) uint8) func(_dafny.Int) interface{} {
return func(arg104 _dafny.Int) interface{} {
return coer103(arg104)
}
}(func(_8___v0 _dafny.Int) uint8 {
return uint8(0)
}))
var _9_commitmentKey _dafny.Sequence
_ = _9_commitmentKey
_9_commitmentKey = (_1_wrappedMaterial).Subsequence((m_Constants.Companion_Default___.ECDH__COMMITMENT__KEY__INDEX()).Uint32(), (m_Constants.Companion_Default___.ECDH__WRAPPED__KEY__MATERIAL__INDEX()).Uint32())
var _10_wrappedKey _dafny.Sequence
_ = _10_wrappedKey
_10_wrappedKey = (_1_wrappedMaterial).Subsequence((m_Constants.Companion_Default___.ECDH__WRAPPED__KEY__MATERIAL__INDEX()).Uint32(), ((m_Constants.Companion_Default___.ECDH__WRAPPED__KEY__MATERIAL__INDEX()).Plus(_4_KeyLength)).Uint32())
var _11_authTag _dafny.Sequence
_ = _11_authTag
_11_authTag = (_1_wrappedMaterial).Drop(((m_Constants.Companion_Default___.ECDH__WRAPPED__KEY__MATERIAL__INDEX()).Plus(_4_KeyLength)).Uint32())
var _12_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_UTF8.Companion_ValidUTF8Bytes_.Witness())
_ = _12_valueOrError2
_12_valueOrError2 = (m_UTF8.Encode(Companion_Default___.CurveSpecTypeToString((_this).CurveSpec()))).MapFailure(func(coer104 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg105 interface{}) interface{} {
return coer104(arg105.(_dafny.Sequence))
}
}(Companion_Default___.E))
if (_12_valueOrError2).IsFailure() {
res = (_12_valueOrError2).PropagateFailure()
return res
}
var _13_curveSpecUtf8 _dafny.Sequence
_ = _13_curveSpecUtf8
_13_curveSpecUtf8 = (_12_valueOrError2).Extract().(_dafny.Sequence)
var _14_valueOrError3 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _14_valueOrError3
_14_valueOrError3 = m_CanonicalEncryptionContext.Companion_Default___.EncryptionContextToAAD((input).Dtor_encryptionContext())
if (_14_valueOrError3).IsFailure() {
res = (_14_valueOrError3).PropagateFailure()
return res
}
var _15_canonicalizedEC _dafny.Sequence
_ = _15_canonicalizedEC
_15_canonicalizedEC = (_14_valueOrError3).Extract().(_dafny.Sequence)
var _16_fixedInfo _dafny.Sequence
_ = _16_fixedInfo
_16_fixedInfo = Companion_Default___.SerializeFixedInfo(m_Constants.Companion_Default___.ECDH__KDF__UTF8(), _13_curveSpecUtf8, (_this).SenderPublicKey(), (_this).RecipientPublicKey(), _15_canonicalizedEC, (_this).KeyringVersion())
var _17_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _17_valueOrError4
var _out0 m_Wrappers.Result
_ = _out0
_out0 = Companion_Default___.DeriveSharedKeyingMaterial((_this).SharedSecret(), _16_fixedInfo, _6_kdfNonce, (_this).Crypto())
_17_valueOrError4 = _out0
if (_17_valueOrError4).IsFailure() {
res = (_17_valueOrError4).PropagateFailure()
return res
}
var _18_derivedKeyingMaterial _dafny.Sequence
_ = _18_derivedKeyingMaterial
_18_derivedKeyingMaterial = (_17_valueOrError4).Extract().(_dafny.Sequence)
var _19_calculatedCommitmentKey _dafny.Sequence
_ = _19_calculatedCommitmentKey
_19_calculatedCommitmentKey = (_18_derivedKeyingMaterial).Subsequence(0, 32)
var _20_sharedKeyingMaterial _dafny.Sequence
_ = _20_sharedKeyingMaterial
_20_sharedKeyingMaterial = (_18_derivedKeyingMaterial).Drop(32)
var _21_valueOrError5 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _21_valueOrError5
_21_valueOrError5 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_19_calculatedCommitmentKey).Cardinality())).Cmp(_dafny.IntOfUint32((_9_commitmentKey).Cardinality())) == 0, Companion_Default___.E(_dafny.SeqOfString("Calculated commitment key length does NOT match expected commitment key length")))
if (_21_valueOrError5).IsFailure() {
res = (_21_valueOrError5).PropagateFailure()
return res
}
var _22_check_q bool
_ = _22_check_q
var _out1 bool
_ = _out1
_out1 = (_this).CommitmentKeyCheck(_19_calculatedCommitmentKey, _9_commitmentKey)
_22_check_q = _out1
var _23_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _23_valueOrError6
_23_valueOrError6 = m_Wrappers.Companion_Default___.Need(_22_check_q, Companion_Default___.E(_dafny.SeqOfString("Commitment keys do not match")))
if (_23_valueOrError6).IsFailure() {
res = (_23_valueOrError6).PropagateFailure()
return res
}
var _24_maybeUnwrappedPdk m_Wrappers.Result
_ = _24_maybeUnwrappedPdk
var _out2 m_Wrappers.Result
_ = _out2
_out2 = ((_this).Crypto()).AESDecrypt(m_AwsCryptographyPrimitivesTypes.Companion_AESDecryptInput_.Create_AESDecryptInput_(m_Constants.Companion_Default___.ECDH__AES__256__ENC__ALG(), _20_sharedKeyingMaterial, _10_wrappedKey, _11_authTag, _7_iv, _16_fixedInfo))
_24_maybeUnwrappedPdk = _out2
var _25_valueOrError7 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _25_valueOrError7
_25_valueOrError7 = (_24_maybeUnwrappedPdk).MapFailure(func(coer105 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg106 interface{}) interface{} {
return coer105(arg106.(m_AwsCryptographyPrimitivesTypes.Error))
}
}(func(_26_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyMaterialProvidersTypes.Error {
return m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_26_e)
}))
if (_25_valueOrError7).IsFailure() {
res = (_25_valueOrError7).PropagateFailure()
return res
}
var _27_unwrappedPdk _dafny.Sequence
_ = _27_unwrappedPdk
_27_unwrappedPdk = (_25_valueOrError7).Extract().(_dafny.Sequence)
var _28_valueOrError8 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _28_valueOrError8
_28_valueOrError8 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_27_unwrappedPdk).Cardinality())).Cmp(_dafny.IntOfInt32(m_AlgorithmSuites.Companion_Default___.GetEncryptKeyLength((input).Dtor_algorithmSuite()))) == 0, Companion_Default___.E(_dafny.SeqOfString("Invalid Key Length")))
if (_28_valueOrError8).IsFailure() {
res = (_28_valueOrError8).PropagateFailure()
return res
}
var _29_output m_MaterialWrapping.UnwrapOutput
_ = _29_output
_29_output = m_MaterialWrapping.Companion_UnwrapOutput_.Create_UnwrapOutput_(_27_unwrappedPdk, Companion_EcdhUnwrapInfo_.Create_EcdhUnwrapInfo_())
res = m_Wrappers.Companion_Result_.Create_Success_(_29_output)
return res
return res
}
}