A model checking-based approach for security policy verification of mobile systems

DOI10.1007/S00165-010-0159-YMaRDI QIDQ432137zbMATH OpenOpenAlexFDO

Authors Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi

Publication date 3 July 2012

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-010-0159-y

zbMATH Keywords

information flowaccess controlsoftware verificationmobile systemsprogram security and safetysecurity policies

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic Semantics for the Verification of Security Properties of Mobile Petri Nets
• Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K
• Verification of security-relevant behavior model and security policy for model-carrying code

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670562 (Why is no real title available?)
• scientific article; zbMATH DE number 1231689 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 2087553 (Why is no real title available?)
• scientific article; zbMATH DE number 1834570 (Why is no real title available?)
• scientific article; zbMATH DE number 794257 (Why is no real title available?)
• A calculus of kells
• A model checking-based approach for security policy verification of mobile systems
• CONCUR 2004 - Concurrency Theory
• Computer Aided Verification
• Integrated Formal Methods
• Mobile ambients
• Model Checking Software
• Model checking JAVA programs using JAVA PathFinder
• Programming Languages and Systems
• Static Analysis
• TLPVS
• The Kell calculus: operational semantics and type system.
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of Boolean programs with unbounded thread creation
• Verifying safety properties of concurrent Java programs using 3-valued logic

Cited in

(8)

• A UTP approach for rTiMo
• UTP semantics for rTiMo
• A model checking-based approach for security policy verification of mobile systems
• scientific article; zbMATH DE number 1612498 (Why is no real title available?)
• Evaluating Security Policies in Pervasive Mobile Environments Using Context Information
• Process expression of security automaton
• Verification of security-relevant behavior model and security policy for model-carrying code
• LoPSiL: A location-based policy-specification language

Describes a project that uses

Uses Software

• Aglets
• MAGIC
• SatAbs
• TLPVS
• KLAIM
• Bebop
• Java PathFinder
• ComFoRT
• SPIN
• SLAM
• BLAST

This page was built for publication: A model checking-based approach for security policy verification of mobile systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q432137)