-- RSAPrivateCrtKey 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[] valueDP1;
--   private byte[] valueDQ1;
--   private byte[] valueP;
--   private byte[] valuePQ;
--   private byte[] valueQ;
--   private boolean isInitDP1;
--   private boolean isInitDQ1;
--   private boolean isInitP;
--   private boolean isInitPQ;
--   private boolean isInitQ;


context RSAPrivateCrtKey def:
   let valueDP1: Sequence(JByte)
   let valueDQ1: Sequence(JByte)
   let valueP: Sequence(JByte)
   let valuePQ: Sequence(JByte)
   let valueQ: Sequence(JByte)
   let isInitDP1: Boolean
   let isInitDQ1: Boolean
   let isInitP: Boolean
   let isInitPQ: Boolean
   let isInitQ: Boolean


context RSAPrivateCrtKey inv:
      self.isInitDP1
      and
      self.isInitDQ1
      and
      self.isInitP
      and
      self.isInitPQ
      and
      self.isInitQ
   implies
      self.isInitialized()


context RSAPrivateCrtKey::setP(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.isInitP
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valueP, 0, buffer, offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.ILLEGAL_VALUE
        )


context RSAPrivateCrtKey::setQ(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
           isInitQ
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.ILLEGAL_VALUE
        )


context RSAPrivateCrtKey::setDP1(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.isInitDP1
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valueDP1, 0, buffer, offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.ILLEGAL_VALUE
        )


context RSAPrivateCrtKey::setDQ1(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.isInitDQ1
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valueDQ1, 0, buffer, offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.ILLEGAL_VALUE
        )


context RSAPrivateCrtKey::setPQ(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.isInitPQ
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valuePQ, 0, buffer, offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.ILLEGAL_VALUE
        )


context RSAPrivateCrtKey::getP(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.valueP->size()
        and
        Util.arrayCompare(self.valueP, 0, buffer, offset, 
                                       self.valueP->size()) = 0


context RSAPrivateCrtKey::getQ(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.valueQ->size()
        and
        Util.arrayCompare(self.valueQ, 0, buffer, offset, 
                                       self.valueQ->size()) = 0


context RSAPrivateCrtKey::getDP1(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.valueDP1->size()
        and
        Util.arrayCompare(self.valueDP1, 0, buffer, offset, 
                                       self.valueDP1->size()) = 0


context RSAPrivateCrtKey::getDQ1(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.valueDQ1->size()
        and
        Util.arrayCompare(self.valueDQ1, 0, buffer, offset, 
                                       self.valueDQ1->size()) = 0


context RSAPrivateCrtKey::getPQ(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.valuePQ->size()
        and
        Util.arrayCompare(self.valuePQ, 0, buffer, offset, 
                                       self.valuePQ->size()) = 0


endpackage