Theory of Security and Applications

Name: Theory of Security and Applications | Joint Workshop, TOSCA 2011, Saarbrücken, Germany,March 31-April 1, 2011, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

Joint Workshop, TOSCA 2011, Saarbrücken, Germany,March 31-April 1, 2011, Revised Selected Papers

Sebastian Moedersheim Catuscia Palamidessi(Herausgeber*in)

Springer (Verlag)

Erschienen am 11. Januar 2012

IX, 225 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-27375-9 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Title
Preface
Organization
Table of Contents
Union and Intersection Types for Secure Protocol Implementations
Introduction
Contributions
Related Work
Outline
Our Type System at Work
Protocol Description and Security Annotations
Types for Cryptography
Type-Checking the NSL Protocol
The RCF Calculus
Type System
Typing Environment and Entailment
Subtyping and Kinding
Encoding Types Un and Private in RCF
Typing Values and Expressions
Implementation of Symbolic Cryptography
Dynamic Sealing
Digital Signatures
Public-Key Encryption
Encoding of Zero-Knowledge
Illustrative Example: Simplified DAA
High-Level Specification
Automatic Code Generation
Implementation
Related Work on Unions and Intersections
Conclusions and Future Work
References
Secure Composition of Protocols
References
Constructive Cryptography - A New Paradigm for Security Definitions and Proofs
Introduction and Motivation
Modularity in Constructive Disciplines
Traditional Security Definitions in Cryptography
Constructive Cryptography
Outline of the Paper
Motivating Example: The One-Time Pad
The Traditional Security Proof for the One-Time Pad
Two ``Security Problems'' of the One-Time Pad
Computational Security: Additive Stream Ciphers
Explaining the Security of the One-Time Pad in Constructive Cryptography
The Basic Approach
The One-Time Pad Example
The Simulator
Computational Security
Distinguishers and Computational Indistinguishability
One-Time Pad Encryption over an Insecure Channel
An Abstract Theory of Systems
Abstraction in Cryptography
Levels of Abstraction: Bottom-Up vs. Top-Down
Resources and Converters
Cryptographic Algebras
Distinguisher-Based Pseudo-Metrics
Constructive Cryptography for the Alice-Bob-Eve Setting
Defining ``Secure Construction''
Composability
History and Related Work
Conclusions and Future Work
References
G2C: Cryptographic Protocols from Goal-Driven Specifications
Introduction
Contributions
Related Work
Outline
Illustrative Example
Compilation to Symbolic Protocols
Intermediate Representation as Data Flow Graphs
Condensed Data Flow Graphs - Selection of the Protocol Skeleton
Synthesizing Cryptographic Protocols for the Applied -Calculus
Anonymity
Anonymity as Symmetric Paths in the Graph
Cryptographic Primitives for Anonymity
Verification of Anonymity in the Synthesized Protocol
Conclusions and Future Work
References
Modeling Long-Term Signature Validation for Resolution of Dispute
Introduction
Statement of the Problem
Related Work
Motivations and Organization of the Paper
Security Model and Notations
Resolution of Dispute
Threat Model
RDR Semantics
Discussions
Calculus for Long-Term Signature Validation
Statements
Initial View Construction
Inference Rules
Statement Validity
Implementing the Resolution of Dispute Rule
Expiration of the Judgment Proof
Using the Calculus in the Real World
Conclusion and Future Work
References
Formal Analysis of Privacy for Anonymous Location Based Services
Introduction
The VPriv Scheme
Description
Privacy
Formal Model
Messages
Processes
Privacy for Interactive Zero-Knowledge Protocols
Equivalences
Formal Definition of Privacy
Checking Privacy with ProVerif
Privacy Analysis
Simplifications
Analysis Model
Analysis Results
Evaluation
Conclusion
References
Formal Analysis of the EMV Protocol Suite
Introduction
EMV Fundamentals
An EMV Protocol Session
Initialisation
Card Authentication
Cardholder Verification
The Transaction
Formalisation in F#
Security Requirements
Including the Issuer
Conclusions
References
Security Goals and Protocol Transformations
Introduction
Some Protocol Transformations
Security Analysis of HD and YN
What Is Protocol Analysis?
The Preservation Theorem
The Language L(?) of a Protocol ?
Preserving Security Goal Formulas
References
Model-Checking Secure Information Flow for Multi-threaded Programs
Introduction
Program Model
Syntax
Semantics
Secure Information Flow
Eager Trace Invariance
Observational Determinism
A Temporal Logic Characterisation of Secure Information Flow
Modal -Calculus
Observational Determinism in Temporal Logic
Eager Trace Invariance in Temporal Logic
Encoding in the Concurrency WorkBench
CWB Encoding of the Program Model
CWB Encoding of Observational Determinism
Conclusions and Future Work
References
Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus
Introduction
Preliminaries
The Case of Several Congruence Relations
Adding a Background Term Rewrite System
Application to the Spatial Logic for Frames
Frames
The Frame Logic FSL
From Spatial to Equational
Deciding the Model-Checking of FSL and Static Equivalence
Conclusion
References
Automated Code Injection Prevention for Web Applications
Introduction
Overview
A Multitier Language
Syntax
Hop Web Application Semantics
A More Fine-Grained Semantics
Client-Code Compilation
A Naive Client Compiler
A Secure Client Compiler
Practical Discussion
Conclusion
References
Soundness of Removing Cancellation Identities in Protocol Analysis under Exclusive-OR
Introduction
Background
The Problems and Our Contributions
Protocol Model
Term Algebra
Attacker Deductions
Protocol Analysis Using Constraint Solving
Purity and EVX-Freedom Imply Soundness
Attacker Deduction Rules, D and DE
Purity and EVX-Freedom Requirements
Soundness Proofs
Structured Protocols
Attacker Deductions
Proofs
Related Work
Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken