A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols

This thesis presents a Probabilistic Polynomial-time Process Calculus (PPC) for security analysis and applies the calculus to examples from security. Expressions in PPC represent systems of concurrently executing programs that can communicate with each other. Each expression can be evaluated in probabilistic polynomial-time, thus aligning PPC with the foundations of modern cryptography. Expressions in PPC are evaluated by allowing entities to perform local computation until some communication with another entity is required. This communication is selected probabilistically, and the cycle is repeated until further communication is impossible.; We define an observational equivalence relation that relates two expressions if there is not PPC context that distinguishes them. We then develop an equational proof system for PPC that allows the axiomatic derivation of security properties of protocols expressed in PPC. The proof system is proved sound using a form of probabilistic bisimulation: two expressions are bisimilar if they produce the same distributions on observable behaviour. Since bisimulation does not explicitly quantify over contexts, it is simpler than observational equivalence. Consequently, showing the soundness of many of the proof rules becomes easier when bisimulation is used.; The equational proof system is applied to various examples from computer security. Since PPC captures probabilistic poly-time computation, and observational equivalence quantifies over all contexts, we can succinctly state that a protocol is secure using observational equivalence between the protocol and a specification. This approach provides a natural equivalence-based treatment of fundamental notions such as computational indistinguishability, pseudorandomness, semantic security, various definitions of hash function security, as well as assumptions such as the Decision Diffie-Hellman Assumption (DDHA) and the Discrete Log Assumption (DLOG). We can also axiomatically derive well known results such as the equivalence of the semantic security of El Gamal encryption and DDHA. While these relationships are not new, their formal development here demonstrates the expressivity and power of PPC. The thesis concludes by investigating the relationships between various methods of asserting the security of a protocol using a specification. We can, for the first time, show axiomatically that Universal Composability, Blackbox Simulatability, and Process Simulatability are equivalent under certain reasonable assumptions about how principals communicate.