A Testing Theory for a Higher-Order Cryptographic Language
Citation:
Vasileios Koutavas and Matthew Hennessy., A Testing Theory for a Higher-Order Cryptographic Language, 20th European Symposium on Programming (ESOP'11), Saarbrucken, Germany, March, 2011Download Item:
Abstract:
We study a higher-order concurrent language with cryptographic
primitives, for which we develop a sound and complete, rstorder
testing theory for the preservation of safety properties. Our theory
is based on co-inductive set simulations over transitions in a rst-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 quanti cation 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)
06 IN.1 1898
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PRESENTEDSaarbrucken, Germany
Author: HENNESSY, MATTHEW
Other Titles:
20th European Symposium on Programming (ESOP'11)Type of material:
Conference PaperAvailability:
Full text availableKeywords:
Computer sciences, bisimulationDOI:
http://dx.doi.org/10.1007/978-3-642-19718-5_19Metadata
Show full item recordLicences: