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