-- interface DSAKey


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[] valueP;
--   private byte[] valueQ;
--   private byte[] valueG;
--   private boolean isInitP;
--   private boolean isInitQ;
--   private boolean isInitG;


context DSAKey def:
   let valueP: Sequence(JByte)
   let valueQ: Sequence(JByte)
   let valueG: Sequence(JByte)
   let isInitP: Boolean
   let isInitQ: Boolean
   let isInitG: Boolean


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


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


context DSAKey::getP(buffer: Sequence(JByte),
                     offset: JShort): JShort
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        offset.asInt() < buffer->size()
  post: result.asInt() = self.valueP->size()
        and
        Util.arrayCompare(self.valueP, 0, buffer, offset, 
                                       self.valueP->size()) = 0


context DSAKey::getQ(buffer: Sequence(JByte),
                     offset: JShort): JShort
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        offset.asInt() < buffer->size()
  post: result.asInt() = self.valueP->size()
        and
        Util.arrayCompare(self.valueQ, 0, buffer, offset, 
                                       self.valueQ->size()) = 0


context DSAKey::getG(buffer: Sequence(JByte),
                     offset: JShort): JShort
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        offset.asInt() < buffer->size()
  post: result.asInt() = self.valueG->size()
        and
        Util.arrayCompare(self.valueG, 0, buffer, offset, 
                                       self.valueG->size()) = 0


endpackage