View the KIV projects

For some of the projects done with the KIV system we provide XML representations of the specifications, theorems and proofs. The project pages can be viewed with most modern web browsers. Best view is provided when using Firefox 2.0, Internet Explorer may have some problems displaying unicode characters for logical symbols.
Collection of projects dealing with the Mondex Case Study:

A complete list of all projects for the Mondex case study can be found on this site .

Some selected Mondex projects are:

Improved version of the Mondex case study using ASM Refinement (that avoids denial of service attack)
The Mondex case study using ASM Refinement (including libraries for ASM Refinement)
The Mondex case study using Data Refinement (including libraries for data refinement)
A correct implementation of the Mondex Case Study in JavaCard with Refinement Proof (Web Presentation of accepted paper for FM 08)
A Concept-Driven Construction of the Mondex protocol using Three Refinements (Web Presentation of accepted paper at ABZ 08)
A generic theory for refining atomic actions into protocols (Web Presentation of KIV specifications providing formal definitions for a FAC submission)

We also provide reference implementations for the case study. They can be found here . Other currently available projects:

The basic KIV library with basic data types
Extensions to the KIV library with additional data types
The Java Verification project
Formal Java Semantics. This specification is part of the dissertation Verification of Java Card Programs

ASN1-light: A Verified Message Encoding for security protocols

The electronic wallet (E-WALLET) case study.

E-Wallet: The electronic wallet (E-WALLET) with an arbitrary number of cardlets and terminals. All proofs included.

E-Wallet-V2:The specification of the E-Wallet case study based on PROSECCO-lib.

CINDY case study: Cinema tickets on your mobile. The development graph of the projects is on this page. The protocol ASM, i.e. the core of the application model, is defined in the specification CINDY. Security properties can be found in the specifications security and user-bill-OK.

CINDY refinement to a Java program.

PROSECCO-lib: The basic library for modeling Smart Card applications in PROSECCO.

An algebraic theory of messages. Used in the verification of cryptographic protocols.

Generic Java documents. They are a Java representation of abstract documents to exchange messages. They are used in the CINDY refinement case study (see above).

A formalisation of relational concurrent refinement. This is a version of data refinement where data types have external and internal operations. Operations may be blocked and sets of blocked operations are used as final observations (refusals). The possibility of an infinite run of internal operations is interpreted as divergence. This allows to prove that data refinement for such data types coincides with failures-divergence refinement in CSP. More information is given in the paper on which this case study is based (cited in the case study).

Completeness proofs for ASM Refinement and for IO Automata refinement (Web Presentation for Refinement Workshop at FM 08)

Completeness proofs for Fair ASM Refinement (Web Presentation for FACS Special Issue of Refinement Workshop at FM 08)

All xml files in these projects are generated automatically, but not at the same time. Since projects may depend on other projects, the following situation may occur: A theorem in project A uses a theorem from project B, but the link to this theorem is dead. This does not mean that the project is inconsistent, but simply that this documentation is not up-to-date.