The Modelling and Analysis of Security Protocols: the CSP Approach

9.11. Provable security

Up until now all the frameworks we have discussed have abstracted away from the details of the cryptographic algorithms and primitives.

There are some well-known ways to characterize the security of cryptographic primitives. These involve probability and complexity theory and are quite technical. We will not go into the details here but refer the reader to, for example [9] and [71]. Interestingly they typically boil down to a sort of process equivalence, or at least approximate equivalence. The intruder is thought of as being able to perform an unbounded number of tests, for example by asking for the encryption of some piece of text of his choice. He can do this repeatedly, possibly basing his choice of text on the outcome ...