The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study

Technischer Bericht

Autor(en):Bernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt und Tomasz Truderung
Institution:Department of Informatics, Karlsruhe Institute of Technology
Reihe:Karlsruhe Reports in Informatics
Nummer:2012-8
Jahr:2012
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000027497

Abstract

In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by Küsters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties.

BibTeX

@TechReport{BeckertBrunsKuestersEtAl12,
  author	= {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and
		   Christoph Scheben and Peter H. Schmitt and Tomasz
		   Truderung},
  title		= {The {\KeY} Approach for the Cryptographic Verification of
		   {J}ava Programs: {A} Case Study},
  institution	= {Department of Informatics, Karlsruhe Institute of
		   Technology},
  number	= {2012-8},
  year		= 2012,
  month		= aug,
  series	= {Karlsruhe Reports in Informatics},
  language	= {english},
  url		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000027497},
  urn		= {urn:nbn:de:swb:90-274973},
  license	= {http://creativecommons.org/licenses/by-nc-nd/3.0/},
  abstract	= {In this paper, we report on an ongoing case study in
		   which we use the {\KeY} tool, a theorem prover for checking
		   functional correctness and noninterference properties of
		   Java programs, to establish computational
		   indistinguishability for a simple Java program that
		   involves clients sending encrypted messages over an
		   untrusted network to a server. The analysis uses a general
		   framework, recently proposed by K{\"u}sters et al., which
		   enables program analysis tools, such as {\KeY}, that can
		   check (standard) noninterference properties for Java
		   programs to establish computational indistinguishability
		   properties.}
}