A semantics and a calculi for reasoning about credential-based systems