An authentication logic with formal semantics supporting synchronization, revocation, and recency

Stuart G. Stubblebine, Rebecca N. Wright

Research output: Contribution to journalArticlepeer-review

16 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages (from-to)256-285
Number of pages30
JournalIEEE Transactions on Software Engineering
Volume28
Issue number3
DOIs
StatePublished - Mar 1 2002
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Authentication
  • Authentication logic
  • Clock synchronization
  • Computer security
  • Distributed systems security
  • Formal methods
  • Protocol analysis
  • Reasoning about time
  • Recent-secure authentication
  • Revocation
  • Security analysis
  • Security policies

Fingerprint Dive into the research topics of 'An authentication logic with formal semantics supporting synchronization, revocation, and recency'. Together they form a unique fingerprint.

Cite this