-- Cipher


package javacardx::crypto


context Cipher def:
   let key: Key
   let mode: JByte
   let algorithm: JByte
   let initialized: Boolean = false


context Cipher::getInstance(algorithm: JByte, 
                            externalAccess: Boolean): Cipher
  pre : true
  post: (
           not excThrown(java::lang::Exception)
           and
           self.algorithm.asInt() = algorithm.asInt()
        )
        or
        (
           excThrown(javacard::security::CryptoException)
           and
           javacard::security::CryptoException.systemInstance.getReason()
              = javacard::security::CryptoException.NO_SUCH_ALGORITHM
        )


context Cipher::init(theKey: Key, theMode: JByte)
  pre : true
  post: (
           not excThrown(java::lang::Exception)
           and
           self.key = theKey
           and
           self.mode.asInt() = theMode.asInt()
           and
           self.initialized = true
        )
        or
        (
           excThrown(javacard::security::CryptoException)
           and
           javacard::security::CryptoException.systemInstance.getReason()
              = javacard::security::CryptoException.ILLEGAL_VALUE
        )


context Cipher::init(theKey: Key, 
                     theMode: JByte,
                     bArray: Sequence(JByte),
                     bOff: JShort,
                     bLen: JShort)
  pre : true
  post: (
           not excThrown(java::lang::Exception)
           and
           self.key = theKey
           and
           self.mode.asInt() = theMode.asInt()
           and
           self.initialized = true
        )
        or
        (
           excThrown(javacard::security::CryptoException)
           and
           javacard::security::CryptoException.systemInstance.getReason()
              = javacard::security::CryptoException.ILLEGAL_VALUE
        )


context Cipher::getAlgorithm(): JByte
  pre : true
  post: result = self.algorithm


context Cipher::update(inBuff: Sequence(JByte),
                       inOffset: JShort,
                       inLength: JShort,
                       outBuff: Sequence(JByte),
                       outOffset: JShort): JShort
  pre : true
  post: (
           not excThrown(java::lang::Exception)
        )
        or
        (
           excThrown(javacard::security::CryptoException)
           and
           (
              (
                 javacard::security::CryptoException.systemInstance.getReason()
                    = javacard::security::CryptoException.UNINITIALIZED_KEY
                 and
                 not self.key.isInitialized()
              )
              or
              (
                 javacard::security::CryptoException.systemInstance.getReason()
                    = javacard::security::CryptoException.INVALID_INIT
                 and
                 not self.initialized
              )
              or
              javacard::security::CryptoException.systemInstance.getReason()
                 = javacard::security::CryptoException.ILLEGAL_USE
           )
        )


context Cipher::doFinal(inBuff: Sequence(JByte),
                        inOffset: JShort,
                        inLength: JShort,
                        outBuff: Sequence(JByte),
                        outOffset: JShort): JShort
  pre : true
  post: (
           not excThrown(java::lang::Exception)
        )
        or
        (
           excThrown(javacard::security::CryptoException)
           and
           (
              (
                 javacard::security::CryptoException.systemInstance.getReason()
                    = javacard::security::CryptoException.UNINITIALIZED_KEY
                 and
                 not self.key.isInitialized()
              )
              or
              (
                 javacard::security::CryptoException.systemInstance.getReason()
                    = javacard::security::CryptoException.INVALID_INIT
                 and
                 not self.initialized
              )
              or
              javacard::security::CryptoException.systemInstance.getReason()
                 = javacard::security::CryptoException.ILLEGAL_USE
           )
        )


endpackage