Skip to Main content Skip to Navigation

Security Properties in the lambda-calculus.

Abstract : We examine security properties in the lambda-calculus through the labelled lambda-calculus. Labels express dynamically the dependence between current terms and past reductions. The property of context irreversibility holds in the labelled lambda-calculus: once a context is involved in a reduction, it irreversibly disappears in the remaining of the reduction. We examine fundamental properties of variants of the labelled lambda-calculus. For that purpose, we introduce an elegant proof of Finite Developments Theorem. We then prove that the labels of the weak lambda-calculus express a sharing property. Lambda-calculus labels allow to express security policies such as Stack Inspection and Chinese Wall. We define independence. Intuitively, a reduction is independent from the interaction between principals A and B if it may be decomposed into two reductions: ! a reduction ignoring A and a reduction ignoring B. We prove that this independence property is guaranteed by the Chinese Wall policy. Lambda-calculus labels also express the interference property. In this case, we identify the subterms of a term M that influence the result of the reduction of M. In a lambda-calculus with references, in addition to the functional interference that already exists in the pure lambda-calculus, we identify a memory interference due to the use of references. Labels allow to identify the time intervals during which a reference influences the result of a reduction.
Document type :
Complete list of metadatas

Cited literature [45 references]  Display  Hide  Download
Contributor : Ecole Polytechnique <>
Submitted on : Thursday, July 29, 2010 - 9:37:33 AM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Document(s) archivé(s) le : Thursday, November 4, 2010 - 9:46:34 AM


  • HAL Id : pastel-00002090, version 1



Tomasz Blanc. Security Properties in the lambda-calculus.. Cryptographie et sécurité [cs.CR]. Ecole Polytechnique X, 2006. Français. ⟨pastel-00002090⟩



Record views


Files downloads