Shikuma, Naokata and Igarashi, Atsushi - Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus

lmcs:683 - Logical Methods in Computer Science, September 20, 2008, Volume 4, Issue 3
Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus

Authors: Shikuma, Naokata and Igarashi, Atsushi

Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.'s DCC in terms of logical relations and given a proof of noninterference by reduction to parametricity of System F. Unfortunately, their proof contains errors in a key lemma that their translation from DCC to System F preserves the logical relations defined for both calculi. In fact, we have found a counterexample for it. In this article, instead of DCC, we prove noninterference for sealing calculus, a new variant of DCC, by reduction to the basic lemma of a logical relation for the simply typed lambda-calculus, using a fully complete translation to the simply typed lambda-calculus. Full completeness plays an important role in showing preservation of the two logical relations through the translation. Also, we investigate relationship among sealing calculus, DCC, and an extension of DCC by Tse and Zdancewic and show that the first and the last of the three are equivalent.


Source : oai:arXiv.org:0808.3307
DOI : 10.2168/LMCS-4(3:10)2008
Volume: Volume 4, Issue 3
Published on: September 20, 2008
Submitted on: September 25, 2007
Keywords: Computer Science - Programming Languages,Computer Science - Cryptography and Security,D.3.1,F.3.2,F.3.3


Share

Consultation statistics

This page has been seen 33 times.
This article's PDF has been downloaded 8 times.