Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security
Joint Workshop, ARSPA-WITS 2010, Paphos, Cyprus, March 27-28, 2010, Revised Selected Papers
Published on 5. October 2010
IX, 185 pages
978-3-642-16074-5 (ISBN)
Description
More details
Other editions
Additional editions
Alessandro Armando | Gavin Lowe
Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security
Joint Workshop, ARSPA-WITS 2010, Paphos, Cyprus, March 27-28, 2010, Revised Selected Papers
Book
10/2010
1st Edition
Springer
€64.19
Article exhausted; check different version
Content
- Title
- Preface
- Organization
- Table of Contents
- The CaPiTo Approach to Protocol Validation
- Reasoning about Probabilistic Security Using Task-PIOAs
- Introduction
- Comparison with Other Work
- Ordered Structures and Domain-Theoretic Arguments
- Probabilistic Input/Output Automata
- Tasks
- Applying Task Schedules
- Comparing PIOAs
- Dining Cryptographers
- A Model of Dining Cryptographers
- Proving the Protocol Secure
- A Deterministic Master
- The Probabilistic Case
- Summary and Future Work
- References
- Appendix - Proofs
- Secrecy and Authenticity Types for Secure Distributed Messaging
- Introduction
- The Calculus
- The Type System
- Properties of the Type System
- Subject Reduction
- Secrecy
- Authenticity
- Typing a Variant of 2KP
- Conclusions
- References
- Appendix
- Modular Plans for Secure Service Composition
- Introduction
- An Example
- Service Network
- Syntax
- Operational Semantics
- Type and Effect System
- History Expressions
- Typing Relation
- Modular Plans
- Properties of Plans
- Conclusion and Related Work
- References
- A Type System for Access Control Views in Object-Oriented Languages
- Introduction
- Core Language
- Type System
- Typing Rules
- Type Safety
- Further Discussion
- Related Work
- Concluding Remarks
- References
- Formal Analysis of Key Integrity in PKCS#11
- Introduction
- Background: The DKS-Model of PKCS#11
- Extending the Model: Key Integrity
- The H-Transition System
- Adding Trusted Keys
- Conclusions
- References
- DKS-Rules Modelling Cryptographic Operations
- Proofs from Section 4
- Secure Upgrade of Hardware Security Modules in Bank Networks
- Introduction
- The HSM Upgrading Problem
- Upgrading vs. Decontaminating
- Upgrading Strategies
- Estimating the Upgrading Cost: An Example
- Conclusion
- References
- Interactive Information Flow
- References
- Portunes: Representing Attack Scenarios Spanning through the Physical, Digital and Social Domain
- Introduction
- Related Work
- Portunes
- Requirements and Motivation
- The Portunes Model
- The Portunes Language
- Using the Portunes Framework to Calculate Attack Scenarios
- Conclusion and Future Work
- References
- Appendix
- Match It or Die: Proving Integrity by Equality
- Introduction
- Secret-Sensitive Noninterference
- Hash Functions and Secrecy
- Proving Integrity by Equality
- Security Type System
- Related Works
- Conclusions
- References
- Case Studies
- Towards Automatic Analysis of Election Verifiability Properties
- Introduction
- Contribution
- Related Work
- Outline
- Applied Pi Calculus
- Syntax
- Semantics
- Notational Conventions
- Events and Reachability Assertions
- Election Verifiability
- Overview
- Verifying an Election
- Election Verifiability in the Applied Pi Calculus
- Case Studies
- Postal Ballot Protocol
- Protocol Due to Fujioka, Okamoto and Ohta
- Protocol Due to Juels, Catalano and Jakobsson and Clarkson, Chong and Myers
- Conclusion
- References
- AnBx - Security Protocols Design and Verification
- Introduction
- AnBx: Declarative Protocol Narrations
- A Cryptographic Translation for AnBx
- Implementing the Translation: The AnBx Compiler
- A Case Study: e-Payment Systems
- Related Work and Conclusion
- References
- Revised iKP Narration
- Author Index
