(* 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" "Proto"beginend