Adaptación divulgativa: Edison Narváez
Publicado: Septiembre 2026
Área: Ciberseguridad · Sistemas Distribuidos · Computación Confiable
Resumen
Los sistemas de información distribuidos permiten que personas y organizaciones intercambien archivos, documentos, claves y otros activos digitales sin compartir un mismo entorno físico. Cuando las partes no confían plenamente unas en otras, aparece el reto de garantizar que el intercambio sea justo y que la información confidencial no quede expuesta a intermediarios.
El artículo “Implementation and Analysis of a Synchronisation Protocol for Fair Exchange with Strong Fairness and Privacy” presenta la implementación y el análisis de un protocolo de sincronización basado en el modelo Fair Exchange Without Disputes (FEWD). La arquitectura divide el tercero de confianza en dos entornos de ejecución confiables —uno por participante— y un Public Bulletin Board (PBB), utilizado para sincronizar los resultados. El trabajo modela el comportamiento mediante máquinas de estados finitos, formaliza el protocolo en Promela y utiliza el verificador SPIN para examinar sus propiedades. Además, presenta una implementación de la sincronización en Python.
El estudio informa que la verificación formal examinó escenarios de éxito y cancelación, así como propiedades de justicia fuerte y cancelación oportuna. Es importante precisar que la implementación descrita no incorpora todavía todos los módulos confiables para manipular los documentos: las operaciones de depósito, verificación y liberación/restauración de los attestables se consideran fuera del alcance de esa etapa.
Palabras clave: intercambio justo, privacidad, sistemas distribuidos, FEWD, Trusted Execution Environment, TEE, SPIN, Promela, Python, Public Bulletin Board.
1. Introducción
Las transacciones digitales suelen implicar el intercambio de elementos entre dos participantes que no necesariamente se conocen o confían entre sí. Un ejemplo es la entrega de un contrato firmado a cambio de otro documento, el intercambio de claves criptográficas o la transferencia de un activo digital. En estos escenarios, cada parte necesita tener garantías de que la contraparte también cumplirá lo acordado.
Los protocolos de intercambio justo (Fair Exchange Protocols, FEP) buscan impedir que una parte termine con los dos elementos mientras la otra no recibe ninguno. Sin embargo, conseguir justicia fuerte y privacidad al mismo tiempo resulta complejo. Algunas soluciones recurren a un tercero centralizado que coordina la transacción, pero ese intermediario puede llegar a acceder a información sensible y convertirse en un punto crítico de fallo.
El artículo analizado investiga una alternativa basada en un tercero de confianza dividido. En lugar de concentrar las funciones en un único servidor, distribuye el cómputo entre entornos protegidos y utiliza un registro público de mensajes para sincronizar el estado de la operación.
2. ¿Qué es el intercambio justo?
El intercambio justo es una propiedad de los protocolos que coordinan la entrega de dos elementos. En el escenario básico, Alice tiene un elemento D_A y Bob tiene un elemento D_B. El objetivo es que ambos intercambien sus elementos conforme a las condiciones pactadas.
El artículo distingue dos enfoques:
Intercambio justo fuerte (strong fairness): al finalizar, ambos participantes obtienen el elemento de la contraparte o los dos conservan sus elementos originales o quedan protegidos conforme al resultado de cancelación definido por el protocolo.
Intercambio justo débil (weak fairness): pueden existir resultados injustos que exijan una resolución posterior, por ejemplo mediante arbitraje o intervención humana.
La justicia fuerte es especialmente relevante en transacciones donde una disputa posterior sería costosa o donde no existe una autoridad externa capaz de resolver rápidamente el conflicto.
3. El reto: justicia y privacidad
La justicia y la privacidad están relacionadas, pero no son la misma propiedad. Un protocolo puede coordinar correctamente el intercambio y, aun así, revelar datos a un intermediario. Por otro lado, un protocolo que protege la confidencialidad puede no asegurar que ambas partes terminen en un estado consistente.
El trabajo busca combinar varias propiedades:
Justicia fuerte: evitar que una parte consiga ambos elementos mientras la otra queda sin el suyo.
Privacidad: reducir la exposición de información confidencial a terceros.
Cancelación oportuna: permitir que un participante cancele sin depender indefinidamente de la respuesta de la contraparte.
Consistencia: lograr que ambos participantes reconozcan un resultado final compatible, ya sea éxito o cancelación.
El desafío técnico consiste en conservar esas garantías cuando los mensajes pueden retrasarse, perderse o llegar en un orden distinto, y cuando una de las partes deja de responder.
4. ¿Qué propone el artículo?
El artículo implementa y analiza un protocolo de sincronización inspirado en Fair Exchange Without Disputes (FEWD). La propuesta utiliza un tercero de confianza dividido —split TTP— compuesto por tres piezas: un componente attestable para Alice, otro para Bob y un Public Bulletin Board (PBB).
Los attestables son módulos que se espera ejecutar en entornos confiables y que realizan operaciones críticas del protocolo. El PBB actúa como un punto de coordinación: conserva y devuelve tokens que indican si cada participante desea continuar o cancelar.
La contribución central del artículo es avanzar más allá de una descripción conceptual mediante una implementación funcional de la sincronización, la representación del protocolo como máquinas de estados finitos y la verificación formal con SPIN.
5. ¿Qué es un entorno de ejecución confiable?
Un entorno de ejecución confiable (Trusted Execution Environment, TEE) es un entorno aislado diseñado para proteger código y datos frente a accesos no autorizados desde otras partes del sistema. Según la plataforma, puede apoyarse en funciones de hardware para separar operaciones sensibles de los procesos ordinarios.
En la arquitectura estudiada, los attestables de Alice y Bob representan los componentes que deberían ejecutar las operaciones críticas bajo protección. La separación permite que cada participante controle su propio componente, en lugar de entregar toda la información a un intermediario central.
La existencia de un TEE no elimina por sí sola todos los riesgos. Las garantías dependen de la plataforma concreta, su configuración, el software ejecutado y el modelo de amenazas. Por ello, la propuesta debe entenderse junto con sus supuestos de confianza.
6. ¿Qué función cumple el Public Bulletin Board?
El Public Bulletin Board (PBB) es un registro o tablero de mensajes compartido que se utiliza para sincronizar a los participantes. En la implementación descrita, el PBB almacena tokens y permite que las aplicaciones consulten el registro para decidir cuál es el siguiente estado del protocolo.
El PBB no sustituye las operaciones que deberían ejecutarse dentro de los attestables. Su función principal es hacer visible el registro de sincronización para que ambas partes puedan llegar a una decisión coherente.
La arquitectura utiliza un servidor PBB y servidores de aplicación separados para Alice y Bob. Cada entidad mantiene su propia base de datos, y las comunicaciones entre los servicios se realizan mediante canales autenticados y cifrados con TLS.
7. Las cuatro operaciones básicas
El artículo describe el intercambio justo como un proceso compuesto por cuatro operaciones básicas, precedidas por una negociación inicial o handshake.
1. Handshake. Alice y Bob acuerdan los términos del intercambio, las identidades, el PBB que utilizarán y la descripción de los elementos.
2. Deposit (depósito). Cada parte prepara o entrega el elemento para que el protocolo pueda gestionar el intercambio.
3. Verify (verificación). Se comprueba que el elemento recibido o descrito corresponda con lo esperado y con las condiciones acordadas.
4. Synchronisation (sincronización). Los participantes publican y consultan tokens para determinar si el protocolo debe continuar o cancelarse.
5. Release/restore (liberación o restauración). Cuando se alcanza un resultado válido, los elementos se liberan o se ejecuta la acción de restauración definida para la cancelación.
La implementación presentada se concentra en la sincronización y en los mecanismos necesarios para iniciar el protocolo. El artículo aclara que la implementación de las operaciones de manipulación de documentos dentro de los attestables no forma parte de esta etapa.
8. ¿Cómo se modeló y verificó el protocolo?
Para analizar formalmente el comportamiento del protocolo, los autores lo representaron mediante máquinas de estados finitos (Finite State Machines, FSM). Una máquina de estados describe las situaciones posibles de un participante y las transiciones que se producen cuando recibe o publica determinados mensajes.
El modelo se formalizó con Promela y se verificó utilizando SPIN, una herramienta de model checking. Esta técnica explora las secuencias posibles de ejecución del modelo para identificar si se cumplen propiedades especificadas o si existen caminos que conducen a estados no deseados.
El análisis utiliza registros de ejecución generados por SPIN, conocidos como archivos .trail, para reconstruir las secuencias examinadas. Los autores revisan, entre otros casos, escenarios en los que ambas partes completan el intercambio y escenarios en los que una de ellas cancela.
9. Resultados principales
Según los resultados descritos en el artículo, el modelo verificado converge a uno de dos estados finales: éxito del protocolo o cancelación. En los escenarios de éxito, las máquinas de estados de Alice y Bob alcanzan de forma consistente el estado de intercambio completado. En los escenarios de cancelación, ambos participantes reconocen que el protocolo terminó sin completar el intercambio.
El estudio también analiza la cancelación oportuna. Por ejemplo, si Alice publica tokens de sincronización y no recibe respuesta de Bob, puede publicar un token de cancelación. Cuando Bob consulta posteriormente el registro, observa la cancelación y puede terminar también el protocolo.
Los autores señalan que las secuencias revisadas mediante SPIN respaldan las propiedades especificadas en el modelo, particularmente la justicia fuerte y la posibilidad de cancelar oportunamente. Estas conclusiones se refieren al modelo y a la implementación de sincronización evaluados; no equivalen a una garantía universal de seguridad para cualquier sistema real.
El trabajo incluye una implementación en Python que utiliza servicios REST construidos con Flask, bases de datos PostgreSQL y contenedores Docker para separar los servidores de Alice, Bob y el PBB. Las comunicaciones entre servicios se protegen mediante TLS.
10. Arquitectura de la implementación
APLICACIÓN DE ALICE ↔ ATTESTABLE DE ALICE
↘
PUBLIC BULLETIN BOARD (PBB)
↗
APLICACIÓN DE BOB ↔ ATTESTABLE DE BOB
SERVICIOS: Flask / API REST · BASES DE DATOS: PostgreSQL
DESPLIEGUE: Docker · COMUNICACIONES: TLS
Esquema explicativo simplificado basado en la descripción de la arquitectura del artículo. Los módulos attestable se presentan como componentes previstos para las operaciones confiables; el trabajo indica que deposit, verify y release/restore no fueron implementados en esa fase.
11. Tecnologías utilizadas y su aporte
Python: lenguaje utilizado para implementar la lógica de sincronización.
Promela: lenguaje empleado para describir formalmente el comportamiento del protocolo.
SPIN: verificador utilizado para examinar secuencias y propiedades del modelo.
Flask y API REST: permiten la comunicación entre los servicios de Alice, Bob y el PBB.
PostgreSQL: almacena los registros y estados que corresponden a cada entidad.
Docker: facilita separar y desplegar los componentes de la arquitectura.
TLS: protege la comunicación entre los servicios mediante canales autenticados y cifrados.
12. Diferencias frente a un tercero centralizado
| Aspecto | TTP centralizado | TTP dividido del artículo |
| Organización | Las funciones se concentran en una entidad. | Las funciones se distribuyen entre dos attestables y el PBB. |
| Privacidad | El intermediario puede acceder a datos de las partes. | Se busca limitar la exposición mediante componentes confiables separados. |
| Sincronización | El tercero central controla el proceso. | El PBB permite compartir tokens para coordinar el estado. |
| Cancelación | Depende del diseño del protocolo central. | El protocolo analiza tokens de cancelación y finalización oportuna. |
| Validación | Depende de las pruebas y controles implementados. | Se combina implementación de sincronización con model checking mediante SPIN. |
13. Aplicaciones potenciales
Las siguientes son posibles áreas de aplicación del concepto; no deben interpretarse como despliegues probados por los autores del artículo:
Intercambio de documentos digitales entre empresas que no desean entregar toda su información a un intermediario.
Procesos de firma y entrega de documentos en los que ambas partes necesitan confirmar el cumplimiento de condiciones.
Transferencia coordinada de archivos, credenciales o claves criptográficas.
Sistemas de información distribuidos que requieren privacidad y resultados coherentes ante fallos de comunicación.
Prototipos de comercio electrónico en los que se necesita formalizar qué sucede cuando una parte desiste.
Antes de utilizar una arquitectura de este tipo en producción, se necesitarían pruebas de seguridad, evaluación del hardware confiable, revisión de las claves y controles operativos, además de analizar requisitos legales y de disponibilidad.
14. Limitaciones y aspectos por considerar
Una distinción importante del artículo es que la verificación formal se realiza sobre un modelo y que la implementación en Python se concentra en la sincronización. Las operaciones de depósito, verificación y liberación/restauración de documentos dentro de los attestables se consideran fuera del alcance de la implementación presentada.
Por esa razón, los resultados de SPIN respaldan las propiedades del modelo bajo las condiciones especificadas, pero no demuestran automáticamente que todos los componentes de una solución completa sean invulnerables. La seguridad real también depende del código, las bibliotecas, el hardware, las configuraciones, la gestión de claves y la disponibilidad del PBB.
También es importante distinguir entre demostrar que un conjunto de estados y transiciones satisface propiedades formales y medir el rendimiento de un sistema bajo carga real. Las conclusiones de corrección del modelo no deben transformarse en cifras de velocidad, ahorro o resistencia a ataques que el artículo no reporte.
La arquitectura distribuye responsabilidades, pero conserva supuestos de confianza sobre los componentes confiables y sobre el funcionamiento de la infraestructura. Estos supuestos deben revisarse antes de adaptar el diseño a escenarios productivos.
15. Futuras líneas de investigación
Implementar los módulos attestable sobre plataformas TEE reales y evaluar sus operaciones de extremo a extremo.
Integrar las operaciones de depósito, verificación y liberación/restauración en un prototipo completo.
Probar el protocolo bajo retrasos, pérdida y reordenamiento de mensajes, interrupciones y recuperación de servicios.
Evaluar el comportamiento y la disponibilidad del PBB en diferentes condiciones de despliegue.
Medir tiempos de respuesta, consumo de recursos y escalabilidad con cargas representativas.
Ampliar la verificación formal para explorar nuevas condiciones de fallo y supuestos de amenazas.
Comparar la solución con otros protocolos de intercambio justo usando criterios y escenarios reproducibles.
16. Conclusiones
El artículo presenta una contribución relevante al problema de coordinar intercambios digitales justos sin depender completamente de un intermediario central que acceda a los datos de los participantes. Su propuesta se basa en dividir el tercero de confianza entre dos entornos de ejecución confiables y un Public Bulletin Board que sincroniza el resultado mediante tokens.
La combinación de máquinas de estados finitos, Promela y SPIN permite analizar formalmente las secuencias del protocolo y revisar si los participantes convergen a un estado final consistente, tanto en caso de éxito como de cancelación. La implementación de sincronización en Python, con Flask, PostgreSQL, Docker y TLS, acerca el diseño a una arquitectura técnica concreta.
Sin embargo, el alcance debe expresarse con precisión: las operaciones de manipulación de documentos dentro de los attestables quedaron fuera de la implementación descrita. Por ello, la verificación formal y los resultados obtenidos son evidencia sobre el modelo y la sincronización evaluados, no una certificación integral de una solución lista para cualquier entorno de producción.
En conclusión, el trabajo conecta el diseño formal de protocolos con una implementación práctica y ofrece una base para seguir investigando soluciones que equilibren justicia, privacidad y capacidad de cancelación en sistemas distribuidos.
Referencia bibliográfica
Quixabeira, D., Teles-Borges, M., Roos-Frantz, F., Frantz, R. Z., & Sawicki, S. (2026). Implementation and Analysis of a Synchronisation Protocol for Fair Exchange with Strong Fairness and Privacy (Implementação e Análise de um Protocolo de Sincronização para Troca Justa com Justiça Forte e Privacidade). iSys – Journal of Information Systems, 19, 1:1–1:32. https://doi.org/10.5753/isys.2026.6859