An authentication logic with formal semantics supportingsynchronization, revocation, and recency

摘要

Distributed systems inherently involve dynamic changes to thenvalue of security-relevant attributes such as the goodness of encryptionnkeys, trustworthiness of participants, and synchronization betweennprincipals. Since concurrent knowledge is usually infeasible ornimpractical, it is often necessary for the participants of distributednprotocols to determine and act on beliefs that may not be supported bynthe current state of the system. Policies for determining beliefs innsuch situations can range from extremely conservative, such as onlynbelieving statements if they are very recent, to extremely optimistic,nsuch as believing all statements that are not yet known to be revoked.nSuch security policies often are heavily dependent on timing of receivednmessages and on synchronization between principals. We present a logicnfor analyzing cryptographic protocols that has the capability to specifyntime and synchronization details. This capability considerably advancesnthe scope of known techniques both for expressing practicalnauthentication policies of protocol participants as constraints and fornreasoning about protocol goals subject to these constraints