(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) section ‹Blanqui's "guard" concept: protocol-independent secrecy› theory Auth_Guard_Public imports P1 P2 Guard_NS_Public Proto begin end