Foundations and Applications of Security Analysis: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March 28-29, 2009, Revised Selected Papers

Fine-Grain Models and Noninterference......Page 9
Markovian Process Calculus......Page 11
Bisimulation Semantics......Page 14
Bisimulation-Based Strong Noninterference......Page 17
Bisimulation-Based Strong Local Noninterference......Page 21
Conclusions......Page 23
Introduction......Page 25
Secure Information Flow......Page 26
Information Flow Policy Patterns......Page 28
Analysis for Deterministic System Models......Page 29
Language-Based Analysis......Page 30
The Attacker\'s Observational Power......Page 31
Policies For Encryption......Page 32
Analysis for Nondeterministic System Models......Page 34
Language-Based Instantiation......Page 36
Related Work......Page 37
References......Page 40
Introduction......Page 42
The General Attacker......Page 43
Extending the Validation Method over the General Attacker......Page 46
Basics of SAT-Based Model Checking......Page 47
Formalising the General Attacker......Page 48
Formalising Protocol Properties under the General Attacker......Page 51
Validating the NSPK++ Protocol under the General Attacker......Page 53
Conclusions......Page 57
References......Page 58
Introduction......Page 60
Usage Automata......Page 61
On the Expressive Power of Usage Automata......Page 69
Run-Time Enforcement of Usage Policies......Page 73
Conclusions......Page 75
References......Page 76
Introduction......Page 78
The Calculus......Page 81
The Control Flow Analysis......Page 85
Conclusion......Page 93
References......Page 94
Improving the Semantics of Imperfect Security......Page 96
References......Page 99
Introduction......Page 100
Formal Model......Page 101
Term Algebra......Page 102
API Rewrite Systems......Page 103
Towards Static Attribute Policies......Page 105
Reducing APIs with Static Attribute Policies to Bounded Models......Page 108
Experiments......Page 112
References......Page 113
Introduction......Page 115
Some Examples......Page 117
Messages, Protocols, Skeletons......Page 121
Transformations......Page 125
Transformations and Homomorphisms......Page 128
Conclusion......Page 130
References......Page 131
Introduction......Page 132
Basic Notation and Definitions......Page 134
Main Protocol......Page 135
Recovery Subprotocol......Page 136
OFEPSP+ Validation with AVISPA and SPAN......Page 137
OFEPSP+ Specification in HLPSL......Page 138
HLPSL Correctness Verification......Page 140
OFEPSP+ Security Validation......Page 141
Conclusions and Work in Progress......Page 143
References......Page 144
Introduction......Page 146
Message Terms......Page 148
Strands, Strand Spaces and Bundles......Page 149
Woo and Lam\'s Protocol Attack......Page 151
The KP Protocol......Page 152
Implementation......Page 154
Protocol Repair at the Abstract Level......Page 156
Protocol Repair at the Concrete Level......Page 158
Conclusions......Page 160
References......Page 161
Introduction......Page 163
FOL-Based Crypto-Protocol Verification: Derivations vs. Models......Page 164
Model-Theoretic Foundations......Page 165
Case Studies......Page 170
RSA-PSS......Page 171
Wired Equivalent Privacy......Page 172
Needham-Schroeder-Lowe with ECB......Page 174
Conclusion......Page 175
References......Page 176
A Appendix......Page 179
Introduction......Page 181
Background......Page 182
Type System......Page 183
Operational Semantics......Page 184
Typing Rules......Page 186
Progress and Preservation......Page 187
Indistinguishability......Page 191
Non-interference......Page 193
Example: Wrap/Decrypt Attack......Page 195
Related Work......Page 197
Conclusions and Future Work......Page 198
References......Page 199
Introduction......Page 201
Related Work......Page 205
Adaptive Corruption in Indistinguishability-Based Security of Encryption......Page 206
Security of Encryption with Adaptive Corruption......Page 207
Computational Soundness with Adaptive Corruptions......Page 209
References......Page 214
A Proof of Theorem 1......Page 216
Introduction......Page 219
Remote Voting......Page 220
A Brief History of Verifiable Voting......Page 221
Pen-and-Paper......Page 222
Cryptographic Schemes......Page 223
Prêt à Voter......Page 225
Three-Ballot......Page 226
Scantegrity II......Page 227
References......Page 228