Issue No. 03 - March (2002 vol. 28)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.991320
<p>Distributed systems inherently involve dynamic changes to the value of security-relevant attributes such as the goodness of encryption keys, trustworthiness of participants, and synchronization between principals. Since concurrent knowledge is usually infeasible or impractical, it is often necessary for the participants of distributed protocols to determine and act on beliefs that may not be supported by the current state of the system. Policies for determining beliefs in such situations can range from extremely conservative, such as only believing statements if they are very recent, to extremely optimistic, such as believing all statements that are not yet known to be revoked. Such security policies often are heavily dependent on timing of received messages and on synchronization between principals. We present a logic for analyzing cryptographic protocols that has the capability to specify time and synchronization details. This capability considerably advances the scope of known techniques both for expressing practical authentication policies of protocol participants as constraints and for reasoning about protocol goals subject to these constraints. In the course of reasoning about protocol goals, one is able to exhibit sufficient conditions regarding trust between protocol participants, synchronization between protocol participants, and timeliness of message contents. Our logic is flexible and can support a wide range of security policies including the recent-secure authentication policy for enforcing revocation in distributed systems. 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.</p>
formal methods, protocol analysis, authentication logic, recent-secure authentication, revocation, reasoning about time, security policies, security analysis, authentication, clock synchronization, distributed systems security, computer security
R. Wright and S. Stubblebine, "An Authentication Logic with Formal Semantics Supporting Synchronization, Revocation, and Recency," in IEEE Transactions on Software Engineering, vol. 28, no. , pp. 256-285, 2002.