Static analysis for blinding

Christoffer Rosenkilde Nielsen, Hanne Riis Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review


    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.
    Original languageEnglish
    JournalNordic Journal of Computing
    Issue number1
    Pages (from-to)98 - 116
    Publication statusPublished - 2006


    • Static Analysis
    • Voting Protocols
    • Blinding
    • LySa
    • Cryptography

    Fingerprint Dive into the research topics of 'Static analysis for blinding'. Together they form a unique fingerprint.

    Cite this