consulta ProVerif
10 views
Skip to first unread message
Damián Montenegro
Nov 10, 2012, 5:06:40 PM11/10/12
to seguridad-...@googlegroups.com
Hola, como andan?
Necesito hacer la siguiente consulta:
En el caso del protocolo seguro:
1. A -> B : A
2. B -> A : {B,Nb}pk(A)
3. A -> B : {A,Nb}pk(B)
La idea de los mensajes 2 y 3 es que la identidad de quien esta mandando el mensaje, va encriptada.
Esto implica que el atacante no puede hacer replay de esos mensajes, no? (Si pudiera hacer replay, estariamos en la misma situacion que con el protocolo
1. A -> B : A
2. B -> A : {Nb}pk(A)
3. A -> B : {Nb}pk(B)
el cual, ya sabemos que es inseguro).
¿Como se modelaria esto en ProVerif?
Muchas Gracias.
Saludos
Necesito hacer la siguiente consulta:
En el caso del protocolo seguro:
1. A -> B : A
2. B -> A : {B,Nb}pk(A)
3. A -> B : {A,Nb}pk(B)
La idea de los mensajes 2 y 3 es que la identidad de quien esta mandando el mensaje, va encriptada.
Esto implica que el atacante no puede hacer replay de esos mensajes, no? (Si pudiera hacer replay, estariamos en la misma situacion que con el protocolo
1. A -> B : A
2. B -> A : {Nb}pk(A)
3. A -> B : {Nb}pk(B)
el cual, ya sabemos que es inseguro).
¿Como se modelaria esto en ProVerif?
Muchas Gracias.
Saludos
Ricardo Corin
Nov 10, 2012, 6:17:44 PM11/10/12
to seguridad-...@googlegroups.com
el atacante puede hacer replay de todo el mensaje {B,Nb}pk(A), pero
la idea es que no le sirve en el ataque (porque por ejemplo el que
recibe se da cuenta que el mensaje viene de B, y no es quien esperaba
que sea).
saludos!
2012/11/10 Damián Montenegro <monteneg...@gmail.com>:
> --
>
>
la idea es que no le sirve en el ataque (porque por ejemplo el que
recibe se da cuenta que el mensaje viene de B, y no es quien esperaba
que sea).
saludos!
2012/11/10 Damián Montenegro <monteneg...@gmail.com>:
>
>
Miguel Montes
Nov 11, 2012, 5:24:44 PM11/11/12
to seguridad-...@googlegroups.com
¿Cómo se modela el hecho de que todos conocen la clave pública, pero la clave privada es solo conocida por su dueño?
Si expresamos que la clave pública es pk(y), y se puede descifrar con y (reduc pdecrypt(pencrypt(x,pk(y)),y) = x.). ¿Cómo se expresa que el remitente y el atacante pueden conocer la clave privada, pero no conocen y? ¿Cada participante debe hacer un out de pk(y)?
--
Ricardo Corin
Nov 11, 2012, 7:30:56 PM11/11/12
to seguridad-...@googlegroups.com
Para hacer mas simple el modelo, se puede hacer que los participantes
honestos conocen todas las claves privadas (aunque solo cada
participante honesto usa la suya nomas), por ej:
new skA; new skB; out(c, pk(skA)); out(c, pk(skB)); ( PA | PB )
2012/11/11 Miguel Montes <miguel...@gmail.com>:
> --
>
>
honestos conocen todas las claves privadas (aunque solo cada
participante honesto usa la suya nomas), por ej:
new skA; new skB; out(c, pk(skA)); out(c, pk(skB)); ( PA | PB )
2012/11/11 Miguel Montes <miguel...@gmail.com>:
>
>
Miguel Montes
Nov 11, 2012, 7:37:20 PM11/11/12
to seguridad-...@googlegroups.com
En el query attacker: ¿la pregunta tiene que referirse a una variable free, global? Si pregunto por una creada con un new adentro de un proceso me dice que la variable de la query no está definida. Y el hecho de que sea free no parece modelar el comportamiento de un nonce.
--
Ricardo Corin
Nov 11, 2012, 7:59:21 PM11/11/12
to seguridad-...@googlegroups.com
no necesariamente, no deberia quejarse. Por ej:
free c.
query attacker:k.
process
new k
anda bien. si queres enviame el codigo en privado.
2012/11/11 Miguel Montes <miguel...@gmail.com>:
> --
>
>
free c.
query attacker:k.
process
new k
anda bien. si queres enviame el codigo en privado.
2012/11/11 Miguel Montes <miguel...@gmail.com>:
>
>
Reply all
Reply to author
Forward
0 new messages