La lógica de composición de protocolos es un método formal que se utiliza para probar las propiedades de seguridad de los protocolos que utilizan criptografía de clave simétrica y clave pública . PCL está diseñado en torno a un cálculo de procesos con acciones para posibles pasos de protocolo como generar algún número aleatorio, realizar cifrado y descifrado, enviar y recibir mensajes y acciones de verificación de firma digital .
Se han encontrado algunos problemas con la lógica que implican que algunas pruebas actualmente reivindicadas no pueden probarse dentro de la lógica. [1]