A Sub-graph of Strand Spaces in Security Protocols

In this paper we define the sub-graph of strand spaces by extending the open bundle, which is adopted as the formalism of security protocols that run in an infinite concurrent way. We re-define communication relations amongst nodes and causal predecessor relations by refining sub-term relations respectively. The novel sub-graph of strand spaces of security protocols that run in infinite concurrent ways, which is different from the open bundle contributes to simplifying its strand spaces to reduce the computational complexity of proofs of safety properties based on theorem proving. The extending strand space theory that contains the method of sub-graphs of strand spaces can be also used to analyses of ordinary concurrent systems.