Las fallas de protocolo, como el conocido error Heartbleed, los problemas de seguridad y privacidad o las especificaciones incompletas, en general, representan riesgos para los usuarios directos de un protocolo y otros interesados. Los métodos formales, como las Redes de Petri Coloreadas (CPNs), facilitan el diseño, desarrollo, análisis y verificación de nuevos protocolos; la detección de fallas; y la mitigación de riesgos de seguridad identificados. BlockVoke es un esquema basado en blockchain que descentraliza las revocaciones de certificados, permite a los propietarios de certificados y a las autoridades de certificación revocar certificados y distribuye rápidamente la información de revocación. Las CPNs, en particular, son adecuadas para formalizar protocolos basados en blockchain; así, en este trabajo, formalizamos el protocolo BlockVoke utilizando CPNs, resultando en un modelo CPN verificable y una especificación formal del protocolo. Utilizamos una metodología de modelado orientado a agentes (AOM) para crear modelos de objetivos y modelos de interfaz de comportamiento correspondientes de BlockVoke. Posteriormente, se definen las semánticas de los protocolos y se derivan e implementan los modelos CPN utilizando CPN Tools. Además, se realiza un análisis completo del espacio de estados del modelo CPN resultante para derivar propiedades relevantes del modelo del protocolo. El resultado es una especificación formal completa y correcta de BlockVoke que se utiliza para guiar futuras implementaciones y evaluaciones de seguridad.