DETAILED ACTION
This office action has been issued in response to communications received on 8/10/2026. Claims 1, 3-4, 7, 13-14 and 21-23 were amended. No new claims were added or cancelled. Claims 18-20 were previously cancelled in response to a restriction requirement. Claims 1-17 and 21-23 are presented for examination. The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA .
Response to Arguments
Applicant’s Remarks with respect to the rejection of the claims under 35 USC 103 have been considered, but are found unpersuasive.
Applicant’s arguments filed 8/10/2026, with respect to the rejection of the claims under 35 USC § 103(a) have been fully considered but are moot because newly added claim limitations requiring “the symbolic counterexample expression including abstract variables representing possible inputs to the RBAC policy; providing the satisfiability function representation to the satisfiability solver model to identify a counterexample having a set of values assigned to the abstract variables, the set of values specifying the RBAC policy and violating the validation property” require new grounds of rejection necessitated by amendments.
The remaining arguments fail to comply with 37 C.F.R. 1.111(b) because they amount to a general allegation that the claims define a patentable invention without specifically pointing out how the language of the claims patentably distinguishes them from the references.
Consequently, the rejection of the claims under 35 U.S.C. 103 is sustained.
Claim Rejections - 35 USC § 103
The following is a quotation of 35 U.S.C. 103 which forms the basis for all obviousness rejections set forth in this Office action:
A patent for a claimed invention may not be obtained, notwithstanding that the claimed invention is not identically disclosed as set forth in section 102 of this title, if the differences between the claimed invention and the prior art are such that the claimed invention as a whole would have been obvious before the effective filing date of the claimed invention to a person having ordinary skill in the art to which the claimed invention pertains. Patentability shall not be negated by the manner in which the invention was made.
The factual inquiries set forth in Graham v. John Deere Co., 383 U.S. 1, 148 USPQ 459 (1966), that are applied for establishing a background for determining obviousness under 35 U.S.C. 103 are summarized as follows:
1. Determining the scope and contents of the prior art.
2. Ascertaining the differences between the prior art and the claims at issue.
3. Resolving the level of ordinary skill in the pertinent art.
4. Considering objective evidence present in the application indicating obviousness or non-obviousness.
This application currently names joint inventors. In considering patentability of the claims the examiner presumes that the subject matter of the various claims was commonly owned as of the effective filing date of the claimed invention(s) absent any evidence to the contrary. Applicant is advised of the obligation under 37 CFR 1.56 to point out the inventor and effective filing dates of each claim that was not commonly owned as of the effective filing date of the later invention in order for the examiner to consider the applicability of 35 U.S.C. 102(b)(2)(C) for any potential 35 U.S.C. 102(a)(2) prior art against the later invention.
In the event the determination of the status of the application as subject to AIA 35 U.S.C. 102 and 103 (or as subject to pre-AIA 35 U.S.C. 102 and 103) is incorrect, any correction of the statutory basis for the rejection will not be considered a new ground of rejection if the prior art relied upon, and the rationale supporting the rejection, would be the same under either status.
Claims 1, 5-9, 13-16, and 21-23 are rejected under 35 U.S.C. 103 as being unpatentable over Goel (US 2025/0106256) in view of Hicks (US 20240179182).
Regarding claim 1, Goel discloses the limitations of claim 1 substantially as follows:
A computer-implemented method for validating role-based access control (RBAC) policies comprising:
identifying an RBAC policy and a validation property to validate an intended specification of the RBAC policy (paras. [0018]: identifying role-based access control policies that define and express security requirements for resources and properties of the policies to be validated);
generating a symbolic expression of the RBAC policy that violates the validation property using a symbolic abstraction model (paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the symbolic expression into a satisfiability function representation to be solved by a satisfiability solver model (paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on receiving [[a]] the counterexample from the satisfiability solver model, determining that the RBAC policy is invalid for the validation property (paras. [0072]-[0074]: receiving from the model/SMT solver a counterexample of the access control policy and determining that the property does not hold for all states (i.e. validation property and corresponding policy are invalid)).
Goel does not explicitly disclose the remaining limitations of claim 1 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model, the symbolic counterexample expression including abstract variables representing possible inputs to the RBAC policy;
providing the satisfiability function representation to the satisfiability solver model to identify a counterexample having a set of values assigned to the abstract variables, the set of values specifying the RBAC policy and violating the validation property;
However, in the same field of endeavor Hicks discloses the limitations of claim 1 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model, the symbolic counterexample expression including abstract variables representing possible inputs to the RBAC policy (paras. [0027], [0058], [0249]-[0252]: equivalence functions are generated comprising a policy to be evaluated including the negation of a policy that violates a property (i.e. counterexample), where the policies are symbolically evaluated using symbolic representations of a policy, request and store (i.e. including abstract variables representing possible inputs) and the policies include role-based access control rule/policy (i.e. inputs to RBAC))
providing the satisfiability function representation to the satisfiability solver model to identify a counterexample having a set of values assigned to the abstract variables, the set of values specifying the RBAC policy and violating the validation property (paras. [0027], [0058], [0243]-[0244], [0252]-[0254]: reducing the high-level RBAC policy expressions into SMT-LIB language (i.e. generating satisfiability function representation) and providing them to the Satisfiability Modulo Theory solver (I.e. satisfiability solver model) to check whether the negation of the desired property is unsatisfiable or satisfiable (i.e. identifying a counterexample that violates a validation property) and outputting if there is a concrete input for which the property fails to hold (i.e. set of values specify the RBAC policy and violating the validation property));
Hicks is combinable with Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Hick’s method of testing whether the negation of a desired property is unsatisfiable with the system of Goel in order to improve the accuracy of determining counterexamples by enabling testing their symbolic expressions in a SAT model to verify the validity of the error represented by the counterexample and refine the search process for additional counterexamples.
Regarding claim 5, Goel and Hicks disclose the limitations of claim 1.
Goel discloses the limitations of claim 5 as follows:
The computer-implemented method of claim 1, wherein the RBAC policy is part of a set of RBAC policies implemented by a cloud computing system to authorize access to resources of the cloud computing system (paras. [0017]-[0018], [0023]:role-based access control policies are implemented by a cloud network environment comprising cloud-based applications and authorizing access to resources of the environment).
Regarding claim 6, Goel and Hicks disclose the limitations of claim 1.
Goel discloses the limitations of claim 6 as follows:
The computer-implemented method of claim 1, wherein the symbolic abstraction model generates the symbolic counterexample expression into a common intermediate language that encodes semantics of multiple source languages (paras. [0016], [0020], [0054], [0058]: the policies are compiled into a unified policy language broad enough to include diverse policy features, yet specific enough for automated analysis).
Regarding claim 7, Goel and Hicks disclose the limitations of claim 1.
Hicks discloses the limitations of claim 7 as follows:
The computer-implemented method of claim 1, wherein the counterexample includes a user requirement input having the set of values (paras. [0027], [0058], [0243]-[0244], [0252]-[0254]: the equation provided to the SMT solver a request (i.e. user input) for the RBAC policy and checking whether the negation of the desired property is unsatisfiable or satisfiable comprises checking for a concrete input/user request (i.e. user requirement input having the set of values) for which the negation is true).
The same motivation to combine utilized in claim 1 is equally applicable in the instant claim.
Regarding claim 8, Goel and Hicks disclose the limitations of claims 1 and 7.
Goel discloses the limitations of claim 8 as follows:
The computer-implemented method of claim 7, wherein the user requirement input includes a principal value, an action value, and a scope value (paras. [0047]: access control policies specify the principal, and action and the resources impacted/scope).
Regarding claim 9, Goel and Hicks disclose the limitations of claims 1 and 7-8.
Goel discloses the limitations of claim 9 as follows:
The computer-implemented method of claim 8, wherein the user requirement input is provided to a cloud computing system to request access to a resource of the cloud computing system (paras. [0016], [0027], [0033], [0062], [0063], [0131]: requests by a user to access resources of cloud services/provider are subject to the access control policies).
Regarding claim 13, Goel and Hicks disclose the limitations of claim 1.
Goel and Hicks discloses the limitations of claim 13 as follows:
The computer-implemented method of claim 1, further comprising:
generating a second symbolic counterexample expression (Hicks, paras. [0027], [0058], [0249]-[0252]: equivalence functions are generated comprising a policy to be evaluated including the negation of a policy that violates a property (i.e. counterexample), where the policies are symbolically evaluated using symbolic representations of a policy, request and store (i.e. including abstract variables representing possible inputs) and the policies include role-based access control rule/policy (i.e. inputs to RBAC)) of the RBAC policy violating a second validation property using the symbolic abstraction model (Goel, paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the second symbolic counterexample expression (Hicks, paras. [0027], [0058], [0243]-[0244], [0252]-[0254]: reducing the high-level RBAC policy expressions into SMT-LIB language (i.e. generating satisfiability function representation) into a second satisfiability function representation to be solved by the satisfiability solver model (Goel, paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on failing to receive any counterexample from the satisfiability solver model, determining that the RBAC policy is valid for the second validation property (Goel, paras. [0072]-[0074]: based on not receiving a counterexample from the model/SMT solver, determining that the property holds true for all states (i.e. validation property and corresponding policy are valid)).
The same motivation to combine utilized in claim 1 is equally applicable in the instant claim.
Regarding claim 14, Goel discloses the limitations substantially as follows:
A system for validating role-based access control (RBAC) policies comprising:
a processing system; and
a computer memory comprising instructions that, when executed by the processing system, cause the system to perform operations of:
identifying an RBAC policy and a validation property to validate an intended specification of the RBAC policy (paras. [0018]: identifying role-based access control policies that define and express security requirements for resources and properties of the policies to be validated);
generating a symbolic expression of the RBAC policy that violates the validation property using a symbolic abstraction model (paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the symbolic expression into a satisfiability function representation to be solved by a satisfiability solver model (paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on receiving a counterexample from the satisfiability solver model, determining that the RBAC policy is invalid for the validation property (paras. [0072]-[0074]: receiving from the model/SMT solver a counterexample of the access control policy and determining that the property does not hold for all states (i.e. validation property and corresponding policy are invalid)).
Goel does not explicitly disclose the remaining limitations of claim 14 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model, the symbolic counterexample expression including abstract variables representing possible inputs to the RBAC policy;
providing the satisfiability function representation to the satisfiability solver model to identify a counterexample having a set of values assigned to the abstract variables, the set of values specifying the RBAC policy and violating the validation property;
However, in the same field of endeavor Hicks discloses the limitations of claim 14 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model, the symbolic counterexample expression including abstract variables representing possible inputs to the RBAC policy (paras. [0027], [0058], [0249]-[0252]: equivalence functions are generated comprising a policy to be evaluated including the negation of a policy that violates a property (i.e. counterexample), where the policies are symbolically evaluated using symbolic representations of a policy, request and store (i.e. including abstract variables representing possible inputs) and the policies include role-based access control rule/policy (i.e. inputs to RBAC))
providing the satisfiability function representation to the satisfiability solver model to identify a counterexample having a set of values assigned to the abstract variables, the set of values specifying the RBAC policy and violating the validation property (paras. [0027], [0058], [0243]-[0244], [0252]-[0254]: reducing the high-level RBAC policy expressions into SMT-LIB language (i.e. generating satisfiability function representation) and providing them to the Satisfiability Modulo Theory solver (I.e. satisfiability solver model) to check whether the negation of the desired property is unsatisfiable or satisfiable (i.e. identifying a counterexample that violates a validation property) and outputting if there is a concrete input for which the property fails to hold (i.e. set of values specify the RBAC policy and violating the validation property));
Hicks is combinable with Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Hick’s method of testing whether the negation of a desired property is unsatisfiable with the system of Goel in order to improve the accuracy of determining counterexamples by enabling testing their symbolic expressions in a SAT model to verify the validity of the error represented by the counterexample and refine the search process for additional counterexamples.
Regarding claim 15, Goel and Hicks disclose the limitations of claim 14.
Goel discloses the limitations of claim 15 as follows:
The system of claim 14, wherein the satisfiability solver model is a satisfiability modulo theories (SMT) solver (paras. [0072]-[0074] satisfiability solver model SMT solver).
Regarding claim 16, Goel and Hicks disclose the limitations of claim 14.
Goel discloses the limitations of claim 16 as follows:
The system of claim 14, wherein the satisfiability solver model utilizes Boolean, arithmetic, bit-vectors, arrays, or uninterpreted functions to solve the satisfiability function representation (paras. [0067], [0070], [0072]-[0074]: the quotiented target access control policies are converted into a logic-based representation which the satisfiability solver analyzes (using Boolean for logic) defining behaviors as theorems (i.e. uninterpreted functions)).
Regarding claim 21 Goel discloses the limitations substantially as follows:
A non-transitory computer-readable storage medium for validating role-based access control (RBAC) policies comprising, and comprising instructions that, when executed by a processor, cause a computing device to carry out operations comprising:
identifying an RBAC policy and a validation property to validate an intended specification of the RBAC policy (paras. [0018]: identifying role-based access control policies that define and express security requirements for resources and properties of the policies to be validated);
generating a symbolic expression of the RBAC policy that violates the validation property using a symbolic abstraction model (paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the symbolic expression into a satisfiability function representation to be solved by a satisfiability solver model (paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on receiving a counterexample from the satisfiability solver model, determining that the RBAC policy is invalid for the validation property (paras. [0072]-[0074]: receiving from the model/SMT solver a counterexample of the access control policy and determining that the property does not hold for all states (i.e. validation property and corresponding policy are invalid)).
Goel does not explicitly disclose the remaining limitations of claim 21 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model, the symbolic counterexample expression including abstract variables representing possible inputs to the RBAC policy;
providing the satisfiability function representation to the satisfiability solver model to identify a counterexample having a set of values assigned to the abstract variables, the set of values specifying the RBAC policy and violating the validation property;
However, in the same field of endeavor Hicks discloses the limitations of claim 21 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model, the symbolic counterexample expression including abstract variables representing possible inputs to the RBAC policy (paras. [0027], [0058], [0249]-[0252]: equivalence functions are generated comprising a policy to be evaluated including the negation of a policy that violates a property (i.e. counterexample), where the policies are symbolically evaluated using symbolic representations of a policy, request and store (i.e. including abstract variables representing possible inputs) and the policies include role-based access control rule/policy (i.e. inputs to RBAC))
providing the satisfiability function representation to the satisfiability solver model to identify a counterexample having a set of values assigned to the abstract variables, the set of values specifying the RBAC policy and violating the validation property (paras. [0027], [0058], [0243]-[0244], [0252]-[0254]: reducing the high-level RBAC policy expressions into SMT-LIB language (i.e. generating satisfiability function representation) and providing them to the Satisfiability Modulo Theory solver (I.e. satisfiability solver model) to check whether the negation of the desired property is unsatisfiable or satisfiable (i.e. identifying a counterexample that violates a validation property) and outputting if there is a concrete input for which the property fails to hold (i.e. set of values specify the RBAC policy and violating the validation property));
Hicks is combinable with Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Hick’s method of testing whether the negation of a desired property is unsatisfiable with the system of Goel in order to improve the accuracy of determining counterexamples by enabling testing their symbolic expressions in a SAT model to verify the validity of the error represented by the counterexample and refine the search process for additional counterexamples.
Regarding claim 22, Goel and Hicks disclose the limitations of claim 21.
Goel and Hicks discloses the limitations of claim 22 as follows:
The non-transitory computer-readable storage medium claim 21, wherein:
the counterexample includes a user requirement input having the set of values (Hicks, paras. [0027], [0058], [0243]-[0244], [0252]-[0254]: the equation provided to the SMT solver a request (i.e. user input) for the RBAC policy and checking whether the negation of the desired property is unsatisfiable or satisfiable comprises checking for a concrete input/user request (i.e. user requirement input having the set of values) for which the negation is true);
the user requirement input includes a principal value, an action value, and a scope value (Goel, paras. [0047]: access control policies specify the principal, and action and the resources impacted/scope); and
the user requirement input is provided to a cloud computing system to request access to a resource of the cloud computing system (Goel, paras. [0016], [0027], [0033], [0062], [0063], [0131]: requests by a user to access resources of cloud services/provider are subject to the access control policies).
The same motivation to combine utilized in claim 21 is equally applicable in the instant claim.
Regarding claim 23, Goel and Hicks disclose the limitations of claim 21.
Goel discloses the limitations of claim 23 as follows:
The non-transitory computer-readable storage medium claim 21, wherein the symbolic abstraction model generates the symbolic counterexample expression into a common intermediate language that encodes semantics of multiple source languages (paras. [0016], [0020], [0054], [0058]: the policies are compiled into a unified policy language broad enough to include diverse policy features, yet specific enough for automated analysis).
Claims 2-4, 10-12 and 17 are rejected under 35 U.S.C. 103 as being unpatentable over Goel (US 2025/0106256) in view of Hicks (US 20240179182), as applied to claims 1 and 14, further in view of Bolignano (US 11483317).
Regarding claim 2, Goel and Hicks disclose the limitations of claim 1.
Goel discloses the limitations of claim 2 as follows:
The computer-implemented method of claim 1, wherein the RBAC policy defines an effect, a principal, an action, (paras. [0018], [0047]-[0048]: components of an access control policy define include principals, actions, the outcome/effect -whether the action is allowed or denied).
Neither Goel or Hicks disclose a not-action, however in the same field of endeavor Bolignano discloses a non-action (col. 25, ll. 45-60: NotAction element would apply to all actions except those listed).
Bolignano is combinable with Hicks and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of using NonActions to define statements and matching elements with the system of Hicks and Goel in order to increase the flexibility of the system by enabling the system to specify policies or permissions that should be excluded.
Regarding claim 3, Goel, Hicks and Bolignano disclose the limitations of claims 1 and 2.
Goel discloses the limitations of claim 3 as follows:
The computer-implemented method of claim 2, wherein the RBAC policy defines a scope and a condition; and the effect is to deny or allow a request based on corresponding definitions being satisfied (paras. [0018], [0047]-[0048]: components of an access control policy define the resources the policy applies to (i.e. scope) and a condition and the outcome/effect -whether the action is allowed or denied).
Regarding claim 4, Goel, Hicks and Bolignano disclose the limitations of claims 1-2.
Hicks discloses the limitations of claim 4 as follows:
The computer-implemented method of claim 2, wherein the symbolic counterexample expression is converted into the satisfiability function representation using the symbolic abstract model (paras. [0027], [0058], [0243]-[0244], reducing the high-level symbolic RBAC policy expressions into SMT-LIB language (i.e. generating satisfiability function representation).
It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Hick’s method of converting the policy expressions into SMT-LIB language with the system of Goel and Bolignano in order to enable the system to provide the policies in a format understood by the SMT policy evaluator.
Regarding claim 10, Goel and Hicks disclose the limitations of claim 1.
Neither Goel or Hicks disclose the limitations of claim 10, however in the same field of endeavor, Bolignano discloses the limitations of claim 10 as follows:
The computer-implemented method of claim 1, further comprising modifying the RBAC policy to disallow the counterexample based on determining that the RBAC policy is vulnerable to allowing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: modifying the security policy/requirement specifying a user’s access rights based upon their role (i.e. RBAC policy) to prevent an event detected as leading to a counterexample from reoccurring based upon receiving a notification that the security requirement was violated (i.e. that the policy is vulnerable to being violated).
Bolignano does not explicitly disclose that the policy is modified in order to prevent the counterexample from being triggered but it would have been obvious to one of ordinary skill in the art that Bolignano discloses such functionality because Bolignano discloses the security policy may be deleted or changed after receiving a notification that a current security requirement was violated by a counter-example, therefore one of ordinary skill in the art would have found it obvious that the proposed change could be use the information from the notification to revise the security policy to prevent the violation from reoccurring.
Bolignano is combinable with Hicks and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of changing or deleting a security policy to prevent reoccurrence of a violation of the security policy with the system of Hicks and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Regarding claim 11, Goel and Hicks disclose the limitations of claim 1.
Neither Goel or Hicks disclose the limitations of claim 11, however in the same field of endeavor, Bolignano discloses the limitations of claim 11 as follows:
The computer-implemented method of claim 1, further comprising removing the RBAC policy based on determining that the RBAC policy is vulnerable to allowing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: deleting the security policy/requirement specifying a user’s access rights based upon their role (i.e. RBAC policy) to prevent an event detected as leading to a counterexample from reoccurring based upon receiving a notification that the security requirement was violated (i.e. that the policy is vulnerable to being violated).
Bolignano does not explicitly disclose that the policy is deleted in order to prevent the counterexample from being triggered but it would have been obvious to one of ordinary skill in the art that Bolignano discloses such functionality because Bolignano discloses the security policy may be deleted or changed after receiving a notification that a current security requirement was violated by a counter-example, therefore one of ordinary skill in the art would have found it obvious that the proposed deletion could be use the information from the notification to revise the security policy to prevent the violation from reoccurring.
Bolignano is combinable with Hicks and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of changing or deleting a security policy to prevent reoccurrence of a violation of the security policy with the system of Hicks and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Regarding claim 12, Goel and Hicks disclose the limitations of claim 1.
Neither Goel or Hicks disclose the limitations of claim 12, however in the same field of endeavor, Bolignano discloses the limitations of claim 12 as follows:
The computer-implemented method of claim 1, further comprising flagging the RBAC policy for review based on determining that the RBAC policy is vulnerable to performing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: sending the administrator a notification about a security policy/requirement specifying a user’s access rights based upon their role (i.e. RBAC policy) which has been violated (i.e. flatting the RBAC policy for review) based on determining that a counter-example violation of the policy has occurred (i.e. it is vulnerable to adverse actions)).
Bolignano is combinable with Hicks and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of changing or deleting a security policy to prevent reoccurrence of a violation of the security policy with the system of Hicks and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Regarding claim 17, Goel and Hicks disclose the limitations of claim 14.
Neither Goel or Hicks disclose the limitations of claim 17, however in the same field of endeavor, Bolignano discloses the limitations of claim 17 as follows:
The system of claim 14, wherein determining that the RBAC policy is invalid for the validation property includes determining that the RBAC policy is vulnerable to allowing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: receiving a notification with a counter-example indicating that the security policy was violated (i.e. determining that the policy needs to be amended because it is vulnerable to being violated) and proposing to change or delete a security policy).
Bolignano does not explicitly disclose that the policy is determined to be invalid (i.e. in need of being changed or deleted) based upon the notification, but it would have been obvious to one of ordinary skill in the art that Bolignano discloses such functionality because Bolignano discloses receiving notifications when a security policy has been violated, therefore it would be obvious to one of ordinary skill in the art that an administrator receiving multiple notifications about a particular security policy always being violated would determine that security policy needs to be either changed or replaced (i.e. because the policy is invalid).
Bolignano is combinable with Hicks and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of providing notifications of violations of security policies and enabling changing or deleting a security policy with the system of Hicks and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Prior art not relied upon but applied/considered includes:
1) Ganai (US 2010/0305919) disclosing A method for symbolic model checking of sequential systems includes alternating between state-based and state-less symbolic model checking methods by combining a Presburger-based Symbolic technique (state-based), and SMT-based Bounded Model Checking (stateless) in a tightly integrated tool called a HMC (Hybrid Model Checker). A state-based approach such as MIX model checking may be employed to compute a reachable state set in a breadth-first search (BFS) up to some depth. With each partition S.sub.p as the state constraint at depth d, we use satisfiability modulo theories (SMT)-based bounded model checking (BMC) from the depth d to check if error blocks can be reached or show that termination is reached. Using the set S.sub.p as a state constraint depth d, starting BMC depth d, we invoke SMT-based BMC to check for counter-examples (CEX) for the error blocks E in block 29. If we find CEX, we update the set E. In block 30, if all error blocks are reached i.e. |E|=0, we stop in block 38. If for the input state constraint S.sub.p, we reach the completeness threshold, i.e., we explored all the paths, we return "termination reached" status. Otherwise, we return when a predetermined resource is exhausted. we consider symbolic formulas with Boolean expressions bool-expr and integer term expressions int-expr in Presburger arithmetic, a decidable subset of first-order theory. (paras. [0008], [0020], [0021], [0038], [0053]).
Conclusion
For the above reasons, claims 1-17 and 21-23 are rejected.
THIS ACTION IS MADE FINAL. Applicant is reminded of the extension of time policy as set forth in 37 CFR 1.136(a).
A shortened statutory period for reply to this final action is set to expire THREE MONTHS from the mailing date of this action. In the event a first reply is filed within TWO MONTHS of the mailing date of this final action and the advisory action is not mailed until after the end of the THREE-MONTH shortened statutory period, then the shortened statutory period will expire on the date the advisory action is mailed, and any nonprovisional extension fee (37 CFR 1.17(a)) pursuant to 37 CFR 1.136(a) will be calculated from the mailing date of the advisory action. In no event, however, will the statutory period for reply expire later than SIX MONTHS from the mailing date of this final action.
Any inquiry concerning this communication or earlier communications from the examiner should be directed to SHARON S LYNCH whose telephone number is (571)272-4583. The examiner can normally be reached on 10AM-6PM.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, Taghi T Arani can be reached on 571-272-3787. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300.
Information regarding the status of an application may be obtained from the Patent Application Information Retrieval (PAIR) system. Status information for published applications may be obtained from either Private PAIR or Public PAIR. Status information for unpublished applications is available through Private PAIR only. For more information about the PAIR system, see http://pair-direct.uspto.gov. Should you have questions on access to the Private PAIR system, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative or access to the automated information system, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000.
/SHARON S LYNCH/Primary Examiner, Art Unit 2438
