in releases/go/encryption-sdk/AwsEncryptionSdkOperations/AwsEncryptionSdkOperations.go [577:823]
func (_static *CompanionStruct_Default___) InternalDecrypt(config Config, cmm m_AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, buffer m_SerializeFunctions.ReadableBuffer, inputEncryptionContext m_Wrappers.Option) m_Wrappers.Result {
var output m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyEncryptionSdkTypes.Companion_DecryptOutput_.Default())
_ = output
var _0_v4Retry bool
_ = _0_v4Retry
_0_v4Retry = false
var _1_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{}
_ = _1_valueOrError0
_1_valueOrError0 = (m_Header.Companion_Default___.ReadHeaderBody(buffer, (config).Dtor_maxEncryptedDataKeys(), (config).Dtor_mpl())).MapFailure(func(coer33 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} {
return func(arg34 interface{}) interface{} {
return coer33(arg34.(m_SerializeFunctions.ReadProblems))
}
}(m_EncryptDecryptHelpers.Companion_Default___.MapSerializeFailure(_dafny.SeqOfString(": ReadHeaderBody"))))
if (_1_valueOrError0).IsFailure() {
output = (_1_valueOrError0).PropagateFailure()
return output
}
var _2_headerBody m_SerializeFunctions.SuccessfulRead
_ = _2_headerBody
_2_headerBody = (_1_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead)
var _3_rawHeader _dafny.Sequence
_ = _3_rawHeader
_3_rawHeader = ((buffer).Dtor_bytes()).Subsequence(((buffer).Dtor_start()).Uint32(), (((_2_headerBody).Dtor_tail()).Dtor_start()).Uint32())
var _4_algorithmSuite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo
_ = _4_algorithmSuite
_4_algorithmSuite = ((_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody)).Dtor_algorithmSuite()
var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _5_valueOrError1
_5_valueOrError1 = (((config).Dtor_mpl()).ValidateCommitmentPolicyOnDecrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnDecryptInput_.Create_ValidateCommitmentPolicyOnDecryptInput_((_4_algorithmSuite).Dtor_id(), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_((config).Dtor_commitmentPolicy())))).MapFailure(func(coer34 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} {
return func(arg35 interface{}) interface{} {
return coer34(arg35.(m_AwsCryptographyMaterialProvidersTypes.Error))
}
}(func(_6_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error {
return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_6_e)
}))
if (_5_valueOrError1).IsFailure() {
output = (_5_valueOrError1).PropagateFailure()
return output
}
var _7___v1 _dafny.Tuple
_ = _7___v1
_7___v1 = (_5_valueOrError1).Extract().(_dafny.Tuple)
var _8_valueOrError2 m_Wrappers.Result = m_Wrappers.Result{}
_ = _8_valueOrError2
var _out0 m_Wrappers.Result
_ = _out0
_out0 = m_EncryptDecryptHelpers.Companion_Default___.GetDecryptionMaterials(cmm, (_4_algorithmSuite).Dtor_id(), (_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody), inputEncryptionContext, (config).Dtor_commitmentPolicy(), (config).Dtor_mpl())
_8_valueOrError2 = _out0
if (_8_valueOrError2).IsFailure() {
output = (_8_valueOrError2).PropagateFailure()
return output
}
var _9_decMat m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials
_ = _9_decMat
_9_decMat = (_8_valueOrError2).Extract().(m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials)
var _10_suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo
_ = _10_suite
_10_suite = (_9_decMat).Dtor_algorithmSuite()
var _11_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _11_valueOrError3
_11_valueOrError3 = m_Wrappers.Companion_Default___.Need((_10_suite).Equals(_4_algorithmSuite), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Stored header algorithm suite does not match decryption algorithm suite.")))
if (_11_valueOrError3).IsFailure() {
output = (_11_valueOrError3).PropagateFailure()
return output
}
var _12_valueOrError4 m_Wrappers.Result = m_Wrappers.Result{}
_ = _12_valueOrError4
_12_valueOrError4 = (m_HeaderAuth.Companion_Default___.ReadHeaderAuthTag((_2_headerBody).Dtor_tail(), _10_suite)).MapFailure(func(coer35 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} {
return func(arg36 interface{}) interface{} {
return coer35(arg36.(m_SerializeFunctions.ReadProblems))
}
}(m_EncryptDecryptHelpers.Companion_Default___.MapSerializeFailure(_dafny.SeqOfString(": ReadHeaderAuthTag"))))
if (_12_valueOrError4).IsFailure() {
output = (_12_valueOrError4).PropagateFailure()
return output
}
var _13_headerAuth m_SerializeFunctions.SuccessfulRead
_ = _13_headerAuth
_13_headerAuth = (_12_valueOrError4).Extract().(m_SerializeFunctions.SuccessfulRead)
var _14_maybeDerivedDataKeys m_Wrappers.Result
_ = _14_maybeDerivedDataKeys
var _out1 m_Wrappers.Result
_ = _out1
_out1 = m_KeyDerivation.Companion_Default___.DeriveKeys(((_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody)).Dtor_messageId(), ((_9_decMat).Dtor_plaintextDataKey()).Dtor_value().(_dafny.Sequence), _10_suite, (config).Dtor_crypto(), (config).Dtor_netV4__0__0__RetryPolicy(), false)
_14_maybeDerivedDataKeys = _out1
var _15_valueOrError5 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _15_valueOrError5
_15_valueOrError5 = m_Wrappers.Companion_Default___.Need((_14_maybeDerivedDataKeys).Is_Success(), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Failed to derive data keys")))
if (_15_valueOrError5).IsFailure() {
output = (_15_valueOrError5).PropagateFailure()
return output
}
var _16_derivedDataKeys m_KeyDerivation.ExpandedKeyMaterial
_ = _16_derivedDataKeys
_16_derivedDataKeys = (_14_maybeDerivedDataKeys).Dtor_value().(m_KeyDerivation.ExpandedKeyMaterial)
var _17_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _17_valueOrError6
_17_valueOrError6 = m_Wrappers.Companion_Default___.Need(m_Header.Companion_Default___.HeaderVersionSupportsCommitment_q(_10_suite, (_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody)), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Invalid commitment values found in header body")))
if (_17_valueOrError6).IsFailure() {
output = (_17_valueOrError6).PropagateFailure()
return output
}
if ((_10_suite).Dtor_commitment()).Is_HKDF() {
var _18_valueOrError7 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _18_valueOrError7
var _out2 m_Wrappers.Result
_ = _out2
_out2 = m_EncryptDecryptHelpers.Companion_Default___.ValidateSuiteData(_10_suite, (_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody), ((_16_derivedDataKeys).Dtor_commitmentKey()).Dtor_value().(_dafny.Sequence))
_18_valueOrError7 = _out2
if (_18_valueOrError7).IsFailure() {
output = (_18_valueOrError7).PropagateFailure()
return output
}
var _19___v2 _dafny.Tuple
_ = _19___v2
_19___v2 = (_18_valueOrError7).Extract().(_dafny.Tuple)
}
var _20_headerEncryptionContext _dafny.Map
_ = _20_headerEncryptionContext
_20_headerEncryptionContext = m_EncryptionContext.Companion_Default___.GetEncryptionContext(((_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody)).Dtor_encryptionContext())
var _21_encryptionContextToOnlyAuthenticate _dafny.Map
_ = _21_encryptionContextToOnlyAuthenticate
_21_encryptionContextToOnlyAuthenticate = Companion_Default___.BuildEncryptionContextToOnlyAuthenticate(_9_decMat)
var _22_canonicalReqEncryptionContext _dafny.Sequence
_ = _22_canonicalReqEncryptionContext
_22_canonicalReqEncryptionContext = m_EncryptionContext.Companion_Default___.GetCanonicalEncryptionContext(_21_encryptionContextToOnlyAuthenticate)
var _23_serializedReqEncryptionContext _dafny.Sequence
_ = _23_serializedReqEncryptionContext
_23_serializedReqEncryptionContext = m_EncryptionContext.Companion_Default___.WriteEmptyEcOrWriteAAD(_22_canonicalReqEncryptionContext)
var _24_maybeHeaderAuth m_Wrappers.Result
_ = _24_maybeHeaderAuth
var _out3 m_Wrappers.Result
_ = _out3
_out3 = ((config).Dtor_crypto()).AESDecrypt(m_AwsCryptographyPrimitivesTypes.Companion_AESDecryptInput_.Create_AESDecryptInput_(((_10_suite).Dtor_encrypt()).Dtor_AES__GCM(), (_16_derivedDataKeys).Dtor_dataKey(), _dafny.SeqOf(), ((_13_headerAuth).Dtor_data().(m_HeaderTypes.HeaderAuth)).Dtor_headerAuthTag(), ((_13_headerAuth).Dtor_data().(m_HeaderTypes.HeaderAuth)).Dtor_headerIv(), _dafny.Companion_Sequence_.Concatenate(_3_rawHeader, _23_serializedReqEncryptionContext)))
_24_maybeHeaderAuth = _out3
if (((_24_maybeHeaderAuth).Is_Failure()) && (((config).Dtor_netV4__0__0__RetryPolicy()).Equals(m_AwsCryptographyEncryptionSdkTypes.Companion_NetV4__0__0__RetryPolicy_.Create_ALLOW__RETRY_()))) && ((_0_v4Retry) == (false)) {
_0_v4Retry = true
var _out4 m_Wrappers.Result
_ = _out4
_out4 = m_KeyDerivation.Companion_Default___.DeriveKeys(((_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody)).Dtor_messageId(), ((_9_decMat).Dtor_plaintextDataKey()).Dtor_value().(_dafny.Sequence), _10_suite, (config).Dtor_crypto(), (config).Dtor_netV4__0__0__RetryPolicy(), true)
_14_maybeDerivedDataKeys = _out4
var _25_valueOrError8 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _25_valueOrError8
_25_valueOrError8 = m_Wrappers.Companion_Default___.Need((_14_maybeDerivedDataKeys).Is_Success(), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Failed to derive data keys")))
if (_25_valueOrError8).IsFailure() {
output = (_25_valueOrError8).PropagateFailure()
return output
}
_16_derivedDataKeys = (_14_maybeDerivedDataKeys).Dtor_value().(m_KeyDerivation.ExpandedKeyMaterial)
_23_serializedReqEncryptionContext = m_EncryptionContext.Companion_Default___.WriteAAD(_22_canonicalReqEncryptionContext)
var _out5 m_Wrappers.Result
_ = _out5
_out5 = ((config).Dtor_crypto()).AESDecrypt(m_AwsCryptographyPrimitivesTypes.Companion_AESDecryptInput_.Create_AESDecryptInput_(((_10_suite).Dtor_encrypt()).Dtor_AES__GCM(), (_16_derivedDataKeys).Dtor_dataKey(), _dafny.SeqOf(), ((_13_headerAuth).Dtor_data().(m_HeaderTypes.HeaderAuth)).Dtor_headerAuthTag(), ((_13_headerAuth).Dtor_data().(m_HeaderTypes.HeaderAuth)).Dtor_headerIv(), _dafny.Companion_Sequence_.Concatenate(_3_rawHeader, _23_serializedReqEncryptionContext)))
_24_maybeHeaderAuth = _out5
}
var _26_valueOrError9 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _26_valueOrError9
_26_valueOrError9 = (_24_maybeHeaderAuth).MapFailure(func(coer36 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} {
return func(arg37 interface{}) interface{} {
return coer36(arg37.(m_AwsCryptographyPrimitivesTypes.Error))
}
}(func(_27_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error {
return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_27_e)
}))
if (_26_valueOrError9).IsFailure() {
output = (_26_valueOrError9).PropagateFailure()
return output
}
var _28___v3 _dafny.Sequence
_ = _28___v3
_28___v3 = (_26_valueOrError9).Extract().(_dafny.Sequence)
var _29_header m_Header.HeaderInfo
_ = _29_header
_29_header = m_Header.Companion_HeaderInfo_.Create_HeaderInfo_((_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody), _3_rawHeader, _20_headerEncryptionContext, _10_suite, (_13_headerAuth).Dtor_data().(m_HeaderTypes.HeaderAuth))
var _30_key _dafny.Sequence
_ = _30_key
_30_key = (_16_derivedDataKeys).Dtor_dataKey()
var _31_plaintext _dafny.Sequence = _dafny.EmptySeq
_ = _31_plaintext
var _32_messageBodyTail m_SerializeFunctions.ReadableBuffer = m_SerializeFunctions.Companion_ReadableBuffer_.Default()
_ = _32_messageBodyTail
var _source0 m_HeaderTypes.ContentType = ((_29_header).Dtor_body()).Dtor_contentType()
_ = _source0
{
{
if _source0.Is_NonFramed() {
var _33_valueOrError10 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf(_dafny.EmptySeq, m_SerializeFunctions.Companion_ReadableBuffer_.Default()))
_ = _33_valueOrError10
var _out6 m_Wrappers.Result
_ = _out6
_out6 = m_EncryptDecryptHelpers.Companion_Default___.ReadAndDecryptNonFramedMessageBody((_13_headerAuth).Dtor_tail(), _29_header, _30_key, (config).Dtor_crypto())
_33_valueOrError10 = _out6
if (_33_valueOrError10).IsFailure() {
output = (_33_valueOrError10).PropagateFailure()
return output
}
var _34_decryptRes _dafny.Tuple
_ = _34_decryptRes
_34_decryptRes = (_33_valueOrError10).Extract().(_dafny.Tuple)
_31_plaintext = (*(_34_decryptRes).IndexInt(0)).(_dafny.Sequence)
_32_messageBodyTail = (*(_34_decryptRes).IndexInt(1)).(m_SerializeFunctions.ReadableBuffer)
goto Lmatch0
}
}
{
var _35_valueOrError11 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf(_dafny.EmptySeq, m_SerializeFunctions.Companion_ReadableBuffer_.Default()))
_ = _35_valueOrError11
var _out7 m_Wrappers.Result
_ = _out7
_out7 = m_EncryptDecryptHelpers.Companion_Default___.ReadAndDecryptFramedMessageBody((_13_headerAuth).Dtor_tail(), _29_header, _30_key, (config).Dtor_crypto())
_35_valueOrError11 = _out7
if (_35_valueOrError11).IsFailure() {
output = (_35_valueOrError11).PropagateFailure()
return output
}
var _36_decryptRes _dafny.Tuple
_ = _36_decryptRes
_36_decryptRes = (_35_valueOrError11).Extract().(_dafny.Tuple)
_31_plaintext = (*(_36_decryptRes).IndexInt(0)).(_dafny.Sequence)
_32_messageBodyTail = (*(_36_decryptRes).IndexInt(1)).(m_SerializeFunctions.ReadableBuffer)
}
goto Lmatch0
}
Lmatch0:
var _37_valueOrError12 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_SerializeFunctions.Companion_ReadableBuffer_.Default())
_ = _37_valueOrError12
var _out8 m_Wrappers.Result
_ = _out8
_out8 = m_EncryptDecryptHelpers.Companion_Default___.VerifySignature(_32_messageBodyTail, ((_32_messageBodyTail).Dtor_bytes()).Subsequence(((buffer).Dtor_start()).Uint32(), ((_32_messageBodyTail).Dtor_start()).Uint32()), _9_decMat, (config).Dtor_crypto())
_37_valueOrError12 = _out8
if (_37_valueOrError12).IsFailure() {
output = (_37_valueOrError12).PropagateFailure()
return output
}
var _38_signature m_SerializeFunctions.ReadableBuffer
_ = _38_signature
_38_signature = (_37_valueOrError12).Extract().(m_SerializeFunctions.ReadableBuffer)
var _39_valueOrError13 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _39_valueOrError13
_39_valueOrError13 = m_Wrappers.Companion_Default___.Need(((_38_signature).Dtor_start()).Cmp(_dafny.IntOfUint32(((_38_signature).Dtor_bytes()).Cardinality())) == 0, m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Data after message footer.")))
if (_39_valueOrError13).IsFailure() {
output = (_39_valueOrError13).PropagateFailure()
return output
}
output = m_Wrappers.Companion_Result_.Create_Success_(m_AwsCryptographyEncryptionSdkTypes.Companion_DecryptOutput_.Create_DecryptOutput_(_31_plaintext, ((_29_header).Dtor_encryptionContext()).Merge(_21_encryptionContextToOnlyAuthenticate), (((_29_header).Dtor_suite()).Dtor_id()).Dtor_ESDK()))
return output
}