La lógica de Burrows-Abadi-Needham (también conocida como lógica BAN ) es un conjunto de reglas para definir y analizar protocolos de intercambio de información. Específicamente, la lógica BAN ayuda a sus usuarios a determinar si la información intercambiada es confiable, protegida contra escuchas o ambas cosas. La lógica de BAN comienza con la suposición de que todos los intercambios de información ocurren en medios vulnerables a la manipulación y el monitoreo público. Esto se ha convertido en el popular mantra de seguridad, "No confíe en la red".
La lógica BAN utiliza postulados y definiciones , como todos los sistemas axiomáticos , para analizar los protocolos de autenticación . El uso de la lógica BAN a menudo acompaña a una formulación de notación de protocolo de seguridad de un protocolo y, a veces, se proporciona en documentos.
La lógica BAN y las lógicas de la misma familia son decidibles : existe un algoritmo que toma hipótesis BAN y una supuesta conclusión, y que responde si la conclusión es o no derivable de las hipótesis. Los algoritmos propuestos utilizan una variante de conjuntos mágicos . [2]
La lógica BAN inspiró muchos otros formalismos similares, como la lógica GNY . Algunos de ellos intentan reparar una debilidad de la lógica BAN: la falta de una buena semántica con un significado claro en términos de conocimiento y universos posibles. Sin embargo, a partir de mediados de la década de 1990, los protocolos de cifrado se analizaron en modelos operativos (asumiendo una criptografía perfecta) utilizando verificadores de modelos, y se encontraron numerosos errores en los protocolos que se "verificaron" con lógica BAN y formalismos relacionados. [ cita requerida ] En algunos casos, el análisis de BAN consideró que un protocolo era seguro, pero de hecho era inseguro. [3] Esto ha llevado al abandono de las lógicas de la familia BAN en favor de métodos de prueba basados en el razonamiento de invariancia estándar. [ cita requerida]
Las definiciones y sus implicaciones se encuentran a continuación ( P y Q son agentes de red, X es un mensaje y K es una clave de cifrado ):
P debe creer que X está fresco aquí. Si no se sabe que X sea nuevo, entonces podría ser un mensaje obsoleto, reproducido por un atacante.