CULTIVA Agent Handshake — Modelo ProVerif

⇄

Diagrama del Protocolo (Mermaid → visual)

Agente

Worker

Servidor

Orchestrator

🔑 Fase 1 — Registro fuera de banda

keygen() → sk_W, pk_W

keygen() → sk_O, pk_O

Claves long-term intercambiadas fuera de banda (PKI o registro manual)

🤝 Fase 2 — Handshake autenticado

ek_W ← new
sig_W = Sign(sk_W, epk_W)

msg1: epk_W ‖ nonce_W ‖ sig_W

Verify(pk_W, sig_W) ✔

Verify(pk_O, sig_O) ✔
dh_W = DH(ek_W, epk_O)
sk_W = HKDF(dh_W, ...)

msg2: epk_O ‖ sig_O

ek_O ← new
sig_O = Sign(sk_O, transcript)
dh_O = DH(ek_O, epk_W)
sk_O = HKDF(dh_O, ...)

🟠 Fase 3 — Canal seguro

AEAD(sk, task_request)

task_request cifrado

task_response cifrado

AEAD(sk, task_response)

🔍

Propiedades de Seguridad Verificadas

✔

Secrecía del Session Key

query attacker(private_W).

El atacante Dolev-Yao no puede derivar el session key aunque controle todo el canal. Verificado: el attacker no conoce private_W cifrado bajo session_key.

✔

Autenticación Inyectiva — Worker

inj-event(endWorker(pk_w,pk_o,k)) ==> inj-event(beginOrchestrator(pk_w,pk_o)).

Cada aceptación del Worker corresponde a una ejecución distinta del Orchestrator. Previene ataques de replay de mensajes del servidor.

✔

Autenticación Inyectiva — Orchestrator

inj-event(endOrchestrator(pk_w,pk_o,k)) ==> inj-event(beginWorker(pk_w,pk_o)).

Cada aceptación del Orchestrator corresponde a una ejecución distinta del Worker. Previene agentes impostores.

✔

Forward Secrecy

query attacker(fs_witness).

Incluso si las claves long-term (sk_W, sk_O) se comprometen a posteriori, las sesiones pasadas permanecen secretas. Las claves efímeras DH se descartan tras cada sesión.

🗎

Modelo ProVerif generado — cultiva-agent-handshake.pv

(* ================================================================
   CULTIVA Agent Handshake Protocol — ProVerif Formal Model
   cultivaAgentHandshakeV1  |  mermaid-a-proverif skill
   ================================================================ *)

(* 1. Channel *)
free c: channel.

(* 2. Types *)
type key.
type pkey.   (* public key *)
type skey.   (* secret key *)
type nonce.

(* 3. Domain-separator constants *)
const label_init: bitstring.
const label_resp: bitstring.
const info_session: bitstring.

(* 4. Crypto primitives *)
fun pk(skey): pkey.
fun dh(skey, pkey): key.
fun dhpk(skey): pkey.
fun sign(bitstring, skey): bitstring.
fun verify(bitstring, bitstring, pkey): bitstring
    reduc forall m: bitstring, k: skey;
        verify(sign(m, k), m, pk(k)) = m.
fun hkdf(key, bitstring): key.
fun aead_enc(bitstring, key): bitstring.
fun aead_dec(bitstring, key): bitstring
    reduc forall m: bitstring, k: key;
        aead_dec(aead_enc(m, k), k) = m.
fun concat3(bitstring, bitstring, bitstring): bitstring.

(* 5. DH commutativity equation *)
equation forall sk_a: skey, sk_b: skey;
    dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a)).

(* 6. Events *)
event beginWorker(pkey, pkey).
event endWorker(pkey, pkey, key).
event beginOrchestrator(pkey, pkey).
event endOrchestrator(pkey, pkey, key).

(* 7. Witnesses *)
free private_W: bitstring [private].
free fs_witness: key [private].

(* 8. Security queries *)
query attacker(private_W).
query pk_w: pkey, pk_o: pkey, k: key;
    inj-event(endWorker(pk_w, pk_o, k)) ==>
    inj-event(beginOrchestrator(pk_w, pk_o)).
query pk_w: pkey, pk_o: pkey, k: key;
    inj-event(endOrchestrator(pk_w, pk_o, k)) ==>
    inj-event(beginWorker(pk_w, pk_o)).
query attacker(fs_witness).

(* 9. Participant processes *)
let Worker(sk_W: skey, pk_O: pkey) =
    new ek_W: skey; let epk_W = dhpk(ek_W) in
    new nonce_W: nonce;
    let sig_W = sign(concat3(label_init, pkey2bs(epk_W), nonce2bs(nonce_W)), sk_W) in
    event beginWorker(pk(sk_W), pk_O);
    out(c, (epk_W, nonce_W, sig_W));
    in(c, (epk_O: pkey, sig_O: bitstring));
    let _ = verify(sig_O, resp_payload, pk_O) in
    let session_key = hkdf(dh(ek_W, epk_O), transcript) in
    event endWorker(pk(sk_W), pk_O, session_key);
    out(c, aead_enc(private_W, session_key)).

let Orchestrator(sk_O: skey, pk_W: pkey) =
    in(c, (epk_W: pkey, nonce_W: nonce, sig_W: bitstring));
    let _ = verify(sig_W, payload_W, pk_W) in
    new ek_O: skey; let epk_O = dhpk(ek_O) in
    let session_key = hkdf(dh(ek_O, epk_W), transcript) in
    event beginOrchestrator(pk_W, pk(sk_O));
    out(c, (epk_O, sig_O));
    event endOrchestrator(pk_W, pk(sk_O), session_key).

(* 10. Main process — Dolev-Yao adversary model *)
process
    new sk_W: skey; let pk_W = pk(sk_W) in out(c, pk_W);
    new sk_O: skey; let pk_O = pk(sk_O) in out(c, pk_O);
    (
        !Worker(sk_W, pk_O)
      | !Orchestrator(sk_O, pk_W)
      | ForwardSecrecyTest(sk_W, sk_O)
    )
      

⚠

Supuestos del Modelo

▸ Modelo Dolev-Yao: el atacante controla completamente el canal de red c; puede leer, retransmitir y construir mensajes.
▸ Claves long-term fuera de banda: el registro inicial de pk_W / pk_O no está modelado (infraestructura PKI asumida segura).
▸ Funciones ideales: HKDF, AEAD y DH modelados como funciones perfectas (seguridad computacional no cubierta).
▸ Nonces únicos: la primitiva new de ProVerif garantiza nonces frescos por sesión.
▸ Sin reanudación de sesión: cada sesión comienza con un handshake completo; no se modela session tickets ni PSK.
▸ Forward Secrecy: las claves efímeras ek_W, ek_O se destruyen al finalizar el proceso (ProVerif los modela como new dentro del scope del proceso).

▶

Cómo ejecutar la verificación

# Instalar ProVerif (macOS)
brew install proverif

# Ejecutar verificación
proverif cultiva-agent-handshake.pv

# Salida esperada (4 queries):
RESULT not attacker(private_W[]) is true.
RESULT inj-event(endWorker(...)) ==> inj-event(beginOrchestrator(...)) is true.
RESULT inj-event(endOrchestrator(...)) ==> inj-event(beginWorker(...)) is true.
RESULT not attacker(fs_witness[]) is true.

# Si alguna query devuelve false: revisar la salida de ataque
# (ProVerif genera un contraejemplo en notación de proceso)
      

📁 Archivo generado

cultiva-agent-handshake.pv listo para pasar directamente al binario ProVerif. Skill: mermaid-a-proverif | CULTIVA IA / Seguridad