9.7. The non-interference approach

In the mid 1990s Gorrieri et al. started applying the process algebra CCS(Calculus of Communicating Systems [66]) to information security, first to formalizing notions of secrecy in the form of non-interference [32] and then to the analysis of security protocols [31].

They introduce an extension to the CCSlanguage to allow for action hiding, that they call SPA (Secure Process Algebra). Non-interference can be expressed as the property that a process with high level events hidden is equivalent to the process with high level events blocked. In other words, the view at the low level is unable to tell whether or not high level activity has occurred. Different notions of equivalence—traces, may and must testing, ...

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.