1(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory 2 Copyright 1996 University of Cambridge 3*) 4 5section \<open>Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols\<close> 6 7theory Auth_Shared 8imports 9 NS_Shared 10 Kerberos_BAN 11 Kerberos_BAN_Gets 12 KerberosIV 13 KerberosIV_Gets 14 KerberosV 15 OtwayRees 16 OtwayRees_AN 17 OtwayRees_Bad 18 OtwayReesBella 19 WooLam 20 Recur 21 Yahalom 22 Yahalom2 23 Yahalom_Bad 24 ZhouGollmann 25begin 26 27end 28