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