(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge*)header {* Blanqui's "guard" concept: protocol-independent secrecy *}theory Auth_Guard_Sharedimports "Guard_OtwayRees" "Guard_Yahalom"beginend