El protocolo de rana de boca ancha es un protocolo de verificación de redes informáticas que normalmente se utiliza en redes no seguras. Permite que las personas se comuniquen a través de una red para verificar su identidad entre sí, también ayuda a prevenir ataques de reproducción o espionaje y ofrece la detección de cualquier alteración y la prevención de cualquier lectura no deseada. Esto se puede demostrar mediante la lógica BAN (Burrows-Abadi-Needham). Sin embargo, para evitar ataques activos, se debe usar alguna forma de autenticación de mensajes o cifrado autenticado.
El protocolo se puede especificar de la siguiente manera en notación de protocolo de seguridad, donde el usuario A se verifica ante el usuario B mediante un servidor S:
- Donde las identidades del usuario A, el usuario B y el servidor de confianza son A, B y S respectivamente.
- Las marcas de tiempo generadas por el usuario A y el servidor S son TS1 y TS2 respectivamente.
- Una clave simétrica KAS que solo conocen A y S.
- Una clave simétrica generada KAB, que será la clave de sesión de la sesión entre el usuario A y el usuario B.
- Un KBS de clave simétrica que solo conocen B y S.
A → S: A, {T{S1}, B, K{AB}}K{AS}
S → B: {T{S2}, A, K{AB}}K{BS}
Protocolo de rana de boca ancha
Funcionamiento del protocolo de rana de boca ancha:
Para comprender el funcionamiento, consideremos el ejemplo del protocolo Wide-Mouthed-Frog:
M1 A → S: {T{S1}.B.K{AB}}SKey(A)
M2 S → B: {T{S2}.A.K{AB}}SKey(B)
Aquí el servidor comparte dos claves diferentes que son SKey(A) y SKey(B) con A y B; el propósito del protocolo es establecer una clave de sesión K{AB} entre el usuario A y el usuario B, y verificar A a B. Después de eso, el usuario A crea una clave de sesión y la dirige al servidor junto con una marca de tiempo TS1; el servidor luego envía la clave al usuario B junto con una nueva marca de tiempo TS2. Las marcas de tiempo se utilizan generalmente para que los usuarios puedan obtener indicaciones de que los mensajes que han recibido se crearon recientemente. Cabe señalar que para el paso y el funcionamiento de este mecanismo es necesario sincronizar los relojes de los diferentes usuarios; el reloj de cada usuario es crucial para la seguridad del protocolo.
Para comprender este protocolo, necesitaremos ver cómo se puede modelar el tiempo en Casper , algunas otras características de la sintaxis de Casper y la pragmática de seleccionar el sistema para verificar. Para esto, tomemos en consideración cuatro sistemas diferentes que ejecutan el protocolo. FDR descubre que no hay ningún ataque al sistema A, aunque descubrió tres ataques diferentes a los otros sistemas. Los sistemas grandes necesitan mucho más tiempo para verificar, por lo que un enfoque práctico sería comenzar con un sistema más pequeño y avanzar hacia arriba. El sistema D que comprobamos, sin duda, se ha adaptado hasta cierto punto para permitir un ataque en particular; sin embargo, los sistemas A, B y C son ejemplos de sistemas que uno siempre debe considerar.
La mayor parte del modelado del protocolo es generalmente simple; algunos puntos se dan a continuación.
#Free variables A, B : User S : Server SKey : User → SKeys KAB : SEKey TS1, TS2 : TimeStamp InverseKeys = (SKey, SKey)
El usuario puede seleccionar la mayoría de los nombres de tipos en los scripts de Casper, aunque la marca de tiempo es una excepción.
Las marcas de tiempo se modelan en Casper mediante números naturales. Por lo tanto, no haga suposiciones sobre el tamaño de la unidad de tiempo en comparación con el tiempo necesario para enviar un mensaje; pueden surgir numerosos mensajes dentro de la misma unidad de tiempo, y también es posible que algunas unidades de tiempo puedan pasar entre mensajes consecutivos.
#Processes
INITIATOR (A, S, KAB) knows SKey(A)
RESPONDER(B) knows Skey(B)
SERVER(s) knows SKey
#Protocol description
0. → A : B
1. A → S : {B, TS1, K{AB}}{SKey(A)}
[TS1==now or TS1+1==now]
2. S → B : {A, TS2, K{AB}}{SKey(B)}
[TS2==now or TS2+1==now]
Los usuarios en el protocolo Wide Mouth Frog obtienen un mensaje, pueden verificar si las marcas de tiempo que reciben son recientes o no. Las realiza el usuario que obtiene el mensaje precedente; y si la verificación falla, el usuario puede cancelar la ejecución.
#Specification TimedAgreement(A, B, 2, [KAB])
El requisito es que si un usuario respondedor B finaliza una ejecución del protocolo, con el usuario A, entonces el usuario A debería haber estado ejecutando el protocolo dentro de las dos unidades de tiempo precedentes; además, los dos usuarios deben aprobar el valor de KAB, y debe haber una relación de uno a uno entre las ejecuciones de A y B. Todas estas pruebas que se realizan en las marcas de tiempo permiten un retraso de la unidad de una sola vez. cada uno, por lo tanto, haciendo un retraso máximo posible de dos unidades de tiempo.
Sin embargo, para que esta especificación tenga alguna posibilidad de funcionar, debe haber una demora insignificante entre S que verifica el mensaje 1 y envía el mensaje 2.
Veamos ahora el sistema A, considerando un sistema con un solo iniciador, el usuario A, y un solo respondedor, el usuario B, ambos pueden ejecutar el protocolo una vez; tomando todos los tipos de datos para que sean lo más pequeños posible y consistentes con este sistema. Generalmente, la descripción de las variables reales es simple; la única característica nueva es cómo se modela el tiempo aquí:
#Actual variables User A, User B, kcbt : User mkcbt : Server KAB : SessionKey TimeStamp = 0 .. 0 MaxRunTime = 0
#System INITIATOR(User A, mkcbt, KAB) RESPONDER(User B) SERVER(mkcbt)
#Functions symbolic ServerKey
#Intruder Information
Intruder = kcbt
IntruderKnowledge = {User A, User B, kcbt, mkcbt, SKey(kcbt)}
Aquí asumimos que el intruso puede producir todas las marcas de tiempo; por lo tanto, no tienen que estar incluidos en el conocimiento inicial del intruso. Por lo tanto, cuando el archivo anterior se compila utilizando Casper, FDR no puede encontrar ningún ataque al sistema posterior.
Ahora, echemos un vistazo al sistema B, considerando un sistema donde el usuario A puede ejecutar el protocolo una vez como iniciador, simultáneamente.
#System INITIATOR(user A, mkcbt, kcbt) RESPONDER(user A) SERVER(mkcbt)
Aquí, FRD descubre que el protocolo no autentica correctamente al usuario B iniciador al usuario A respondedor. Por lo tanto, al usar el depurador FRD encontramos la forma del ataque como se indica a continuación.
M α.1 A → mkcbt: {B.0.KAB}SKey(A)
M β.2 Imkcbt → kcbt: {B.0.KAB}Skey(A)
El atacante simplemente vuelve a ejecutar el primer mensaje del usuario A en el propio usuario, que interpretan como el mensaje 2 de una ejecución iniciada por el usuario B.
Ahora, echemos un vistazo al sistema C, donde el usuario de respuesta B puede ejecutar el protocolo secuencialmente dos veces.
#System INITIATOR(A, mkcbt, KAB) RESPONDER(B) ; RESPONDER(B) SERVER(mkcbt)
Puede ser atacado si el usuario puede ejecutar el protocolo más de una vez; aunque, por lo general, el atacante puede usar la información de la primera ejecución para falsificar una segunda ejecución.
#System INITIATOR(A, mkcbt, KAB) RESPONDER(B) RESPONDER(B) SERVER(mkcbt)
Ahora, en esto, el FCR nos dice que el usuario A no está correctamente autenticado. Por lo tanto, el depurador FDR se puede usar para exhibir algunos de los siguientes ataques, ya que violan la propiedad de autenticación inyectiva.
M α.1 A → mkcbt : {B.0.KAB}SKey(A)
M α.2 mkcbt → B : {A.0.KAB}SKey(B)
M β.2 Imkcbt → B : {A.0.KAB}SKey(B)
El problema aquí es que el usuario B percibe que ha completado dos ejecuciones del protocolo, mientras que el usuario A solo quería realizar una única ejecución. Aquí, el atacante básicamente reproduce el mensaje de mkcbt al usuario B, de modo que el usuario B cree que el usuario A está intentando establecer una segunda sesión.
Ahora, echemos un vistazo al sistema D, aquí un atacante puede romper el límite de dos unidades. Es decir, el usuario B completa una ejecución de más de dos unidades de tiempo después de la ejecución correspondiente del usuario A.
TimeStamp = 0 . . 3 #System INITIATOR(A, mkcbt, KAB) RESPONDER(B) SERVER(mkcbt) ; SERVER(mkcbt) ; SERVER(mkcbt)
Después de verificar el sistema, FDR observa que el usuario iniciador A no está autenticado según la especificación cronometrada anteriormente. Entonces, después de usar un depurador, se pueden encontrar los siguientes ataques.
M α.1 A → mkcbt : {B.0.KAB}SKey(A)
M α.2 mkcbt → IB : {A.0.KAB}SKey(B)
tock
M β.1 IB → mkcbt : {A.0.KAB}SKey(B)
M β.2 mkcbt → IA : {B.1.KAB}SKey(A)
tock
M γ.1 IA → mkcbt : {B.1.KAB}SKey(A)
M γ.2 mkcbt → IB : {A.2.KAB}SKey(B)
tock
M δ.1 Imkcbt → B : {A.2.KAB}SKey(B)
Problemas en el protocolo de boca ancha:
- Requiere un reloj global.
- El servidor S tiene acceso a todas las claves.
- El valor de la clave de sesión KAB lo determina el usuario A.
- Solo puede reproducir los mensajes dentro del período de marca de tiempo válido.
- El usuario A no está seguro de que exista el usuario B.
- Es un protocolo con estado.