Abstract
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 language | English |
---|---|
Pages (from-to) | 19-36 |
Number of pages | 18 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 118 |
DOIs | |
Publication status | Published - 1 Feb 2005 |
Event | Proceedings of the International Workshop on Software - Duration: 14 Dec 2003 → 14 Dec 2003 |
Keywords
- Cryptographic Protocols
- Denotational Semantics
- Static Analysis