-- interface DESKey extends SecretKey


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.
--
--    // The data that constitutes the actual key
--    private byte[] data;


context DESKey::setKey(keyData: Sequence(JByte), kOff: JShort)
  pre : not (keyData = null)
        and
        kOff.asInt() >= 0
        and
        kOff.asInt() < keyData->size()
  post: (
           not excThrown(java::lang::Exception)
           and
           self.isInitialized()
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.data, 0, keyData, kOff, 
                                               self.getSize()/8) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()
              = CryptoException.ILLEGAL_VALUE
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 kOff.asInt() + self.getSize()/8 > keyData->size()
           )
        )


context DESKey::getKey(keyData: Sequence(JByte), kOff: JShort): JByte
  pre : keyData <> null
        and
        kOff.asInt() >= 0
        and
        kOff.asInt() < keyData->size()
        and
        self.isInitialized()
  post: result = self.getSize()/8
        and
        Util.arrayCompare(self.data, 0, keyData, kOff, self.getSize()/8) = 0



endpackage