The Modelling and Analysis of Security Protocols: the CSP Approach

1.3. Hiding and renaming

One normally expects the internal details of how a program runs to be invisible to a user, who only gets to see the program’s defined external interface (e.g. a procedure’s parameters, or the externally available operations on an object). It is natural to want the same degree of abstraction in CSP, but this is something the language we have seen so far, lacks when it comes to building parallel networks. Consider the process B2 defined on page 51. In this case we can divide the set of events used into two parts: the natural external interface {|left, right |} and the rest, which represent internal communications between the processes making up the system. Thus two systems with different internal communications will not ...