A computer-implemented method for real-time evaluation of a reverse query to an attribute-based access control policy, ABAC policy, which is enforced to control access to one or more resources in a computer network, said method comprising the steps of: i) receiving a reverse query indicating a given decision (d), which is one of permit access and deny access, and a subset of access requests, which is defined by constraints over the set of possible access requests; ii) constructing a partial request (r partial) as a representation of the subset of access requests, by specifying at least one conditional expression on at least one attribute, thereby restricting possible values of the attribute; iii) reducing the ABAC policy in accordance with the partial request; iv) caching the policy after said reducing, as a simplified policy (P'); v) translating the cached simplified policy (P') and the given decision (d) into a satisfiable logic proposition in Boolean variables (v i, i = 1, 2,...) by either representing at least part of the simplified policy (P') as a binary decision diagram or representing the simplified policy (P') with a tree structure, wherein, whenever a sub-tree in the simplified policy represents a Boolean expression that compares an attribute with a fixed value and/or a Boolean expression having at least one child evaluating to a non-Boolean value, said sub-tree is replaced by a variable (v i); and vi) deriving all variable assignments (c j = [v 1 = x j1, v 2 = x j2,...], j = 1, 2,...) satisfying the logic proposition, in case the simplified policy (P') is represented as a binary decision diagram, by deriving all paths in the binary decision diagram evaluating to either true or false, or, in case the simplified policy (P') is represented as a tree structure, by means of a SAT solver, wherein a sequence ([c 1,..., c k]) of conditions are yielded, each of which corresponds to a variable assignment satisfying the logic proposition; converting the sequence of conditions into a set of valid requests, which are contained in the subset and evaluate to the given decision, or into at least one comparison between an attribute and a fixed value, wherein the comparison is in agreement with the subset of access requests. i) receiving a reverse query indicating a given decision (d), which is one of permit access and deny access, and a subset of access requests, which is defined by constraints over the set of possible access requests; ii) constructing a partial request (r partial) as a representation of the subset of access requests, by specifying at least one conditional expression on at least one attribute, thereby restricting possible values of the attribute; iii) reducing the ABAC policy in accordance with the partial request; iv) caching the policy after said reducing, as a simplified policy (P'); v) translating the cached simplified policy (P') and the given decision (d) into a satisfiable logic proposition in Boolean variables (v i, i = 1, 2,...) by either representing at least part of the simplified policy (P') as a binary decision diagram or representing the simplified policy (P') with a tree structure, wherein, whenever a sub-tree in the simplified policy represents a Boolean expression that compares an attribute with a fixed value and/or a Boolean expression having at least one child evaluating to a non-Boolean value, said sub-tree is replaced by a variable (v i); and vi) deriving all variable assignments (c j = [v 1 = x j1, v 2 = x j2,...], j = 1, 2,...) satisfying the logic proposition, in case the simplified policy (P') is represented as a binary decision diagram, by deriving all paths in the binary decision diagram evaluating to either true or false, or, in case the simplified policy (P') is represented as a tree structure, by means of a SAT solver, wherein a sequence ([c 1,..., c k]) of conditions are yielded, each of which corresponds to a variable assignment satisfying the logic proposition;