Static Analysis for Blinding |
Christoffer Rosenkilde Nielsen, Hanne Riis Nielson
|
| Abstract | 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. |
| Keywords | Static analysis, Blinding, Protocols, Process Algebras, LySa |
| Type | Journal paper [With referee] |
| Journal | Nordic Journal of Computing |
| Year | 2006 Vol. 13 No. 1-2 pp. 98-116 |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |