We investigate the fragment of intuitionistic logic consisting of hereditary Harrop formulas [MNPS91] 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 λProlog [NM88.NM99] 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 [NS78]. In this paper we report on the results of our experiments and we discuss potentially interesting directions of future research.
展开▼
