RFC PV-PROOF-001 : ProbatioVault ProofEnvelope Protocol¶

Statut : Proposition interne Version : 1.2.0 Date : 2026-03-02 Auteur : ProbatioVault Engineering Verification formelle : TLA+ (TLC), Alloy (SAT), Z Notation, Prolog Revision : 1.2.0 — resolution conflit PENDING/immutabilite, nommage seal unifie, schema canonique, statut agrege, politique de confiance offline, niveaux de preuve formelle

1. Introduction¶

1.1 Objectif¶

Ce document specifie le protocole PV ProofEnvelope, le format standard de preuve composite ProbatioVault. Une ProofEnvelope assemble toutes les evidences cryptographiques et legales necessaires pour prouver, de maniere independante et offline, qu'un acces legal a un document chiffre a ete realise conformement au protocole.

1.2 Portee¶

Ce protocole couvre :

• La structure canonique de la preuve composite (5 sections d'evidence)
• La chaine de preuve a 4 maillons (document hash, Merkle proof, TSA timestamp, blockchain anchor)
• La procedure de verification offline (sans acces ProbatioVault)
• L'immutabilite apres generation
• Le materiel de verification inclus dans la preuve
• L'absence de secrets cryptographiques dans la preuve

1.3 References normatives¶

1.4 Terminologie¶

2. Vue d'ensemble du protocole¶

2.1 Structure de la ProofEnvelope¶

+----------------------------------------------------------------------+
|                        ProofEnvelope v1                              |
|  proofId: UUID                                                       |
|  mandateId: UUID                                                     |
|  version: "1.0.0"                                                    |
|  generatedAt: ISO 8601 UTC                                           |
+----------------------------------------------------------------------+
|                                                                      |
|  +------------------+  +------------------+  +--------------------+  |
|  | 1. Mandate       |  | 2. Dual          |  | 3. ReKey           |  |
|  |    Evidence       |  |    Validation    |  |    Lifecycle       |  |
|  |                  |  |    Evidence       |  |    Evidence        |  |
|  | - eIDAS mandate  |  | - DPO approval   |  | - generation       |  |
|  | - TSP verify     |  | - Legal approval |  | - re-encryptions   |  |
|  | - certificate    |  | - timestamps     |  | - terminal state   |  |
|  +------------------+  +------------------+  | - destruction      |  |
|                                              +--------------------+  |
|  +------------------+  +------------------+                          |
|  | 4. Audit Log     |  | 5. Anchoring     |                          |
|  |    Evidence       |  |    Evidence       |                          |
|  |                  |  |                  |                          |
|  | - signed events  |  | - Merkle leaves  |                          |
|  | - SHA3 hashes    |  | - batch refs     |                          |
|  | - HSM sigs       |  | - tx hashes      |                          |
|  | - TSA token refs |  | - block numbers  |                          |
|  +------------------+  +------------------+                          |
|                                                                      |
|  +--------------------------------------------------------------+   |
|  | Verification Material                                         |   |
|  | - HSM key label (pv-master-signing-*)                        |   |
|  | - Hash algorithm (SHA3-256)                                   |   |
|  | - Signature algorithm (ECDSA_SHA384 / P-384)                 |   |
|  | - Public key (SPKI/DER)                                       |   |
|  +--------------------------------------------------------------+   |
|                                                                      |
|  +--------------------------------------------------------------+   |
|  | 4-Link Chain Verification                                     |   |
|  | [Document Hash] -> [Merkle Proof] -> [TSA Token] -> [Anchor] |   |
|  |      OK/KO            OK/KO           OK/KO         OK/KO   |   |
|  +--------------------------------------------------------------+   |
|                                                                      |
|  +--------------------------------------------------------------+   |
|  | Envelope Seal (PROOF-14)                                      |   |
|  | - canonicalHash: SHA3-256(JCS(envelope))                      |   |
|  | - signature: ECDSA P-384(canonicalHash)                       |   |
|  | - certificateChain: [HSM cert + intermediaires]               |   |
|  +--------------------------------------------------------------+   |
+----------------------------------------------------------------------+

2.2 Flux de generation¶

1. InitiateProof : Creation avec mandateId, sections vides
2. AttachMandateEvidence : Evidence du mandat eIDAS + verification TSP
3. AttachValidationEvidence : Evidence de la double validation (DPO + Legal)
4. AttachReKeyEvidence : Evidence du lifecycle ReKey (precondition : aucun ReKey ACTIVE)
5. AttachAuditEvidence : Events audit signes (SHA3 + HSM + TSA refs)
6. AttachAnchoringEvidence : Merkle leaves + batch refs + blockchain refs
7. FinalizeProof : Verification completude (5 sections non-vides) + immutabilite

2.3 Propriete d'independance¶

EXIGENCE PROOF-09 : La ProofEnvelope DOIT etre verifiable de maniere independante, sans acces a ProbatioVault. Deux niveaux de verification sont definis :

Le maillon 4 (Blockchain Anchor) ne peut pas etre verifie en mode air-gapped strict. La ProofEnvelope inclut les references necessaires (tx hash, block number, batch ID) mais la confirmation requiert l'acces a la blockchain publique. Un verificateur offline strict DOIT traiter le maillon 4 comme INDETERMINATE s'il n'a pas acces a une source blockchain.

Pour les maillons 1 a 3, toutes les donnees necessaires (cle publique, hashes, signatures, algorithmes, certificats) sont incluses dans la preuve.

3. Specifications detaillees¶

3.1 Sections d'evidence¶

EXIGENCE PROOF-01 : Une ProofEnvelope DOIT contenir exactement 5 sections d'evidence. Prouve formellement (TLA+ INV-02 FiveSectionsComplete, Alloy EveryProofHasFiveSections).

EXIGENCE PROOF-03 : Chaque section DOIT etre non-vide pour qu'une preuve soit finalisable. Prouve formellement (TLA+ FinalizeProof precondition).

3.2 Precondition ReKey¶

EXIGENCE PROOF-02 : Au moment de la generation de la preuve, il NE DOIT PAS y avoir de ReKey a l'etat ACTIVE pour le mandat concerne. Tous les ReKeys doivent avoir atteint un etat terminal (REVOKED, EXPIRED, COMPLETED) ou DESTROYED. Prouve formellement (TLA+ INV-03 NoActiveReKeys, Alloy NoActiveReKeysInProof).

3.3 Versioning¶

EXIGENCE PROOF-04 : Chaque ProofEnvelope possede une version. La version est immutable apres generation. Prouve formellement (TLA+ INV-05 VersionPresent).

3.4 Materiel de verification¶

EXIGENCE PROOF-05 : Toute ProofEnvelope finalisee DOIT inclure le materiel de verification :

EXIGENCE PROOF-05b : Pour la verification offline des certificats eIDAS et TSA, la ProofEnvelope DOIT inclure le materiel de validation au moment de la generation :

Strategie de validation a l'instant T : Les reponses OCSP et/ou CRLs sont capturees au moment de la generation de la preuve (validationTimestamp). Elles attestent que les certificats n'etaient pas revoques a cet instant. Un verificateur offline utilise ces preuves de non-revocation embarquees au lieu de contacter les serveurs OCSP/CRL.

Prouve formellement (TLA+ INV-06 VerificationMaterialPresent, Alloy VerificationMaterialComplete).

3.5 Evidence audit¶

EXIGENCE PROOF-06 : Chaque event audit reference dans la preuve DOIT inclure : - Le hash SHA3-256 du contenu canonique (RFC 8785) - La signature HSM ECDSA P-384 - La reference au token TSA (RFC 3161)

Prouve formellement (TLA+ INV-08 AuditEventsHaveSignatures, Alloy AuditEventsHaveCryptoBinding).

3.6 Evidence ancrage¶

EXIGENCE PROOF-07 : L'evidence d'ancrage DOIT inclure, pour chaque event ancre : - La reference au leaf Merkle (leaf hash + leaf index) - La reference au batch d'ancrage (batch ID) - Le hash de la transaction blockchain - Le numero de bloc

Prouve formellement (Alloy AnchoringRefsValid).

3.7 Chaine de preuve (4 maillons)¶

EXIGENCE PROOF-08 : La ProofEnvelope DOIT verifier les 4 maillons de la chaine de preuve. Chaque maillon a un statut explicite :

Prouve formellement (TLA+ INV-04 ChainLinkExplicit, Alloy AllChainLinksExplicit).

3.7.1 Etats de verification et finalisation (PD-280)¶

Les resultats de verification d'un maillon suivent une machine a etats stricte :

EXIGENCE PROOF-15 : FinalizeProof DOIT verifier que les 4 maillons de la chaine sont dans un etat terminal {OK, KO, INDETERMINATE}. Si un maillon est a l'etat PENDING, la finalisation DOIT etre refusee. Cette exigence garantit que le scellement (PROOF-14) porte toujours sur un artefact dont l'etat ne changera plus.

Consequence : l'etat PENDING est un etat pre-finalisation uniquement. L'artefact ProofEnvelope persiste et scelle ne contient jamais PENDING. En API, la valeur null dans linkResults signifie "preuve non encore finalisee" (en cours de construction).

EXIGENCE PROOF-15a : Le pendingResolutionTtl definit le delai maximum avant qu'un maillon PENDING soit reclassifie en INDETERMINATE (defaut 72h, bornes [1h, 30j]). Cette reclassification a lieu en amont de la finalisation — elle est une precondition, pas une modification post-seal.

Regles de transition : - PENDING -> OK | KO | INDETERMINATE : autorise (resolution du maillon, avant finalisation) - PENDING -> INDETERMINATE (SLA) : si pendingResolutionTtl depasse, reclassification automatique - OK | KO | INDETERMINATE -> * : interdit (etats terminaux, monotonie stricte) - FinalizeProof : refuse si un maillon est PENDING (PROOF-15)

3.8 Timestamp¶

EXIGENCE PROOF-10 : Le timestamp de generation (generatedAt) DOIT etre au format ISO 8601 UTC.

3.9 Absence de secrets¶

EXIGENCE PROOF-11 : La ProofEnvelope NE DOIT contenir AUCUN secret cryptographique. Seuls les elements publics sont inclus : cles publiques, hashes, signatures, certificats, references. Prouve formellement (TLA+ INV-09 NoSecretsInProof, Alloy NoSecretsLeaked).

3.10 Immutabilite¶

EXIGENCE PROOF-12 : Une ProofEnvelope persistee est immutable. Aucune modification n'est autorisee apres persistance (enforced par trigger PostgreSQL BEFORE UPDATE OR DELETE). Prouve formellement (TLA+ INV-07 ImmutableAfterFinalize, Alloy ImmutableAfterGeneration).

3.11 Audit trail¶

EXIGENCE PROOF-13 : Chaque generation de preuve DOIT etre tracee dans l'audit trail (PV-AUDIT-001). L'audit log est append-only. Prouve formellement (TLA+ INV-10 AuditAppendOnly).

3.12 Scellement cryptographique de l'enveloppe¶

EXIGENCE PROOF-14 : Toute ProofEnvelope finalisee DOIT etre scellee par une signature HSM portant sur sa serialisation canonique. Ce scellement garantit qu'un tiers peut verifier l'integrite de l'enveloppe exportee sans acces a ProbatioVault.

Procedure de scellement :

1. Serialisation canonique : envelopeCanonical = JCS(proofEnvelope sans envelopeSeal) (RFC 8785). Le champ envelopeSeal dans son integralite est exclu de la canonicalisation. Aucun autre champ n'est exclu.
2. Hash : sealHash = SHA3-256(envelopeCanonical)
3. Signature : sealSignature = ECDSA_P384(sealHash, hsmPrivateKey)
4. Inclusion : Le hash, la signature et la chaine de certificats publique sont ajoutes a l'enveloppe dans le champ envelopeSeal.

Verification par un tiers : Recalculer JCS(envelope sans envelopeSeal), hasher en SHA3-256, verifier la signature avec la cle publique de la chaine de certificats. Prouve formellement (TLA+ INV-11 EnvelopeSealValid, Alloy EnvelopeSealIntegrity, Z INV-11).

3.13 Schema canonique de la ProofEnvelope¶

EXIGENCE PROOF-18 : La ProofEnvelope DOIT respecter le schema JSON suivant. Les champs marques "requis" DOIVENT etre presents dans toute ProofEnvelope finalisee. Les noms de champs sont normatifs et ne DOIVENT PAS varier entre implementations.

Les encodages sont : UUID en string RFC 4122 lowercase, dates en ISO 8601 UTC avec Z suffixe, hashes en hex lowercase, signatures en Base64 standard (RFC 4648 §4), certificats en PEM, cles publiques en SPKI/DER Base64.

3.14 Statut agrege de verification¶

EXIGENCE PROOF-16 : Le statut agrege de la ProofEnvelope est determine par les resultats des 4 maillons :

Le statut agrege est calcule au moment de la finalisation et inclus dans l'artefact scelle. Prouve formellement (INV-14 AggregateStatusConsistent).

3.15 Politique de confiance pour verification offline¶

EXIGENCE PROOF-17 : La ProofEnvelope DOIT inclure les informations necessaires pour qu'un verificateur offline puisse etablir une chaine de confiance complete. Les regles de verification sont :

1. Trust anchors : les certificats racines admis pour la verification des chaines eIDAS et TSA DOIVENT etre documentes dans la politique de confiance de ProbatioVault (document separe, reference par URL ou identifiant dans la ProofEnvelope).
2. Validation temporelle : le validationTimestamp (PROOF-05b) est la reference temporelle pour la verification des certificats. Un certificat est considere valide s'il n'etait pas revoque a cet instant.
3. Resolution OCSP/CRL : si les reponses OCSP et les CRL embarquees divergent sur le statut de revocation d'un certificat, la source la plus recente (par thisUpdate / lastUpdate) prevaut.
4. Expiration des preuves de non-revocation : si les reponses OCSP et les CRL embarquees sont toutes expirees (au regard du validationTimestamp), le resultat de verification du certificat concerne est INDETERMINATE.
5. Absence de materiel : si le materiel de validation (PROOF-05b) est absent ou incomplet, la verification des certificats est INDETERMINATE.

4. Modele formel¶

4.1 Etats et transitions¶

Le protocole est modelise comme un systeme a etats avec 8 actions :

InitiateProof -----> AttachMandateEvidence -----> AttachValidationEvidence
                                                         |
                     AttachReKeyEvidence <----------------+
                            |
                     AttachAuditEvidence
                            |
                     AttachAnchoringEvidence
                            |
                     FinalizeProof -----> VerifyChainLink (x4)

4.2 Invariants de surete¶

Niveaux de preuve :

Note sur TLC : Le model checking utilise une configuration bornee (MAX_PROOFS=2, MAX_SECTIONS=5, MAX_ITERATIONS=12). La verification TLC est bornee : elle explore exhaustivement l'espace d'etats dans ces limites. Des garanties complementaires proviennent des assertions structurelles Alloy (scope 5, solveur SAT) et des schemas Z (invariants universels). Les theoremes TLA+ (THM-01 a THM-10) fournissent des preuves par induction non bornees.

4.3 Theoremes prouves¶

• THM-01 : Spec => []TypeInvariant
• THM-02 : Spec => []FiveSectionsComplete
• THM-03 : Spec => []NoActiveReKeys
• THM-04 : Spec => []ChainLinkExplicit
• THM-05 : Spec => []VerificationMaterialPresent
• THM-06 : Spec => []ImmutableAfterFinalize
• THM-07 : Spec => []NoSecretsInProof
• THM-08 : Spec => []AuditAppendOnly
• THM-09 : Spec => []PendingFreeAtFinalize
• THM-10 : Spec => []AggregateStatusConsistent

4.4 Assertions structurelles (Alloy)¶

5. Considerations de securite¶

5.1 Modele de menace¶

5.2 Limitations connues¶

• La preuve ne contient pas le contenu du document lui-meme, seulement son hash. La verification du maillon 1 (Document Hash) necessite l'acces au document original.
• Le statut INDETERMINATE pour un maillon ne constitue pas une preuve d'integrite. Il indique une incapacite temporaire a verifier (ex: blockchain inaccessible).
• La cle publique incluse dans la preuve doit correspondre a la cle HSM au moment de la signature. Si la cle HSM a ete tournee entre-temps, la verification offline reste possible mais necessite la cle publique historique.

6. Ancrage au code reel¶

6.1 Etat d'implementation¶

7. Annexes¶

7.1 Specifications formelles associees¶

7.2 Matrice de tracabilite¶

7.3 Vecteurs de test¶

7.4 Historique des revisions¶