Process calculi

Process calculi and logics

Process calculi are simple mathematical formalisms that allow us to reason about the behaviour of programs in an implementation-independent fashion. If you have followed the course Semantics and verification, you will already have come across a process calculus, namely CCS. CCS dates back to the early 1980s, but a lot has happened since then.
Access control

Static analysis

Almost all interesting properties of programs are undecidable. Therefore, one of the most interesting ideas here is that of using static analysis. A static program analysis examines the text of a program instead of the execution of the program. Very often, quite a lot of information can be gleaned in this way.
On the other hand, a static analysis is bound to be approximate: The analysis may reject a program, even though the program does not exhibit the flaw that we were trying to find. On the other hand the analysis will guarantee that every program that the analysis accepts will be correct!
Often, static analysis takes the form of a type system. A type system consists of a number of typing rules. The intention is that if a program is well-typed according to these rules, then the program will be correct.

Process calculi with locations

Cryptographic protocols

A starting point here is one of the many process calculi proposed in recent years, namely thespi calculus. If you would like to read more, a good starting point is the original paper by Abadi and Gordon about the spi calculus here (in PDF-format).
Testing is not always enough

Traditionally, security protocols have been tested by means of testing, either by testing a running version of the protocol or by paper-and-pencil testing.
However, such testing cannot not reveal all bugs. For instance, 18 years passed between the invention of the Denning-Sacco protocol for digital signatures and the discovery by Gavin Lowe of an attack on this protocol!
Today, the general agreement is that a scientific approach is called for: One should strive for a systematic and exhaustive, mathematically based theory that will allow us to predict the behaviour of a protocol.
Process calculi for security protocols

Another important insight is that a security protocol is a concurrent and communicating system and that one can therefore use the mathematical models of behaviour that are already being used to analyse concurrent and communicating systems.
The spi calculus is a process calculus due to Martin Abadi and Andrew Gordon. The calculus allows one to describe the behaviour of security protocols. The idea is to extend the pi calculus of Milner, Parrow and Walker with new primitives for encryption and decryption.
The $\pi$ -calculus

The $\pi$ -calculus is a process language that makes it easy to describe processes that exchange the names of communication channels and to describe the scopes of channel names. The $\pi$ -calculus originates with the work of Milner, Walker and Parrow.
Here is a protocol in the $\pi$ -calculus:

The server creates and sends out the channel name from its scope and thereby extends the scope to encompass the processes and . These components can now use for communication.

Expressing security protocols in a process calculus

Three basic assumptions are

We do not describe the actual encryption algorithm; we only describe that data can be encrypted and decrypted.

We do not describe the structure of data or channels other than assume that data, channels and variables have names

Encryption is perfect; cryptanalysis is not the basis of the attacks that we consider.

The spi calculus

We will now show how one can describe a protocol that uses encryption. This example uses the full spi calculus. But before we can describe the example, we have to agree on the syntax of the calculus.
Processes

Conditions

Data

Expressions

A key exchange protocol

Now for our example, a simple key exchange protocol which involves two principals and a trusted key server.

In our spi calculus description of the protocol we have

A channel for each connection

A process for each principal

A protocol is the parallel composition of all principals

Components of the protocol

where , and are as just defined.

Correctness as equivalence

We now go on to describe how one can use our description of the protocol and a notion of behavioural equivalence to express some natural requirements of the protocol.

Authenticity and integrity

When is a protocol correct w.r.t. authenticity and integrity?
It is correct if it always behaves like the ideal protokol $P_{\mbox{\small ideel}}$ which eventually acts as if it received the correct message.
We can write this as

$\begin{displaymath}P(M) \sim P_{\mbox{\small ideel}}(M) \end{displaymath}$

for all . $\sim$ is a suitable notion of behavioural equivalence (some notion of bisimulation equivalence, for instance.)

Secrecy

When is a protocol correct w.r.t. secrecy?
It is correct if its observable behaviour does not depend on the message being sent. In other words:

$\begin{displaymath}P(M) \sim P(M') \end{displaymath}$

for alle and .

Correctness of our example protocol

The ideal protocol is a protocol which states that always acts as if he had received :

Correctness checking as equivalence checking

The above hints at a common understanding of correctness checking for security protocols: It is really a question of checking bisimilarity.
Correctness checking as type checking!

But the story does not end here. Gordon and Jeffrey have founded the Cryptyc project whose aim is to check the correctness of security protocols using type checking.