Kunz, César Darío, 1980-

Un análisis de algunos sistemas formales para verificar protocolos de seguridad sobre spi-cálculo / César Darío Kunz ; dir. por Daniel Edgardo Fridlender. - [S.l. : s.n.], 2004. - 89 h. : il. ; 30 cm.



Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2004.

Incluye referencias bibliográficas: p. 88-89.

Pi-cálculo es un modelo computacional basado en la comunicación de mensajes a través de canales. Fue desarrollado originalmente para analizar la movilidad de canales entre procesos paralelos. Spi-cálculo, con todas sus variantes, es una extensión de Pi-cálculo con primitivas criptográficas y algunas construcciones sintácticas que facilitan la programación y lectura. Al ser un lenguaje de procesos concuerrentes sirve como herramienta para la especificación de prtocolos criptográficos como así también para la descripción y verificación de las propiedades que se espera que tengan. Originalemente, las propiedades eran definidas en función de equivalencias entre procesos, un método muy flexible pero que por lo general requiere gran trabajo y conocimiento del protcolo. Por otro lado, los métodos más recientes están basados en sistemas de tipos y programación lógica. Estos son por lo general, herramientas automatizables pero están destinados a probar propiedades aisladas.


Specifying and verifying and reasoning about programs.
Especificación, verificación y razonamiento sobre programas.
Security and protection.
Seguridad y protección.