A static analysis of the applied Pi calculus
File(s)
Published version
Author(s)
Aziz, Benjamin
Type
Report
Abstract
We present in this technical report a non-uniform static analysis for
detecting the term-substitution property in systems specified in the language
of the applied pi calculus. The analysis implements a denotational
framework that has previously introduced analyses for the pi calculus and
the spi calculus. The main novelty of this analysis is its ability to deal with
systems specified in languages with non-free term algebras, like the applied
pi calculus, where non-identity equations may relate different terms
of the language. We demonstrate the applicability of the analysis to one
famous security protocol, which uses non-identity equations, namely the
Diffie-Hellman protocol.
detecting the term-substitution property in systems specified in the language
of the applied pi calculus. The analysis implements a denotational
framework that has previously introduced analyses for the pi calculus and
the spi calculus. The main novelty of this analysis is its ability to deal with
systems specified in languages with non-free term algebras, like the applied
pi calculus, where non-identity equations may relate different terms
of the language. We demonstrate the applicability of the analysis to one
famous security protocol, which uses non-identity equations, namely the
Diffie-Hellman protocol.
Date Issued
2006-01-01
Citation
Departmental Technical Report: 06/15, 2006, pp.1-21
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
21
Journal / Book Title
Departmental Technical Report: 06/15
Copyright Statement
© 2006 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
06/15