La lógica de composición de protocolos es un método formal que se puede utilizar para demostrar las propiedades de seguridad de los protocolos criptográficos que utilizan criptografía de clave pública y de clave simétrica . PCL está diseñado en torno a un cálculo de proceso con acciones para varios pasos posibles del protocolo (por ejemplo, generar números aleatorios, realizar operaciones de cifrado, descifrado y firma digital , así como enviar y recibir mensajes). [1]
Se han encontrado algunos problemas con la lógica, lo que implica que algunos resultados actualmente reclamados no pueden probarse dentro de la lógica. [2]