(* 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