Search arXivSearch

arXiv · 2609.01192

Verification of $K$- and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions

Abstract

Anonymity is an information flow property that provides privacy protection in the sense of non-uniqueness of system information at certain moments with respect to observations. The notion of $K$-step anonymity in the context of discrete-event systems characterizes the scenario that the state estimates cannot be a singleton within at most $K$ observational steps prior to the current instant, while infinite-step anonymity is the same as $K$-step anonymity without considering the limit on $K$. In this paper, we lucubrate $K$- and infinite-step anonymity for partially-observed discrete-event systems modeled by non-deterministic finite-state automata. First, we define two strong types and two weak types of $K$- and infinite-step anonymity that are fundamentally different from the existing notions of $K$- and infinite-step anonymity due to the consideration of strong and weak anonymous projections. Then, we develop a new methodology by exploiting the concurrent-composition technique to verify these four types of anonymity. Based on the constructed concurrent compositions, verifiable necessary and sufficient conditions for the four types of anonymity are provided, along with their complexity analysis. Finally, the upper bounds on $K$ for $K$-step strong anonymity and weak anonymity are computed.

Explore related subjects

Keep this discovery

BibTeXRIS

Jiahui Zhang, Kuize Zhang, Xiaoguang Han, Zhiwu Li. 2026-09-01. Verification of $K$- and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions. https://arxiv.org/abs/2609.01192

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

CARVY-FL: Client Anticlustering for Robust Voting in Provably Secure Federated Learning

Federated learning (FL) enables collaborative training without directly sharing raw data, but remains vulnerable to malicious clients. Voting-based FL improves robustness by partitioning clients into groups, training one model per group, and aggregating predictions by plurality voting. However, under class-disjoint non-IID data, distribution-oblivious grouping can yield highly variable certified accuracy (CA). We propose CARVY-FL, which estimates client distribution types from one-epoch model updates and uses anticlustering to increase within-group distributional diversity. Under a fixed grouping, CARVY-FL retains the voting-based CA guarantee while increasing vote margins. Experiments on MNIST and Fashion-MNIST show higher CA than FLCert. Under BadNets with model replacement, CARVY-FL improves the AUC of 100-ASR by 11.1% and 14.9%, respectively.

cs.CR

Privacy-Enhanced Zero-Order Federated Learning via xMK-CKKS over Wireless Channels

Homomorphic encryption (HE) enables privacy-preserving aggregation in federated learning (FL) by allowing the server to operate on encrypted data without decryption. Existing HE-over-the-air (OTA) methods mainly rely on single-key HE schemes and require channel estimation or pre-equalization to compensate for wireless fading. However, single-key HE remains vulnerable to honest-but-curious (HBC) clients holding the shared secret key, while multi-key HE provides stronger client-level security by assigning each device its own secret key. We propose a four-phase protocol that enables the aggregation of xMK-CKKS over a shared wireless channel without channel estimation. The protocol retransmits partial public keys and ciphertexts through the same channel realization, so that the dominant large-modulus encryption terms cancel algebraically during decryption. We integrate this protocol with zero-order FL over slowly varying LoS-dominant channels, where each device transmits a single encrypted scalar per round and the communication/encryption overhead is independent of the model dimension. We show that the residual noise induced by encryption and wireless aggregation preserves the standard convergence rate \(O(1/\sqrt{K})\) up to a negligible noise floor, where $K$ is the number of communication rounds. The protocol assumes a non-trusted server and is secure against HBC clients, preventing any client from recovering the local updates of other participants. Numerical results on MNIST and CIFAR-10 validate the theoretical analysis.

cs.CR

Federated Attack Campaign Detection via Contrastive Encoding of Threat Indicators in Gradient Updates

Detecting orchestrated cyberattack campaigns that span multiple organizations traditionally requires sharing sensitive telemetry and threat intelligence across institutional boundaries and country borders, a barrier that Federated Learning removes by training shared threat detectors directly on local data. We propose FedIoC, a modular framework in which clients fold locally available structured threat indicators into their gradient updates; we instantiate the client-side encoder with a supervised contrastive loss over IoC-matched flows. Within each training batch, flows that match any known indicator pattern form the positive set; the contrastive objective pulls their learned embeddings together and pushes non-IoC embeddings away, so that campaign-relevant structure is, by design, expressed in the gradient direction. Clients sharing indicators for the same attack campaign then produce aligned gradient components, which the server clusters by the cosine similarity of their updates to recover global campaign patterns without any direct IoC transmission. We evaluate FedIoC on two public threat-detection benchmarks distributed across FL clients that each observe only a fragment of every active campaign and hold disjoint indicator sets derived from their local telemetry. In this regime the FL server recovers cross-organizational campaign cohorts directly from gradient geometry. We contribute FedIoC as a modular framework for this setting, and use it to pinpoint the non-IID gradient structure as the main driver of recovery and to define the open problem of designing encoders that improve on it.

cs.LG