Partial model checking and theorem proving for ensuring security properties
Published 27 November 2002
Fabio Martinelli
Citations37
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The author presents a methodology based on known techniques in concurrency and process logics theory for ensuring information flow security properties, similar to the ones proposed by Focardi and Gorrieri (1995, 1997).
Abstract
The author presents a methodology based on known techniques in concurrency and process logics theory for ensuring information flow security properties, similar to the ones proposed by Focardi and Gorrieri (1995, 1997). Recently, they have shown that concepts from information flow theory can be used in the analysis of authentication protocols. This kind of problem may be tackled by his methodology. This has been implemented over mudiv, a tool for partial model checking.
Keywords
Computer ScienceSocial Sciences
Medical Entomology and ZoologyHandbook of theoretical computer science
4,202 Citations1990Jan Van Leeuwen
Security Policies and Security Models
2,099 Citations1982Joseph A. Goguen, José Meseguer
Secure Computer System: Unified Exposition and Multics Interpretation
1,913 Citations1976David E. Bell, L.J. La Padula
A suggestive interpretation of the model in the context of Multics and a discussion of several other important topics (such as communications paths, sabotage and integrity) conclude the report.
The Coq proof assistant : reference manual, version 6.1
984 Citations1997Bruno Barras, Samuel Boutin +12 more
Coq V6.1 is a proof assistant based on a higher-order logic allowing powerful definitions of functions and is available by anonymous ftp at ftp.ens-lyon.fr/INRIA/Projects/coq/V 6.1.
Lecture notes in computer scienceBreaking and fixing the Needham-Schroeder Public-Key Protocol using FDR
852 Citations1996Gavin Lowe
This paper uses FDR, a refinement checker for CSP to discover an attack upon the Needham-Schroeder Public-Key Protocol, which allows an intruder to impersonate another agent, and adapt the protocol, and uses FDR to show that the new protocol is secure, at least for a small system.
Breaking and Fixing the Needham−Schroeder Public−Key Protocol Using FDR
584 Citations1996Gavin Lowe
Information and ComputationCCS expressions, finite state processes, and three problems of equivalence
535 Citations1990Paris C. Kanellakis, Scott A. Smolka
Journal of Computer SecurityA Classification of Security Properties for Process Algebras1
310 Citations1995Riccardo Focardi, Roberto Gorrieri
This work provides a process algebra similar to CCS with a set of security notions, hence relating these two areas of concurrency research and showing that some of these security properties are composable w.r.t. the operators of parallelism and action restriction.
Proving properties of security protocols by induction
255 Citations2002Lawrence C. Paulson
The method applies to both symmetric key and public key protocols and has no restriction to finite state systems and the approach is not based on belief logics.
Information and ComputationAn automata theoretic decision procedure for the propositional mu-calculus
218 Citations1989Robert S. Streett, E. Allen Emerson
An elementary time decision procedure is given, using a reduction to the emptiness problem for automata on infinite trees, and a small model theorem is obtained as a corollary.
Elsevier eBooksOperational and Algebraic Semantics of Concurrent Processes
209 Citations1990Robin Milner
This chapter presents a particular class of mathematical models for concurrent communicating processes, namely, the class of algebraic calculi, and describes a small language whose constructions reflect simple operational ideas that are presented by means of structured operational semantics.
IEEE Transactions on Software EngineeringThe Compositional Security Checker: a tool for the verification of information flow security properties
195 Citations1997Riccardo Focardi, Roberto Gorrieri
An application in the area of network security is presented: it is shown that the theory (and the tool) can be reasonably applied also for singling out security flaws in a simple, yet paradigmatic, communication protocol.
Lecture notes in computer scienceClassification of Security Properties
134 Citations2004Riccardo Focardi, Roberto Gorrieri +1 more
Verifying authentication protocols with CSP
114 Citations2002Steve Schneider
A specific theory appropriate to the analysis of authentication protocols is developed, built on top of the general CSP semantic framework, to combine the ability to express protocols in a natural and precise way with the facility to reason formally about the properties they exhibit.
Information and ComputationCharacteristic Formulas for Processes with Divergence
106 Citations1994Bernhard Steffen, Anna Ingólfsdóttir
This paper builds the theoretical basis for a uniform and efficient method to automatically verify bisimulation-like relations between processes by means of model checking and demonstrates the expressive power of intuitionistically interpreted Hennessy-Milner Logic with mutual recursion.
Partial model checking
95 Citations2002Henrik Rasmus Andersen
This paper presents a new approach based on partial model checking where parts of the concurrent system are gradually removed while transforming the specification accordingly, when the intermediate specifications constructed in this manner can be kept small, the state-explosion problem is avoided.
Partial Model Checking (Extended Abstract)
62 Citations1995Henrik Reif Andersen
DAIMI Report SeriesVerification of Temporal Properties of Concurrent Systems
48 Citations1993Henrik Reif Andersen
This thesis is concerned with the verification of concurrent systems modelled by process algebras and provides methods and techniques for reasoning about temporal properties as described by assertions from an expressive modal logic -- the modal µ-calculus.
Comparing two information flow security properties
23 Citations2002Riccardo Focardi
It is proved that BNDC applied to a restricted class of systems, the low-deterministic and non-divergent ones, is equal to L-Sec, so these two properties, which are based on quite different underlying intuitions, become the same if the authors add some conditions to B NDC.
Using temporal logic to specify and verify cryptographic protocols
22 Citations2002James W. Gray, John McLean
It is argued that using standard temporal logic provides greater flexibility and generality, firmer foundations, easier integration with other formal methods, and greater confidence in the verification results.
BRICS Report SeriesA Complete Deductive System for the mu-Calculus
20 Citations1995Igor Walukiewicz
The propositional mu-calculus as introduced by Kozen in [12] is considered and a different finitary axiomatisation of the logic is proposed and proved to be complete.