Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1403.1846

Verification of A Security Adaptive Protocol Suite Using SPIN

Shamim Ripon·Sumaya Mahbub·K. M. Intiaz-ud-Din
View original source ↗Read source document ↗Export metadata ↓

Abstract

The advancement of mobile and wireless communication technologies in recent years introduced various adaptive protocols to adapt the need for secured communications. Security is a crucial success factor for any communication protocols, especially in mobile environment due to its ad hoc behavior. Formal verification plays an important role in development and application of safety critical systems. Formalized exhausted verification techniques to analyze the security and the safety properties of communications protocols increase and confirm the protocol confidence. SPIN is a powerful model checker that verifies the correctness of distributed communication models in a rigorous and automated fashion. This short paper proposes a SPIN based formal verification approach of a security adaptive protocol suite. The protocol suite includes a neighbor discovery mechanism and routing protocol. Both parts of the protocol suite are modeled into SPIN and exhaustively checked various temporal properties which ensure the applicability of the protocol suite in real-life applications.

Explore related subjects

cs.NI

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Shamim Ripon, Sumaya Mahbub, K. M. Intiaz-ud-Din. 2014-03-07. Verification of A Security Adaptive Protocol Suite Using SPIN. https://doi.org/10.7763/ijet.2013.v5.553

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

KEEP EXPLORING

Related papers

arXiv2026

Dynamic Content Caching with Waiting Costs via Restless Multi-Armed Bandits

We consider a system with a local cache connected to a backend server and an end user population. A set of contents are stored at the the server where they continuously get updated. The local cache keeps copies, potentially stale, of a subset of the contents. The users make content requests to the local cache which either can serve the local version if available or can fetch a fresh version or can wait for additional requests before fetching and serving a fresh version. Serving a stale version of a content incurs an age-of-version(AoV) dependent ageing cost, fetching it from the server incurs a fetching cost, and making a request wait incurs a per unit time waiting cost. We focus on the optimal actions subject to the cache capacity constraint at each decision epoch, aiming at minimizing the long term average cost. We pose the problem as a Restless Multi-armed Bandit(RMAB) Problem and propose a Whittle index based policy which is known to be asymptotically optimal. We explicitly characterize the Whittle indices. We numerically evaluate the proposed policy and also compare it to a greedy policy. We show that it is close to the optimal policy and substantially outperforms the exising policies.

cs.NI↗
arXiv2026

FUSION: Forecast-Embedded Agent Scheduling with Service Incentive Optimization over Distributed Air-Ground Edge Networks

This paper introduces a forecasting-driven, incentive-aware service provisioning framework for distributed air--ground integrated networks with human--machine coexistence. Agent pairs (APs), each comprising a vehicle and its carried uncrewed aerial vehicles (UAVs), are proactively dispatched to overloaded hotspots to augment the computing capacity of edge servers (ESs). This design introduces four coupled challenges: uncertain spatio-temporal workloads, coupling between vehicular mobility and UAV capacity, forecast-driven contracting risks, and heterogeneous quality-of-service (QoS) requirements of human users (HUs) and machine users (MUs). To address these challenges, we propose FUSION, a two-stage framework with offline service preparation and online task scheduling. In the offline stage, a liquid neural network forecasts multi-step ES demand, an enhanced ant colony optimization scheme constructs AP service routes, and an auction-based mechanism establishes ES--AP contracts. In the online stage, we formulate congestion-aware scheduling as an exact-potential game among service demanders (SDs) and develop a potential-guided best-response dynamics algorithm. For a fixed online state, the algorithm converges to an $\varepsilon$-Nash equilibrium (NE) under a positive improvement threshold and to a pure-strategy NE when the threshold is zero. Within the considered contracting model, we theoretically establish that the offline mechanism satisfies individual rationality, near-truthfulness, and weak budget balance. Experiments on synthetic data and real-world load traces show that FUSION achieves higher social welfare while maintaining interaction delay and signaling energy overheads comparable to the considered benchmarks.

cs.NI↗
arXiv2026

Exploiting Overlapping Fields of View for Redundancy-Aware Uplink Transmission in Vehicular 6G

Emerging uplink-dominant 6G use cases, such as cooperative vehicular streaming, require efficient transmission of high-volume visual data over limited wireless resources. While semantic communications can reduce traffic by prioritizing task-relevant content, most existing approaches treat users independently and therefore overlook spatial redundancy among nearby devices' observations. This paper proposes a semantic-aware multiple access scheme that exploits overlapping fields of view among vehicular users to reduce redundant uplink transmissions. We formulate a joint perception and transmission control problem in which users decide which image patches to transmit, when to transmit them, and over which channel, subject to communication constraints. To address the resulting complexity, we introduce a practical two-phase approach. First, nearby vehicles share selected observation patches over Vehicle-to-Vehicle (V2V) links to calculate inter-user spatial redundancy. Second, users transmit only semantically important, non-redundant patches to the base station, where observations can be reconstructed using the received patches and complementary views from neighboring vehicles. Simulation results in a dense urban vehicular scenario demonstrate that our approach improves the proportion of users who achieve high-fidelity reconstruction, highlighting the potential of semantic-aware multiple access for sustainable and resource-efficient 6G uplink systems.

cs.NI↗