-- OwnerPIN implements PIN


package javacard::framework


-- 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 maxPINSize;
--    private byte maxTries;
--    private boolean isValidated;
--    private byte triesRemaining;
--    private byte[] pin;



context OwnerPIN def:
   let maxPINSize: JByte
   let maxTries: JByte
   let isValidated: Boolean
   let triesRemaining: JByte
   let pin: Sequence(JByte)



context OwnerPIN inv:
   self.maxPINSize.asInt() > 0
   and
   self.maxTries.asInt() > 0
   and
   self.triesRemaining.asInt() >= 0
   and
   self.triesRemaining.asInt() <= self.maxTries.asInt()
   and
   self.pin <> null
   and
   self.pin->size() <= self.maxPINSize.asInt()



-- protected
context OwnerPIN::getValidatedFlag(): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        result = self.isValidated



-- protected
context OwnerPIN::setValidatedFlag(value: Boolean)
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        self.isValidated = value



context OwnerPIN::OwnerPIN(tryLimit: JByte, maxPINSize: JByte)
  pre : maxPINSize.asInt() > 0
        and
        tryLimit.asInt() > 0
  post: (
           not excThrown(java::lang::Exception)
           and
           self.maxPINSize.asInt() = maxPINSize.asInt()   
           and
           self.maxTries.asInt() = tryLimit.asInt()
           and
           self.triesRemaining.asInt() = tryLimit.asInt()
           and
           not self.isValidated
        )
        or
        (
           excThrown(PINException)
           and
           PINException.systemInstance.getReason().asInt()
              = PINException.ILLEGAL_VALUE
           and
           maxPINSize.asInt() < 1
        )
        or
        (
           excThrown(SystemException)
           and
           SystemException.systemInstance.getReason().asInt()
              = SystemException.NO_TRANSIENT_SPACE
        )
        

context OwnerPIN::update(pin: Sequence(JByte), offset: JShort, 
                         length: JByte)
  pre : pin <> null
        and
        offset.asInt() >= 0
        and
        offset.asInt()+length.asInt() <= pin->size()
        and
        length.asInt() >= 0
  post: (
           not excThrown(java::lang::Exception)
           and
           Util.arrayCompare(self.pin, 0, pin, offset, length) = 0
        ) 
        or
        (
           excThrown(PINException)
           and
           length.asInt() > self.maxPINSize
        )
        or
        (
           excThrown(TransactionException)
           and
           TransactionException.systemInstance.reason
              = TransactionException.BUFFER_FULL
        )


context OwnerPIN::resetAndUnblock()
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        not self.isValidated
        and
        self.triesRemaining = self.maxTries


context OwnerPIN::getTriesRemaining(): JByte
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        result.asInt() = self.triesRemaining


context OwnerPIN::isValidated(): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        result = self.isValidated


context OwnerPIN::reset()
  pre : self.isValidated
  post: not excThrown(java::lang::Exception)
        and
        not self.isValidated
        and
        self.triesRemaining = self.triesRemaining@pre


context OwnerPIN::check(pin: Sequence(JByte), 
                        offset: JShort,
                        length: JByte): Boolean
  pre : true
  post: if
           self.triesRemaining = 0
        then
           result = false
        endif
        and
        if
        (
           self.triesRemaining > 0
           and
           pin <> null
           and
           offset.asInt() >= 0
           and
           length.asInt() >= 0
           and
           offset.asInt()+length.asInt() <= pin->size()
           and
           Util.arrayCompare(self.pin, 0, pin, offset, length).asInt() = 0
        )
        then
        (
           result = true
           and
           self.isValidated
           and
           self.triesRemaining.asInt() = self.maxTries.asInt()
        )
        endif
        and
        if
        (
           self.triesRemaining.asInt() > 0
           and
           not
           (
              pin <> null
              and
              offset.asInt() >= 0
              and
              length.asInt() >= 0
              and
              offset.asInt()+length.asInt() <= pin->size()
              and
              Util.arrayCompare(self.pin, 0, pin, offset, length).asInt() = 0
           )
        )
        then
        (
           not self.isValidated
           and
           self.triesRemaining.asInt() = self.triesRemaining@pre.asInt()-1
           and
           (
              (
                 not excThrown(java::lang::Exception)
                 and
                 result = false
              )
              or
              excThrown(java::lang::NullPointerException)
              or
              excThrown(java::lang::ArrayIndexOutOfBoundsException)
           )
        )
        endif
  


endpackage