Abstract
The work of Abadi and Fournet introduces the notion of a frame to describe the knowledge of the environment of a cryptographic protocol. Frames are lists of terms; two frames are indistinguishable under the notion of static equivalence if they satisfy the same equations on terms. We present a first-order logic for frames with quantification over environment knowledge which, under certain general conditions, characterizes static equivalence and is amenable to construction of characteristic formulae. The logic can be used to reason about environment knowledge and can be adapted to a particular application by defining a suitable signature and associated equational theory. The logic can furthermore be extended with modalities to yield a modal logic for e.g. the Applied Pi calculus.
Bidragets oversatte titel | En logisk karakterisation af statisk ækvivalens |
---|---|
Originalsprog | Engelsk |
Titel | Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII) |
Redaktører | Marcelo Fiore |
Forlag | Pergamon Press |
Publikationsdato | 2007 |
Sider | 139-159 |
DOI | |
Status | Udgivet - 2007 |
Begivenhed | Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII) - New Orleans, USA Varighed: 19 maj 2010 → … Konferencens nummer: 23 |
Konference
Konference | Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII) |
---|---|
Nummer | 23 |
Land/Område | USA |
By | New Orleans |
Periode | 19/05/2010 → … |
Navn | Electronic Notes in Theoretical Computer Science |
---|---|
Nummer | 173 |
ISSN | 1571-0661 |
Emneord
- pi-kalkyle
- logik
- datalogi