More Web Proxy on the site http://driver.im/

research-article

An Authentication Logic with Formal Semantics Supporting Synchronization, Revocation, and Recency

Authors:

Stuart G. Stubblebine,

Rebecca N. WrightAuthors Info & Claims

IEEE Transactions on Software Engineering, Volume 28, Issue 3

Pages 256 - 285

https://doi.org/10.1109/32.991320

Published: 01 March 2002 Publication History

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.

References

[1]

M. Abadi, M. Burrows, B. Lampson, and G. Plotkin, "A Calculus for Access Control in Distributed Systems," ACM Trans. Programming Language Systems, vol. 15, no. 4, pp. 706-734, 1993.]]

Digital Library

[2]

M. Abadi and A. Gordon, "A Calculus for Cryptographic Protocols: The Spi Calculus," Information and Computation, vol. 148, no. 1, pp 1-70, 1999.]]

Digital Library

[3]

M. Abadi and M.R. Tuttle, "A Semantics for a Logic of Authentication," Proc. 10th Ann. ACM Symp. Principles of Distributed Computing, pp. 201-218, Aug. 1991.]]

Digital Library

[4]

M. Burrows, M. Abadi, and R. Needham, 'A Logic of Authentication," Technical Report SRC Research Report 39, Digital Equipment Corp., Feb. 1989.]]

Digital Library

[5]

A. Bleeker and L. Meertens, "A Semantics for BAN Logic," DIMACS Workshop Design and Formal Verification of Security Protocols, Sept. 1997.]]

[6]

CCITT, "The Directory-Authentication Framework," Technical Report X.509, Int'l Telegraph and Telephone Consultative Committee, Feb. 1993.]]

[7]

J. Clark and J. Jacob, A Survey of Authentication Protocol Literature: Version 1.0. available at http://www.cs.york.ac.uk/jac/papers/ drareview.ps.gz, 1997.]]

[8]

S. Dusse, P. Hoffman, B. Ramsdell, L. Lundblade, and L. Repka, "S/MIME Version 2 Message Specification," Internet Draft, Nov. 1997.]]

Digital Library

[9]

S. Dusse, P. Hoffman, B. Ramsdell, and J. Weinstein, "S/MIME Version 2 Certificate Handling," Internet Draft, Nov. 1997.]]

Digital Library

[10]

R. Fagin, J. Halpern, Y. Moses, and M. Vardi, Reasoning About Knowledge. Cambridge, Mass.: MIT Press, 1995.]]

Digital Library

[11]

A. Freir, P. Karlton, and P. Kocher, "The SSL Protocol Version 3.0," Internet Draft, Nov. 1996.]]

[12]

L. Gong, R. Needham, and R. Yahalom, "Reasoning About Belief in Cryptographic Protocols," Poor. 14th IEEE Symp. Research in Security and Privacy, pp. 234-245, May 1990.]]

[13]

K. Gaarder and E. Snekkenes, "Applying a Formal Analysis Technique to the CCITF X.509 Strong Two-Way Authentication Protocol," J. Cryptology, vol. 3, no. 2, pp. 81-98,1991.]]

Digital Library

[14]

J. Kohl and C. Neuman, "The Kerberos Network Authentication Service (V5)," IETF Networking Working Group, RFC 1510, Sept. 1993.]]

Digital Library

[15]

B. Lampson, M. Abadi, M. Burrows, and E. Wobber, "Authentication in Distributed Systems: Theory and Practice," ACM Trails. Computer Systems, vol. 10, no. 4, pp. 265-310,1992.]]

Digital Library

[16]

W. Mao, "An Augmentation of BAN-like Logics," Proc. Eighth IEEE Computer Security Foundations Workshop, pp. 44-56, June 1995.]]

Digital Library

[17]

Y. Moses and B. Bloom, "Knowledge, Timed Precedence and Clocks," Technical Report 95-21, Weizmann Inst., July 1995.]]

Digital Library

[18]

B.C. Neuman and T. Ts'o, "Kerberos: An Authentication Service for Computer Networks," IEEE Comm., vol. 32, no. 9, 1994.]]

[19]

S.G. Stubblebine, "Recent-Secure Authentication: Enforcing Revocation in Distributed Systems," Proc. 19th IEEE Symp. Security and Privacy, pp. 224-235, May 1995.]]

Digital Library

[20]

S.G. Stubblebine and R.N. Wright, "An Authentication Logic Supporting Synchronization, Revocation, and Recency," Proc. Third ACM Conf. Computer and Comm. Security, pp. 95-105, Mar. 1996.]]

Digital Library

[21]

P.F. Syverson and P.C. van Oorschot, "A Unified Cryptographic Protocol Logic," An earlier version of this work appears as "On Unifying Some Cryptographic Protocol Logics" Proc. 18th IEEE Symp. Research in Security and Privacy, pp. 14-28, May 1994.]]

Digital Library

[22]

P.F. Syverson, "Adding Time to a Logic of Authentication," Proc. First Conf. Computer and Comm. Security, pp. 97-101, Nov. 1993.]]

Digital Library

[23]

G. Wedel and V. Kessler, "Formal Semantics for Authentication Logics," Proc. European Symp. Research in Computer Security-ESORICS '96. Sept. 1996.]]

Digital Library

Cited By

Hommersom AMeyer Jde Vink E(2005)Toward Reasoning about Security ProtocolsElectronic Notes in Theoretical Computer Science (ENTCS)10.5555/2772081.2772271126:C(53-75)Online publication date: 8-Mar-2005
https://dl.acm.org/doi/10.5555/2772081.2772271
Popescu BCrispo BTanenbaum AKamperman FKiayias A(2004)A DRM security architecture for home networksProceedings of the 4th ACM workshop on Digital rights management10.1145/1029146.1029150(1-10)Online publication date: 25-Oct-2004
https://dl.acm.org/doi/10.1145/1029146.1029150
Liu HLi M(2004)SVO logic based formalisms of GSI protocolsProceedings of the 5th international conference on Parallel and Distributed Computing: applications and Technologies10.1007/978-3-540-30501-9_145(744-747)Online publication date: 8-Dec-2004
https://dl.acm.org/doi/10.1007/978-3-540-30501-9_145

Index Terms

An Authentication Logic with Formal Semantics Supporting Synchronization, Revocation, and Recency

Recommendations

Proxy Signature with Revocation
Proceedings, Part II, of the 21st Australasian Conference on Information Security and Privacy - Volume 9723

Proxy signature is a useful cryptographic primitive that allows signing right delegation. In a proxy signature scheme, an original signer can delegate his/her signing right to a proxy signer or a group of proxy signers who can then sign documents on ...
On the Security of Some Password Authentication Protocols

In an internet environment, such as UNIX, a remote user has to obtain the access right from a server before doing any job. The procedure of obtaining acess right is called a user authentication protocol. User authentication via user memorable password ...
Efficient revocation and threshold pairing based cryptosystems
PODC '03: Proceedings of the twenty-second annual symposium on Principles of distributed computing

Boneh, Ding, Tsudik and Wong recently proposed a way for obtaining fast revocation of RSA keys. Their method consists in using security mediators that keep a piece of each user's private key in such a way that every decrytion or signature operation ...

Reviews

Reviewer: Srini Ramaswamy

Building upon the BAN logic of authentication for analyzing (and reasoning about) cryptographic protocols, this paper presents a logic that allows for revocation and for the possibility of holding arbitrary beliefs between different runs. The authors define strict and specific policies for belief extensions from one point of time to another. Their logic distinguishes between recentness and freshness, a critical issue in implementing distributed protocols. The authors demonstrate the flexibility of the logic in enforcing revocation in the recent-secure authentication security policy. The logic does not suffer from stiff granularities of time, as compared to other temporal formalisms of security policies, and provides an arbitrary granularity of time. The paper is well written and coherent, and will benefit those researchers working on distributed systems and related applications. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image IEEE Transactions on Software Engineering

IEEE Transactions on Software Engineering Volume 28, Issue 3

March 2002

111 pages

ISSN:0098-5589

Issue’s Table of Contents

Copyright © Copyright © 2002 IEEE. All Rights Reserved.

Publisher

IEEE Press

Publication History

Published: 01 March 2002

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Hommersom AMeyer Jde Vink E(2005)Toward Reasoning about Security ProtocolsElectronic Notes in Theoretical Computer Science (ENTCS)10.5555/2772081.2772271126:C(53-75)Online publication date: 8-Mar-2005
https://dl.acm.org/doi/10.5555/2772081.2772271
Popescu BCrispo BTanenbaum AKamperman FKiayias A(2004)A DRM security architecture for home networksProceedings of the 4th ACM workshop on Digital rights management10.1145/1029146.1029150(1-10)Online publication date: 25-Oct-2004
https://dl.acm.org/doi/10.1145/1029146.1029150
Liu HLi M(2004)SVO logic based formalisms of GSI protocolsProceedings of the 5th international conference on Parallel and Distributed Computing: applications and Technologies10.1007/978-3-540-30501-9_145(744-747)Online publication date: 8-Dec-2004
https://dl.acm.org/doi/10.1007/978-3-540-30501-9_145

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents