Cryptographic Analysis in Cubic Time

Flemming Nielson, Hanne Riis Nielson, H. Seidl

    Research output: Contribution to journalJournal articleResearchpeer-review


    The spi-calculus is a variant of the polyadic pi-calculus that admits symmetric cryptography and that admits expressing communication protocols in a precise though still abstract way. This paper shows that context-independent control flow analysis can be calculated in cubic time despite the fact that the spi-calculus operates over an infinite universe of values. Our approach is based on Horn Clauses with Sharing and we develop transformations to pass from the infinite to the finite and to deal with the polyadic nature of input and output. We prove that this suffices for obtaining a cubic time implementation without sacrificing precision and without making simplifying assumptions on the nature of keys.
    Original languageEnglish
    JournalElectronic Notes in Theoretical Computer Science
    Issue number17
    Pages (from-to)1
    Publication statusPublished - 2004

    Fingerprint Dive into the research topics of 'Cryptographic Analysis in Cubic Time'. Together they form a unique fingerprint.

    Cite this