A model checking-based approach for security policy verification of mobile systems
type: Item
instance of: scholarly article
title: A model checking-based approach for security policy verification of mobile systems
zbMATH Open document ID: 1242.68153
author: Chiara Braghin
author: Natasha Sharygina
author: Katerina Barone-Adesi
published in: Formal Aspects of Computing
publication date: 2012-07-03T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N30
zbMATH DE Number: 6052549
zbMATH Keywords: software verification
zbMATH Keywords: program security and safety
zbMATH Keywords: mobile systems
zbMATH Keywords: security policies
zbMATH Keywords: access control
zbMATH Keywords: information flow
cites work: TLPVS
cites work: Static Analysis
cites work: Q2753756
cites work: Q4553257
cites work: Q4847017
cites work: Formal Methods for Open Object-Based Distributed Systems
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Integrated Formal Methods
cites work: Q4738363
cites work: Mobile ambients
cites work: Computer Aided Verification
cites work: Model Checking Software
cites work: Verification of Boolean programs with unbounded thread creation
cites work: CONCUR 2004 - Concurrency Theory
cites work: Programming Languages and Systems
cites work: Q4551162
cites work: Q4426384
cites work: Model checking JAVA programs using JAVA PathFinder
cites work: Q4223018
cites work: Q4326390
cites work: Q4779111
cites work: A calculus of kells
cites work: Q2753763
cites work: Verifying safety properties of concurrent Java programs using 3-valued logic
describes a project that uses: TLPVS
describes a project that uses: SLAM
describes a project that uses: SPIN
describes a project that uses: KLAIM
describes a project that uses: ComFoRT
describes a project that uses: SatAbs
describes a project that uses: MAGIC
describes a project that uses: Aglets
describes a project that uses: BLAST
describes a project that uses: Java PathFinder
describes a project that uses: Bebop
MaRDI profile type: Publication
full work available at URL: s00165-010-0159-y
OpenAlex ID: W2045440241
DOI: 10.1007/S00165-010-0159-Y
Recommended article: Symbolic Semantics for the Verification of Security Properties of Mobile Petri Nets
Recommended article: Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K
Recommended article: Verification of Security-Relevant Behavior Model and Security Policy for Model-Carrying Code
description: scientific article; zbMATH DE number 6052549