Model-checking the Secure Release of a Time-locked Secret over a Network