Formal specification of Gemplus' electronic purse case study
N. Cataño,
M. Huisman
In the proceedings of Formal Methods Europe (FME 2002), to appear.
Number 2391 of LNCS, pages 272-289. Springer-Verlag, 2002.
© Springer-Verlag
The annotations are constructed by Néstor Cataño and Marieke Huisman.
This work is done as part of the VerifiCard project at INRIA.
| Filename | Remarks |
| Annee | |
| Decimal |
Post conditions of isGreaterThan and isSmallerThan
cannot be established, needs reformulation of postconditions
of equal Several postconditions commented out, because of simplify error |
| DecimalException | |
| Jour | Mois |
| PacapException |
| Filename | Remarks |
| PurseLoyaltyInterface | |
| TransactionInterface |
| Filename | Remarks |
| AccessCondition | ESC/Java cannot establish that the invariant is preserved by method addCondition |
| AccessConditionException | |
| AccessControl | |
| AccessControlTable | We can not fully specify the postcondition of the method verify |
| AllowedLoyalty | Postcondition of delSaler can not be established by ESC/Java |
| AllowedLoyaltyException | |
| Currencies | |
| Date | Explicit assumption needed in method getDate on array length in JavaCard |
| DateException | |
| ExchangeRecord |
- ESC/Java can not establish that addExchangeSession preserves invariant - ESC/Java can not establish that precondition of clone is satisfied in defrag, because we can not express that arrays are referenced to only once - ESC/Java can not establish that defrag preserves invariant - ESC/Java can not establish postconditions of prevIndex and nextIndex |
| ExchangeSession | |
| Heure | Explicit assumption needed in method getHeure on offset in array |
| HeureException | |
| LoyaltiesTable |
- ESC/Java can not establish postcondition of delLoyalty - ESC/Java can not establish postcondition of getAllowedLoyalty - ESC/Java can not establish postcondition of removeNotification - ESC/Java can not establish postcondition of contents |
| LoyaltiesTableException | |
| LoyaltyInterfaceObject | Uses javacardx.crypto.Cipher.spec and visa.openplatform.OPSystem.spec |
| PacapCertificate |
Light weight specification Assumptions needed for ESC/Java that casting an array length to a short preserves that the value is >= 0 |
| PacapCipher |
- Light weight specification - Uses javacardx.crypto.Cipher.spec - Precondition of call to Util.arrayFillNonAtomic cannot be established by ESC/Java |
| PacapKey | Light weight specification |
| PacapRandom | Light weight specification |
| PacapSecureMessaging |
- Light weight specification - Assumptions needed for ESC/Java that casting an array length to a short preserves that the value is >= 0 |
| PacapSignature |
- Light weight specification - Preconditions of Util.arrayFillNonAtomic, instance.sign and instance.verify in methods sign and verify cannot be established by ESC/Java |
| PartnerID | |
| Purse |
- Light weight specification - Uses javacardx.crypto.Cipher.spec and visa.openplatform.OPSystem.spec - Several specifications not completely checked, because too much time required |
| PurseApplet |
- Light weight specification - Uses visa.openplatform.OPSystem.spec - Several specifications not completely checked, because too much time required |
| SalerID | |
| Security |
- Light weight specification - Uses javacardx.crypto.Cipher.spec and visa.openplatform.OPSystem.spec - Several specifications not completely checked, because too much time required |
| Transaction | |
| TransactionInterfaceObject | |
| TransactionRecord |
- ESC/Java can not establish that addTransaction preserves invariant - ESC/Java can not establish that precondition of clone is satisfied in defrag, because we can not express that arrays are referenced to only once - ESC/Java can not establish that defrag preserves invariant - ESC/Java can not establish postconditions of prevIndex and nextIndex - No postcondition specified for getTransaction and getNbTransactions |