Debugging Security Protocols in Lambda Prolog
A Case-study: the Needham-Schroeder Public Key Protocol
Giorgio Delzanno
In [Del00],
we investigate the fragment of
intuitionistic logic consisting of
hereditary Harrop formulas as a specification language for security protocols.
In this setting, embedded implications and universal quantification
provide a natural built-in mechanism to model the dynamics in the knowledge
of the agents involved in a protocol.
We take advantage of the system lambdaProlog in order to turn
specifications in hereditary Harrop formulas into executable
prototypes, ready to be debugged.
To exploit these features, we select as main case-study
the well-known Needham-Schroeder protocol.
In this paper we report on the results of our experiments and we
discuss potentially interesting directions of future research.
- Lambda Prolog Specification, written in
Terzo
- Usage
- first, load the module using #load "security.mod". in Terzo;
- then, enter the interpreter level using #query security.;
- finally, execute :-go. to find the error-traces described in the paper.
[Del00] G. Delzanno,
Specifying and
Debugging Security Protocols in the hhf Fragment of
Intuitionistic Logic - A Case-study -
September 2000.