Projects

Jobs

Contact

On Generalized Authorization Problems

This paper defines a framework in which one can formalize a variety of authorization and policy issues that arise in access control of shared computing resources. Instantiations of the framework address such issues as privacy, recency, validity, and trust. The paper presents an efficient algorithm for solving all authorization problems in the framework; this approach yields new algorithms for a number of specific authorization problems.

• Stefan Schwoon, Somesh Jha, Thomas Reps, and Stuart Stubblebine. On generalized authorization problems. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW), pages 202–218. IEEE Computer Society, June 2003. (paper in pdf).

Group Principals and the Formalization of Anonymity

The notion of group principals appears to be a useful concept for reasoning about various properties of electronic commerce and security protocols. In this paper, we present a number of different classes of group principals, including threshold-group-principals. We provide an epistemic language and logic for reasoning about anonymity protocols and anonymity services where protection properties are formulated from the intruder's knowledge of group principals. Using our language, we give an epistemic characterization of anonymity properties. We also present a simple specification and informal assessment using our theory.

• P. Syverson and S. Stubblebine. Group Principals and the Formalization of Anonymity. World Congress on Formal Methods '99, Toulouse, France, LNCS 1708, Springer-Verlag, September, 1999, pp. 814-833.(paper in pdf).

Known and Chosen and Plaintext-Ciphertext Pairs

Formal methods have been successfully applied to exceedingly abstract system specifications to verify high level security properties such as authentication, key exchange, and fail-safe revocation. Furthermore, considerable research exists on evaluating particular ciphers and secure hash functions used to implement high level security properties. However, verifying that less abstract system specifications satisfy low level security properties has been largely impractical. This is evidenced by innumerable system vulnerabilities where high level properties are not attained due to failed assumptions of low level properties. This paper presents ongoing work on investigating known and chosen ciphertext pairs using the NRL Protocol Analyzer. We give a formal characterization of known and chosen pairs, and map it to the NRL Protocol Analyzer model. We also describe the use of the Analyzer to rediscover attacks on an early version of the ESP protocol, and show how our experience in using it has led us to refine our model. This was the first use of the Analyzer to model protocols at such a low level of abstraction.

• S. Stubblebine and C. Meadows. Formal Characterization and Automated Analysis of Known-Pair and Chosen-Text Attacks. In IEEE Journal on Selected Areas in Communications, Special issue on Network Security, Vol. 18, No. 4, April, 2000. (paper in pdf)

• S. Stubblebine and C. Meadows. On Searching for Known and Chosen Cipher Pairs Using the NRL Protocol Analyzer. DIMACS Workshop on Design and Formal Verification of Security Protocols, September, 1997. (paper in pdf).

Authentication Logic Supporting Synchronization, Revocation, and Recency

Earlier research gives a general method for formally specifying and reasoning about distributed systems with any desired degree of immediacy for revoking authentication. This project extends this work by enabling one to specify and reason about protocols against a variety of verification policies used in practice today. 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.

• S. Stubblebine and R. Wright, An Authentication Logic with Formal Semantics Supporting Synchronization, Revocation, and Recency.IEEE Transactions on Software Engineering, Vol. 28, No. 3, March 2002. (paper in ps). 

• S. Stubblebine and R. Wright, An Authentication Logic Supporting Synchronization, Revocation, and Recency, Third ACM Conference on Computer and Communications Security, New Deli, India, March, 1996, pp. 95-105. (paper in pdf), (slides in pdf). 

Analysis and Design of Message Integrity in Cryptographic Protocols

There has been considerable cryptographic analysis of low level security mechanisms such as block ciphers and digital signatures. Furthermore, there has been much research on the analysis and verification of high level security properties such as mutual authentication (e.g., using authentication logics). These higher level properties assume the correct uses of cryptographic mechanisms to achieve intermediate security properties of integrity and confidentiality. However, until now, very little research had existed on assuring that intermediate security properties such as message integrity are satisfied. This work demonstrates the vulnerability of numerous protocols in practice and gives techniques for analysis and design.

• S. Stubblebine and V. Gligor, On Message Integrity in Cryptographic Protocols, IEEE Computer Society Symposium on Research in Security and Privacy, Oakland, CA, May, 1992, pp. 85-104. (Electronic version not available :(

• S. Stubblebine and V. Gligor, Protocol Design for Integrity Protection, IEEE Computer Society Symposium on Research in Security and Privacy, Oakland, CA, May, 1993, pp. 41-53. (paper inpdf).

• S. Stubblebine and V. Gligor, Protecting the Integrity of Privacy-enhanced Electronic Mail with DES-based Authentication Codes, Proceedings PSRG Workshop on Network and Distributed System Security, San Diego, CA, February, 11-12, 1993, pp. 75-80. (paper in pdf)

• R. Kailar, V. Gligor, and S. Stubblebine, Reasoning About Message Integrity, Proc. Fourth IFIP Working Conference on Dependable Computing for Critical Applications, San Diego, CA, January, 1994. (paper in pdf)

Virtues and Limitations of Authentication Logics

This work offers a perspective on the virtues and limitations of several logics for cryptographic protocols focusing primarily on the logics of authentication. We emphasize the scope limitations of these logics rather than their virtues because we consider their virtues to be better understood and accepted than their limitations, and we hope to stimulate further research that will expand their scope.

• V. Gligor, R. Kailar, S. Stubblebine, and L. Gong. Logics for Cryptographic Protocols - Virtues and Limitations. IEEE Proc. of the Computer Security Foundations Workshop IV, June 1991. (paper in pdf)