This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
One Picture Is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements
July-September 2007 (vol. 4 no. 3)
pp. 216-227
ASCII Text
x 
 
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-September, 2007.
 
 
BibTex
x
 
@article{ 10.1109/TDSC.2007.70206,
author = {Iliano Cervesato and Catherine Meadows},
title = {One Picture Is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements},
journal ={IEEE Transactions on Dependable and Secure Computing},
volume = {4},
number = {3},
issn = {1545-5971},
year = {2007},
pages = {216-227},
doi = {http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.70206},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Dependable and Secure Computing
TI - One Picture Is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements
IS - 3
SN - 1545-5971
SP216
EP227
EPD - 216-227
A1 - Iliano Cervesato,
A1 - Catherine Meadows,
PY - 2007
KW - C.2.0.f Network-level security and protection
KW - C.2.2.c Protocol verification
KW - F.4.3 Formal Languages
VL - 4
JA - IEEE Transactions on Dependable and Secure Computing
ER -
 
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] 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
Usage of this product signifies your acceptance of the Terms of Use.