Proving trust in systems of second-order processes

We consider the problem of proving correctness properties for concurrent systems with features such as higher-order communication and dynamic resource generation. As examples we consider operational models of security and authentication protocols based on the higher-order π-calculus. Key features such as nonces/time stamps, encryption/decryption, and key generation are modelled using channel name generation and second-order process communication. A temporal logic based on the modal μ-calculus is used to express secrecy and authenticity. Extensions include function space constructions to deal with process input and output. Contravariant recursion can be dealt with in two different ways, of which one, an iterative solution, is discussed in the paper. We propose a predicate of trust in a monotonically increasing set of channels as an example, and establish structural decomposition principles for this predicate for concurrent composition and local channel declaration. On this basis a type system for trust inference can be derived quite easily