(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge*)section \<open>Blanqui's "guard" concept: protocol-independent secrecy\<close>theory Auth_Guard_Publicimports P1 P2 Guard_NS_Public Protobeginend