A Logical Characterisation of Static Equivalence
Publikation: Forskning - peer review › Konferenceartikel i proceeding
| Bidragets oversatte titel | En logisk karakterisation af statisk ækvivalens |
|---|
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.
| Originalsprog | Engelsk |
|---|---|
| Titel | Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII) |
| Redaktører | Marcelo Fiore |
| Udgiver | Pergamon Press |
| Udgivelsesdato | 2007 |
| Sider | 139-159 |
| DOI | |
| Status | Udgivet |
Konference
| Konference | Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII) |
|---|---|
| Nummer | 23 |
| Land | USA |
| By | New Orleans |
| Periode | 19-05-10 → … |
| Navn | Electronic Notes in Theoretical Computer Science |
|---|---|
| Nummer | 173 |
| ISSN (Trykt) | 1571-0661 |
Emneord
- pi-kalkyle, logik, datalogi
Indlæser lokationer...
ID: 13519826