Abstract
The spi-calculus is a variant of the polyadic π-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 language | English |
---|---|
Pages (from-to) | 7-23 |
Number of pages | 17 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 62 |
DOIs | |
State | Published - Jun 2002 |
Externally published | Yes |
Event | TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types - Udine, Italy Duration: 19 Nov 2001 → 21 Nov 2001 |