The concept of Layered Proving Trees and Its Application to the Automation of Security Protocol and Verification

Dojen, R., & Coffey, T. (2005). The concept of Layered Proving Trees and Its Application to the Automation of Security Protocol and Verification. ACM Transactions on Information and System Security, 8, 287-311. Retrieved September 13, 2006, from the ACM Digital Library database.

In this article, Dojen and Coffey presented the theoretical concept of Layered Proving Trees as a way of automatically employing a logically based security protocol verification.

While security protocols are important to maintaining secure communications, their construction leaves them vulnerable to attack. Verification of security protocols is essential but techniques used have had limited success. In response, the authors proposed the use of Layered Proving Trees using modal logics. The bonuses of Layered Proving Trees include that they have few resource requirements, allow for easy tracing of all decisions after completion of the proofs, and allow for the performance of exhaustive searches for proof of traces.

The authors explained the basic structure of a Layered Proving Tree including its levels, nodes (children and parents), and links between them, and then presented an algorithm which can be used to construct a Layered Proving Tree. They addressed implementation issues including proof of soundness (only true conclusions are reached) and proof of completeness (all true conclusions are reached), and also addressed avoiding non-termination which happens when the construction algorithm never runs out of nodes to be expanded. Non-termination can be classified into two groups: direct non-termination and indirect non-termination (which caused non-termination with other postulates). The authors suggested ways of preventing both types of non-termination.

The authors addressed the logic-specific issues of the Layered Proving Tree in a case study for the previously developed GNY logic. The issues were grammar, unification of terms, structure of postulates, and termination. The grammar developed had statements as its basic unit. A protocol was defined as a group of statements each consisting of a principal, operator and data. Data was an atom, a conjunction of data, data encrypted under a symmetric, public or private key, or the result of a function applied to some data. The type of data provided the idea of giving public and private keys to principals and the concept of two principal sharing secret and symmetric keys. The atoms of the grammar were: symmetric, public and private keys, principals, nonces, timestamps, functions and hash-functions.

The authors then set up a prototype and tested it against many security protocols, some of which had well known problems such as those in the BCY protocol. The automatic verifications from the prototype corresponded to the manual verifications, including detection of all the known problems in the protocols that were studied. Performance and scalability issues of setting up the prototype were summarized. The author’s results showed that a Layered Proving Tree has low memory and computing power requirements.

In conclusion, the Layered Proving Tree approach modeling the process of logic-based security protocol verification was proven to be effective and correc