Static analysis for blinding

The classical key distribution protocols are based on symmetric and asymmetric encryption as well as digital signatures. Protocols with different purposes often requires different cryptographic primitives, an example is electronic voting protocols which are often based on the cryptographic operation blinding.

In this paper we study the theoretical foundations for one of the successful approaches to validating cryptographic protocols and we extend it to handle the blinding primitive. Our static analysis approach is based on Flow Logic; this gives us a clean separation between the specification of the analysis and its realisation in an automatic tool.

We concentrate on the former in the present paper and provide the semantic foundation for our analysis of protocols using blinding - also in the presence of malicious attackers.