Sciweavers

Share
FAC
2008

Verification of Mondex electronic purses with KIV: from transactions to a security protocol

11 years 5 months ago
Verification of Mondex electronic purses with KIV: from transactions to a security protocol
The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results. First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study. Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework ning such protocols based on abstract state machines (ASMs). ...
Dominik Haneberg, Gerhard Schellhorn, Holger Grand
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where FAC
Authors Dominik Haneberg, Gerhard Schellhorn, Holger Grandy, Wolfgang Reif
Comments (0)
books