An Analysis of a Public-Key Protocol with Membranes

In this paper, we develop an analysis of the Needham-Schroeder Public-Key Protocol in the framework of membrane computing. This analysis is used to validate the protocol and exhibits, as expected, a well known logical attack. The novelty of our approach is to use multiset rewriting in a nest of membranes. The use of membranes enables to tight the conditions for detecting an attack. The approach has been validated by developing a full implementation for several versions of the analysis