View article

A logic is presented for analyzing public key protocols which provide time-dependent confidentiality using a trusted party. The logic is developed as an extension to an existing cryptographic modal logic with time due to Coffey and Saidha. The extension is designed to help capture aspects of timed-release public key protocols that are not captured in the Coffey-Saidha logic. The explicit use of time in the logic is shown to facilitate reasoning about the correctness of an example protocol.