Principles of Security and Trust
First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings
Published on 22. March 2012
XIV, 431 pages
978-3-642-28641-4 (ISBN)
Description
This book constitutes the refereed proceedings of the first International Conference on Principles of Security and Trust, POST 2012, held in Tallinn, Estonia, in March/April 2012, as part of ETAPS 2012, the European Joint Conferences on Theory and Practice of Software.
The 20 papers, presented together with the abstract of an invited talk and a joint-ETAPS paper, were selected from a total of 67 submissions. Topics covered by the papers include: foundations of security, authentication, confidentiality, privacy and anonymity, authorization and trust, network security, protocols for security, language-based security, and quantitative security properties.
More details
Other editions
Additional editions
Pierpaolo Degano | Joshua D. Guttman
Principles of Security and Trust
First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings
Book
03/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Foreword
- Preface
- Organization
- Table of Contents
- Differential Privacy and the Power of (Formalizing) Negative Thinking
- References
- Security Protocol Verification: Symbolic and Computational Models
- Security Protocols
- An Example of Protocol
- Models of Protocols
- Security Properties
- Verifying Protocols in the Symbolic Model
- Verification Techniques
- ProVerif
- Verifying Protocols in the Computational Model
- Computational Soundness
- Adapting Techniques from the Symbolic Model
- Direct Computational Proofs
- Verifying Protocol Implementations
- Conclusion and Future Challenges
- References
- Analysing Routing Protocols: Four Nodes Topologies Are Sufficient
- Introduction
- Messages and Attacker Capabilities
- Messages
- Attacker Capabilities
- Functions over Terms
- Models for Protocols
- Syntax
- Example: Modeling the SRP Protocol
- Configuration and Topology
- Execution Model
- Security Properties
- Reduction Results
- From an Arbitrary Topology to a Quasi-Complete One
- Reducing the Size of the Topology
- Only Five Topologies Are Sufficient!
- Case Studies Using ProVerif
- Proverif
- Case Studies
- Results
- Conclusion
- References
- Parametric Verification of Address Space Separation
- Introduction
- Related Work
- Address Space Translation and Separation
- Address Space Translation
- Address Space Separation
- Definitions of PGCL+ and PTSL+
- PGCL+ Syntax
- ShadowVisor Code in PGCL+
- PGCL+ Semantics
- Specification Formalism
- Small Model Theorems
- Case Studies
- ShadowVisor
- Xen
- Conclusion
- References
- Verification of Security Protocols with Lists: From Length One to Unbounded Length
- Introduction
- A Reminder on ProVerif
- Abstract Representation of Protocols by Generalized Horn Clauses
- Running Example
- Need for Generalizing Horn Clauses
- Syntax
- Representation of the Protocol
- Type System for the New Clauses
- Translation from Generalized Horn Clauses to Horn Clauses
- From Any Length to Length One
- Main Result
- Examples
- Proof of Theorem 1
- An Approximation Algorithm
- Approximation Algorithm
- Examples
- Conclusions and Future Work
- References
- Privacy Supporting Cloud Computing: ConfiChair, a Case Study
- Introduction
- Description of the Problem and Related Work
- Desired Properties and Threat Model
- Related Work
- The Protocol
- Description
- Discussion
- Implementation
- Formal Model and Verification
- The Process Calculus
- Properties and Analysis
- Conclusion
- References
- A Formal Analysis of the Norwegian E-voting Protocol
- Introduction
- Norwegian E-voting Protocol
- Setting Phase
- Submission Phase
- Counting Phase
- Applied Pi Calculus
- Terms
- Processes
- Operational Semantics
- Equivalences
- Modelling the Protocol in Applied-Pi Calculus
- Equational Theory
- Norwegian Protocol Process Specification
- Formal Analysis of Ballot Secrecy
- Ballot Secrecy with Corrupted Voters
- Attacks
- Further Corruption Cases Using ProVerif
- Discussion
- References
- Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication
- The ISO/IEC 9798 Standard
- Overview
- Notation
- Protocol Examples
- Optional Fields and Variants
- Threat Model and Security Properties
- Protocol Analysis
- Role-Mixup Attacks
- Type Flaw Attacks
- Attacks Involving TTPs That Perform Multiple Roles
- Reflection Attacks
- Repairing the Protocols
- Root Causes of the Problems
- Associated Design Principles
- Proposed Modifications to the Standard
- Proving the Correctness of the Repaired Protocols
- Related Work
- Conclusions
- References
- Security Proof with Dishonest Keys
- Introduction
- Motivation : Some Examples of Insufficiency of Current Models
- Model
- Syntax and Deduction
- Operational Semantics
- Examples
- Observational Equivalence
- Computational Interpretation
- Simple Processes
- Computational Model
- Main Result
- Results
- Sketch of Proof
- Application
- Specification of the Protocol
- Security
- Conclusion
- References
- Reduction of Equational Theories for Verification of Trace Equivalence: Re-encryption, Associativity and Commutativity
- Introduction
- Preliminaries
- Terms and Equational Theories
- Processes and Operational Semantics
- Trace Equivalence and Secrecy
- Motivation and Statement of the Reduction Result
- Starting Point: The Case Study
- General Setting for the Reduction
- Reduction of the Set of Traces
- Occurence Order for a Frame
- Local Traces in General
- Local Traces for Re-encryption
- Local Traces for Associativity-Commutativity
- Main Results of This Section
- Reduction of Equational Theories
- Conclusion and Future Work
- References
- Towards Unconditional Soundness: Computationally Complete Symbolic Attacker
- Introduction
- Symbolic and Computational Models
- Terms and Frames
- Formulas
- Protocols
- Axioms and Security Properties
- Computational Interpretation
- Computational Validity of Security Properties and Axioms
- Computational Soundness
- Examples of Axioms
- Examples of Axioms That Are Computationally Valid
- Secrecy Axiom
- Conclusions
- References
- Verified Indifferentiable Hashing into Elliptic Curves
- Introduction
- An Overview of CertiCrypt
- Representation of Distributions
- Programming Model
- Reasoning Tools
- Statistical Distance
- A Logic for Bounding Statistical Distance
- Reasoning about Failure Events
- Weak Equivalences
- Approximate Observational Equivalence
- A Conditional Variant
- Indifferentiability
- Application to Elliptic Curves
- Related Work
- Conclusion
- References
- Provable De-anonymization of Large Datasets with Sparse Dimensions
- Introduction
- Related Work
- Definitions
- Analysis of Generic Scoring Algorithm
- Analysis of Weighted Scoring Algorithm
- Empirical Results
- Isolation Attack
- Information Amplification Attack
- Conclusion
- References
- Revisiting Botnet Models and Their Implications for Takedown Strategies
- Introduction
- Related Work
- Constructing and Measuring Assortative Networks
- Degree Assortativity
- Degree Assortativity in Botnets
- Generating Assortative Networks
- Metrics
- Network Resilience
- Uniform and Degree-Based Takedown Strategies
- Other Takedown Strategies
- Network Recovery
- Recovering from Uniform and Degree-Based Strategies
- Recovering from Other Takedown Strategies
- Discussion
- Conclusion
- References
- A Game-Theoretic Analysis of Cooperation in Anonymity Networks
- Introduction
- Game-Theoretic Incentive Framework
- Strategies and Equilibriums
- The General Model in Anonymity Systems
- Crowds
- Cooperation Analysis in Crowds
- The Anonymity Analysis
- Measuring Anonymity Payoffs
- The Cost Analysis
- Balancing between Cost and Anonymity in Crowds
- Adding Incentives: The Analysis of Gold-Star Mechanism
- The Anonymity Analysis with Gold-StarMechanism
- The Performance Analysis
- Balancing between Performance and Anonymity
- Related Work
- Conclusion
- References
- Deciding Selective Declassification of Petri Nets
- Introduction
- Basic Definitions and Decidability Results
- Noninterference Properties, and Previous Results
- Selective Non-interference
- Decidability of the INISD Property
- Undecidability for Non-plain or Non-injective Labellings
- Another Example
- INISD and Information Flow Security
- Equivalent Reformulation of Definition
- Mantel's Framework
- Van der Meyden's Framework
- Conclusion
- References
- Enforceable Security Policies Revisited
- Introduction
- Enforceability
- Policy Enforcement Based on Execution Monitoring
- Formalization
- Relation between Enforceability and Safety
- Generalizing Safety
- Characterizing Enforceability
- Realizability
- Automata-Based Specification Languages
- Logic-Based Specification Languages
- Related Work
- Conclusion
- References
- Towards Incrementalization of Holistic Hyperproperties
- Introduction
- Background
- Partial Automata, Coalgebras and Languages `a la Rutten
- Systems - From Sets of Traces to G-Coalgebras
- Holistic and Incremental Hyperproperties
- Holistic Hyperproperty Logic HL
- Incremental Hyperproperty Logic IL
- Incrementalization of Holistic Hyperproperties
- Incrementalization of PHH
- Incrementalization of SHH
- Incrementalization of OHH
- Verification of Incremental Hyperproperties
- Sample Hyperproperties in PHH
- Sample Hyperproperties in SHH
- Sample Hyperproperties in OHH
- Related Work
- Conclusion
- References
- Type-Based Analysis of PKCS#11 Key Management
- Introduction
- A Language for PKCS#11 Key Management
- Type System
- Type Soundness
- Type-Based Analysis
- Conclusions
- References
- A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow
- Introduction
- Background
- Evidence Representations
- Preliminaries
- Evidence
- Auxiliary Evidence
- Manipulating 2-Assertions
- Generating Evidence
- For Loops
- Machine-Checked Evidence and Soundness Overview
- Representation of Evidence
- Soundness
- Evaluation
- Related Work
- Conclusions and Future Work
- References
- PTaCL: A Language for Attribute-Based Access Control in Open Systems
- Introduction
- Attribute-Based Requests
- Targets
- Evaluation
- Interface Targets
- On Functional Completeness
- Policies
- Policy Evaluation
- On the Non-monotonicity of Targets
- Decision Operators
- Related Work
- Concluding Remarks
- References
- A Core Calculus for Provenance
- Introduction
- Examples
- Summary
- Background
- Core Language
- Dynamic Semantics
- Basic Properties of Traces
- Provenance Views and Trace Queries
- Provenance Extraction
- Patterns, Partial Traces, and Trace Queries
- Disclosure and Obfuscation Analysis
- Disclosure
- Obfuscation
- Discussion
- Related Work
- Conclusions
- References
- Author Index
