From 73f32d788d1dc72cac0f635210edd3c9b9e11f59 Mon Sep 17 00:00:00 2001 From: "Jan Winkelmann (keks)" Date: Tue, 3 Feb 2026 09:53:28 +0100 Subject: [PATCH] refactor: allow multiple source documents --- checksets/01-leaf_node.dhall | 41 +++++--- checksets/02-key_package.dhall | 18 ++-- .../03-regular_commit_proposal_list.dhall | 42 ++++++--- .../04-external_commit_proposal_list.dhall | 36 +++++-- checksets/05-add_proposal.dhall | 6 +- checksets/06-update_proposal.dhall | 6 +- checksets/07-remove_proposal.dhall | 6 +- checksets/08-presharedkey_proposal.dhall | 12 ++- checksets/09-reinit_proposal.dhall | 6 +- .../10-groupcontextextensions_proposal.dhall | 6 +- checksets/11-update-path.dhall | 5 +- checksets/12-commit.dhall | 30 ++++-- checksets/13-framing.dhall | 23 +++-- checksets/14-welcome.dhall | 48 +++++++--- checksets/15-external_proposal.dhall | 15 ++- checksets/16-extension_types.dhall | 15 ++- types.dhall | 94 +++++++++++++------ utils/html.dhall | 13 +-- views/bookmarkletPage.dhall | 2 +- 19 files changed, 285 insertions(+), 139 deletions(-) diff --git a/checksets/01-leaf_node.dhall b/checksets/01-leaf_node.dhall index 9ce1948..1f365ce 100644 --- a/checksets/01-leaf_node.dhall +++ b/checksets/01-leaf_node.dhall @@ -14,13 +14,14 @@ let descText = '' -let desc = types.RfcRef/single descText "section-7.3" +let desc = types.DocumentRef/single descText types.Document.MlsRfc "section-7.3" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single "Verify that the credential in the LeafNode is valid, as described in Section 5.3.1." + types.Document.MlsRfc "section-7.3-4.1" ) types.Status.Unknown @@ -30,8 +31,9 @@ let checks = ) , types.Check/new 2 - ( types.RfcRef/single + ( types.DocumentRef/single "Verify that the signature on the LeafNode is valid using signature_key." + types.Document.MlsRfc "section-7.3-4.2" ) types.Status.Complete @@ -39,8 +41,9 @@ let checks = types.Notes/empty , types.Check/new 3 - ( types.RfcRef/single + ( types.DocumentRef/single "Verify that the LeafNode is compatible with the group's parameters. If the GroupContext has a required_capabilities extension, then the required extensions, proposals, and credential types MUST be listed in the LeafNode's capabilities field." + types.Document.MlsRfc "section-7.3-4.3" ) types.Status.Complete @@ -52,7 +55,7 @@ let checks = ) , types.Check/new 4 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that the credential type is supported by all members of the group, as specified by the capabilities field of each member's @@ -60,6 +63,7 @@ let checks = indicates support for all the credential types currently in use by other members. '' + types.Document.MlsRfc "section-7.3-4.4" ) types.Status.Complete @@ -67,13 +71,14 @@ let checks = types.Notes/empty , types.Check/new 5 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the `lifetime` field: If the LeafNode appears in a message being sent by the client, e.g., a Proposal or a Commit, then the client MUST verify that the current time is within the range of the lifetime field. '' + types.Document.MlsRfc [ "section-7.3-4.5.1", "section-7.3-4.5.2.1" ] ) types.Status.Complete @@ -86,7 +91,7 @@ let checks = ) , types.Check/new 6 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the `lifetime` field: If instead the LeafNode appears in a message being received by the client, e.g., a Proposal, a Commit, @@ -96,6 +101,7 @@ let checks = mandatory because the LeafNode might have expired in the time between when the message was sent and when it was received.) '' + types.Document.MlsRfc [ "section-7.3-4.5.1", "section-7.3-4.5.2.2" ] ) types.Status.Complete @@ -103,12 +109,13 @@ let checks = types.Notes/empty , types.Check/new 7 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that the extensions in the LeafNode are supported by checking that the ID for each extension in the extensions field is listed in the capabilities.extensions field of the LeafNode. '' + types.Document.MlsRfc "section-7.3-4.6" ) types.Status.Complete @@ -116,11 +123,12 @@ let checks = types.Notes/empty , types.Check/new 8 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the `leaf_node_source` field: If the LeafNode appears in a KeyPackage, verify that leaf_node_source is set to key_package. '' + types.Document.MlsRfc [ "section-7.3-4.7.1", "section-7.3-4.7.2.1" ] ) types.Status.Complete @@ -128,13 +136,14 @@ let checks = types.Notes/empty , types.Check/new 9 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the `leaf_node_source` field: If the LeafNode appears in an Update proposal, verify that leaf_node_source is set to update and that encryption_key represents a different public key than the encryption_key in the leaf node being replaced by the Update proposal. '' + types.Document.MlsRfc [ "section-7.3-4.7.1", "section-7.3-4.7.2.2" ] ) types.Status.Complete @@ -142,12 +151,13 @@ let checks = types.Notes/empty , types.Check/new 10 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the `leaf_node_source` field: If the LeafNode appears in the leaf_node value of the UpdatePath in a Commit, verify that leaf_node_source is set to commit. '' + types.Document.MlsRfc [ "section-7.3-4.7.1", "section-7.3-4.7.2.3" ] ) types.Status.Complete @@ -155,11 +165,12 @@ let checks = types.Notes/empty , types.Check/new 11 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify that the following fields are unique among the members of the group: `signature_key` '' + types.Document.MlsRfc [ "section-7.3-4.8.1", "section-7.3-4.7.8.1" ] ) types.Status.Complete @@ -167,11 +178,12 @@ let checks = types.Notes/empty , types.Check/new 12 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify that the following fields are unique among the members of the group: `encryption_key` '' + types.Document.MlsRfc [ "section-7.3-4.8.1", "section-7.3-4.7.8.2" ] ) types.Status.Complete @@ -179,10 +191,11 @@ let checks = types.Notes/empty , types.Check/new 13 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify that the credential type used in the LeafNode is included in the credentials field of the capabilities field. '' + types.Document.MlsRfc [ "section-7.2-7" ] ) types.Status.Complete diff --git a/checksets/02-key_package.dhall b/checksets/02-key_package.dhall index 212b383..37ec58c 100644 --- a/checksets/02-key_package.dhall +++ b/checksets/02-key_package.dhall @@ -13,16 +13,18 @@ let descText = '' -let desc = types.RfcRef/new descText [ "section-12.2-1", "section-12.2-2" ] +let desc = + types.DocumentRef/new + descText + types.Document.MlsRfc + [ "section-12.2-1", "section-12.2-2" ] let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' It contains an individual proposal that is invalid as specified invalid Section 12.1. '' + types.Document.MlsRfc "section-12.2-3.1" ) types.Status.Complete @@ -37,8 +42,9 @@ let checks = types.Notes/empty , types.Check/new 2 - ( types.RfcRef/single + ( types.DocumentRef/single "It contains an Update proposal generated by the committer." + types.Document.MlsRfc "section-12.2-3.2" ) types.Status.Complete @@ -46,8 +52,9 @@ let checks = types.Notes/empty , types.Check/new 3 - ( types.RfcRef/single + ( types.DocumentRef/single "It contains a Remove proposal that removes the committer." + types.Document.MlsRfc "section-12.2-3.3" ) types.Status.Complete @@ -55,13 +62,14 @@ let checks = types.Notes/empty , types.Check/new 4 - ( types.RfcRef/single + ( types.DocumentRef/single '' It contains multiple Update and/or Remove proposals that apply to the same leaf. If the committer has received multiple such proposals they SHOULD prefer any Remove received, or the most recent Update if there are no Removes. '' + types.Document.MlsRfc "section-12.2-3.4" ) types.Status.Complete @@ -69,12 +77,13 @@ let checks = types.Notes/empty , types.Check/new 5 - ( types.RfcRef/single + ( types.DocumentRef/single '' It contains multiple Add proposals that contain KeyPackages that represent the same client according to the application (for example, identical signature keys). '' + types.Document.MlsRfc "section-12.2-3.5" ) types.Status.Complete @@ -87,13 +96,14 @@ let checks = ) , types.Check/new 6 - ( types.RfcRef/single + ( types.DocumentRef/single '' It contains an Add proposal with a KeyPackage that represents a client already in the group according to the application, unless there is a Remove proposal in the list removing the matching client from the group. '' + types.Document.MlsRfc "section-12.2-3.6" ) types.Status.Complete @@ -107,11 +117,12 @@ let checks = ) , types.Check/new 7 - ( types.RfcRef/single + ( types.DocumentRef/single '' It contains multiple PreSharedKey proposals that reference then same PreSharedKeyID. '' + types.Document.MlsRfc "section-12.2-3.7" ) types.Status.Complete @@ -119,8 +130,9 @@ let checks = types.Notes/empty , types.Check/new 8 - ( types.RfcRef/single + ( types.DocumentRef/single "It contains multiple GroupContextExtension proposals." + types.Document.MlsRfc "section-12.2-3.8" ) types.Status.Complete @@ -128,13 +140,14 @@ let checks = types.Notes/empty , types.Check/new 9 - ( types.RfcRef/single + ( types.DocumentRef/single '' It contains a ReInit proposal together with any other proposal. If the committer has received other proposals during the epoch, they SHOULD prefer them over the ReInit proposal, allowing the ReInit to be resent and applied in a subsequent epoch. '' + types.Document.MlsRfc "section-12.2-3.9" ) types.Status.Missing @@ -147,8 +160,9 @@ let checks = ) , types.Check/new 10 - ( types.RfcRef/single + ( types.DocumentRef/single "It contains an ExternalInit proposal." + types.Document.MlsRfc "section-12.2-3.10" ) types.Status.Complete @@ -156,13 +170,14 @@ let checks = types.Notes/empty , types.Check/new 11 - ( types.RfcRef/single + ( types.DocumentRef/single '' It contains a Proposal with a non-default proposal type that is not supported by some members of the group that will process the Commit (i.e., members being added or removed by the Commit do not need to support the proposal type). '' + types.Document.MlsRfc "section-12.2-3.11" ) types.Status.Complete @@ -170,12 +185,13 @@ let checks = types.Notes/empty , types.Check/new 12 - ( types.RfcRef/single + ( types.DocumentRef/single '' After processing the Commit the ratchet tree is invalid, in particular, if it contains any leaf node that is invalid according to Section 7.3. '' + types.Document.MlsRfc "section-12.2-3.12" ) types.Status.Missing diff --git a/checksets/04-external_commit_proposal_list.dhall b/checksets/04-external_commit_proposal_list.dhall index d68e3db..d2c7ce4 100644 --- a/checksets/04-external_commit_proposal_list.dhall +++ b/checksets/04-external_commit_proposal_list.dhall @@ -20,18 +20,26 @@ let descText =

'' -let desc = types.RfcRef/new descText [ "section-12.2-1", "section-12.2-5" ] +let desc = + types.DocumentRef/new + descText + types.Document.MlsRfc + [ "section-12.2-1", "section-12.2-5" ] let checks = [ types.Check/new 1 - (types.RfcRef/single "Exactly one ExternalInit" "section-12.2-6.1") + ( types.DocumentRef/single + "Exactly one ExternalInit" + types.Document.MlsRfc + "section-12.2-6.1" + ) types.Status.Complete types.Status.Unknown types.Notes/empty , types.Check/new 2 - ( types.RfcRef/single + ( types.DocumentRef/single '' At most one Remove proposal, with which the joiner removes an old version of themselves. If a Remove proposal is present, then the @@ -41,6 +49,7 @@ let checks = LeafNode MUST present a set of identifiers that is acceptable to the application for the removed participant. '' + types.Document.MlsRfc "section-12.2-6.2" ) types.Status.Complete @@ -54,8 +63,9 @@ let checks = ) , types.Check/new 3 - ( types.RfcRef/single + ( types.DocumentRef/single "Zero or more PreSharedKey proposals" + types.Document.MlsRfc "section-12.2-6.3" ) types.Status.Complete @@ -67,17 +77,22 @@ let checks = ) , types.Check/new 4 - (types.RfcRef/single "No other proposals" "section-12.2-6.4") + ( types.DocumentRef/single + "No other proposals" + types.Document.MlsRfc + "section-12.2-6.4" + ) types.Status.Complete types.Status.Missing types.Notes/empty , types.Check/new 5 - ( types.RfcRef/single + ( types.DocumentRef/single '' External Commits MUST contain a path field (and is therefore a "full" Commit). The joiner is added at the leftmost free leaf node (just as if they were added with an Add proposal), and the path is calculated relative to that leaf node. '' + types.Document.MlsRfc "section-12.4.3.2-11.1" ) types.Status.Complete @@ -85,11 +100,12 @@ let checks = types.Notes/empty , types.Check/new 6 - ( types.RfcRef/single + ( types.DocumentRef/single '' The Commit MUST NOT include any proposals by reference, since an external joiner cannot determine the validity of proposals sent within the group. '' + types.Document.MlsRfc "section-12.4.3.2-11.2" ) types.Status.Complete @@ -97,11 +113,12 @@ let checks = types.Notes/empty , types.Check/new 7 - ( types.RfcRef/single + ( types.DocumentRef/single '' External Commits MUST be signed by the new member. In particular, the signature on the enclosing AuthenticatedContent MUST verify using the public key for the credential in the leaf_node of the path field. '' + types.Document.MlsRfc "section-12.4.3.2-11.3" ) types.Status.Complete @@ -109,10 +126,11 @@ let checks = types.Notes/empty , types.Check/new 8 - ( types.RfcRef/single + ( types.DocumentRef/single '' The sender type for the AuthenticatedContent encapsulating the external Commit MUST be new_member_commit. '' + types.Document.MlsRfc "section-12.4.3.2-11.5" ) types.Status.Complete diff --git a/checksets/05-add_proposal.dhall b/checksets/05-add_proposal.dhall index bab2dcb..4c64143 100644 --- a/checksets/05-add_proposal.dhall +++ b/checksets/05-add_proposal.dhall @@ -12,16 +12,18 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.1.1" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.1.1" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' An Add proposal is invalid if the KeyPackage is invalid according to Section 10.1. '' + types.Document.MlsRfc "section-12.1.1-3" ) types.Status.Complete diff --git a/checksets/06-update_proposal.dhall b/checksets/06-update_proposal.dhall index ac50344..b388798 100644 --- a/checksets/06-update_proposal.dhall +++ b/checksets/06-update_proposal.dhall @@ -13,16 +13,18 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.1.2" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.1.2" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' An Update proposal is invalid if the LeafNode is invalid for an Update proposal according to Section 7.3. '' + types.Document.MlsRfc "section-12.1.2-3" ) types.Status.Complete diff --git a/checksets/07-remove_proposal.dhall b/checksets/07-remove_proposal.dhall index a09bcbc..25ca70f 100644 --- a/checksets/07-remove_proposal.dhall +++ b/checksets/07-remove_proposal.dhall @@ -11,15 +11,17 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.1.3" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.1.3" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' A Remove proposal is invalid if the removed field does not identify a non-blank leaf node. '' + types.Document.MlsRfc "section-12.1.3-3" ) types.Status.Complete diff --git a/checksets/08-presharedkey_proposal.dhall b/checksets/08-presharedkey_proposal.dhall index b20c798..8e08788 100644 --- a/checksets/08-presharedkey_proposal.dhall +++ b/checksets/08-presharedkey_proposal.dhall @@ -15,17 +15,19 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.1.4" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.1.4" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' The PreSharedKey proposal is not being processed as part of a reinitialization of the group (see Section 11.2), and the PreSharedKeyID has psktype set to resumption and usage set to reinit. '' + types.Document.MlsRfc "section-12.1.4-4.1" ) types.Status.Complete @@ -33,12 +35,13 @@ let checks = (types.Notes/single "ReInit is not implemented") , types.Check/new 2 - ( types.RfcRef/single + ( types.DocumentRef/single '' The PreSharedKey proposal is not being processed as part of a subgroup branching operation (see Section 11.3), and the PreSharedKeyID has psktype set to resumption and usage set to branch. '' + types.Document.MlsRfc "section-12.1.4-4.2" ) types.Status.Complete @@ -46,10 +49,11 @@ let checks = (types.Notes/single "Subgroup branching is not implemented") , types.Check/new 3 - ( types.RfcRef/single + ( types.DocumentRef/single '' The psk_nonce is not of length KDF.Nh. '' + types.Document.MlsRfc "section-12.1.4-4.3" ) types.Status.Complete diff --git a/checksets/09-reinit_proposal.dhall b/checksets/09-reinit_proposal.dhall index 27a2c53..fe8400f 100644 --- a/checksets/09-reinit_proposal.dhall +++ b/checksets/09-reinit_proposal.dhall @@ -14,16 +14,18 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.1.5" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.1.5" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' A ReInit proposal is invalid if the version field is less than the version for the current group. '' + types.Document.MlsRfc "section-12.1.5-3" ) types.Status.Missing diff --git a/checksets/10-groupcontextextensions_proposal.dhall b/checksets/10-groupcontextextensions_proposal.dhall index 29f0aab..d25f2c5 100644 --- a/checksets/10-groupcontextextensions_proposal.dhall +++ b/checksets/10-groupcontextextensions_proposal.dhall @@ -11,17 +11,19 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.1.7" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.1.7" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' A GroupContextExtensions proposal is invalid if it includes a required_capabilities extension and some members of the group do not support some of the required capabilities (including those added in the same Commit, and excluding those removed). '' + types.Document.MlsRfc "section-12.1.7-3" ) types.Status.Complete diff --git a/checksets/11-update-path.dhall b/checksets/11-update-path.dhall index 3735866..8c80333 100644 --- a/checksets/11-update-path.dhall +++ b/checksets/11-update-path.dhall @@ -11,18 +11,19 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-7.6" +let desc = types.DocumentRef/single descText types.Document.MlsRfc "section-7.6" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' For each UpdatePathNode, the resolution of the corresponding copath node MUST exclude all new leaf nodes added as part of the current Commit. The length of the encrypted_path_secret vector MUST be equal to the length of the resolution of the copath node (excluding new leaf nodes), with each ciphertext being the encryption to the respective resolution node. '' + types.Document.MlsRfc "section-7.6-3" ) types.Status.Complete diff --git a/checksets/12-commit.dhall b/checksets/12-commit.dhall index ae37a66..59f679b 100644 --- a/checksets/12-commit.dhall +++ b/checksets/12-commit.dhall @@ -9,16 +9,18 @@ let descText =

A member of the group applies a Commit message by taking the following steps:

'' -let desc = types.RfcRef/single descText "section-12.4.2" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.4.2" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that the epoch field of the enclosing FramedContent is equal to the epoch field of the current GroupContext object. '' + types.Document.MlsRfc "section-12.4.2-2.1" ) types.Status.Complete @@ -26,11 +28,12 @@ let checks = types.Notes/empty , types.Check/new 2 - ( types.RfcRef/new + ( types.DocumentRef/new '' Unprotect the Commit using the keys from the current epoch: If the message is encoded as PublicMessage, verify the membership MAC using the membership_key. '' + types.Document.MlsRfc [ "section-12.4.2-2.2.1", "section-12.4.2-2.2.2.1" ] ) types.Status.Complete @@ -38,10 +41,11 @@ let checks = types.Notes/empty , types.Check/new 3 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify the signature on the FramedContent message as described in Section 6.1. '' + types.Document.MlsRfc "section-12.4.2-2.3" ) types.Status.Complete @@ -49,10 +53,11 @@ let checks = types.Notes/empty , types.Check/new 4 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that the proposals vector is valid according to the rules in Section 12.2. '' + types.Document.MlsRfc "section-12.4.2-2.4" ) types.Status.Complete @@ -60,10 +65,11 @@ let checks = types.Notes/empty , types.Check/new 5 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that all PreSharedKey proposals in the proposals vector are available. '' + types.Document.MlsRfc "section-12.4.2-2.5" ) types.Status.Complete @@ -71,12 +77,13 @@ let checks = types.Notes/empty , types.Check/new 6 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that the path value is populated if the proposals vector contains any Update or Remove proposals, or if it's empty. Otherwise, the path value MAY be omitted. '' + types.Document.MlsRfc "section-12.4.2-2.7" ) types.Status.Complete @@ -84,12 +91,13 @@ let checks = types.Notes/empty , types.Check/new 7 - ( types.RfcRef/new + ( types.DocumentRef/new '' If the path value is populated, validate it and apply it to the tree: Validate the LeafNode as specified in Section 7.3. The leaf_node_source field MUST be set to commit. '' + types.Document.MlsRfc [ "section-12.4.2-2.8.1", "section-12.4.2-2.8.2.2" ] ) types.Status.Complete @@ -101,12 +109,13 @@ let checks = ) , types.Check/new 8 - ( types.RfcRef/new + ( types.DocumentRef/new '' If the path value is populated, validate it and apply it to the tree: Verify that the encryption_key value in the LeafNode is different from the committer's current leaf node. '' + types.Document.MlsRfc [ "section-12.4.2-2.8.1", "section-12.4.2-2.8.2.3" ] ) types.Status.Complete @@ -116,12 +125,13 @@ let checks = ) , types.Check/new 9 - ( types.RfcRef/new + ( types.DocumentRef/new '' If the path value is populated, validate it and apply it to the tree: Verify that none of the public keys in the UpdatePath appear in any node of the new ratchet tree. '' + types.Document.MlsRfc [ "section-12.4.2-2.8.1", "section-12.4.2-2.8.2.4" ] ) types.Status.Complete diff --git a/checksets/13-framing.dhall b/checksets/13-framing.dhall index 04474da..1fc90b6 100644 --- a/checksets/13-framing.dhall +++ b/checksets/13-framing.dhall @@ -13,16 +13,17 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-7.6" +let desc = types.DocumentRef/single descText types.Document.MlsRfc "section-7.6" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' Recipients of an MLSMessage MUST verify the signature with the key depending on the sender_type of the sender as described above. '' + types.Document.MlsRfc "section-6.1-6" ) types.Status.Complete @@ -32,11 +33,12 @@ let checks = ) , types.Check/new 2 - ( types.RfcRef/single + ( types.DocumentRef/single '' When decoding a PublicMessage into an AuthenticatedContent, the application MUST check membership_tag and MUST check that the FramedContentAuthData is valid. '' + types.Document.MlsRfc "section-6.2-6" ) types.Status.Complete @@ -44,7 +46,7 @@ let checks = types.Notes/empty , types.Check/new 3 - ( types.RfcRef/single + ( types.DocumentRef/single '' The padding field is set by the sender, by first encoding the content (via the select) and the auth field, and then appending the chosen number of zero bytes. A receiver @@ -56,6 +58,7 @@ let checks = check ensures that the padding process is deterministic, so that, for example, padding cannot be used as a covert channel. '' + types.Document.MlsRfc "section-6.3.1-3" ) types.Status.Complete @@ -63,11 +66,12 @@ let checks = types.Notes/empty , types.Check/new 4 - ( types.RfcRef/single + ( types.DocumentRef/single '' When decoding a PrivateMessageContent, the application MUST check that the FramedContentAuthData is valid. '' + types.Document.MlsRfc "section-6.3.1-10" ) types.Status.Complete @@ -75,11 +79,12 @@ let checks = types.Notes/empty , types.Check/new 5 - ( types.RfcRef/single + ( types.DocumentRef/single '' When constructing a SenderData object from a Sender object, the sender MUST verify Sender.sender_type is member and use Sender.leaf_index for SenderData.leaf_index. '' + types.Document.MlsRfc "section-6.3.2-3" ) types.Status.Complete @@ -87,12 +92,13 @@ let checks = types.Notes/empty , types.Check/new 6 - ( types.RfcRef/single + ( types.DocumentRef/single '' When parsing a SenderData struct as part of message decryption, the recipient MUST verify that the leaf index indicated in the leaf_index field identifies a non-blank node. '' + types.Document.MlsRfc "section-6.3.2-9" ) types.Status.Complete @@ -100,7 +106,7 @@ let checks = types.Notes/empty , types.Check/new 7 - ( types.RfcRef/single + ( types.DocumentRef/single '' On receiving a FramedContent containing a Proposal, a client MUST verify the signature inside FramedContentAuthData and that the epoch field of the enclosing FramedContent @@ -108,6 +114,7 @@ let checks = successful, then the Proposal should be cached in such a way that it can be retrieved by hash (as a ProposalOrRef object) in a later Commit message. '' + types.Document.MlsRfc "section-12.1-3" ) types.Status.Complete diff --git a/checksets/14-welcome.dhall b/checksets/14-welcome.dhall index 12a880b..39501ac 100644 --- a/checksets/14-welcome.dhall +++ b/checksets/14-welcome.dhall @@ -11,17 +11,22 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.4.3.1-7" +let desc = + types.DocumentRef/single + descText + types.Document.MlsRfc + "section-12.4.3.1-7" let checks = [ types.Check/new 1 - ( types.RfcRef/single + ( types.DocumentRef/single '' If a PreSharedKeyID is part of the GroupSecrets and the client is not in possession of the corresponding PSK, return an error. Additionally, if a PreSharedKeyID has type resumption with usage reinit or branch, verify that it is the only such PSK. '' + types.Document.MlsRfc "section-12.4.3.1-10.1" ) types.Status.Missing @@ -29,13 +34,14 @@ let checks = (types.Notes/single "reinit and branch are not implement so far") , types.Check/new 2 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify the signature on the GroupInfo object. The signature input comprises all of the fields in the GroupInfo object except the signature field. The public key is taken from the LeafNode of the ratchet tree with leaf index signer. If the node is blank or if signature verification fails, return an error. '' + types.Document.MlsRfc "section-12.4.3.1-12.1" ) types.Status.Complete @@ -43,11 +49,12 @@ let checks = types.Notes/empty , types.Check/new 3 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that the group_id is unique among the groups that the client is currently participating in. '' + types.Document.MlsRfc "section-12.4.3.1-12.2" ) types.Status.Missing @@ -57,11 +64,12 @@ let checks = ) , types.Check/new 4 - ( types.RfcRef/single + ( types.DocumentRef/single '' Verify that the cipher_suite in the GroupInfo matches the cipher_suite in the KeyPackage. '' + types.Document.MlsRfc "section-12.4.3.1-12.3" ) types.Status.Complete @@ -82,11 +90,12 @@ let checks = ) , types.Check/new 5 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: Verify that the tree hash of the ratchet tree matches the tree_hash field in GroupInfo. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1", "section-12.4.3.1-12.4.2.1" ] ) types.Status.Complete @@ -94,12 +103,13 @@ let checks = types.Notes/empty , types.Check/new 6 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: For each non-empty parent node, verify that it is "parent-hash valid", as described in Section 7.9.2. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1", "section-12.4.3.1-12.4.2.2" ] ) types.Status.Complete @@ -107,11 +117,12 @@ let checks = types.Notes/empty , types.Check/new 7 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: For each non-empty leaf node, validate the LeafNode as described in Section 7.3. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1", "section-12.4.3.1-12.4.2.3" ] ) types.Status.Complete @@ -119,13 +130,14 @@ let checks = types.Notes/empty , types.Check/new 8 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: For each non-empty parent node and each entry in the node's unmerged_leaves field: Verify that the entry represents a non-blank leaf node that is a descendant of the parent node. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1" , "section-12.4.3.1-12.4.2.4.1" , "section-12.4.3.1-12.4.2.4.2.1" @@ -136,13 +148,14 @@ let checks = types.Notes/empty , types.Check/new 9 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: For each non-empty parent node and each entry in the node's unmerged_leaves field: Verify that every non-blank intermediate node between the leaf node and the parent node also has an entry for the leaf node in its unmerged_leaves. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1" , "section-12.4.3.1-12.4.2.4.1" , "section-12.4.3.1-12.4.2.4.2.2" @@ -153,13 +166,14 @@ let checks = types.Notes/empty , types.Check/new 10 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: For each non-empty parent node and each entry in the node's unmerged_leaves field: Verify that the encryption key in the parent node does not appear in any other node of the tree. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1" , "section-12.4.3.1-12.4.2.4.1" , "section-12.4.3.1-12.4.2.4.2.3" @@ -170,12 +184,13 @@ let checks = types.Notes/empty , types.Check/new 11 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: Verify the confirmation tag in the GroupInfo using the derived confirmation key and the confirmed_transcript_hash from the GroupInfo. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1", "section-12.4.3.1-12.9" ] ) types.Status.Complete @@ -183,12 +198,13 @@ let checks = types.Notes/empty , types.Check/new 12 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: If a PreSharedKeyID was used that has type resumption with usage reinit or branch, verify that the epoch field in the GroupInfo is equal to 1. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1", "section-12.4.3.1-12.11.1" ] ) types.Status.Missing @@ -196,7 +212,7 @@ let checks = (types.Notes/single "reinit isn't currently implemented") , types.Check/new 13 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: For usage reinit, verify that the last Commit to the referenced group contains a @@ -205,6 +221,7 @@ let checks = Additionally, verify that all the members of the old group are also members of the new group, according to the application. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1", "section-12.4.3.1-12.11.2.1" ] ) types.Status.Missing @@ -212,13 +229,14 @@ let checks = (types.Notes/single "reinit isn't currently implemented") , types.Check/new 14 - ( types.RfcRef/new + ( types.DocumentRef/new '' Verify the integrity of the ratchet tree: For usage branch, verify that the version and cipher_suite of the new group match those of the old group, and that the members of the new group compose a subset of the members of the old group, according to the application. '' + types.Document.MlsRfc [ "section-12.4.3.1-12.4.1", "section-12.4.3.1-12.11.2.2" ] ) types.Status.Missing diff --git a/checksets/15-external_proposal.dhall b/checksets/15-external_proposal.dhall index 38c3ef6..81b7ab5 100644 --- a/checksets/15-external_proposal.dhall +++ b/checksets/15-external_proposal.dhall @@ -11,15 +11,17 @@ let descText =

'' -let desc = types.RfcRef/single descText "section-12.1.8-1" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-12.1.8-1" let checks = [ types.Check/new 1 - ( types.RfcRef/new + ( types.DocumentRef/new '' sender_type: external: The content_type of the message MUST be proposal. '' + types.Document.MlsRfc [ "section-6.1-4", "section-6.1-5.2" ] ) types.Status.Complete @@ -29,10 +31,11 @@ let checks = ) , types.Check/new 2 - ( types.RfcRef/new + ( types.DocumentRef/new '' sender_type: external: the proposal_type MUST be a value that is allowed for external senders. Only the following types may be sent by an external sender: add, remove, psk, reinit, group_context_extensions. '' + types.Document.MlsRfc [ "section-6.1-4", "section-6.1-5.2", "section-12.1.8-5" ] ) types.Status.Complete @@ -42,10 +45,11 @@ let checks = ) , types.Check/new 3 - ( types.RfcRef/new + ( types.DocumentRef/new '' sender_type: new_member_proposal: The content_type of the message MUST be proposal. '' + types.Document.MlsRfc [ "section-6.1-4", "section-6.1-5.4" ] ) types.Status.Complete @@ -55,10 +59,11 @@ let checks = ) , types.Check/new 4 - ( types.RfcRef/new + ( types.DocumentRef/new '' sender_type: new_member_proposal: The proposal_type of the Proposal MUST be add. '' + types.Document.MlsRfc [ "section-6.1-4", "section-6.1-5.4" ] ) types.Status.Complete diff --git a/checksets/16-extension_types.dhall b/checksets/16-extension_types.dhall index c76069e..3fd620a 100644 --- a/checksets/16-extension_types.dhall +++ b/checksets/16-extension_types.dhall @@ -20,15 +20,17 @@ let descText = '' -let desc = types.RfcRef/single descText "section-17.3" +let desc = + types.DocumentRef/single descText types.Document.MlsRfc "section-17.3" let checks = [ types.Check/new 1 - ( types.RfcRef/new + ( types.DocumentRef/new '' LeafNode: application_id, GREASE '' + types.Document.MlsRfc [ "section-17.3-3.3.1", "section-17.3-4" ] ) types.Status.Unknown @@ -36,10 +38,11 @@ let checks = types.Notes/empty , types.Check/new 2 - ( types.RfcRef/new + ( types.DocumentRef/new '' GroupInfo: ratchet_tree, external_pub, GREASE '' + types.Document.MlsRfc [ "section-17.3-3.3.1", "section-17.3-4" ] ) types.Status.Unknown @@ -47,10 +50,11 @@ let checks = types.Notes/empty , types.Check/new 3 - ( types.RfcRef/new + ( types.DocumentRef/new '' GroupContext: required_capabilities, external_senders '' + types.Document.MlsRfc [ "section-17.3-3.3.1", "section-17.3-4" ] ) types.Status.Unknown @@ -58,10 +62,11 @@ let checks = types.Notes/empty , types.Check/new 4 - ( types.RfcRef/new + ( types.DocumentRef/new '' KeyPackage: GREASE '' + types.Document.MlsRfc [ "section-17.3-3.3.1", "section-17.3-4" ] ) types.Status.Unknown diff --git a/types.dhall b/types.dhall index cbf026a..3214cc6 100644 --- a/types.dhall +++ b/types.dhall @@ -41,44 +41,73 @@ let Url/new : Text -> Url = \(url : Text) -> url -let RfcRef +let Document : Type - = { text : Text, rfcFragments : List Text } + = < MlsRfc | MlsExtensions | Other > -let RfcRef/single - : Text -> Text -> RfcRef +let Document/show + : Document -> Text + = \(doc : Document) -> + merge + { MlsRfc = "RFC 9420" + , MlsExtensions = "MLS Extensions" + , Other = "Other" + } + doc + +let Document/baseUrl + : Document -> Text + = \(doc : Document) -> + merge + { MlsRfc = "https://www.rfc-editor.org/rfc/rfc9420.html" + , MlsExtensions = + "https://datatracker.ietf.org/doc/html/draft-ietf-mls-extensions" + , Other = "https://" + } + doc + +let DocumentRef + : Type + = { text : Text, document : Document, fragments : List Text } + +let DocumentRef/single + : Text -> Document -> Text -> DocumentRef = \(text : Text) -> - \(rfcFragment : Text) -> - let rfcFragments = [ rfcFragment ] in { text, rfcFragments } - -let RfcRef/new - : Text -> List Text -> RfcRef - = \(text : Text) -> \(rfcFragments : List Text) -> { text, rfcFragments } - -let RfcRef/urls - : RfcRef -> List Url - = \(ref : RfcRef) -> - Prelude.List.map - Text - Url - ( \(fragment : Text) -> - "https://www.rfc-editor.org/rfc/rfc9420.html#${fragment}" - ) - ref.rfcFragments + \(doc : Document) -> + \(fragment : Text) -> + { text, document = doc, fragments = [ fragment ] } + +let DocumentRef/new + : Text -> Document -> List Text -> DocumentRef + = \(text : Text) -> + \(doc : Document) -> + \(fragments : List Text) -> + { text, document = doc, fragments } + +let DocumentRef/urls + : DocumentRef -> List Url + = \(ref : DocumentRef) -> + let baseUrl = Document/baseUrl ref.document + + in Prelude.List.map + Text + Url + (\(fragment : Text) -> "${baseUrl}#${fragment}") + ref.fragments let Check : Type = { id : Natural - , desc : RfcRef + , desc : DocumentRef , implStatus : Status , testStatus : Status , notes : Notes } let Check/new - : Natural -> RfcRef -> Status -> Status -> Notes -> Check + : Natural -> DocumentRef -> Status -> Status -> Notes -> Check = \(id : Natural) -> - \(desc : RfcRef) -> + \(desc : DocumentRef) -> \(implStatus : Status) -> \(testStatus : Status) -> \(notes : Notes) -> @@ -86,13 +115,13 @@ let Check/new let CheckSet : Type - = { id : Natural, name : Text, desc : RfcRef, checks : List Check } + = { id : Natural, name : Text, desc : DocumentRef, checks : List Check } let CheckSet/new - : Natural -> Text -> RfcRef -> List Check -> CheckSet + : Natural -> Text -> DocumentRef -> List Check -> CheckSet = \(id : Natural) -> \(name : Text) -> - \(desc : RfcRef) -> + \(desc : DocumentRef) -> \(checks : List Check) -> let checks = Prelude.List.map @@ -138,10 +167,13 @@ in { Notes , Notes/empty , Url , Url/new - , RfcRef - , RfcRef/single - , RfcRef/new - , RfcRef/urls + , Document + , Document/show + , Document/baseUrl + , DocumentRef + , DocumentRef/single + , DocumentRef/new + , DocumentRef/urls , Check , Check/new , CheckSet diff --git a/utils/html.dhall b/utils/html.dhall index 31904fd..4e7e060 100644 --- a/utils/html.dhall +++ b/utils/html.dhall @@ -82,16 +82,16 @@ let XML/p , content = [ XML.text text ] } -let RfcRef/links - : Types.RfcRef -> XML.Type - = \(ref : Types.RfcRef) -> +let DocumentRef/links + : Types.DocumentRef -> XML.Type + = \(ref : Types.DocumentRef) -> XML/asUl "rfcref-links" ( Prelude.List.map Types.Url XML.Type (Url/link "ref") - (Types.RfcRef/urls ref) + (Types.DocumentRef/urls ref) ) let Check/tableRow @@ -132,7 +132,8 @@ let Check/tableRow XML.element { name = "td" , attributes = XML.emptyAttributes - , content = [ XML/p check.desc.text, RfcRef/links check.desc ] + , content = + [ XML/p check.desc.text, DocumentRef/links check.desc ] } let notesUl = @@ -233,7 +234,7 @@ let CheckSet/table , attributes = [ XML.attribute "class" "check-set-desc" ] , content = [ XML.rawText checkSet.desc.text - , RfcRef/links checkSet.desc + , DocumentRef/links checkSet.desc ] } , XML.element diff --git a/views/bookmarkletPage.dhall b/views/bookmarkletPage.dhall index 5a409b6..e00a5fc 100644 --- a/views/bookmarkletPage.dhall +++ b/views/bookmarkletPage.dhall @@ -12,7 +12,7 @@ let checksets = ../checksets.dhall let XML = Prelude.XML -let Check/fragments = \(check : Types.Check) -> check.desc.rfcFragments +let Check/fragments = \(check : Types.Check) -> check.desc.fragments let CheckSet/fragments = \(checkSet : Types.CheckSet) ->