RFC PV-PRE-001 : ProbatioVault Proxy Re-Encryption Protocol (Umbral)¶

Statut : Proposition interne Version : 1.3.0 Date : 2026-03-02 Auteur : ProbatioVault Engineering Verification formelle : TLA+ (TLC), Alloy (SAT), Z Notation, Prolog Changelog : v1.3 — PRE-16b binding crypto complet (algorithme + JCS + signature HSM), PRE-16c fail-closed binding, PRE-11 TTL en secondes reelles, PRE-19 wire format exact, PRE-20 stockage/transport KFrags, note ecarts spec/code

1. Introduction¶

1.1 Objectif¶

Ce document specifie le protocole PV PRE (Proxy Re-Encryption), base sur le schema Umbral (NuCypher), pour l'acces legal judiciaire aux documents chiffres dans ProbatioVault.

Le proxy peut re-chiffrer un ciphertext de la cle du proprietaire vers la cle du requerant legal, sans jamais pouvoir dechiffrer le contenu. Cette propriete zero-knowledge est un garde architectural : le modele ne contient aucune operation decrypt, et le code Prolog verifie l'absence de methode decrypt dans l'implementation. Au niveau cryptographique, les garanties de securite du schema Umbral (cf. NuCypher, "Umbral: A Threshold Proxy Re-Encryption Scheme") assurent l'impossibilite de dechiffrement par le proxy.

1.2 Portee¶

Ce protocole couvre :

• La generation de cles de re-chiffrement (ReKey) avec seuil (t, n)
• La double validation (DPO + legal) obligatoire avant re-chiffrement
• Le cycle de vie complet des ReKeys (ACTIVE -> terminal -> DESTROYED)
• La production de fragments cryptographiques (KFrag, CFrag, Capsule)
• Le binding cryptographique mandate-contexte
• La PKI (chaque cle publique liee a un certificat)
• L'anti-rejeu par nonce unique sur chaque re-encryption
• La destruction explicite (KFrags memoire + DB + cache)
• L'audit exhaustif de chaque operation

1.3 References normatives¶

Note sur secp256k1 : Cette courbe est choisie pour la compatibilite avec l'ancrage blockchain Ethereum de ProbatioVault. Pour des usages purement PRE sans contrainte blockchain, Curve25519 offrirait de meilleures performances. Le choix de secp256k1 est un compromis interoperabilite/performance documente.

Note terminologique : Le seuil (t, n) utilise dans Umbral est un secret sharing polynomial (variante de Feldman/Pedersen VSS), pas le schema de Shamir classique. Shamir reconstruit un secret unique ; Umbral distribue une capacite de re-chiffrement sans jamais reconstituer la cle privee du proprietaire. La distinction est importante : dans Umbral, meme avec t KFrags, le proxy ne peut PAS dechiffrer — il ne fait que transformer le ciphertext.

1.4 Terminologie¶

2. Vue d'ensemble du protocole¶

2.1 Acteurs¶

+----------------+          +----------------+          +------------------+
|  Proprietaire  |          |     Proxy      |          |   Requerant      |
|  (Owner)       |          |  (ProbatioVault|          |   Legal          |
|                |          |   zero-knowledge)         |   (Magistrat,    |
|  pk_owner      |          |                |          |   OPJ, DPO)      |
|  sk_owner      |          |  NO sk_owner   |          |   pk_recipient   |
|  cert_owner    |          |  NO sk_recipient          |   sk_recipient   |
+-------+--------+          +-------+--------+          +--------+---------+
        |                           |                            |
        |  1. GenerateReKey(t,n)    |                            |
        |  [PKI: cert_owner valide] |                            |
        |-------------------------->|                            |
        |     [n KFrags]            |                            |
        |                           |                            |
        |                           |  2. DualValidate           |
        |                           |     (DPO + Legal)          |
        |                           |<---------------------------|
        |                           |     [Mandat bound au ctx]  |
        |                           |     [cert_recipient valide]|
        |                           |                            |
        |                           |  3. ReEncrypt(KFrag_i,     |
        |                           |              nonce_i)      |
        |                           |  (repete t fois,           |
        |                           |   nonce unique/operation)  |
        |                           |------------------------->  |
        |                           |     [CFrag_1..CFrag_t]     |
        |                           |                            |
        |                           |            4. Reconstruct  |
        |                           |            (sk_recipient)  |
        |                           |            Dechiffre le    |
        |                           |            document        |

2.2 Propriete zero-knowledge¶

EXIGENCE PRE-01 : Le proxy NE DOIT JAMAIS pouvoir dechiffrer le contenu.

Cette propriete est garantie a deux niveaux :

1. Garde architectural : Aucune operation decrypt n'existe dans le modele formel (TLA+, Alloy, Z, Prolog). C'est une garantie structurelle par absence de construction.
2. Garantie cryptographique : Les garanties de securite du schema Umbral (NuCypher, "Umbral: A Threshold Proxy Re-Encryption Scheme") assurent que le proxy, meme avec tous les KFrags, ne peut pas reconstruire la cle privee du proprietaire ni dechiffrer le contenu. Seul le destinataire (sk_recipient) peut dechiffrer apres reconstruction des CFrags.

Prouve par : Alloy NoDecryptInModel, Prolog check_pre_no_decrypt.

2.3 Cycle de vie d'un ReKey¶

                    GenerateReKey
                    [PKI + Mandate binding]
                         |
                         v
                    +---------+
                    |  ACTIVE  |
                    +----+----+
                         |
            +------------+------------+
            |            |            |
            v            v            v
      +---------+  +---------+  +-----------+
      | REVOKED |  | EXPIRED |  | COMPLETED |
      +---------+  +---------+  +-----------+
            |            |            |
            +------------+------------+
                         |
                         v
                   +------------+
                   |  DESTROYED |
                   | (zeroize   |
                   |  KFrags +  |
                   |  DB + cache)|
                   +------------+

EXIGENCE PRE-02 : Les etats terminaux (REVOKED, EXPIRED, COMPLETED) sont IRREVERSIBLES. Un ReKey terminal ne peut pas revenir a ACTIVE. Prouve formellement (TLA+ TerminalIsFinal, Alloy AllTerminalAreFinal).

EXIGENCE PRE-03 : Un ReKey DESTROYED ne peut plus etre utilise pour aucune operation. L'etat DESTROYED est final et absorbant.

3. Specifications detaillees¶

3.1 Generation de ReKey¶

Procedure :

1. Le proprietaire genere un ReKey avec les parametres (t, n, context, TTL)
2. PKI : Les cles publiques pk_owner et pk_recipient sont validees via certificats eIDAS
3. Mandate binding : Le mandat judiciaire est lie cryptographiquement au contexte du ReKey (mandate.scope = rekey.context, mandate.boundReKey = rekey.id)
4. Le ReKey est initialise a l'etat ACTIVE avec kfragsZeroized = false
5. n KFrags sont generes par le schema polynomial Umbral
6. L'ensemble des nonces utilises est initialise a vide

EXIGENCE PRE-04 : Le seuil DOIT respecter 1 <= t <= n <= 10. Prouve formellement (TLA+ ThresholdValid, Alloy ThresholdValid).

EXIGENCE PRE-05 : Le proprietaire et le requerant DOIVENT etre des entites DIFFERENTES (owner != recipient). Prouve formellement (Alloy RequesterNotOwner).

EXIGENCE PRE-06 : Les cles publiques utilisent secp256k1 en format compresse (33 bytes). Chaque cle DOIT etre liee a un certificat eIDAS valide (INV-11 PKIAuthenticity). Le provider Umbral DOIT supporter secp256k1. Prouve formellement (Alloy AuthenticatedKeys, PKIAlwaysPresent).

3.2 Double validation¶

EXIGENCE PRE-07 : Aucun re-chiffrement n'est autorise sans double validation prealable. Cette regle est prouvee formellement (TLA+ DualValidationRequired, Alloy DualValidationRequired).

La double validation requiert :

Procedure :

1. Le requerant soumet un mandat (Mandate) avec un certificat (Certificate)
2. Le mandat DOIT couvrir le meme contexte que le ReKey (binding verifie)
3. Le DPO approuve ou rejette
4. L'autorite legale approuve ou rejette
5. La DualValidation passe a approved = TRUE seulement si BOTH approuvent
6. Le re-chiffrement est alors debloque

3.3 Re-chiffrement¶

Preconditions :

• ReKey a l'etat ACTIVE
• Double validation approuvee (dual_validated[id] = TRUE)
• TTL > 0 (non expire)
• Nombre de CFrags < n (borne du seuil)
• Nonce unique : chaque operation fournit un nonce qui n'a pas encore ete utilise pour ce ReKey

EXIGENCE PRE-08 : Le nombre de CFrags produits NE DOIT PAS depasser n (le parametre du seuil). Prouve formellement (TLA+ CFragBound, Alloy CFragBound).

EXIGENCE PRE-18 : Chaque KFrag NE DOIT produire au plus qu'un CFrag pour une capsule donnee. Cette propriete est une consequence de PRE-08 (CFrags <= n) combinees aux n KFrags generes et au nonce anti-rejeu (PRE-15). L'implementation DOIT garantir qu'un KFrag consomme n'est pas reutilisable.

EXIGENCE PRE-15 : Chaque operation de re-encryption DOIT fournir un nonce unique. Le proxy DOIT rejeter tout nonce deja utilise pour le meme ReKey. Le nombre de nonces utilises DOIT etre egal au nombre de CFrags produits. Prouve formellement (TLA+ NoReplay, Alloy NonceAntiReplay).

EXIGENCE PRE-15a : Le nonce DOIT etre >= 96 bits (12 bytes) d'aleatoire genere par un CSPRNG. Les nonces bases sur un timestamp ou un compteur simple sont INTERDITS.

EXIGENCE PRE-15b : L'unicite du nonce est exigee au moins par ReKey. Le systeme DOIT rester sur en cas de retry reseau : une re-soumission avec le meme nonce DOIT etre rejetee de maniere idempotente (pas de double CFrag, pas d'erreur fatale).

Procedure :

1. Le proxy recoit un KFrag, le ciphertext original (Capsule), et un nonce unique
2. Le proxy verifie que le nonce n'est pas dans l'ensemble des nonces deja utilises
3. Le proxy produit un CFrag via l'operation Umbral
4. Le CFrag est enregistre avec le contexte du ReKey
5. Le nonce est ajoute a l'ensemble des nonces utilises
6. L'operation est tracee dans l'audit log

3.4 Coherence de contexte¶

EXIGENCE PRE-09 : Tous les artefacts d'un meme flux de re-chiffrement (KFrags, CFrags) DOIVENT partager le meme ContextId que le ReKey. Prouve formellement (Alloy ContextCoherence).

3.5 Binding mandate-contexte¶

EXIGENCE PRE-16 : Le mandat judiciaire DOIT etre lie cryptographiquement au contexte du ReKey. Cette liaison empeche la reutilisation d'un mandat pour un autre ReKey. Prouve formellement (Alloy MandateContextBinding, MandateAlwaysBound).

EXIGENCE PRE-16a : Le binding mandat-contexte DOIT etre verifiable independamment de la base de donnees : toute modification de mandate, contextId ou rekey.id DOIT etre detectable sans interroger l'etat serveur. Prouve formellement (Alloy MandateBindingVerifiable).

EXIGENCE PRE-16b : Le binding est calcule comme suit :

1. Construire l'objet binding :

   {
     "mandateHash": "<SHA3-256 du mandat canonique (JCS), hex 64 chars>",
     "pkOwner": "<cle publique owner, SEC1 compresse hex 66 chars (33 bytes)>",
     "pkRecipient": "<cle publique recipient, SEC1 compresse hex 66 chars (33 bytes)>",
     "scope": "<contextId UUID>",
     "rekeyId": "<rekey UUID>",
     "validationTimestamp": "<ISO 8601 UTC>"
   }
   

2. Canonicaliser via JCS (RFC 8785)
3. bindingHash = SHA3-256(JCS(bindingObject))
4. bindingSignature = ECDSA_P384(bindingHash, hsmPrivateKey)

Le binding est stocke avec le ReKey. La verification par un tiers recalcule bindingHash a partir des champs en clair et verifie bindingSignature avec la cle publique HSM.

EXIGENCE PRE-16c : Toute modification d'un champ couvert par le binding (mandateHash, pkOwner, pkRecipient, scope, rekeyId, validationTimestamp) invalide le binding. La verification DOIT echouer (fail-closed) si le bindingHash recalcule ne correspond pas au bindingHash stocke. La verification DOIT egalement echouer si la signature bindingSignature est invalide ou si la cle publique HSM n'est pas dans le trust-store.

3.6 Reconstruction¶

Le requerant collecte t CFrags et reconstruit la cle symetrique du document avec sa cle privee (sk_recipient). Cette operation se fait EXCLUSIVEMENT cote requerant — le proxy n'y participe pas.

3.7 Revocation¶

EXIGENCE PRE-10 : La revocation est immediate et irreversible. Un ReKey revoque ne peut plus produire de CFrags.

Declencheurs de revocation :

• Ordre du DPO (violation RGPD detectee)
• Demande du proprietaire
• Invalidation du mandat judiciaire
• Detection d'anomalie par le systeme de monitoring

3.8 Expiration (TTL)¶

EXIGENCE PRE-11 : Chaque ReKey a un TTL exprime en secondes de temps reel, borne par REKEY_MAX_TTL (defaut : 259200 secondes = 72 heures, bornes [3600, 2592000] = [1h, 30j]). Le TTL est fixe a la creation par le demandeur et clamp dans les bornes. L'expiration est evaluee par comparaison now() >= created_at + ttl_seconds. Quand le TTL est ecoule, le ReKey passe automatiquement a EXPIRED. L'horloge logique du modele formel (Tick) est une abstraction du temps reel ; chaque Tick correspond a un quantum de temps configurable. Prouve formellement (TLA+ TTLBound).

3.9 Destruction cryptographique¶

EXIGENCE PRE-12 : Un ReKey dans un etat terminal (REVOKED, EXPIRED, COMPLETED) DOIT etre DESTROYED. La destruction couvre explicitement :

Prouve formellement : TLA+ DestroyedImpliesZeroized, Alloy DestructionZeroizes.

EXIGENCE PRE-13 : Chaque ReKey DOIT etre associe a un contexte. Prouve formellement (TLA+ ContextPresent).

3.10 Audit trail¶

EXIGENCE PRE-14 : Chaque operation DOIT etre tracee dans un audit trail append-only. L'audit NE DOIT contenir AUCUN secret cryptographique (cles, KFrags, CFrags). Prouve structurellement (Alloy NoSecretsInAudit : AuditEntry ne contient que operation + contextId). Prouve en TLA+ par AuditAppendOnly.

EXIGENCE PRE-14a : L'audit DOIT etre stocke sur un support offrant des proprietes d'immutabilite ou de verifiabilite a posteriori (ex: stockage WORM, chainage de hash, ancrage blockchain). L'append-only logique seul (contrainte applicative) ne suffit pas face a un attaquant DB.

3.11 PKI et authenticite des cles¶

EXIGENCE PRE-17 : Chaque cle publique utilisee dans le protocole (owner et recipient) DOIT etre liee a un certificat eIDAS valide. Cette PKI previent les attaques par substitution de cle (rogue key attack). Prouve formellement (Alloy AuthenticatedKeys, Z INV-11 PKIAuthenticity).

3.12 Format de serialisation des artefacts PRE¶

EXIGENCE PRE-19 : Les artefacts PRE sont serialises selon les formats suivants :

Toute entree dont la taille depasse la borne ou dont la deserialisation echoue DOIT etre rejetee (fail-closed). Les tailles indicatives sont basees sur l'implementation NuCypher reference (secp256k1) ; les bornes max (256 bytes) sont les contraintes validees par les modeles formels.

Note sur secp256k1 : La courbe secp256k1 utilise des points de 33 bytes en representation compressee (SEC1). Les KFrags, CFrags et Capsules encapsulent des points de courbe + preuves dont la taille varie selon l'implementation du provider Umbral. Le format de serialisation exact depend du provider utilise ; l'exigence normative porte sur les bornes de taille et la validation de deserialisation.

3.13 Stockage et transport des KFrags¶

EXIGENCE PRE-20 : Les KFrags DOIVENT etre stockes chiffres au repos (AES-256-GCM avec cle derivee de l'envelope HSM). Le transport des KFrags entre composants DOIT utiliser TLS 1.3 minimum. Les KFrags NE DOIVENT JAMAIS transiter en clair sur le reseau ni etre stockes en clair sur disque.

EXIGENCE PRE-20a : La cle de chiffrement des KFrags au repos DOIT etre derivee via HKDF-SHA256 a partir de la cle HSM du service, avec le rekeyId comme salt et "pv-kfrag-storage-v1" comme info. La rotation de la cle HSM entraine le re-chiffrement de tous les KFrags stockes.

4. Modele formel¶

4.1 Etats et transitions¶

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

GenerateReKey ----> DualValidate ----> ReEncrypt(nonce) ----> CompleteReKey
                                                                    |
                                       RevokeReKey <----------------+
                                                                    |
                                       ExpireReKey <--- Tick
                                                                    |
                                       DestroyReKey <---------------+
                                       (zeroize KFrags)

Note sur la verification bornee : Le model checking TLC explore exhaustivement l'espace d'etats pour les bornes specifiees dans PV_PRE.cfg (MAX_REKEYS=2, MAX_THRESHOLD=2, REKEY_MAX_TTL=2, MAX_ITERATIONS=12). Cela couvre toutes les combinaisons possibles dans ces bornes. Pour des bornes plus grandes, les theoremes TLA+ fournissent des preuves par induction (non bornees). Alloy fournit des preuves structurelles complementaires (scope 5).

4.2 Invariants de surete¶

Les proprietes suivantes sont verifiees par model checking :

4.3 Theoremes prouves¶

Les theoremes suivants sont demontres en logique temporelle (TLA+) :

• THM-01 : Spec => []TypeInvariant
• THM-02 : Spec => []TerminalIsFinal
• THM-03 : Spec => []ThresholdValid
• THM-04 : Spec => []DualValidationRequired
• THM-05 : Spec => []CFragBound
• THM-06 : Spec => []NoReplay
• THM-07 : Spec => []DestroyedImpliesZeroized
• THM-08 : Spec => []AuditAppendOnly

4.4 Assertions structurelles (Alloy)¶

Les assertions suivantes sont prouvees par le solveur SAT (UNSAT = pas de contre-exemple) :

4.5 Propriete zero-knowledge (garde architectural)¶

La propriete zero-knowledge du proxy est garantie a deux niveaux :

Niveau architectural (garde formel) :

1. Le modele Alloy ne contient aucune signature Decrypt
2. Le modele TLA+ ne contient aucune action Decrypt
3. La spec Z ne definit aucun schema Decrypt
4. Les regles Prolog verifient l'absence de methode decrypt dans le code (check_no_decrypt)

Niveau cryptographique (garantie Umbral) :

Les garanties de securite du schema Umbral (NuCypher, "Umbral: A Threshold Proxy Re-Encryption Scheme") assurent que le proxy, meme en possession de tous les KFrags, ne peut pas :

• Reconstruire la cle privee du proprietaire (sk_owner)
• Dechiffrer le ciphertext original
• Produire un plaintext a partir des CFrags seuls

Seul le destinataire (sk_recipient) peut dechiffrer apres reconstruction des t CFrags.

5. Considerations de securite¶

5.1 Modele de menace¶

5.2 Conformite RGPD¶

Le protocole est concu pour la conformite RGPD :

• Art. 17 (Droit a l'effacement) : La destruction cryptographique (DESTROYED) couvre KFrags memoire, entrees DB, et cache applicatif
• Art. 25 (Protection par defaut) : Zero-knowledge par construction (garde + Umbral)
• Art. 35 (DPIA) : L'audit trail append-only exhaustif permet la verification a posteriori
• Art. 32 (Securite) : Seuil (t, n) empeche un acteur unique d'acceder aux donnees ; PKI previent la substitution de cle

5.3 Limitations connues¶

• La destruction cryptographique (DESTROYED) detruit les artefacts PRE (KFrags, metadonnees) mais pas le ciphertext original. Le proprietaire conserve l'acces a ses propres donnees.
• Le seuil (t, n) est fixe a la creation du ReKey. Il ne peut pas etre modifie apres coup.
• Le choix de secp256k1 est motive par l'interoperabilite blockchain ; pour des usages sans blockchain, Curve25519 serait preferable.

6. Ancrage au code reel¶

Les specifications formelles sont ancrees aux artefacts reels du code ProbatioVault via extract-facts.py. Cet ancrage garantit que les modeles ne divergent pas de l'implementation.

6.1 Etat d'implementation¶

Note implementation : Les composants marques "Non implemente" representent des ecarts spec/code bloquants. Le protocole n'est pas considere comme verrouille operationnellement tant que ces composants ne sont pas implementes et que les checks Prolog ne passent pas a PASS.

7. Annexes¶

7.1 Specifications formelles associees¶

7.2 Matrice de tracabilite¶

7.3 Vecteurs de test¶

7.4 Historique des revisions¶