Formalni sustav za analizu sigurnosnih protokola

Tema seminara je formalizam specijaliziran za analizu svojstava
kriptografskih protokola [1], te neke njegove primjene i prosirenja
[2, 3]. Sustav se sastoji od dva dijela, jezika za opis protokola
zvanog Cord Calculus te logike za dedukciju svojstva protokola. Cord
Calculus spada u kategoriju "action calculusa", slican je
pi-calculusu te ima jednostavnu operativnu semantiku. Logicki sustav
se bazira na Floyd-Hoare logikama, te stoga omogucuje vezanje
logickih formula za akcije Cord Calculusa. Upotrebom formalnog
sustava, izvest cemo svojstva klasnicnih primjera kao sto su
Needham-Schroeder-Lowe protokol i standardni Challenge-Response
protokol baziran na elektronskom potpisu. Takodjer, pokazati cemo
kako se formalni sustav moze koristiti za formalizaciju kompozicije
protokola.

[1] N. Durgin, J. C. Mitchell, D. Pavlovic, "A Compositional Logic
for Proving Security Properties of Protocols", in Journal of Computer
Security, 2003

[2] A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic,  "A Derivation
System for Security Protocols and its Logical Formalization", in
Proceedings of 16th IEEE Computer Security Foundations Workshop, 2003

[3] A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic, "Secure Protocol
Composition", to appear in Proceedings of 19th Annual Conference on
Mathematical Foundations of Programming Semantics, Electronic Notes
in Theoretical Computer Science, 2004