Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization