Indexed Principal Processes of Concurrent Cryptographic Protocols

In this paper, we present an indexed principal process language and apply it to modeling for concurrent cryptographic protocols running in an infinite concurrent manner. The indexed principal process algebra according to CCS language for concurrent computing in cryptographic protocols is adopted as the formal operating semantics of the indexed principal process language. And we introduce a symbolic transition graph and its variant with a binary equivalence relation over topological spaces of the indexed principal processes based on CCS with infinite assignments, which is used to express one cryptographic protocol being independent of other cryptographic protocol or of its different run in an infinite concurrent manner. The result applies to partition the cryptographic protocol and its multi-runs over topological spaces of its conversation domain to reduce computational complexities to prove security attributes of cryptographic protocols running in an infinite concurrent manner.