Authentication logic supporting synchronization, revocation, and recency

Abstract

A logic for analyzing cryptographic protocols and has the capability to specify time and synchronization details is presented. Such capability considerably advances the scope of known techniques for both expressing practical authentication policies of protocol participants as constraints, and for reasoning about protocol goals subject to these constraints. The logic is flexible and can support a wide range of security policies. Lastly, the ability to reason about the conjunction of individual participant policies and protocols will be especially important as public and private key infrastructures are deployed and new and unanticipated policies are put into use.