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