Classification of Security Properties (Part II: Network Security)

Many security properties of cryptographic protocols can be all formalized as specific instances of a general scheme, called Generalized Non Deducibility on Composition (GNDC). This scheme derives from the NDC property we proposed a few years ago for studying information flow in computer systems. The theory is formulated for CryptoSPA, a process algebra we introduced for the specification of cryptographic protocols. One of the advantages of our unifying GNDC-based theory is that that formal comparison among security properties become easier, being them all instances of a unique general property. Moreover, the full generality of the approach has helped us in finding a few undocumented attacks on cryptographic protocols. This paper is based on the results of [20,22–25] and covers the second part of the course “Classification of Security Properties” given by Roberto Gorrieri and Riccardo Focardi at the FOSAD’00 and FOSAD’01 schools.