Skip to main content
One Picture is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements
Computer Science Department
  • Iliano Cervesato, Carnegie Mellon University
  • Catherine Meadows, Naval Research Laboratory
Date of Original Version
Abstract or Description
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.
This paper appears in:IEEE Transactions on Dependable and Secure Computing,
Publication Date: July-Sept. 2007
Volume: 4 , Issue: 3
On page(s): 216 - 227
©2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
Citation Information
Iliano Cervesato and Catherine Meadows. "One Picture is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements" (2007)
Available at: