-- Signature

package javacard::security


-- static final
context Signature::getInstance(algorithm: JByte, 
                               externalAccess: Boolean): Signature
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()  
              = CryptoException.NO_SUCH_ALGORITHM
        )


-- abstract
context Signature::init(theKey: Key, theMode: JByte)
  pre : theKey <> null
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()  
              = CryptoException.ILLEGAL_VALUE
        )


-- abstract
context Signature::init(theKey: Key,
                        theMode: JByte,
                        bArray: Sequence(JByte),
                        bOff: JShort,
                        bLen: JShort)
  pre : theKey <> null
        and
        bArray->notEmpty()
        and
        bOff.asInt() >= 0
        and
        bLen.asInt() >= 0
        and
        bOff.asInt()+bLen.asInt() <= bArray->size()
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()  
              = CryptoException.ILLEGAL_VALUE
        )


-- abstract
context Signature::getAlgorithm(): JByte
  pre : true
  post: result.asInt() >= 1  -- self.ALG_DES_MAC4_NOPAD
        and
        result.asInt() <= 16  -- self.ALG_RSA_MD5_RFC2409


-- abstract
context Signature::getLength(): JShort
  pre : true
  post: true


-- abstract
context Signature::update(inBuff: Sequence(JByte),
                          inOffset: JShort,
                          inLength: JShort)
  pre : inBuff <> null
        and
        inOffset.asInt() >= 0
        and
        inLenght.asInt() >= 0
        and
        inOffset.asInt()+inLength.asInt() <= inBuff->size()
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.UNINITIALIZED_KEY
        )


-- abstract
context Signature::sign(inBuff: Sequence(JByte),
                        inOffset: JShort,
                        inLength: JShort,
                        sigBuff: Sequence(JByte),
                        sigOffset: JShort): JShort
  pre : inBuff <> null
        and
        sigBuff <> null
        and
        inOffset.asInt() >= 0
        and
        inLength.asInt() >= 0
        and
        sigOffset.asInt() >= 0
        and
        inOffset.asInt()+inLength.asInt() <= inBuff->size()
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           (
              CryptoException.systemInstance.getReason().asInt()  
                 = CryptoException.UNINITIALIZED_KEY
              or
              CryptoException.systemInstance.getReason().asInt()  
                 = CryptoException.INVALID_INIT
              or
              CryptoException.systemInstance.getReason().asInt()  
                 = CryptoException.ILLEGAL_USE
           )
        ) 


-- abstract
context Signature::verify(inBuff: Sequence(JByte),
                          inOffset: JShort,
                          inLength: JShort,
                          sigBuff: Sequence(JByte),
                          sigOffset: JShort,
                          sigLength: JShort): Boolean
  pre : inBuff <> null
        and
        sigBuff <> null
        and
        inOffset.asInt() >= 0
        and
        inLength.asInt() >= 0
        and
        sigOffset.asInt() >= 0
        and
        sigLength.asInt() >= 0
        and
        inOffset.asInt()+inLength.asInt() <= inBuff->size()
        and
        sigOffset.asInt()+sigLength.asInt() <= sigBuff->size()
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           (
              CryptoException.systemInstance.getReason().asInt() 
                 = CryptoException.UNINITIALIZED_KEY
              or
              CryptoException.systemInstance.getReason().asInt() 
                 = CryptoException.INVALID_INIT
              or
              CryptoException.systemInstance.getReason().asInt() 
                 = CryptoException.ILLEGAL_USE
           )
        )
  

endpackage