-- KeyPair


package javacard::security


-- PRIVATE FIELDS
-- The variables below are not part of the informal specification given by SUN.
-- They are given a name, a type and a meaning that reflects a part of the 
-- system state, in order to be able to make a meaningful specification. An 
-- implementer of this class is naturally free to represent the system state 
-- with the help of other class and instance fields.
--
--   private PrivateKey privateKey;
--   private PublicKey publicKey;


context KeyPair def:
   let privateKey: PrivateKey
   let publicKey: PublicKey


-- final
context KeyPair::genKeyPair()
  pre : true
  post: (
           not excThrown(java::lang::Exception)
           and
           privateKey <> null
           and
           publicKey <> null
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()
              = CryptoException.ILLEGAL_VALUE
        )


context KeyPair::KeyPair(algorithm: JByte, keyLength: JShort)
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()
              = CryptoException.NO_SUCH_ALGORITHM
        )


context KeyPair::KeyPair(publicKey: PublicKey, privateKey: PrivateKey)
  pre : publicKey <> null
        and
        privateKey <> null
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           (
              CryptoException.systemInstance.getReason().asInt()
                 = CryptoException.NO_SUCH_ALGORITHM
              or
              CryptoException.systemInstance.getReason().asInt()
                 = CryptoException.ILLEGAL_VALUE
           )
        )


-- Why not: result = self.publicKey?
context KeyPair::getPublic(): PublicKey
  pre : true
  post: self.privateKey = self.privateKey@pre
        and
        self.publicKey = self.publicKey@pre


-- Why not: result = self.privateKey?
context KeyPair::getPrivate(): PrivateKey
  pre : true
  post: self.privateKey = self.privateKey@pre
        and
        self.publicKey = self.publicKey@pre


endpackage