A Denotational Approach to the Static Analysis of Cryptographic Processes

Benjamin Aziz*, Geoff W. Hamilton, David Gray

*Corresponding author for this work

Research output: Contribution to journalConference articlepeer-review


We present in this paper, a non-uniform static analysis for detecting the term-substitution property in processes specified in the spi calculus. The property is essential in defining security breaches, like secrecy and authenticity. The analysis is fully denotational, preserving compositionality and facilitating implementations in functional programming.

Original languageEnglish
Pages (from-to)19-36
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 1 Feb 2005
EventProceedings of the International Workshop on Software -
Duration: 14 Dec 200314 Dec 2003


  • Cryptographic Protocols
  • Denotational Semantics
  • Static Analysis


Dive into the research topics of 'A Denotational Approach to the Static Analysis of Cryptographic Processes'. Together they form a unique fingerprint.

Cite this