-- SecurityService extends Service



package javacard::framework::service



context SecurityService::isAuthenticated(principal: JShort): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(ServiceException)
           and
           ServiceException.systemInstance.getReason().asInt()
              = ServiceException.ILLEGAL_PARAM
           and
           principal.asInt() <> SecurityService.PRINCIPAL_CARDHOLDER
           and
           principal.asInt() <> SecurityService.PRINCIPAL_CARD_ISSUER
           and
           principal.asInt() <> SecurityService.PRINCIPAL_APP_PROVIDER
        )



context SecurityService::isChannelSecure(properties: JByte): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(ServiceException)
           and
           ServiceException.systemInstance.getReason().asInt()
              = ServiceException.ILLEGAL_PARAM
           and
           properties.asInt() 
              <> SecurityService.PROPERTY_INPUT_CONFIDENTIALITY
           and
           properties.asInt() <> SecurityService.PROPERTY_INPUT_INTEGRITY
           and
           properties.asInt() 
              <> SecurityService.PROPERTY_OUTPUT_CONFIDENTIALITY
           and
           properties.asInt() <> SecurityService.PROPERTY_OUTPUT_INTEGRITY
        )



context SecurityService::isCommandSecure(properties: JByte): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(ServiceException)
           and
           ServiceException.systemInstance.getReason().asInt()
              = ServiceException.ILLEGAL_PARAM
           and
           properties.asInt() 
              <> SecurityService.PROPERTY_INPUT_CONFIDENTIALITY
           and
           properties.asInt() <> SecurityService.PROPERTY_INPUT_INTEGRITY
           and
           properties.asInt() 
              <> SecurityService.PROPERTY_OUTPUT_CONFIDENTIALITY
           and
           properties.asInt() <> SecurityService.PROPERTY_OUTPUT_INTEGRITY
        )



endpackage