9.10. Spi calculus
The spi-calculus is another fairly new and rather elegant framework for modelling and reasoning about security protocols. It was introduced by Abadi and Gordon in [1]. It is an extension of Milner’s π-calculus designed to deal with cryptographic primitives. The π-calculus is a development of Milner’s process algebra CCS (Calculus of Communicating Systems). CCS, rather like CSP, deals with fixed topologies of interacting processes. That is to say the processes and network topology are established at the outset and do not change as the interactions unfold. In CSP the topology is established by fixing the alphabets or channels of the various processes. Thus a pair of processes that share an alphabet will have a channel of communication. ...
Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
