Theory README

theory README imports Main
begin

section ‹Auth--The Inductive Approach to Verifying Security Protocols›

text ‹
  Cryptographic protocols are of major importance, especially with the growing
  use of the Internet. This directory demonstrates the ``inductive method'' of
  protocol verification, which is described in papers:
  🌐‹http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html›. The operational
  semantics of protocol participants is defined inductively.

  This directory contains proofs concerning:

    ▪ three versions of the Otway-Rees protocol

    ▪ the Needham-Schroeder shared-key protocol

    ▪ the Needham-Schroeder public-key protocol (original and with Lowe's
      modification)

    ▪ two versions of Kerberos: the simplified form published in the BAN paper
    and also the full protocol (Kerberos IV)

    ▪ three versions of the Yahalom protocol, including a bad one that
      illustrates the purpose of the Oops rule

    ▪ a novel recursive authentication protocol

    ▪ the Internet protocol TLS

    ▪ The certified e-mail protocol of Abadi et al.

  Frederic Blanqui has contributed a theory of guardedness, which is
  demonstrated by proofs of some roving agent protocols.
›

end