A static analysis of cryptographic processes: The denotational approach

Benjamin Aziz*, Geoff Hamilton, David Gray

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


This paper presents a non-uniform static analysis for detecting the term-substitution property in infinite cryptographic processes specified by the language of the spi calculus. The analysis is fully compositional following the denotational approach throughout. This renders the implementation of the analysis straightforward in functional programming. The results are then used to detect certain security breaches, like information leakage and authenticity breaches. As an example of its applicability, we apply the analysis to the SPLICE/AS protocol and the FTP server.

Original languageEnglish
Pages (from-to)285-320
Number of pages36
JournalJournal of Logic and Algebraic Programming
Issue number2
Publication statusPublished - 1 Aug 2005


Dive into the research topics of 'A static analysis of cryptographic processes: The denotational approach'. Together they form a unique fingerprint.

Cite this