(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) section \Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard\ theory Auth_Smartcard imports ShoupRubin ShoupRubinBella begin end