M todos formales para verificaci n de protocolos de...

Metodos formales para verificacion

de protocolos de seguridad

Fernando Soler Toscano

Seminario de Logica, Lenguaje e InformacionUniversidad de Sevilla

4 de diciembre de 2008

Fernando Soler Toscano Metodos formales para verificacion de protocolos de seguridad

Componentes de un sistema de comunicacion

El protocolo es el conjunto de reglas que gobiernan la transmisionde datos. Sin un protocolo comun, los dos dispositivos puedenestar conectados pero no comunicarse.


Protocolos de comunicacion

Elementos de un protocolo:

Sintaxis (¿Como se comunica?) Orden en que se agrupan losdatos para formar el mensajeSemantica (¿Que se comunica?) Significado de cada parte delmensajeTemporizacion (¿Cuando se comunica?) Cuando se debe enviarcada mensaje

Un protocolo puede estar, a su vez, compuesto de otrosprotocolos auxiliares. Ası, el protocolo IP de interconexionutiliza cuatro protocolos de soporte.

Existen multitud de protocolos para regular diferentesservicios: TCP, FTP, HTTP, etc.


Protocolos de seguridad

Servicios de seguridad:

Mensaje:

ConfidencialidadIntegridadAutenticacionNo repudio

Entidades que se comunican:

Autenticacion

Un protocolo de seguridad se compone habitualmente de dospartes:

Criptografica (cifrado de los datos)

Logica (estructura y secuenciacion de los mensajes)


Verificacion de protocolos de seguridad

El diseno de un protocolo de seguridad es una tarea muypropensa a errores

La mayorıa de debilidades se encuentran en la parte logica,habitualmente por “suposiciones” que los disenadores hacenacerca del uso que tendra el protocolo

A diferencia de lo que ocurre con el hardware (una CPU tienemiles de millones de puertas logicas), un protocolo no tienemas de unos pocos pasos (Kerberos alrededor de 20) y suverificacion es posible con un coste razonable

Vamos a centrarnos en las posibilidades de verificacion de laparte logica de los protocolos, pero antes presentaremos elalgoritmo de cifrado mas popular, RSA, que usa criptografıade clave asimetrica


Algoritmo RSA

1 Se eligen dos primos muy grandes p y q

2 Se halla n = p × q, el modulo para cifrado y descifrado

3 Se calcula φ = (p − 1) × (q − 1)

4 Se elige un numero aleatorio e y se calcula d de forma qued × e mod φ = 1

5 Se anuncia 〈e, n〉 como clave publica y se mantiene 〈d , n〉como clave privada

Notas:

Lo que se cifra con 〈e, n〉 solo se puede descifrar con 〈d , n〉 yviceversa

La firma se consigue cifrando con la clave privada del emisor

La confidencialidad se consigue cifrando con la clave publicadel receptor


Ejemplo de obtencion de claves

1 p = 7, q = 11

2 n = 7 × 11 = 77

3 φ = (7 − 1) × (11 − 1) = 60

4 Se toma e = 13 y se calcula d = 37 (13 × 37 mod 60 = 1)

5 Clave publica 〈13, 77〉, clave privada 〈37, 77〉

Observaciones:

Dada la clave publica, es posible obtener la clave privadafactorizando 77

La seguridad de RSA depende del tamano de n, ningunalgoritmo actual puede factorizarlo en tiempo polinomial

Solo se conoce un algoritmo de factorizacion en tiempopolinomial pero... ¡Requiere una computadora cuantica!

Las claves tienen usualmente una longitud de 1024-2048 bits

En 2005 se logro factorizar un numero de 640 dıgitos binariosen unos 5 meses con un procesador Opteron a 2.2GHz


Ejemplo de cifrado-descifrado

1 Supongamos que alguien quiere enviar el mensaje confidencial5 al receptor cuya clave publica es 〈13, 77〉

2 Simplemente calcula 513 mod 77 = 26, y envıa 26 (mensajecifrado) al receptor

3 El receptor usa su clave privada 〈37, 77〉: 2637 mod 77 = 5

Notas:

No se puede descifrar con la misma clave: 2613 mod 77 6= 5

El resultado de cifrar con clave privada (firma) habrıa sidodiferente: 577 mod 77 6= 26

Cualquier cadena de texto puede verse como una secuencia denumeros (p.e. UNICODE)

El mensaje a cifrar de divide en bloques de tamano menor a n

Para firmar, suele ser suficiente cifrar un resumen (hash) delmensaje


El problema de la autenticacion

¿Como saber si el usuario que dice serBob es realmente Bob?¿Basta con una contrasena? Unintruso (man in the middle)podrıa obtener la contrasena¿Contrasena cifrada con clave publicadel servidor? Si siempre se cifrala misma contrasena con la misma clave, el resultado essiempre el mismo, un intruso puede obtener el datagrama conla clave cifrada y realizar un replay attackSolucion: clave temporal, nonce (number used once), numeroaleatorio de un solo usoEl servidor envıa un nonce (codificado) al usuario, quien tieneque codificar su contrasena con dicho numeroEl nonce debe ser cada vez nuevoMuchos protocolos de seguridad estan orientados alintercambio de estas claves temporales


Protocolo de autenticacion de Needham-Schroeder (1978)

Alice (A) Bob (B)

〈NA,A〉pub(B)

〈NA,NB〉pub(A)

〈NB〉pub(B)


Sobre el protocolo de Needham-Schroeder

Cada mensaje se puede interpretar como una accion (caracterdinamico) que modifica el estado de creencia (caracterepistemico) de los agentes que intervienen en la comunicacion

Cuando se han enviado los tres mensajes cada uno de losagentes sabe que el otro es quien dice ser

Una variante de este protocolo (con criptografıa de clavesimetrica) fue adoptada como la base del protocolo deautenticacion Kerberos

La version que hemos mostrado, con clave publica, sueletomarse como ejemplo de un protocolo que pese a seraparentemente correcto, es vulnerable al ataque de un intruso

Practicamente cada nueva tecnica de verificacion formal deprotocolos se presenta con este ejemplo


Ataque de Lowe (1995)

Alice (A) Bob (B)Intruso (I)

〈NA,A〉pub(I )

〈NA,NB 〉pub(A)

〈NB〉pub(I )

〈NA,A〉pub(B)

〈NA,NB 〉pub(A)

〈NB〉pub(B)


Comentarios al ataque de Lowe

Al final:

A sabe que se comunica con I pero no sabe que esta siendocomplice de un enganoB cree que se comunica con A pero en realidad se comunicacon ISolo I sabe que se esta enganando a B con la complicidad deA, y puede obtener mensajes que B solo mandarıa a A

El propio Lowe propuso una correccion del protocoloconsistente en que el segundo mensaje, en vez de

B −→ A : 〈NA,NB〉pub(A)

fueraB −→ A : 〈NA,NB ,B〉pub(A)


La logica BAN de autenticacion

M. Burrows, M. Adabi, y R. Needham (1989), A Logic ofAuthentication

Similar a los sistemas de logica dinamica para verificacion deprogramas, pero con operadores epistemicos

Se anota cada paso Si del protocolo de la forma [φ]Si [ψ] yhay que probar que en cualquier estado donde se verifique φ,si se ejecuta Si se obtendra un estado donde se verificara ψ

Todo el protocolo queda anotado:

[α]S1[φ1]S2[φ2] . . . [φn−1]Sn[β]

En α (precondicion del protocolo) estaran las asuncionesiniciales

En β (postcondicion del protocolo) estaran las condicionesque deben cumplirse al final del protocolo (que debe conocercada agente y que no debe conocer)


Logica BAN (ejemplo)

Ejemplos de notacion:

P |≡ X : P cree que X es verdadero

P ⊳ X : En algun momento, P recibio el mensaje X

P |∽ X : En algun momento, P envio X

P k↔Q: P y Q comparten la clave k, que nadie mas conoce

k7→P : P tiene la clave publica k; solo P conoce k−1, la claveprivada

{X}k : Representa X cifrado con la clave k

Ejemplos de reglas:

P |≡ Q k↔P , P ⊳ {X}k

P |≡ Q |∽ X

P |≡ k7→Q, P ⊳ {X}k−1

P |≡ Q |∽ X


Objetivos de la autenticacion

En su forma mas elemental, la autenticacion consiste enestablecer claves de sesion para cifrar la comunicacion entrelos agentes A y B

Suponiendo una unica clave k, el objetivo final serıa:

A |≡ Ak

↔B , B |≡ A

k

↔B

Algunos protocolos exigen que tambien se cumpla:

A |≡ B |≡ Ak

↔B , B |≡ A |≡ A

k

↔B


Comentarios sobre la logica BAN

Problemas:

En una logica del conocimiento podemos introducir el axioma“si P conoce X , entonces X es verdadero”, pero la logicaBAN es un sistema de creencias, no de conocimientos. Que Pcrea X no dice nada de la verdad de X

Se asume que todos los participantes son honestos y creen enla verdad de los mensajes que mandan. Pero la honestidad noes una buena asuncion

Ventajas:

Simplicidad logica y facilidad de uso

Se suele tomar como base para desarrollar sistemas massofisticados


Otras tecnicas de verificacion

Frecuentemente se aborda la verificacion de protocolos deseguridad reduciendola a otro problema para el que existanmas herramientas de razonamiento automatico

En todos los casos, para verificar un protocolo, hay que probardos cosas:

Que el protocolo consigue sus objetivos (postcondiciones)cuando se ejecuta cada uno de los pasos especificados en eldiseno (casos de uso del protocolo)Que no hay posibilidad de un ataque (es decir, no se puedeusar el protocolo de forma fraudulenta)

El el protocolo original de Needham-Schroeder, por ejemplo,se cumple la primera propiedad pero no la segunda


Verificacion con logica de primer orden

C. Weidenbach, Towards an Automatic Analysis of SecurityProtocols in First-Order Logic

Se formaliza el protocolo usando logica de primer orden

C. Weidenbach usa entonces SPASS para probar correccion

En los casos en que no se asegura la decidibilidad, se puedetrabajar con modelos finitos

Los objetivos que hay que demostrar se convierten en:

Los casos de uso del protocolo que se especificaron en eldiseno, son modelos (finitos) de la formalizacion realizadaNo existe ningun modelo (finito) que satisfaga lasprecondiciones pero no la postcondicion. Es decir, ningunaforma de ejecutar el protocolo consigue realizar un ataque


Reduccion a un problema de planificacion

L. C. Aiello, F. Massacci, Planning Attacks to SecurityProtocols: Case Studies in Logic ProgrammingEn un problema de planificacion se da una teorıa del dominioque consta de:

Una descripcion del estado inicialUna descripcion del estado objetivoUna descripcion de las posibles acciones que pueden realizarlos agentes. Cada accion tiene condiciones y efectos

Cada mensaje de modela como una accion cuyos efectos sonla actualizacion correspondiente del conocimiento de losparticipantes

La resolucion de un problema de planificacion es una tarea debusqueda para la que existen diversos enfoques logicos:satisfactibilidad, logica dinamica, calculo de eventos, etc.

Se debe comprobar que los pasos que sigue el protocolo sonun plan para conseguir el objetivo (autenticacion), y que noexiste ningun plan para lograr objetivos fraudulentos


Verificacion mediante abduccion

M. Alberti et.al., Security protocols verification in AbductiveLogic Programming: a case study

Si tenemos un modelo formal del protocolo Θ y φ representael objetivo que buscamos (autenticacion), la solucion alproblema abductivo 〈Θ, φ〉 nos da la secuencia de mensajesque deben enviarse para conseguirlo

Es importante seleccionar bien el conjunto de abducibles, deforma que contenga solo las acciones (mensajes) permitidasen el protocolo

¿Como comprobar que el protocolo es seguro? Si ψ representauna violacion del protocolo, debe comprobarse que elproblema abductivo 〈Θ, ψ〉 no tiene solucion


Protocolos, abduccion y... ¡P sistemas!

A. Atanasiu, Authentication ofmessages using P systems

O. Michel, F. Jacquemard, AnAnalisys of the Needham-SchroederPublic-Key Protocol withMembranes


¿Comunicacion incondicionalmente segura?

Los protocolos habituales son condicionalmente seguros en elsentido en que descansan en el caracter computacionalmentelimitado de los agentes (gran complejidad de la factorizacion)Protocolos incondicionalmente seguros: agentescomputacionalmente ilimitados, perfectamente logicos oracionalesProblema de las cartas rusas: de un paquete de siete cartasconocidas pero mezcladas, dos jugadores —Anne (a) y Bill(b)— cogen tres cada uno y un tercer jugador —Crow (c)—se queda la carta restante. ¿Como pueden A y B informarseabiertamente (publicamente) uno a otro sobre sus cartas sinque C pueda saber de ninguna de ellas? (OlimpiadaMatematica de Moscu, ano 2000)Interes del problema dado que A y B comparten un secreto(como en la autenticacion) mediante anuncios publicosVeremos la solucion de Hans van Ditmarsch usando logicaepistemica


Repartos de cartas

H.P. van Ditmarsch, The Russian cards problem

Definicion. Un reparto de cartas d es una funcion de cartasQ a jugadores (agentes) N. El tamano #d del reparto indicapara cada jugador cuantas cartas tiene. Dos repartosd , e ∈ (Q → N) son indistinguibles (el mismo) para unjugador n ∈ N si #d = #e y d−1(n) = e−1(n)

En el caso de las cartas rusas, las cartas seran 0, 1, 2, 3, 4, 5, 6,y representamos mediante 012|345|6 el reparto d tal qued(0) = a, d(1) = a, d(2) = a, d(3) = b, . . ., d(6) = c . Eltamano lo indicamos en negrita 3|3|1. La mano de Anne esd−1(a) = {0, 1, 2}, y para ella los repartos d = 012|345|6 ye = 012|654|3 son el mismo dado que ambos tienen tamano3|3|1 y d−1(a) = e−1(a) = {0, 1, 2}


Estructuras epistemicas

Definicion (Estructuras epistemicas). Dado un conjunto Nde agentes y un conjunto de atomos proposicionales P , unmodelo M = 〈W ,R ,V 〉 consta de un dominio W de mundoso estados, accesibilidad R : N → P(W × W ) y una valoracionV : P → P(W )

En un modelo epistemico la relacion de accesibilidad ∼n paracada agente n es una relacion de equivalencia. Si w ∼n w ′

decimos que “w es el mismo que w ′ para n”

Si w ∈ M (es decir, w ∈ D(M)), entonces (M,w) es unestado epistemico, cuyo punto es w y modelo subyacente M

Mediante S5N(P) denotamos la clase de todos los modelosepistemicos para los agentes N y atomos P


Lenguaje de la logica epistemica

Definicion (Lenguaje de la logica epistemica). Dado unconjunto N de agentes y un conjunto P de atomos, L�

N(P) esel conjunto mas pequeno tal que si p ∈ P ,φ,ψ ∈ L�

N(P), n ∈ N, entonces

p,¬p, (φ ∧ ψ),Knφ,Cφ, [ψ]φ ∈ L�N(P)

La formula Knφ indica que “el agente n conoce φ”, Cφ que“es conocimiento comun φ” y [ψ]φ que “tras el anuncio(publico y verdadero) de ψ, se verifica φ”

En [ψ]φ, al operador [ψ] se le llama de actualizacion.Definimos [φ;ψ]β como [φ][ψ]β y [φ ∪ ψ]β como [φ]β ∧ [ψ]β


Semantica de la logica epistemica

Definicion (Semantica de la logica epistemica). DadoM ∈ S5N(P), w ∈ M y φ ∈ L�

N(P), donde M = 〈W ,∼,V 〉.Definimos M,w |= φ,

M,w |= p ⇔ w ∈ Vp

M,w |= ¬φ ⇔ M,w 6|= φ

M,w |= φ ∧ ψ ⇔ M,w |= φ y M,w |= ψ

M,w |= Knφ ⇔ ∀w ′ : w ∼n w ′ ⇒ M,w ′ |= φ

M,w |= Cφ ⇔ ∀w ′ : w ∼N w ′ ⇒ M,w ′ |= φ

M,w |= [ψ]φ ⇔ M,w |= ψ ⇒ Mψ,w |= φ

Para Cφ, ∼N := (⋃

n∈N ∼n)∗ (cierre transitivo y reflexivo de la

union de todas las relaciones de equivalencia).Mψ es la restriccion de M a los estados en que es verdaderaψ. Mψ = 〈W ′,∼′,V ′〉 tal que

W ′ := {v ∈ W |M, v |= ψ}∀v , v ′ ∈ W ′ : v ∼′

n v ′ ⇔ v ∼n v ′

V ′

p = Vp |W′

El operador dual de K serıa K y se define Knφ como ¬Kn¬φ


Actualizaciones en el hexagono de van Ditmarsch

(Hexa, 012) |= [Ka(2a → 0b)]C¬2a

(Hexa, 012) |= [Ka(2a → 0b)][Kb(2b → 1a)]C¬Kc0a

http://www.science.uva.nl/projects/opencollege/cognitie/hexagon/


Descripcion logica de juegos de cartas

Definicion Un conjunto de cartas Q y otro de jugadores Ninducen un conjunto de atomos P = Q × N tal que qn

describe el hecho de que el jugador n tiene la carta q. Unestado publico de un juego de cartas es un estado deinformacion (〈D,∼,V 〉, d) tal que D ⊆ (Q → N) y dadosd1, d2 ∈ D : d1 ∼n d2 solo si #d1 = #d2 y d−1

1 (n) = d−12 (n),

y para cada qn ∈ P : Vqn = {d ∈ D|d(q) = n}

Proposicion (Anuncios y estados publicos). Si (M,w) es unestado publico de un juego de cartas para los jugadores N yatomos P , y φ ∈ L�

N(P) tal que M,w |= φ, entonces (Mφ,w)es un estado publico del juego de cartas.

Ojo: no todos los estados epistemicos son estados publicos(Ana le ensena una carta a Bill sin que lo vea Crow)


Descripcion de los repartos de cartas

Es posible describir un reparto de cartas mediante un conjuntode atomos. El reparto 012|345|6 se puede describir:

δ012|345|6 := 0a ∧ 1a ∧ 2a ∧ ¬3a ∧ . . . ∧ ¬0b ∧ . . . ∧ ¬5c ∧ 6c

La mano del jugador a se describe como:

δa012|345|6 := 0a ∧ 1a ∧ 2a ∧ ¬3a ∧ ¬4a ∧ ¬5a ∧ ¬6a

que abreviamos como 012a

Formulas que se satisfacen en el estado inicial(I3|3|1, 012|345|6): Ka0a, Kb¬Ka3b, etc.

Proposicion. Cada anuncio en un estado publico de unjuego de cartas tiene en mismo significado que uno sobrerepartos alternativos


Comunicaciones seguras

Definicion (Postcondiciones). Sea d : Q → {a, b} ∪ O unreparto de cartas. En el estado de informacion (D, d) donde seresuelva el problema, se deben verificar:

aknowsbs∧

e∈D(D)(δbe → Kaδ

be )

bknowsas∧

e∈D(D)(δae → Kbδ

ae)

cignorant∧

c∈O

∧q∈Q

∧n∈{a,b}(¬qc → Kcqn)

Ademas, no solo deben ser verdaderos estos requisitos, sinoconocimiento comun: Caknowsbs, Cbknowsas, Ccignorant

Se toma Ccignorant como invariante bajo la ejecucion decada anuncio publico


Actualizaciones comunicativas

Definicion. Dado un estado publico de cierto juego decartas donde se verifique Ccignorant, hay tres formas deinterpretar que un agente n dice (y es verdad) φ en dichoestado:

[φ] anuncio de φ por observador omnisciente[Knφ] el jugador n comunica φ[Knφ ∧ [Knφ]Ccignorant] comunicacion segura de φ por n

Observar que [Knφ ∧ [Knφ]Ccignorant] equivale a[knφ][Ccignorant].

Es decir, un anuncio seguro de φ es una actualizacion [knφ]tal que Ccignorant se mantiene tras su ejecucion


Intercambios

Definicion (Intercambio). Dado el repartod : Q → {a, b} ∪ O (O no vacıo), un intercambio(“intercambio secreto de manos”) entre dos jugadores a y bes una secuencia finita

Π := π1, π2, . . . , πm

de formulas πi ∈ L�

{a,b}∪Oque se interpretan como

comunicaciones seguras de a y b, tal que tras su ejecucion en(I#d , d) se verifique Caknowsbs ∧ Cbknowsas. Si asumimosque a habla primero y que se turnan, la ejecucion de Π secorresponde con la secuencia de actualizaciones:

[Kaπ1][Ccignorant][Kbπ2][Ccignorant] · · · [Kabπm][Ccignorant]

donde Kab ∈ {Ka,Kb}

Un intercambio directo es un intercambio de longitud dos


Solucion al problema de las cartas rusas

Si el reparto de cartas es 012|345|6, lo siguiente es unintercambio directo:

Anne: “Mi mano esta en {012, 034, 056, 135, 246}”Bill: “Crow tiene la carta 6”

Si π = 012a ∨ 034a ∨ 056a ∨ 135a ∨ 246, se puede probar:1 I3|3|1, 012|345|6 |= Kaπ2 (I3|3|1)Kaπ

|= cignorant3 (I3|3|1)Kaπ

, 012|345|6 |= Kb6c

4 ((I3|3|1)Kaπ)Kb6c

|= cignorant ∧ bknowsas ∧ aknowsbs

Hans van Ditmarsch emplea model ckecking para generar los102 intercambios directos posibles para el reparto 012|345|6

La busqueda esta restringida por ciertas proposiciones quelimitan la forma de los posibles intercambios directos


Comentarios

¿Se puede generalizar para repartos con un numero arbitrariode cartas?

Conjetura: Si es posible un intercambio para un reparto decierto tamano, es posible un intercambio directo

Si se permite que c pueda tener un conocimiento parcial(alguna carta pero no toda la mano) se pueden acortar lassoluciones

¿Como integrar la abduccion en la busqueda de losintercambios?

¿Que ocurre si los agente pueden mentir o realizarcomportamientos estrategicos? Teorıa de juegos

Aplicacion al diseno de protocolos incondicionalmente seguros


M todos formales para verificaci n de protocolos de...

Documents

Transcript of M todos formales para verificaci n de protocolos de...