Supported

RFC 5282 - Using Authenticated Encryption Algorithms with the Encrypted Payload of the Internet Key Exchange version 2 (IKEv2) Protocol

Every requirement this repository extracted from RFC 5282, the tests bound to it, and what a reader has verified about them. This summary is enrolled and gated by ./le rfc check.

Overview

Positive

what Ze has

Tested both ways100.0%19 of 19 gated MUSTs

a positive test proves Ze does what the requirement demands and a negative one proves it refuses what the requirement forbids

One polarity plus reason0.0%0 of 19 gated MUSTs

the requirement admits no counter-case, so one polarity plus a recorded reason is the whole proof available for it

One polarity, unexcused0.0%0 of 19 gated MUSTs

one direction is tested, the other is neither tested nor excused, and nothing states which

Partial proof; remaining gap0.0%0 of 19 gated MUSTs

scoped tests exist; the remaining obligation is unmet or unproven, with zero whole-requirement credit

No test at all0.0%0 of 19 gated MUSTs

no test carries the requirement id, whether or not a gap states why

Proven by a recorded break100.0%50 of 50 tagged units

a red was observed once under a recorded procedure, and the unit, the claim and the producer it rested on still hash to what was recorded. The break is not re-run. A test pair is not a proof until one has been observed

Neutral

measures that are neither good news nor bad

Gated MUSTs19of 30 this summary declares

MUST-level requirements the gate HOLDS. A population, not a result: the shares beside it are what says how Ze stands

Out of scope0of 19 gated MUSTs

an obligation that does not bind Ze. A {not-applicable} annotation says it never bound; a {feature-declined} annotation says its condition is an optional feature Ze does not offer, and quotes the RFC sentence that makes it optional. Scope, not coverage: it stays in the denominator every share on this page is taken over

Not applicable0.0%0 of 19 gated MUSTs

a {not-applicable} annotation says the obligation does not bind Ze, so no test is owed for it. It stays in the denominator every share here is taken over

Met below Ze0.0%0 of 19 gated MUSTs

a {lower-layer} annotation says a layer under Ze performs the behavior, on state Ze installs into that layer, and names the producer that installs it. The obligation binds Ze and is met; Ze proves none of it, because its own boundary carries no value the behavior reads

Optional feature declined0.0%0 of 19 gated MUSTs

a {feature-declined} annotation says the obligation is conditional on a feature the RFC makes optional and Ze does not offer, and it quotes the sentence that makes it optional. The condition is false, so nothing is owed and nothing is missing. It stays in the denominator every share here is taken over

The 8 shares marked as a part above are the whole of the 19 gated MUSTs: they add to 100%. Proven by a recorded break is a share of TAGGED UNITS, a different population, so it is not one of them.

How to read the colors

A color names what the measure MEANS, not how well Ze scores on it. Green is a good outcome at any value, red is a bad one, and neither a population nor a scope count is an outcome, so both take no color. The number under the label is what says how far Ze has got.

Card	Tone here	Why that color
Gated MUSTs	neutral	no color: a population is a scale, and a larger one is neither good news nor bad. It is the accounting total
Out of scope	neutral	no color: an obligation that never bound Ze is neither an achievement nor a failure, and counting it either way would be a claim
Tested both ways	ok	green at every value: a test pair is the outcome this gate exists to produce, and the share under the label is what says how far Ze has got
One polarity plus reason	ok	green at every value: where no counter-case exists, one polarity IS the complete answer, and a recorded reason is what the gate demands beside it
One polarity, unexcused	ok	green at zero, RED above it: half a proof with no reason for the other half
Partial proof; remaining gap	ok	green at zero, RED above it: a tested clause cannot prove the whole requirement
No test at all	ok	green at zero, RED above it: a binding obligation nothing exercises is a claim with nothing behind it, whether or not a reason is stated
Not applicable	neutral	no color: an obligation that never bound Ze is neither an achievement nor a failure, and counting it either way would be a claim
Met below Ze	neutral	no color: an obligation met below Ze is neither a test Ze wrote nor work Ze owes, and the two green shares above are what says how much Ze proves itself
Optional feature declined	neutral	no color: an obligation whose condition Ze never meets is neither an achievement nor a failure. The absent FEATURE is disclosed on the RFC's own status row, as an implementation gap a later scope decision can revisit
Proven by a recorded break	ok	green at every value: an observed break is the outcome the discrimination gate exists to produce. The denominator is TAGGED UNITS, not obligations, so this share is not one of the parts above
Audit verdicts	warn	RED on the first weak, wrong or unimplemented verdict, amber while a verdict is no longer current or a gated MUST is unjudged, green when every one is judged sound and current

At a glance

Field	Value
Public status	Supported
Enrolment	Enrolled
Requirements	30
Gated MUST-level	19
Not applicable, so out of scope	0
Declared gaps	0
Declared gaps a test demonstrates	0
Gated with no test	0
Nightly-only evidence	0
Test tags	50
Tagged units	50
Recorded audit verdicts	18
Discrimination records	50
Summary	`rfc/short/rfc5282.md`
Requirement shard	`rfc/requirements/rfc5282.md`
RFC text	`rfc/full/rfc5282.txt`

Enrolment

Enrolled: Using AEAD Algorithms with the IKEv2 Encrypted Payload (RFC 5282): ze speaks one AEAD cipher for the IKE SA, ENCR_AES_GCM_16 (Transform ID 20) at 128 and 256 bits. buildSKMessageAEADWithMsgID (engine/auth.go) seals an 8-octet IV, a salt-then-IV 12-octet nonce and the IKE-header-through-SK-generic-header associated data; decryptSKPayload and crypto.DecryptIKEAEAD (crypto/cipher.go) open it. encKeyMaterialLen (crypto/keys.go) gives SK_ei and SK_er the RFC 4106 KEYMAT layout (cipher key then 4-octet salt) and leaves SK_ai and SK_ar at zero octets. AES CCM is implemented too, at all three ICV sizes RFC 5282 Section 7.2 assigns a Transform ID: ENCR_AES_CCM_8 (14), ENCR_AES_CCM_12 (15) and ENCR_AES_CCM_16 (16), at 128 and 256 bits. aeadTransforms (crypto/aead.go) carries the salt, the ICV and the mode of every AEAD transform, SealIKEAEAD and OpenIKEAEAD drive them, and ccm.New (internal/core/ccm) is the CCM mode of RFC 3610, which the Go standard library does not carry. Every one of the 19 gated rows now carries a both-polarity tagged test. AES CCM for ESP is not offered: EncryptionImplementedESP (ipsec/algorithm_support.go) refuses it at config parse, because no dataplane backend installs an AES CCM Security Association.

What the public ledger says

Status: Supported

What the ledger says is covered

AES GCM and AES CCM IKEv2 AEAD encryption and decryption framing: the eight-octet IV, the salt-then-IV nonce at twelve octets for AES GCM and eleven for AES CCM, the full-length sixteen-octet AES GCM ICV and the eight, twelve and sixteen octet AES CCM ICVs, the associated data from the fixed header through the Encrypted payload's own generic header, any Padding up to 255 octets on receipt, the KEYMAT layout of SK_ei and SK_er with each cipher's own salt length, and the negotiation rules that carry the Key Length attribute and refuse an integrity transform.

What the ledger says remains

The AES CCM transforms are offered for the IKE SA alone. An esp-group proposal naming one is refused at config parse, because xfrmAEADName (dataplane/xfrm_linux.go) names no kernel AES CCM transform and aeadSaltBytes (dataplane/vpp.go) knows no AES CCM salt. That is an implementation gap in the ESP dataplane, which RFC 4309 governs, and not a conformance gap in this document: every obligation RFC 5282 places on the IKEv2 Encrypted payload is met for both AEAD families.

Coverage

Bucket	Count	What it counts
Positive and negative tests	19	one part of the gated population
Annotated (including scoped evidence)	0	one part of the gated population
One polarity only	0	one part of the gated population
No test and no annotation	0	one part of the gated population
Partial proof; remaining gap (subset of annotated; zero whole-requirement credit)	0	an overlay: each of these is also counted by the part it falls in
Evidence that runs nightly only	0	an overlay: each of these is also counted by the part it falls in
Derived from other rows	0	outside the gated population: each asserts nothing and derives its state from the rows it names, which the parts above already count
Gated MUST-level requirements	19	every gated MUST falls in exactly one bucket above

Positive and negative tests (19): RFC5282-3-1, RFC5282-3.1-1, RFC5282-3.1-2, RFC5282-3.2-1, RFC5282-3.2-2, RFC5282-3.2-3, RFC5282-3.2-4, RFC5282-4-1, RFC5282-4-2, RFC5282-4-3, RFC5282-4-4, RFC5282-5.1-1, RFC5282-5.1-2, RFC5282-7.1-1, RFC5282-7.1-2, RFC5282-7.3-1, RFC5282-7.3-2, RFC5282-8-1, RFC5282-8-2

Requirements

Requirement	Level	Section	Tests
`RFC5282-3-1`	There are no alignment requirements on the length of the Padding field; the recipient MUST accept any amount of Padding up to 255 octets. (§3)
	MUST	3	positive`unit/verifyTestRFC5282AEADReceiveAcceptsAnyPaddingTo255` negative`unit/verifyTestRFC5282AEADReceiveRefusesATruncatedInnerPayload`
`RFC5282-3.1-1`	The Initialization Vector (IV) MUST be eight octets. (§3.1)
	MUST	3.1	positive`unit/verifyTestRFC5282AEADSendIVIsEightOctets` negative`unit/verifyTestRFC5282AEADReceiveRefusesAnIVThatIsNotEightOctets`
`RFC5282-3.1-2`	The IV MUST be chosen by the encryptor in a manner that ensures that the same IV value is used only once for a given key. (§3.1)
	MUST	3.1	positive`unit/verifyTestRFC5282AEADSendIVIsUniquePerKey` negative`unit/verifyTestRFC5282AEADSendIVDoesNotRepeatForARepeatedMessage`
`RFC5282-3.2-1`	The AES GCM ICV consists solely of the AES GCM Authentication Tag. Implementations MUST support a full-length 16 octet ICV (§3.2)
	MUST	3.2	positive`unit/verifyTestRFC5282AEADSendICVIsSixteenOctets` negative`unit/verifyTestRFC5282AEADReceiveRefusesADamagedICV`
`RFC5282-3.2-2`	The AES GCM ICV consists solely of the AES GCM Authentication Tag. Implementations MUST support a full-length 16 octet ICV, MAY support 8 or 12 octet ICVs, and MUST NOT support other ICV lengths. (§3.2)
	MUST NOT	3.2	positive`unit/verifyTestRFC5282AEADRefusesAForbiddenICVLength` negative`unit/verifyTestRFC5282AEADOpensTheFullLengthICV`
`RFC5282-3.2-3`	Implementations MUST support ICV sizes of 8 octets and 16 octets. (§3.2)
	MUST	3.2	positive`unit/verifyTestRFC5282CCMSupportsTheEightAndSixteenOctetICV` negative`unit/verifyTestRFC5282CCMVerifiesTheEightAndSixteenOctetICV`
`RFC5282-3.2-4`	AES CCM provides an encrypted ICV. Implementations MUST support ICV sizes of 8 octets and 16 octets. Implementations MAY also support 12 octet ICVs and MUST NOT support other ICV lengths. (§3.2)
	MUST NOT	3.2	positive`unit/verifyTestRFC5282CCMRefusesEveryOtherICVLength` negative`unit/verifyTestRFC5282CCMSupportsTheThreePermittedICVLengths`
`RFC5282-4-1`	When this default nonce format is used, both the encryptor and decryptor construct the nonce by concatenating the salt with the IV, in that order. For the use of AES GCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used (§4)
	MUST	4	positive`unit/verifyTestRFC5282AEADNonceIsSaltThenIV` positive`unit/verifyTestRFC5282AEADSendSealsUnderSaltThenIV` negative`unit/verifyTestRFC5282AEADRefusesAReversedNonce`
`RFC5282-4-2`	For the use of AES GCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used and a 12 octet nonce MUST be used. (§4)
	MUST	4	positive`unit/verifyTestRFC5282AEADNonceIsTwelveOctets` negative`unit/verifyTestRFC5282AEADRefusesANonceThatIsNotTwelveOctets`
`RFC5282-4-3`	When this default nonce format is used, both the encryptor and decryptor construct the nonce by concatenating the salt with the IV, in that order. For the use of AES GCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used and a 12 octet nonce MUST be used. Note that this format matches the one specified in Section 4 of [RFC4106], providing compatibility between the use of AES GCM in IKEv2 and ESP. All of the requirements of Section 4 of [RFC4106] apply to the use of AES GCM with the IKEv2 Encrypted Payload. For the use of AES CCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used (§4)
	MUST	4	positive`unit/verifyTestRFC5282CCMNonceIsSaltThenIV` negative`unit/verifyTestRFC5282CCMRefusesAReversedNonce`
`RFC5282-4-4`	For the use of AES CCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used and an 11 octet nonce MUST be used. (§4)
	MUST	4	positive`unit/verifyTestRFC5282CCMNonceIsElevenOctets` negative`unit/verifyTestRFC5282CCMRefusesANonceThatIsNotElevenOctets`
`RFC5282-5.1-1`	The associated data (A) MUST consist of the partial contents of the IKEv2 message, starting from the first octet of the Fixed IKE Header through the last octet of the Payload Header of the Encrypted Payload (i.e., the fourth octet of the Encrypted Payload), as shown in Figure 3. (§5.1)
	MUST	5.1	positive`unit/verifyTestRFC5282AEADAssociatedDataCoversAnInterveningPayload` positive`unit/verifyTestRFC5282AEADSendAssociatedDataRunsThroughTheSKHeader` negative`unit/verifyTestRFC5282AEADRefusesAnAlteredInterveningPayload`
`RFC5282-5.1-2`	The Initialization Vector and Ciphertext fields shown in Figure 1 (above) MUST NOT be included in the associated data. (§5.1)
	MUST NOT	5.1	positive`unit/verifyTestRFC5282AEADAssociatedDataExcludesTheIVAndCiphertext` positive`unit/verifyTestRFC5282AEADSendAssociatedDataExcludesTheIVAndCiphertext` negative`unit/verifyTestRFC5282AEADRefusesAssociatedDataCoveringTheIV`
`RFC5282-7.1-1`	When AES GCM or AES CCM is used with the IKEv2 Encrypted Payload, the SK_ai and SK_ar integrity protection keys are not used; each key MUST be treated as having a size of zero (0) octets. (§7.1)
	MUST	7.1	positive`unit/verifyTestRFC5282AEADIntegrityKeysAreZeroOctets` positive`unit/verifyTestRFC5282CCMIntegrityKeysAreZeroOctets` negative`unit/verifyTestRFC5282NonAEADIntegrityKeysAreDerived`
`RFC5282-7.1-2`	The size of each of the SK_ei and SK_er encryption keys includes additional salt bytes. The size and format of each of the SK_ei and SK_er encryption keys MUST be: o For AES GCM, each encryption key has the size and format of the "KEYMAT requested" material specified in Section 8.1 of [RFC4106] for the AES key size being used. For example, if the AES key size is 128 bits, each encryption key is 20 octets, consisting of a 16-octet AES cipher key followed by 4 octets of salt. o For AES CCM, each key has the size and format of the "KEYMAT requested" material specified in Section 7.1 of [RFC4309] for the AES key size being used. For example, if the AES key size is 128 bits, each encryption key is 19 octets, consisting of a 16-octet AES cipher key followed by 3 octets of salt. (§7.1)
	MUST	7.1	positive`unit/verifyTestRFC5282AEADEncryptionKeysCarryTheirSalt` positive`unit/verifyTestRFC5282CCMEncryptionKeysCarryTheirSalt` negative`unit/verifyTestRFC5282NonAEADEncryptionKeysCarryNoSalt`
`RFC5282-7.3-1`	Because the AES supports three key lengths, the Key Length attribute MUST be specified when any of the identifiers for AES GCM or AES CCM, specified in Section 7.2 of this document, is used. (§7.3)
	MUST	7.3	positive`unit/verifyTestRFC5282AEADCCMProposalCarriesTheKeyLengthAttribute` positive`unit/verifyTestRFC5282AEADProposalCarriesTheKeyLengthAttribute` negative`unit/verifyTestRFC5282AEADOfferWithoutAKeyLengthIsRefused`
`RFC5282-7.3-2`	The Key Length attribute MUST have a value of 128, 192, or 256 (§7.3)
	MUST	7.3	positive`unit/verifyTestRFC5282AEADKeyLengthAcceptsTheThreeValues` negative`unit/verifyTestRFC5282AEADKeyLengthRefusesEveryOtherValue`
`RFC5282-8-1`	This document updates [RFC4306] to require that when an authenticated encryption algorithm is selected as the encryption algorithm for any SA (IKE or ESP), an integrity algorithm MUST NOT be selected for that SA. (§8)
	MUST NOT	8	positive`unit/verifyTestRFC5282AEADESPSelectionCarriesNoIntegrityAlgorithm` positive`unit/verifyTestRFC5282AEADSelectionCarriesNoIntegrityAlgorithm` positive`unit/verifyTestRFC5282ResponderSelectsNoIntegrityForAnAEADChildSA` negative`unit/verifyTestRFC5282AEADESPOfferWithIntegrityIsRefused` negative`unit/verifyTestRFC5282AEADOfferWithIntegrityIsRefused` negative`unit/verifyTestRFC5282ResponderRefusesAnAEADChildSAOfferWithIntegrity`
`RFC5282-8-2`	This document further updates [RFC4306] to require that if all of the encryption algorithms in any proposal are authenticated encryption algorithms, then the proposal MUST NOT propose any integrity transforms. (§8)
	MUST NOT	8	positive`unit/verifyTestRFC5282AEADESPProposalCarriesNoIntegrityTransform` positive`unit/verifyTestRFC5282AEADIKEProposalCarriesNoIntegrityTransform` negative`unit/verifyTestRFC5282NonAEADESPProposalKeepsItsIntegrityTransform` negative`unit/verifyTestRFC5282NonAEADIKEProposalKeepsItsIntegrityTransform`
`RFC5282-4-5`	Specific authenticated encryption algorithms MAY use different nonce formats, but they SHOULD use the default nonce format specified in this section. (§4)
	SHOULD	4	positive`no test`no positive test negative`no test`no negative test
`RFC5282-7.2-1`	A 16-octet ICV size SHOULD be used with IKEv2 (§7.2)
	SHOULD	7.2	positive`no test`no positive test negative`no test`no negative test
`RFC5282-7.2-2`	In general, the use of 12-octet ICVs (values 15 and 19) is NOT RECOMMENDED in order to reduce the number of options for ICV size. (§7.2)
	NOT RECOMMENDED	7.2	positive`no test`no positive test negative`no test`no negative test
`RFC5282-7.2-3`	If an ICV size larger than 8 octets is appropriate, 16-octet ICVs SHOULD be used (§7.2)
	SHOULD	7.2	positive`no test`no positive test negative`no test`no negative test
`RFC5282-7.3-3`	The use of the value 192 is NOT RECOMMENDED. (§7.3)
	NOT RECOMMENDED	7.3	positive`no test`no positive test negative`no test`no negative test
`RFC5282-7.3-4`	If an AES key larger than 128 bits is appropriate, a 256-bit AES key SHOULD be used (§7.3)
	SHOULD	7.3	positive`no test`no positive test negative`no test`no negative test
`RFC5282-3-2`	Padding MAY contain any value chosen by the sender (§3)
	MAY	3	positive`no test`no positive test negative`no test`no negative test
`RFC5282-3.1-3`	The encryptor MAY generate the IV in any manner that ensures uniqueness (§3.1)
	MAY	3.1	positive`no test`no positive test negative`no test`no negative test
`RFC5282-3.2-5`	The AES GCM ICV consists solely of the AES GCM Authentication Tag. Implementations MUST support a full-length 16 octet ICV, MAY support 8 or 12 octet ICVs (§3.2)
	MAY	3.2	positive`no test`no positive test negative`no test`no negative test
`RFC5282-3.2-6`	AES CCM provides an encrypted ICV. Implementations MUST support ICV sizes of 8 octets and 16 octets. Implementations MAY also support 12 octet ICVs (§3.2)
	MAY	3.2	positive`no test`no positive test negative`no test`no negative test
`RFC5282-4-6`	Specific authenticated encryption algorithms MAY use different nonce formats (§4)
	MAY	4	positive`no test`no positive test negative`no test`no negative test

Gaps and untested MUSTs

RFC 5282 declares no gap, and every gated MUST it carries has a test bound to it.

Proof state

A tagged unit reads unproven where no discrimination record exists for it: nothing in this tree has been observed to break it, so the claim its tag makes is unproven.

`RFC5282-3-1`

There are no alignment requirements on the length of the Padding field; the recipient MUST accept any amount of Padding up to 255 octets. (§3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: a receiver refusing a message for its Padding length (0..255). Red: TestRFC5282AEADReceiveAcceptsAnyPaddingTo255 fatals 'decryptAndParse = %v, want the message accepted' for every length 0..255. Negative TestRFC5282AEADReceiveRefusesATruncatedInnerPayload bounds it (expectRefused).

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADReceiveRefusesATruncatedInnerPayload`	unit/verify	revert, verified
positive	`TestRFC5282AEADReceiveAcceptsAnyPaddingTo255`	unit/verify	revert, verified

`RFC5282-3.1-1`

The Initialization Vector (IV) MUST be eight octets. (§3.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an IV other than eight octets. Sender: TestRFC5282AEADSendIVIsEightOctets opens ze's LastSentMsg with the first 8 octets as IV and asserts gotIVOctets == 8. Receiver: TestRFC5282AEADReceiveRefusesAnIVThatIsNotEightOctets expectRefused for 7 and 9. The IV length is the shared ikeIVOctets for GCM and CCM.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADReceiveRefusesAnIVThatIsNotEightOctets`	unit/verify	revert, verified
positive	`TestRFC5282AEADSendIVIsEightOctets`	unit/verify	revert, verified

`RFC5282-3.1-2`

The IV MUST be chosen by the encryptor in a manner that ensures that the same IV value is used only once for a given key. (§3.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an IV repeated under one key. Red: TestRFC5282AEADSendIVIsUniquePerKey fatals on any repeat over 512 builds under one SA; TestRFC5282AEADSendIVDoesNotRepeatForARepeatedMessage fatals when two byte-identical builds share an IV.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADSendIVDoesNotRepeatForARepeatedMessage`	unit/verify	revert, verified
positive	`TestRFC5282AEADSendIVIsUniquePerKey`	unit/verify	revert, verified

`RFC5282-3.2-1`

The AES GCM ICV consists solely of the AES GCM Authentication Tag. Implementations MUST support a full-length 16 octet ICV (§3.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: not supporting the 16 octet AES GCM ICV. Red: TestRFC5282AEADSendICVIsSixteenOctets asserts len(raw)==prefix+IV+plaintext+16 and expectOneDelete on the receiver; TestRFC5282AEADReceiveRefusesADamagedICV proves the 16 octets are verified (flipped and stripped ICV refused).

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADReceiveRefusesADamagedICV`	unit/verify	revert, verified
positive	`TestRFC5282AEADSendICVIsSixteenOctets`	unit/verify	revert, verified

`RFC5282-3.2-2`

The AES GCM ICV consists solely of the AES GCM Authentication Tag. Implementations MUST support a full-length 16 octet ICV, MAY support 8 or 12 octet ICVs, and MUST NOT support other ICV lengths. (§3.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: supporting an AES GCM ICV other than 16, 8, 12. Red: TestRFC5282AEADRefusesAForbiddenICVLength fatals if OpenIKEAEAD(ENCR_AES_GCM_16) accepts a real 13, 14 or 15 octet ICV sealing; TestRFC5282AEADOpensTheFullLengthICV keeps 16 open. Lengths below 12 are not constructed (stdlib limit); ze's only GCM transform (20) fixes the tag at 16, so no other length is reachable.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADOpensTheFullLengthICV`	unit/verify	revert, verified
positive	`TestRFC5282AEADRefusesAForbiddenICVLength`	unit/verify	revert, verified

`RFC5282-3.2-3`

Implementations MUST support ICV sizes of 8 octets and 16 octets. (§3.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: not supporting AES CCM ICVs of 8 and 16. Red: TestRFC5282CCMSupportsTheEightAndSixteenOctetICV establishes under CCM8 and CCM16, measures the ICV (t.Errorf on mismatch) and expectOneDelete; TestRFC5282CCMVerifiesTheEightAndSixteenOctetICV refuses a flipped ICV bit and a flipped ciphertext bit at each size.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282CCMVerifiesTheEightAndSixteenOctetICV`	unit/verify	revert, verified
positive	`TestRFC5282CCMSupportsTheEightAndSixteenOctetICV`	unit/verify	revert, verified

`RFC5282-3.2-4`

AES CCM provides an encrypted ICV. Implementations MUST support ICV sizes of 8 octets and 16 octets. Implementations MAY also support 12 octet ICVs and MUST NOT support other ICV lengths. (§3.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an AES CCM ICV length other than 8, 16, 12. Red: TestRFC5282CCMRefusesEveryOtherICVLength sweeps Transform IDs 0..35, errors if AEADICVOctets answers a length outside {8,12,16} or answers for any id beyond 14,15,16,20, and requires SealIKEAEAD/OpenIKEAEAD to refuse the rest; TestRFC5282CCMSupportsTheThreePermittedICVLengths seals and opens 8, 12 and 16.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282CCMSupportsTheThreePermittedICVLengths`	unit/verify	revert, verified
positive	`TestRFC5282CCMRefusesEveryOtherICVLength`	unit/verify	revert, verified

`RFC5282-4-1`

Audit verdict: enforced (the tests do what the requirement demands), fresh. Encryptor: TestRFC5282AEADSendSealsUnderSaltThenIV opens the real initiator IKE_AUTH request and responder response with an independent stdlib AES-GCM under salt||IV and refuses IV||salt (same length, order alone); SealIKEAEAD (crypto/aead.go) is the only seal site. Decryptor: TestRFC5282AEADNonceIsSaltThenIV accepts salt||IV, TestRFC5282AEADRefusesAReversedNonce refuses the reversed nonce. The ikeAEADNonce record is a whole-producer panic (reach); discrimination read from the independent-oracle assertions.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADRefusesAReversedNonce`	unit/verify	revert, verified
positive	`TestRFC5282AEADSendSealsUnderSaltThenIV`	unit/verify	revert, verified
positive	`TestRFC5282AEADNonceIsSaltThenIV`	unit/verify	revert, verified

`RFC5282-4-2`

For the use of AES GCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used and a 12 octet nonce MUST be used. (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an AES GCM nonce other than 12 octets. Red: TestRFC5282AEADNonceIsTwelveOctets asserts len(nonce)==12 and expectOneDelete; TestRFC5282AEADRefusesANonceThatIsNotTwelveOctets refuses 11 and 13. Sender side: the nonce size is fixed once in newIKEAEAD (salt+ikeIVOctets, checked by newAESGCM) and shared by SealIKEAEAD and OpenIKEAEAD, and Go's AEAD panics on a wrong-length nonce, so a sender-only length change is not reachable without reddening the receive units.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADRefusesANonceThatIsNotTwelveOctets`	unit/verify	revert, verified
positive	`TestRFC5282AEADNonceIsTwelveOctets`	unit/verify	revert, verified

`RFC5282-4-3`

When this default nonce format is used, both the encryptor and decryptor construct the nonce by concatenating the salt with the IV, in that order. For the use of AES GCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used and a 12 octet nonce MUST be used. Note that this format matches the one specified in Section 4 of [RFC4106], providing compatibility between the use of AES GCM in IKEv2 and ESP. All of the requirements of Section 4 of [RFC4106] apply to the use of AES GCM with the IKEv2 Encrypted Payload. For the use of AES CCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an AES CCM nonce not built as salt||IV. Encryptor: TestRFC5282CCMNonceIsSaltThenIV opens ze's own sent message with an independent CCM under the 3 salt octets then the wire IV (fatal on failure). Decryptor: TestRFC5282CCMRefusesAReversedNonce refuses IV||salt.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282CCMRefusesAReversedNonce`	unit/verify	revert, verified
positive	`TestRFC5282CCMNonceIsSaltThenIV`	unit/verify	revert, verified

`RFC5282-4-4`

For the use of AES CCM with the IKEv2 Encrypted Payload, this default nonce format MUST be used and an 11 octet nonce MUST be used. (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an AES CCM nonce other than 11 octets. Red: TestRFC5282CCMNonceIsElevenOctets asserts len(nonce)==11 and expectOneDelete; TestRFC5282CCMRefusesANonceThatIsNotElevenOctets refuses 10 and 12. Sender length is fixed by the shared newIKEAEAD (ccm.New with salt+IV), so a sender-only change is not reachable without reddening these.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282CCMRefusesANonceThatIsNotElevenOctets`	unit/verify	revert, verified
positive	`TestRFC5282CCMNonceIsElevenOctets`	unit/verify	revert, verified

`RFC5282-5.1-1`

The associated data (A) MUST consist of the partial contents of the IKEv2 message, starting from the first octet of the Fixed IKE Header through the last octet of the Payload Header of the Encrypted Payload (i.e., the fourth octet of the Encrypted Payload), as shown in Figure 3. (§5.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Sender: TestRFC5282AEADSendAssociatedDataRunsThroughTheSKHeader pins DataOffset 32 on both ends' real messages and opens them under raw[:32] with an independent AES-GCM, not under raw[:31] nor the fixed header alone; auth.go buildSKMessageAEADWithMsgID is the only seal site. Receiver: TestRFC5282AEADAssociatedDataCoversAnInterveningPayload accepts the span over an intervening payload, TestRFC5282AEADRefusesAnAlteredInterveningPayload refuses an altered one.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADRefusesAnAlteredInterveningPayload`	unit/verify	revert, verified
positive	`TestRFC5282AEADSendAssociatedDataRunsThroughTheSKHeader`	unit/verify	revert, verified
positive	`TestRFC5282AEADAssociatedDataCoversAnInterveningPayload`	unit/verify	revert, verified

`RFC5282-5.1-2`

The Initialization Vector and Ciphertext fields shown in Figure 1 (above) MUST NOT be included in the associated data. (§5.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Sender: TestRFC5282AEADSendAssociatedDataExcludesTheIVAndCiphertext opens both ends' real messages under the span stopping before the IV and refuses AAD covering the IV and IV+ciphertext. Receiver: TestRFC5282AEADAssociatedDataExcludesTheIVAndCiphertext accepts, TestRFC5282AEADRefusesAssociatedDataCoveringTheIV refuses.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADRefusesAssociatedDataCoveringTheIV`	unit/verify	revert, verified
positive	`TestRFC5282AEADSendAssociatedDataExcludesTheIVAndCiphertext`	unit/verify	revert, verified
positive	`TestRFC5282AEADAssociatedDataExcludesTheIVAndCiphertext`	unit/verify	revert, verified

`RFC5282-7.1-1`

When AES GCM or AES CCM is used with the IKEv2 Encrypted Payload, the SK_ai and SK_ar integrity protection keys are not used; each key MUST be treated as having a size of zero (0) octets. (§7.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Both ciphers the clause names are now proven. AES GCM: TestRFC5282AEADIntegrityKeysAreZeroOctets (zero-length SK_ai/SK_ar, SK_ei at the prf+ offset right after SK_d). AES CCM: new TestRFC5282CCMIntegrityKeysAreZeroOctets derives every CCM Transform ID (8/12/16) at 128 and 256 bits and asserts SK_ai/SK_ar zero octets AND SK_ei/SK_er at stream offsets 32 and 32+(n+3) computed independently of the producer, so a derivation that returned empty slices while still consuming integrity material turns red. Negative: TestRFC5282NonAEADIntegrityKeysAreDerived (non-AEAD keeps its integrity keys). Records: DeriveSKKeys revert observed red on all three units (panic reverts; the offset assertions are what discriminate a mis-cut stream).

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282NonAEADIntegrityKeysAreDerived`	unit/verify	revert, verified
positive	`TestRFC5282AEADIntegrityKeysAreZeroOctets`	unit/verify	revert, verified
positive	`TestRFC5282CCMIntegrityKeysAreZeroOctets`	unit/verify	revert, verified

`RFC5282-7.1-2`

The size of each of the SK_ei and SK_er encryption keys includes additional salt bytes. The size and format of each of the SK_ei and SK_er encryption keys MUST be: o For AES GCM, each encryption key has the size and format of the "KEYMAT requested" material specified in Section 8.1 of [RFC4106] for the AES key size being used. For example, if the AES key size is 128 bits, each encryption key is 20 octets, consisting of a 16-octet AES cipher key followed by 4 octets of salt. o For AES CCM, each key has the size and format of the "KEYMAT requested" material specified in Section 7.1 of [RFC4309] for the AES key size being used. For example, if the AES key size is 128 bits, each encryption key is 19 octets, consisting of a 16-octet AES cipher key followed by 3 octets of salt. (§7.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Both bullets proven. AES GCM bullet: TestRFC5282AEADEncryptionKeysCarryTheirSalt (20/36 octets, key-then-salt round trip). AES CCM bullet: new TestRFC5282CCMEncryptionKeysCarryTheirSalt, every CCM ID at 128/256 bits: SK_ei and SK_er are exactly cipher key + 3 octets (19/35), and a SealIKEAEAD output is opened by a ccm instance built in the test from key[:n] with nonce = trailing 3 salt octets || 8-octet IV, which is the RFC 4309 Section 7.1 KEYMAT format and Section 4 nonce; a 4-octet GCM salt or salt-first layout fails the length or the open. Negative: TestRFC5282NonAEADEncryptionKeysCarryNoSalt. Records: SealIKEAEAD and encKeyMaterialLen reverts observed red. Residual: the opener uses ze's own internal/core/ccm package, so it checks the key split, not the CCM primitive itself.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282NonAEADEncryptionKeysCarryNoSalt`	unit/verify	revert, verified
positive	`TestRFC5282AEADEncryptionKeysCarryTheirSalt`	unit/verify	revert, verified
positive	`TestRFC5282CCMEncryptionKeysCarryTheirSalt`	unit/verify	revert, verified

`RFC5282-7.3-1`

Because the AES supports three key lengths, the Key Length attribute MUST be specified when any of the identifiers for AES GCM or AES CCM, specified in Section 7.2 of this document, is used. (§7.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. AES GCM: TestRFC5282AEADProposalCarriesTheKeyLengthAttribute (IKE and ESP rails, exactly one attribute), TestRFC5282AEADOfferWithoutAKeyLengthIsRefused (ErrKeyLengthMissing). AES CCM: TestRFC5282AEADCCMProposalCarriesTheKeyLengthAttribute asserts IDs 14/15/16 x 128/256 each carry exactly one Key Length attribute of the key size from buildWireIKEProposals; ESP does not offer CCM (ipsec.EncryptionImplementedESP excludes it). Residual observation: the receive-side refusal names CCM in keyLengthRequired but only a GCM offer is driven.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADOfferWithoutAKeyLengthIsRefused`	unit/verify	revert, verified
positive	`TestRFC5282AEADCCMProposalCarriesTheKeyLengthAttribute`	unit/verify	revert, verified
positive	`TestRFC5282AEADProposalCarriesTheKeyLengthAttribute`	unit/verify	revert, verified

`RFC5282-7.3-2`

The Key Length attribute MUST have a value of 128, 192, or 256 (§7.3)

Audit verdict: not audited: no reader has judged these tests

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADKeyLengthRefusesEveryOtherValue`	unit/verify	revert, verified
positive	`TestRFC5282AEADKeyLengthAcceptsTheThreeValues`	unit/verify	revert, verified

`RFC5282-8-1`

This document updates [RFC4306] to require that when an authenticated encryption algorithm is selected as the encryption algorithm for any SA (IKE or ESP), an integrity algorithm MUST NOT be selected for that SA. (§8)

Audit verdict: enforced (the tests do what the requirement demands), fresh. IKE SA: TestRFC5282AEADSelectionCarriesNoIntegrityAlgorithm / TestRFC5282AEADOfferWithIntegrityIsRefused. ESP SA, initiator re-check: TestRFC5282AEADESPSelectionCarriesNoIntegrityAlgorithm / TestRFC5282AEADESPOfferWithIntegrityIsRefused. ESP SA, responder (where Ze selects the Child SA's algorithms): TestRFC5282ResponderSelectsNoIntegrityForAnAEADChildSA runs selectResponderESP over an AES-GCM-only SAi2 with Hash configured, then espProposalToWire over the selection exactly as buildAuthResponse does, and asserts one AES GCM transform and zero INTEG transforms in SAr2; TestRFC5282ResponderRefusesAnAEADChildSAOfferWithIntegrity refuses AES-GCM + HMAC-SHA2-256 with ErrNoProposalChosen and accepts no proposal. Records revert responder.go::espProposalMatches. Re-judged 2026-09-30 after espProposalMatches gained the Section 3.3.6 emptied-type refusal: the AEAD+INTEG refusal path is untouched (the INTEG transform in the negative carries no unknown attribute), both records re-recorded and observed red, all six units pass.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282AEADESPOfferWithIntegrityIsRefused`	unit/verify	revert, verified
negative	`TestRFC5282AEADOfferWithIntegrityIsRefused`	unit/verify	revert, verified
negative	`TestRFC5282ResponderRefusesAnAEADChildSAOfferWithIntegrity`	unit/verify	revert, verified
positive	`TestRFC5282AEADESPSelectionCarriesNoIntegrityAlgorithm`	unit/verify	revert, verified
positive	`TestRFC5282AEADSelectionCarriesNoIntegrityAlgorithm`	unit/verify	revert, verified
positive	`TestRFC5282ResponderSelectsNoIntegrityForAnAEADChildSA`	unit/verify	revert, verified

`RFC5282-8-2`

This document further updates [RFC4306] to require that if all of the encryption algorithms in any proposal are authenticated encryption algorithms, then the proposal MUST NOT propose any integrity transforms. (§8)

Audit verdict: enforced (the tests do what the requirement demands), fresh. IKE proposal: TestRFC5282AEADIKEProposalCarriesNoIntegrityTransform / TestRFC5282NonAEADIKEProposalKeepsItsIntegrityTransform. ESP proposal: TestRFC5282AEADESPProposalCarriesNoIntegrityTransform (AES-GCM with Hash configured: zero Transform Type 3, ENCR and ESN kept) and TestRFC5282NonAEADESPProposalKeepsItsIntegrityTransform (AES-CBC: exactly one). espProposalToWire is the single ESP builder (IKE_AUTH offer, CREATE_CHILD_SA offer and answer).

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC5282NonAEADIKEProposalKeepsItsIntegrityTransform`	unit/verify	revert, verified
negative	`TestRFC5282NonAEADESPProposalKeepsItsIntegrityTransform`	unit/verify	revert, verified
positive	`TestRFC5282AEADIKEProposalCarriesNoIntegrityTransform`	unit/verify	revert, verified
positive	`TestRFC5282AEADESPProposalCarriesNoIntegrityTransform`	unit/verify	revert, verified

Extraction sign-off

Field	Value
Reviewer	claude-opus-5 (ipsecwalk), spec-rfcgate-6-supported-extraction-signoff
Signed off	2026-08-31
Register	prose
Source	rfc/full/rfc5282.txt
Source fingerprint	e4b60d44518cbcd7
Record	rfc/extraction/rfc5282.json
Mapped sentences	16
Declined as scope	3
Relocated to a spec, which Ze OWES	0
Unclassified	0

Sections

Section	Name	Sites	Disposition	Reason
`front`	Status of This Memo, Abstract and Table of Contents	0	skipped (front-matter)	Status of This Memo, Abstract and Table of Contents.
`1`	not stated	0	walked	not stated
`1.1`	not stated	0	walked	not stated
`2`	not stated	0	walked	not stated
`3`	not stated	1	walked	not stated
`3.1`	not stated	2	walked	not stated
`3.2`	not stated	3	walked	not stated
`4`	not stated	2	walked	not stated
`5`	not stated	0	walked	not stated
`5.1`	not stated	2	walked	not stated
`5.2`	not stated	0	walked	not stated
`6`	not stated	0	walked	not stated
`7`	not stated	0	walked	not stated
`7.1`	not stated	2	walked	not stated
`7.2`	not stated	0	walked	not stated
`7.3`	not stated	2	walked	not stated
`8`	not stated	3	walked	not stated
`9`	not stated	0	walked	not stated
`10`	not stated	0	walked	not stated
`10.1`	not stated	0	walked	not stated
`10.1.1`	not stated	0	walked	not stated
`10.1.2`	not stated	0	walked	not stated
`10.1.3`	not stated	0	walked	not stated
`10.1.4`	not stated	0	walked	not stated
`10.2`	not stated	0	walked	not stated
`10.2.1`	not stated	0	walked	not stated
`10.2.2`	not stated	0	walked	not stated
`10.2.3`	not stated	0	walked	not stated
`10.2.4`	not stated	0	walked	not stated
`10.2.5`	not stated	0	walked	not stated
`10.2.6`	not stated	0	walked	not stated
`10.3`	not stated	0	walked	not stated
`11`	not stated	0	walked	not stated
`12`	not stated	1	skipped (iana)	IANA Considerations: the transform identifiers were already assigned for ESP, and the AEAD registry rows are a registry action rather than an implementation obligation.
`13`	Acknowledgments	0	skipped (acknowledgements)	Acknowledgments.
`14`	References	0	skipped (references)	References.
`14.1`	Normative References	0	skipped (references)	Normative References.
`14.2`	Informative References	1	skipped (references)	Informative References.

Excluded sentences

Site	Excluded kind	Reason	Quote
`8:1`	`cross-document` never bound Ze the obligation belongs to another document that this one only cites	The sentence states what RFC 4306 Section 3.3.3 requires, so the obligation it carries belongs to that document; it is quoted here only as the rule the next two sentences update. Sites 8:2 and 8:3 carry the update this document makes, and both are mapped.	IKEv2 (Section 3.3.3 of [RFC4306]) specifies that both an encryption algorithm and an integrity checking algorithm are required for an IKE SA (Security Association).
`12:1`	`not-a-requirement` never bound Ze the sentence states a fact or describes another document, and directs no implementation	An IANA statement that no registry action is needed for the transform identifiers this document reuses. It imposes nothing on an implementation, and the lowercase 'required' the prose scan matched is the report of an absence.	No IANA actions are required for this usage extension.
`14.2:1`	`not-a-requirement` never bound Ze the sentence states a fact or describes another document, and directs no implementation	IPR boilerplate reproduced from the informative reference section. It addresses 'any interested party' about patent disclosure and states no protocol behavior.	The IETF invites any interested party to bring to its attention any copyrights, patents or patent applications, or other proprietary rights that may cover technology that may be required to implement this standard.

Superseded

No document obsoletes RFC 5282, so its obligations are stated where they were written.