The Neuman-Stubblebine key exchange protocol is formalized in first-order logic and analyzed by the automated theorem prover Spass. In addition to the analysis, we develop the necessary theoretical background providing new (un) decidability results for monadic first-order fragments involved in the analysis. The approach is applicable to a variety of security protocols and we identify possible extensions leading to future directions of research.
展开▼
