TY - GEN
T1 - Proof theory, transformations, and logic programming for debugging security protocols
AU - Delzanno, G.
AU - Etalle, S.
PY - 2001
Y1 - 2001
N2 - In this paper we define a sequent calculus to formally specify, simulate, debug and verify security protocols. In our sequents we distinguish between the current knowledge of principals and the current global state of the session. Hereby, we can describe the operational semantics of principals and of an intruder in a simple and modular way. Furthermore, using proof theoretic tools like the analysis of permutability of rules, we are able to find efficient proof strategies that we prove complete for special classes of security protocols including Needham-Schroeder. Based on the results of this preliminary analysis, we have implemented a Prolog meta-interpreter which allows for rapid prototyping and for checking safety properties of security protocols, and we have applied it for finding error traces and proving correctness of practical examples.
AB - In this paper we define a sequent calculus to formally specify, simulate, debug and verify security protocols. In our sequents we distinguish between the current knowledge of principals and the current global state of the session. Hereby, we can describe the operational semantics of principals and of an intruder in a simple and modular way. Furthermore, using proof theoretic tools like the analysis of permutability of rules, we are able to find efficient proof strategies that we prove complete for special classes of security protocols including Needham-Schroeder. Based on the results of this preliminary analysis, we have implemented a Prolog meta-interpreter which allows for rapid prototyping and for checking safety properties of security protocols, and we have applied it for finding error traces and proving correctness of practical examples.
U2 - 10.1007/3-540-45607-4_5
DO - 10.1007/3-540-45607-4_5
M3 - Conference contribution
SN - 3-540-43915-3
T3 - Lecture Notes in Computer Science
SP - 76
EP - 90
BT - Logic based program synthesis and transformation : 11th international workshop, LOPSTR 2001, Paphos, Cyprus, november 28-30, 2001, selected papers
A2 - Petterossi, A.
PB - Springer
ER -