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

@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.}
}