RFC PV-ENV-001 : ProbatioVault Envelope Protocol¶

Statut : Proposition interne Version : 1.4.0 Date : 2026-03-02 Auteur : ProbatioVault Engineering Verification formelle : TLA+ (TLC), Alloy (SAT), Z Notation, Prolog Changelog : v1.4 — ENV-26/27 encodages binaires HKDF (RFC 5869 + SHA-256), ENV-17 metadata_tag HMAC-SHA256 exact, ENV-28 profil Argon2id versionne, ENV-29 BIP-39 wordlist anglaise figee, ENV-14 generation K_master CSPRNG 256 bits, ENV-30 documentation zeroization runtime

1. Introduction¶

1.1 Objectif¶

Ce document specifie le protocole PV Envelope, un systeme de gestion de cles hierarchique zero-knowledge pour le chiffrement cote client des documents et metadonnees stockes dans ProbatioVault.

Le serveur ne possede jamais les cles en clair. L'utilisateur controle l'integralite de la hierarchie de cles a partir de son mot de passe.

1.2 Portee¶

Ce protocole couvre :

• La derivation de la cle maitre (K_master) a partir du mot de passe utilisateur
• L'enveloppement (wrapping) de K_master dans des enveloppes chiffrees
• La derivation de cles applicatives (partage, document, recherche chiffree)
• La gestion multi-device et la revocation
• La rotation des enveloppes avec metadata binding et audit trail
• Le nettoyage memoire (zeroization) adapte au runtime
• La recovery via BIP-39 mnemonic

1.3 References normatives¶

1.4 Terminologie¶

2. Vue d'ensemble du protocole¶

2.1 Hierarchie de cles¶

Password (utilisateur)
    |
    | Argon2id (RFC 9106)
    |   type=2, memory>=64 MiB, passes>=3
    |   salt>=16 bytes (CSPRNG), output=32 bytes
    v
K_enc (256 bits, ephemere)
    |
    | AES-KW (RFC 3394)
    |   wrapping: 32 bytes -> 40 bytes (32 + 8 IV)
    v
+-------------------+-------------------+-------------------+
|  MASTER envelope  |  DEVICE envelope  | RECOVERY envelope |
|  (password-based) |  (device-bound)   | (BIP-39 24 mots)  |
+-------------------+-------------------+-------------------+
    |                       |                       |
    +-----------+-----------+-----------+-----------+
                |
                v
          K_master (256 bits, persistant)
                |
                | HKDF (RFC 5869)
                |
    +-----------+-----------+-----------+
    |           |           |           |
    v           v           v           |
 K_share    K_doc_i    K_search        |
 (256 bits) (256 bits) (256 bits)      |
 salt=user  salt=docId salt=user       |
    |           |           |           |
    v           v           v           |
 Chiffrement Chiffrement Recherche     |
 utilisateur par document chiffree     |

2.2 Flux de donnees¶

1. Inscription : Password -> Argon2id -> K_enc -> AES-KW(K_enc, K_master) -> MASTER envelope + metadata_tag
2. Connexion : Password -> Argon2id -> K_enc -> AES-KW-unwrap(MASTER envelope) -> K_master
3. Multi-device : K_device -> AES-KW(K_device, K_master) -> DEVICE envelope
4. Derivation K_share/K_search : HKDF(K_master, salt=user_salt, info=ctx) -> K_share | K_search
5. Derivation K_doc : HKDF(K_master, salt=documentId, info="pv-doc-v1") -> K_doc_i (une cle par document)
6. Recovery : BIP-39(24 mots) -> PBKDF2 -> K_recovery -> AES-KW(K_recovery, K_master) -> RECOVERY envelope
7. Rotation : unwrap(ancien) -> K_master -> wrap(nouveau K_enc) -> nouveau envelope + metadata_tag + audit event

3. Specifications detaillees¶

3.1 Derivation du mot de passe (Argon2id)¶

La derivation du mot de passe vers K_enc utilise Argon2id (RFC 9106 type 2) :

Note : Le RFC 9106 §4 impose passes >= 1 comme minimum. ProbatioVault durci a passes >= 3 pour un profil plus resistant. Les deux valeurs (minimum RFC et profil ProbatioVault) sont distinguees dans les modeles formels.

EXIGENCE ENV-01 : Le parametre type DOIT etre 2 (Argon2id). Les variantes Argon2d (type 0) et Argon2i (type 1) sont INTERDITES.

EXIGENCE ENV-02 : Le sel DOIT etre genere par un CSPRNG (ex: crypto.getRandomValues()). Le sel DOIT etre stocke en clair a cote de l'envelope.

EXIGENCE ENV-03 : Les parametres Argon2 DOIVENT etre stockes dans l'envelope pour permettre la re-derivation. Un changement de parametres implique une rotation d'envelope.

EXIGENCE ENV-28 : Le profil Argon2id est versionne. Le profil actuel est "PV-ARGON2-P1" : - type=2, memory=65536 KiB, passes=3, parallelism=1, hashLength=32, salt>=16 bytes

L'identifiant de profil est stocke dans l'envelope (champ argon2Profile). Un changement de profil implique une rotation d'envelope. L'implementation DOIT accepter les envelopes generees avec un profil anterieur (retrocompatibilite en lecture). Les nouveaux wraps DOIVENT utiliser le profil courant.

3.2 Enveloppement AES-KW (RFC 3394)¶

L'enveloppement de K_master utilise AES Key Wrap :

EXIGENCE ENV-04 : Le ciphertext enveloppe DOIT avoir une taille de 40 bytes. Toute taille differente indique une erreur d'implementation.

EXIGENCE ENV-05 : L'operation unwrap(wrap(K_master)) DOIT retourner K_master identique (propriete roundtrip). Cet invariant est verifie formellement (INV-03).

EXIGENCE ENV-06 : Apres unwrap, K_enc DOIT etre immediatement zeroize de la memoire (voir section 3.9 pour les mecanismes par runtime).

3.3 Derivation HKDF (RFC 5869)¶

La derivation de cles applicatives utilise HKDF en mode extract-then-expand :

EXIGENCE ENV-07 : Deux contextes DIFFERENTS avec le meme salt DOIVENT produire des cles DIFFERENTES (isolation par contexte). Prouve formellement (TLA+ INV-06, Alloy ContextSeparation, Z INV-06).

EXIGENCE ENV-07b : Pour K_doc, deux documentIds DIFFERENTS avec le meme contexte DOIVENT produire des cles DIFFERENTES (isolation par salt). Prouve formellement (TLA+ INV-09 DocKeyIsolation, Alloy SaltSeparation, Z INV-11).

EXIGENCE ENV-08 : Le meme triplet (K_master, contexte, salt) DOIT toujours produire la meme cle derivee (determinisme). Prouve par Alloy KeyIsolation.

EXIGENCE ENV-26 : L'algorithme HKDF utilise HMAC-SHA256 (RFC 5869 avec SHA-256) pour toutes les derivations (K_share, K_doc, K_search, K_recovery). L'utilisation de SHA-512 ou d'autres fonctions de hash est INTERDITE pour les derivations HKDF de ce protocole.

EXIGENCE ENV-27 : Les entrees HKDF sont encodees comme suit : - IKM : K_master, 32 bytes bruts - Salt : octets bruts du salt (user_salt = 16+ bytes CSPRNG, documentId = 16 bytes UUID RFC 4122 en representation binaire big-endian) - Info : chaine ASCII sans terminateur null ("pv-share-v1", "pv-doc-v1", "pv-search-v1", "pv-recovery-v1") - OKM : 32 bytes (256 bits)

EXIGENCE ENV-25 : Le user_salt utilise pour K_share et K_search DOIT etre :

• = 16 bytes, genere par un CSPRNG

• Genere une seule fois a l'inscription de l'utilisateur, immuable apres creation
• Stocke en clair cote serveur (meme modele que le sel Argon2)
• Unique par utilisateur (pas de reutilisation inter-utilisateurs)

3.4 Types d'enveloppes¶

Trois types d'enveloppes existent pour un meme K_master :

EXIGENCE ENV-09 : Chaque utilisateur DOIT avoir exactement un (1) envelope de type MASTER. Prouve formellement (TLA+ INV-02, Alloy OneMasterPerUser).

EXIGENCE ENV-10 : Un device revoque (blackliste) NE DOIT PAS avoir d'envelope active. Prouve formellement (TLA+ INV-04, Alloy BlacklistEnforced).

3.5 Versioning des enveloppes¶

EXIGENCE ENV-11 : Chaque envelope possede un compteur de version. La version initiale est 1. Chaque rotation incremente la version de 1.

EXIGENCE ENV-12 : La version est STRICTEMENT croissante (monotone). Prouve formellement (TLA+ INV-05, Alloy VersionPositive).

3.6 Rotation d'enveloppe¶

La rotation permet de changer la cle d'enveloppement (ex: changement de mot de passe) SANS changer K_master.

Procedure :

1. Unwrap K_master avec l'ancien K_enc
2. Deriver le nouveau K_enc (Argon2id du nouveau mot de passe)
3. Wrap K_master avec le nouveau K_enc
4. Incrementer la version
5. Calculer le nouveau metadata_tag (section 3.7)
6. Emettre un evenement d'audit ROTATE (section 3.10)
7. Zeroizer l'ancien K_enc et le nouveau K_enc

EXIGENCE ENV-13 : Apres rotation, K_master DOIT etre identique. Prouve formellement (TLA+ INV-03 RoundtripInvariant).

3.7 Metadata binding¶

Chaque envelope DOIT etre liee a ses metadonnees par un tag d'integrite, verifie cote client au moment du unwrap.

EXIGENCE ENV-17 : Chaque envelope possede un metadata_tag calcule avec HMAC-SHA256 :

metadata_tag = HMAC-SHA256(K_enc, canonical_binding)

ou canonical_binding est la concatenation sans separateur des champs suivants, dans cet ordre : - uid : UUID 16 bytes binaire (RFC 4122, big-endian) - envelope_id : UUID 16 bytes binaire - version : uint32 big-endian (4 bytes) - envelope_type : 1 byte (0x01=MASTER, 0x02=DEVICE, 0x03=RECOVERY) - algorithm : chaine ASCII longueur-prefixee (1 byte longueur + contenu, ex: 0x09 + "AES256-KW") - argon2_salt : octets bruts (16+ bytes)

Le binding DOIT couvrir au minimum :

• Un identifiant stable de l'owner (uid) — empeche le swap inter-utilisateurs
• Un identifiant de l'envelope (envelope_id) — empeche le swap inter-envelopes
• La version et le type — empeche le rollback et la confusion de type

Note architecturale : K_enc est derive du mot de passe, donc le serveur ne peut PAS verifier le tag. La verification se fait exclusivement cote client, au moment du unwrap. Cela signifie qu'un tampering des metadonnees cote serveur ne sera detecte qu'a la prochaine connexion de l'utilisateur. Cette limitation est inherente au modele zero-knowledge.

EXIGENCE ENV-18 : Le metadata_tag DOIT etre non-nul pour toute envelope existante. Prouve formellement (TLA+ INV-10 MetadataBinding, Alloy MetadataBindingValid, Z INV-12).

EXIGENCE ENV-19 : Lors d'une rotation, le metadata_tag DOIT etre recalcule avec la nouvelle version. Prouve formellement (Z THM-08).

3.8 Recovery BIP-39¶

L'envelope RECOVERY utilise un mnemonic BIP-39 comme source de la cle d'enveloppement.

Pipeline :

1. Generer 256 bits d'entropie via CSPRNG
2. Calculer le checksum (8 bits pour 256 bits d'entropie)
3. Encoder en 24 mots selon la wordlist BIP-39
4. Deriver le seed BIP-39 via PBKDF2(mnemonic, passphrase="", 2048 iterations, HMAC-SHA512) -> 64 bytes
5. Deriver K_recovery (32 bytes) via HKDF-SHA256(IKM=seed_64, salt="", info="pv-recovery-v1", L=32)
6. Wrap K_master avec K_recovery via AES-256-KW

Note : PBKDF2-HMAC-SHA512 (BIP-39 §5) produit un seed de 64 bytes. AES-256-KW requiert une cle de 32 bytes. La derivation HKDF intermediaire (etape 5) est obligatoire pour garantir l'interoperabilite. La troncature brute du seed est INTERDITE.

EXIGENCE ENV-20 : L'envelope RECOVERY DOIT utiliser un mnemonic de 24 mots (256 bits d'entropie). Les mnemonics de 12 mots (128 bits) sont INTERDITS pour ProbatioVault.

EXIGENCE ENV-29 : La wordlist BIP-39 utilisee est exclusivement la wordlist anglaise (2048 mots, SHA-256 checksum 2f5eed53a4727b4bf8880d8f3f199d68ad0e19914c3e15805b2e9b093793e7d6). Les wordlists dans d'autres langues sont INTERDITES pour ProbatioVault.

EXIGENCE ENV-21 : Le mnemonic NE DOIT JAMAIS etre stocke sur le serveur. Il DOIT etre presente a l'utilisateur une seule fois pour sauvegarde hors-ligne.

EXIGENCE ENV-22 : Chaque envelope RECOVERY DOIT etre associee a un enregistrement BIP-39. Prouve formellement (Alloy RecoveryBIP39Present, Z schema BIP39Recovery).

3.9 Zeroization¶

EXIGENCE ENV-15 : Toute cle derivee en memoire (K_enc, K_share, K_doc, K_search) DOIT etre zeroizee apres usage. Seul K_master peut persister en memoire le temps de la session.

EXIGENCE ENV-16 : Une cle ne peut etre zeroizee que si elle a ete precedemment derivee. Prouve formellement (TLA+ INV-07 ZeroizeComplete).

Mecanismes par runtime :

Caveat : En environnement JavaScript/V8, la zeroization est best-effort. Pour les cles a haute sensibilite (K_master), privilegier un module natif (N-API) ou WASM avec zeroize garanti.

3.10 Generation de K_master¶

EXIGENCE ENV-14 : K_master DOIT etre genere par un CSPRNG (crypto.getRandomValues ou equivalent) avec 256 bits d'entropie. La generation a lieu une seule fois, a l'inscription de l'utilisateur. K_master n'est jamais derive d'un mot de passe ni d'une autre cle. Le mot de passe sert uniquement a deriver K_enc, qui enveloppe K_master via AES-KW.

3.11 Documentation de la zeroization runtime¶

EXIGENCE ENV-30 : Pour les operations sur K_master (unwrap, rotation, derivation), l'implementation DOIT documenter le niveau de garantie de zeroization de son runtime. Si le runtime ne peut garantir l'absence de copie GC (cas JavaScript/V8), cette limitation DOIT etre documentee dans le rapport de securite du deploiement. Le rapport DOIT specifier : (a) le runtime utilise, (b) le mecanisme de zeroization employe, © les limitations connues, (d) les mesures compensatoires (ex: module N-API, WASM zeroize).

3.12 Audit trail (anti-rollback)¶

EXIGENCE ENV-23 : Chaque operation modifiant une envelope (creation, rotation, revocation) DOIT emettre un evenement d'audit append-only. Prouve formellement (TLA+ INV-11 AuditAppendOnly, Z THM-09).

EXIGENCE ENV-24 : L'audit log NE DOIT JAMAIS etre tronque ni supprime. Les evenements sont immutables. L'append-only DOIT etre garanti par un support offrant des proprietes d'immutabilite verifiable (ex: stockage WORM, chainage de hash, ancrage blockchain).

Evenements audites :

4. Modele formel¶

4.1 Etats et transitions¶

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

                    +----> CreateMasterEnvelope ---+
                    |                              |
GenerateKMaster ----+----> CreateDeviceEnvelope ---+----> DeriveUserKey ----> ZeroizeKey
        |           |                              |
        |           +----> CreateRecoveryEnvelope --+----> DeriveDocKey
        |           |
        +-audit---> +----> RevokeDevice ----> audit
                    |
                    +----> RotateEnvelope ----> audit

4.2 Invariants de surete¶

Les proprietes suivantes sont verifiees par model checking :

Note sur TLC : Le model checking utilise une configuration bornee (MAX_USERS=1, MAX_DEVICES=2, MAX_DOCS=2, 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-08) fournissent des preuves par induction non bornees.

4.3 Theoremes prouves¶

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

• THM-01 : Spec => []TypeInvariant
• THM-02 : Spec => []OneMasterPerUser
• THM-03 : Spec => []BlacklistEnforced
• THM-04 : Spec => []VersionMonotone
• THM-05 : Spec => []ZeroizeComplete
• THM-06 : Spec => []DocKeyIsolation
• THM-07 : Spec => []MetadataBinding
• THM-08 : Spec => []AuditAppendOnly

4.4 Assertions structurelles (Alloy)¶

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

5. Considerations de securite¶

5.1 Modele de menace¶

5.2 Tailles de cles¶

Toutes les cles cryptographiques utilisent 256 bits (32 bytes), conforme a NIST SP 800-131A pour la securite post-2030.

5.3 K_search : leakage deterministe¶

K_search est derivee avec un salt fixe par utilisateur (user_salt, pas par document) pour permettre la recherche chiffree (Searchable Symmetric Encryption). K_search est deterministe : pour un meme (K_master, user_salt), elle produit toujours la meme cle. La portee de ce determinisme couvre les tokens/keywords indexes pour la recherche chiffree. Cette propriete est inherente au design :

• Avantage : Permet de construire un index chiffre consultable sans dechiffrer les documents.
• Risque : Un adversaire observant les requetes peut deduire des patterns d'acces (frequency analysis). Ce risque est documente et accepte.
• Mitigation : K_search est utilisee uniquement pour l'indexation. Le contenu des documents est chiffre avec K_doc_i (salt=docId, non deterministe au niveau global).

5.4 Limitations connues¶

• Le protocole ne protege pas contre un adversaire qui observe la memoire du client en temps reel (cold boot attack). La zeroization reduit la fenetre d'exposition mais ne l'elimine pas, en particulier en JavaScript/V8 (voir section 3.9).
• La recovery envelope (BIP-39) suppose que le mnemonic est stocke hors-ligne par l'utilisateur. Une perte du mnemonic ET du mot de passe entraine une perte irrecuperable de K_master.
• Le model checking TLA+ est borne (voir note section 4.2). Des garanties complementaires proviennent des assertions structurelles Alloy et des schemas Z.

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.

7. Annexes¶

7.1 Specifications formelles associees¶

7.2 Vecteurs de test¶

7.3 Matrice de tracabilite exigences <-> modeles formels¶

7.4 Historique des revisions¶