diff --git a/Cargo.lock b/Cargo.lock
index b5fb23d4a..05e0e522b 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -9646,6 +9646,7 @@ dependencies = [
  "jsonwebtoken",
  "moka",
  "pollster",
+ "proptest",
  "regex",
  "reqwest",
  "rustfs-config",
diff --git a/crates/policy/Cargo.toml b/crates/policy/Cargo.toml
index 0239baeb6..cf1bea10f 100644
--- a/crates/policy/Cargo.toml
+++ b/crates/policy/Cargo.toml
@@ -52,6 +52,7 @@ pollster.workspace = true
 
 [dev-dependencies]
 pollster.workspace = true
+proptest = "1"
 test-case.workspace = true
 temp-env = { workspace = true }
 
diff --git a/crates/policy/tests/policy_eval_proptest.rs b/crates/policy/tests/policy_eval_proptest.rs
new file mode 100644
index 000000000..6ca75e0fc
--- /dev/null
+++ b/crates/policy/tests/policy_eval_proptest.rs
@@ -0,0 +1,208 @@
+// Copyright 2024 RustFS Team
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+//! Property tests for the IAM policy evaluation algebra (backlog#1151 sec-9).
+//!
+//! The wildcard Action/Resource matching and Deny-first evaluation in
+//! `Policy::is_allowed` were guarded only by example-based tests. These
+//! properties pin the three algebraic invariants that authorization safety
+//! rests on, over generated inputs:
+//!
+//!   (a) an explicit Deny matching the request denies it REGARDLESS of how many
+//!       Allow statements co-exist or where the Deny sits in the statement list;
+//!   (b) a wildcard Allow superset (`s3:*` on `bucket/*`) implies every narrower
+//!       concrete Allow: any request allowed by an exact-action/exact-resource
+//!       policy is also allowed by the widened policy;
+//!   (c) an empty policy denies every non-owner request (default deny).
+//!
+//! Pure evaluation: no IO, no global state, parallel-safe. Statements are built
+//! from JSON exactly like production policies arriving via PutPolicy. Generated
+//! bucket/key/action pools avoid wildcard metacharacters so resource patterns
+//! stay exact; the wildcard forms under test are introduced deliberately by the
+//! properties themselves.
+
+use proptest::prelude::*;
+use rustfs_policy::policy::{Args, Policy};
+use serde_json::Value;
+use std::collections::HashMap;
+
+/// Object-level S3 actions safe to pair with an `arn:aws:s3:::<bucket>/<key>`
+/// resource. Kept to real, parseable action names.
+const OBJECT_ACTIONS: &[&str] = &[
+    "s3:GetObject",
+    "s3:PutObject",
+    "s3:DeleteObject",
+    "s3:GetObjectTagging",
+    "s3:PutObjectTagging",
+];
+
+fn statement_json(effect: &str, action: &str, resource: &str) -> String {
+    format!(r#"{{"Effect":"{effect}","Action":["{action}"],"Resource":["{resource}"]}}"#)
+}
+
+fn policy_from_statements(statements: &[String]) -> Policy {
+    let json = format!(r#"{{"Version":"2012-10-17","Statement":[{}]}}"#, statements.join(","));
+    serde_json::from_str(&json).expect("generated policy JSON should parse")
+}
+
+fn is_allowed(policy: &Policy, action: &str, bucket: &str, object: &str) -> bool {
+    let conditions: HashMap<String, Vec<String>> = HashMap::new();
+    let claims: HashMap<String, Value> = HashMap::new();
+    let groups: Option<Vec<String>> = None;
+    pollster::block_on(policy.is_allowed(&Args {
+        account: "PROPTESTUSER",
+        groups: &groups,
+        action: action.try_into().expect("action from the fixed pool should parse"),
+        bucket,
+        conditions: &conditions,
+        is_owner: false,
+        object,
+        claims: &claims,
+        deny_only: false,
+    }))
+}
+
+/// Strategy: a bucket name without wildcard metacharacters.
+fn bucket_strategy() -> impl Strategy<Value = String> {
+    "[a-z][a-z0-9]{2,7}"
+}
+
+/// Strategy: an object key (optionally nested one level) without metacharacters.
+fn key_strategy() -> impl Strategy<Value = String> {
+    "[a-z0-9]{1,12}(/[a-z0-9]{1,12})?"
+}
+
+/// Strategy: one action name from the object-action pool.
+fn action_strategy() -> impl Strategy<Value = &'static str> {
+    proptest::sample::select(OBJECT_ACTIONS)
+}
+
+proptest! {
+    /// (a) Deny anywhere wins: a Deny statement matching the request denies it,
+    /// no matter how many broad Allow statements surround it or at which index
+    /// it appears. A regression here (e.g. Allow short-circuiting before the
+    /// Deny scan, or statement order leaking into the decision) is privilege
+    /// escalation.
+    #[test]
+    fn explicit_deny_anywhere_denies(
+        bucket in bucket_strategy(),
+        key in key_strategy(),
+        action in action_strategy(),
+        allow_count in 0usize..4,
+        deny_pos_seed in 0usize..16,
+        broad in proptest::bool::ANY,
+    ) {
+        // Broad Allow statements that all match the request on their own.
+        let allow_resource = if broad {
+            "arn:aws:s3:::*".to_string()
+        } else {
+            format!("arn:aws:s3:::{bucket}/*")
+        };
+        let mut statements: Vec<String> = (0..allow_count)
+            .map(|_| statement_json("Allow", "s3:*", &allow_resource))
+            .collect();
+
+        // One Deny that matches the exact request.
+        let deny = statement_json("Deny", action, &format!("arn:aws:s3:::{bucket}/{key}"));
+        let deny_pos = deny_pos_seed % (statements.len() + 1);
+        statements.insert(deny_pos, deny);
+
+        let policy = policy_from_statements(&statements);
+
+        // Sanity: without the Deny, the Allows (when present) do allow.
+        if allow_count > 0 {
+            let mut allows_only = statements.clone();
+            allows_only.remove(deny_pos);
+            let allow_policy = policy_from_statements(&allows_only);
+            prop_assert!(
+                is_allowed(&allow_policy, action, &bucket, &key),
+                "sanity: the Allow statements alone should permit {action} on {bucket}/{key}"
+            );
+        }
+
+        prop_assert!(
+            !is_allowed(&policy, action, &bucket, &key),
+            "explicit Deny at index {deny_pos} of {} statements must deny {action} on {bucket}/{key}",
+            statements.len()
+        );
+    }
+
+    /// (b) Wildcard superset implies the narrower concrete match: if an
+    /// exact-action / exact-resource Allow permits a request, then widening
+    /// that policy to `s3:*` on `arn:aws:s3:::<bucket>/*` (and further to
+    /// `*` on `arn:aws:s3:::*`) must also permit it. A regression here means
+    /// wildcard grants silently stop covering what their concrete forms cover.
+    #[test]
+    fn wildcard_superset_implies_concrete_match(
+        bucket in bucket_strategy(),
+        key in key_strategy(),
+        action in action_strategy(),
+        probe_bucket in bucket_strategy(),
+        probe_key in key_strategy(),
+        probe_action in action_strategy(),
+    ) {
+        let narrow = policy_from_statements(&[statement_json(
+            "Allow",
+            action,
+            &format!("arn:aws:s3:::{bucket}/{key}"),
+        )]);
+        let widened = policy_from_statements(&[statement_json(
+            "Allow",
+            "s3:*",
+            &format!("arn:aws:s3:::{bucket}/*"),
+        )]);
+        let widest = policy_from_statements(&[statement_json("Allow", "*", "arn:aws:s3:::*")]);
+
+        // The request the narrow policy was built for is allowed at every width.
+        prop_assert!(is_allowed(&narrow, action, &bucket, &key), "narrow policy must allow its own grant");
+        prop_assert!(is_allowed(&widened, action, &bucket, &key), "s3:* on bucket/* must imply the concrete grant");
+        prop_assert!(is_allowed(&widest, action, &bucket, &key), "* on arn:aws:s3:::* must imply the concrete grant");
+
+        // Implication over arbitrary probes: anything the narrow policy allows,
+        // the supersets allow too (contrapositive-checked on random requests
+        // that may or may not match the narrow grant).
+        if is_allowed(&narrow, probe_action, &probe_bucket, &probe_key) {
+            prop_assert!(
+                is_allowed(&widened, probe_action, &probe_bucket, &probe_key),
+                "superset (s3:* on {bucket}/*) must allow whatever the narrow policy allows: {probe_action} on {probe_bucket}/{probe_key}"
+            );
+            prop_assert!(
+                is_allowed(&widest, probe_action, &probe_bucket, &probe_key),
+                "superset (* on arn:aws:s3:::*) must allow whatever the narrow policy allows"
+            );
+        }
+    }
+
+    /// (c) Default deny: a policy with no statements denies every non-owner
+    /// request, whatever the action/bucket/object.
+    #[test]
+    fn empty_policy_denies_everything(
+        bucket in bucket_strategy(),
+        key in key_strategy(),
+        action in action_strategy(),
+    ) {
+        let empty: Policy = serde_json::from_str(r#"{"Version":"2012-10-17","Statement":[]}"#)
+            .expect("empty policy JSON should parse");
+        prop_assert!(
+            !is_allowed(&empty, action, &bucket, &key),
+            "empty policy must deny {action} on {bucket}/{key}"
+        );
+
+        let default_policy = Policy::default();
+        prop_assert!(
+            !is_allowed(&default_policy, action, &bucket, &key),
+            "Policy::default() must deny {action} on {bucket}/{key}"
+        );
+    }
+}