src/HOL/Auth/Auth_Shared.thy

removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6);
de-facto this alternative never occured in practice, but it can lead to non-termination of the check;

(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge
*)

section {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}

theory Auth_Shared
imports
  "NS_Shared"
  "Kerberos_BAN"
  "Kerberos_BAN_Gets"
  "KerberosIV"
  "KerberosIV_Gets"
  "KerberosV"
  "OtwayRees"
  "OtwayRees_AN"
  "OtwayRees_Bad"
  "OtwayReesBella"
  "WooLam"
  "Recur"
  "Yahalom"
  "Yahalom2"
  "Yahalom_Bad"
  "ZhouGollmann"
begin

end