Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches.

摘要

In this paper we contrast the use of the NRL Protocol Analyzer and Gavin Lowe's use of the model checker FDR 7) to analyze the Needham-Schroeder public key protocol. This is used as a basis to compare and contrast the two systems and to point out possible future directions for research.