🚀 go-pugleaf

For my thesis I have some questions concerning the analysis
of the security of cryptographic protocols.

1. I know the work of Burrows, Abadi and Needham (BAN logic)
   and the enhancements made by Gong, Needham and Yahalom
   (GNY logic). Are these logics of authentication widely
   accepted or are other formal methods currently being
   developed.
2. There is some work that describes analyzing cryptographic
   protocols using finite automatons. This work concentrates on
   analyzing properties like completeness, deadlock freedom or
   termination of a protocols. Is it possible to use the
   automaton approach for analyzing security properties of a
   protocol?
3. Are there formal methods for analyzing zero knowledge
   protocols or cryptographic protocols with other goals
   than authentication?
4. Is it still desirable to have formal methods for analyzing
   cryptographic protocols when such things like Kerberos
   or SPX exist and are widely spread.

Many thanks for your help.

Armin Liebl

-------------------------------------------------------------------------

Armin Liebl
Technische Universitaet Muenchen
Institut fuer Informatik
Postfach 202420
W-8000 Muenchen 2

Email: liebla@informatik.tu-muenchen.de
Tel.:  45 05 52 24
Fax.:  45 05 52 22