MODEL-CHECKING THE SECURE RELEASE OF A TIME-LOCKED SECRET OVER A NETWORK