One Picture Is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements
|
In this paper we show how we can increase the ease of reading and writing security requirements for cryptographic protocols at the Dolev-Yao level of abstraction by developing a visual language based on fault trees. We develop such a semantics for a subset of NPATRL, a temporal language used for expressing safety requirements for cryptographic protocols, and show that the subset is sound and complete with respect to the semantics. We also show how the fault trees can be used to improve the presentation of some specifications that we developed in our analysis of the Group Domain of Interpretation (GDOI) protocol. Other examples involve a property of Kerberos 5, and a visual account of the requirements in Lowe's authentication hierarchy.
[1] 216 F. Butler, I. Cervesato, A. Jaggard, and A. Scedrov, “A Formal Analysis of Some Properties of Kerberos 5 Using MSR,” Proc. 15th IEEE Computer Security Foundations Workshop (CSFW '02), 2002.
[2] I. Cervesato and C. Meadows, “A Fault-Tree Representation of NPATRL Security Requirements,” Proc. Third Workshop Issues in the Theory of Security (WITS '03), R. Gorrieri, ed., pp. 1-10, 2003.
[3] S. Escobar, C. Meadows, and J. Meseguer, “A Rewriting-Based Inference System for the NRL Protocol Analyzer and Its Meta-Logical Properties,” to be published in Theoretical Computer Science, http://www.dsic.upv.es/users/elp/sescobar papers, 2007.
[4] K. Hansen, A. Ravn, and V. Stavridou, “From Safety Analysis to Software Requirements,” IEEE Trans. Software Eng., vol. 24, no. 7, pp. 573-584, July 1998.
[5] G. Lowe, “A Hierarchy of Authentication Specifications,” Proc. 10th IEEE Computer Security Foundations Workshop (CSFW '97), 1997.
[6] J. McDermott and G. Allwein, “A Formalism for Visual Security Protocol Modeling,” to be published in J. Visual Languages and Computing, 2007.
[7] C. Meadows, “The NRL Protocol Analyzer: An Overview,” J. Logic Programming, vol. 26, no. 2, pp. 113-131, Feb. 1996.
[8] C. Meadows, I. Cervesato, and P. Syverson, “Formal Specification and Analysis of the Group Domain of Interpretation Using NPATR and the NRL Protocol Analyzer,” J. Computer Security, vol. 12, no. 6, pp. 893-932, 2004.
[9] C. Meadows and P. Syverson, “A Formal Specification of Requirements for Payment Transactions in the SET Protocol,” Financial Cryptography, pp. 122-140, 1998.
[10] A.P. Moore, R.J. Ellison, and R.C. Linger, “Attack Modeling for Information Security and Survivability,” Technical Note CMU/SEI-2001-TN-001, CMU Software Eng. Inst., Mar. 2001.
[11] A.W. Roscoe, “Intentional Specification of Security Protocols,” Proc. Ninth IEEE Computer Security Foundations Workshop (CSFW '96), pp. 28-38, 1996.
[12] B. Schneier, “Attack Trees : Modeling Security Threats,” Dr. Dobb's J., Dec. 1999.
[13] P. Syverson and I. Cervesato, “The Logic of Authentication Protocols,” Foundations of Security Analysis and Design, LNCS 2171, R. Focardi and R. Gorrieri, eds., pp. 63-136, Springer, 2001.
[14] P. Syverson and C. Meadows, “A Formal Language for Cryptographic Protocol Requirements,” Designs, Codes, and Cryptography, vol. 7, no. 1-2, pp. 27-59, Jan. 1996.
[15] F.J. Thayer, J.C. Herzog, and J.D. Guttman, “Strand Spaces: When Is a Security Protocol Correct,” Proc. IEEE Symp. Security and Privacy (S&P '98), May 1998.
[16] W.E. Vesely, F.F. Goldberg, N.H. Roberts, and D.F. Haasl, “Fault Tree Handbook,” Technical Report NUREG-0492, US Nuclear Regulatory Commission, http:/www.nrc.gov/, Jan. 1981.
Index Terms:
C.2.0.f Network-level security and protection, C.2.2.c Protocol verification, F.4.3 Formal Languages
Citation:
Iliano Cervesato, Catherine Meadows, "One Picture Is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements," IEEE Transactions on Dependable and Secure Computing, vol. 4, no. 3, pp. 216-227, July-Sept. 2007, doi:10.1109/TDSC.2007.70206
PURCHASE ARTICLE: $19
IEEE Xplore Subscribers
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb