-- RSAPrivateKey extends PrivateKey


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 byte[] valueExponent;
--   private byte[] valueModulus;
--   private boolean isInitExponent;
--   private boolean isInitModulus;


context RSAPrivateKey def:
   let valueExponent: Sequence(JByte)
   let valueModulus: Sequence(JByte)
   let isInitExponent: Boolean
   let isInitModulus: Boolean


context RSAPrivateKey inv:
      self.isInitExponent
      and
      self.isInitModulus
   implies
      self.isInitialized()


context RSAPrivateKey::setModulus(buffer: Sequence(JByte),
                                  offset: JShort,
                                  length: JShort)
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        length.asInt() >= 0
        and
        offset.asInt()+length.asInt() <= buffer->size()
  post: (
           not excThrown(java::lang::Exception)
           and
           self.isInitModulus
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valueModulus, 0, buffer, 
                                                   offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()
              = CryptoException.ILLEGAL_VALUE
        )


context RSAPrivateKey::setExponent(buffer: Sequence(JByte),
                                   offset: JShort,
                                   length: JShort)
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        length.asInt() >= 0
        and
        offset.asInt()+length.asInt() <= buffer->size()
  post: (
           not excThrown(java::lang::Exception)
           and
           self.isInitExponent
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valueExponent, 0, buffer, 
                                              offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()
              = CryptoException.ILLEGAL_VALUE
        )


context RSAPrivateKey::getModulus(buffer: Sequence(JByte),
                                  offset: JShort): JShort
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        offset.asInt() < buffer->size()
        and
        self.isInitialized()
  post: result.asInt() = self.valueModulus->size()
        and
        Util.arrayCompare(self.valueModulus, 0, buffer, offset, 
                                       self.valueModulus->size()) = 0


context RSAPrivateKey::getExponent(buffer: Sequence(JByte),
                                   offset: JShort): JShort
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        offset.asInt() < buffer->size()
        and
        self.isInitialized()
  post: result.asInt() = self.valueExponent->size()
        and
        Util.arrayCompare(self.valueExponent, 0, buffer, offset, 
                                       self.valueExponent->size()) = 0


endpackage