A Testing Theory for a Higher-Order Cryptographic Language
![Thumbnail](/themes/edepositireland/images/white_rectangle.jpeg)
File Type:
PDFItem Type:
Conference PaperDate:
2011Author:
Access:
OpenAccessCitation:
Vasileios Koutavas, Matthew Hennessy, A Testing Theory for a Higher-Order Cryptographic Language, Lecture Notes in Computer Science, Programming Languages and Systems, European Symposium on Programming (ESOP), Saarbr?cken, Germany, 2011, Gilles Barth, 6602, Springer Berlin Heidelberg, 2011, 358 - 377Download Item:
Abstract:
We study a higher-order concurrent language with cryptographic primitives, for which we develop a sound and complete, first-order testing theory for the preservation of safety properties. Our theory is based on co-inductive set simulations over transitions in a first-order Labelled Transition System. This keeps track of the knowledge of the observer, and treats transmitted higher-order values in a symbolic manner, thus obviating the quantification over functional contexts. Our characterisation provides an attractive proof technique, and we illustrate its usefulness in proofs of equivalence, including cases where bisimulation theory does not apply.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
SFI 06 IN.1 1898
Author's Homepage:
http://people.tcd.ie/vkoutavDescription:
PUBLISHEDSaarbr?cken, Germany
Author: KOUTAVAS, VASILEIOS
Sponsor:
Science Foundation Ireland (SFI)Other Titles:
Lecture Notes in Computer ScienceProgramming Languages and Systems, European Symposium on Programming (ESOP)
Publisher:
Springer Berlin HeidelbergType of material:
Conference PaperCollections
Series/Report no:
6602Availability:
Full text availableKeywords:
Programming LanguagesDOI:
http://dx.doi.org/10.1007/978-3-642-19718-5_19Metadata
Show full item recordLicences: