Foundations of Security Analysis and Design II: FOSAD 2001/2002 Tutorial Lectures

1 Introduction......Page 8
2.1 Probabilistic Concurrent Constraint Programming......Page 12
2.2 Operational Semantics......Page 13
2.3 Probabilistic Noninterference and Identity Confinement......Page 16
2.4 Approximate Identity Confinement......Page 21
2.5 Statistical Interpretation......Page 24
3.1 Probabilistic Process Algebra......Page 29
3.2 Operational Semantics and Equivalence......Page 33
3.3 Probabilistic Noninterference......Page 37
3.4 Approximate Noninterference......Page 39
3.5 Approximating {\\it PNI}......Page 41
3.6 Statistical Interpretation......Page 43
4 Related Work and Conclusion......Page 45
References......Page 47
1 Introduction......Page 51
1.1 Alice, Bob and the Secret Place......Page 52
1.2 Keys in Cryptography......Page 53
1.3 The Power of {\\em Eve}......Page 54
2 Cryptographic Primitives......Page 55
3 Key Establishment......Page 57
3.1 Computationally Secure Public-Key Based Schemes......Page 58
3.2 Key Transport......Page 62
3.3 Unconditionally Secure Schemes......Page 63
4.1 Key Distribution Center......Page 78
4.2 Distribution of a KDC......Page 79
5 Multicast Schemes......Page 82
6 Tracing Schemes......Page 84
7 Quantum Key Distribution......Page 87
8 Conclusions......Page 89
References......Page 90
1 The Pi Calculus......Page 98
1.1 Syntax and Operational Semantics......Page 99
2 Typing and Subtyping for the Pi Calculus......Page 103
2.2 Typing Rules......Page 105
2.3 Subtyping......Page 106
2.4 Properties of the Type System......Page 107
3 The Join Calculus......Page 108
3.1 Typing......Page 110
3.3 Further Reading......Page 112
4 The Pi Calculus with Groups......Page 113
4.1 Syntax and Operational Semantics......Page 115
4.2 The Type System......Page 116
5.1 Multilevel Security......Page 118
5.2 Syntax of the Security Pi-Calculus......Page 119
5.3 Reduction Semantics......Page 120
5.4 Security as Resource Access Control......Page 121
5.5 Types and Subtypes......Page 122
5.6 Typing Rules......Page 124
5.7 MAC Policies: {\\it Defense} Security......Page 126
5.9 Further Reading......Page 127
6.1 Syntax of the Calculus......Page 128
6.2 The Operational Semantics of CryptoSPA......Page 129
7.1 Syntax and Semantics......Page 131
7.2 Secrecy by Typing in the Spi Calculus......Page 134
7.3 An Example with Key Establishment......Page 138
7.4 Secrecy Types for Asymmetric Communication......Page 139
7.5 Further Reading......Page 142
References......Page 143
1 Introduction......Page 146
1.1 Multilevel Security and Non-interference......Page 147
1.2 Non-interference for Security Protocols......Page 148
1.3 The {\\it GNDC} Scheme......Page 150
1.4 Plan of the Paper......Page 154
2.1 The CryptoSPA Syntax......Page 155
2.2 The Operational Semantics of CryptoSPA......Page 157
3.1 Decorating Protocol Specifications......Page 159
3.2 The Enemy......Page 160
3.3 Behavioural Semantics......Page 162
4 Verification and Compositionality......Page 164
4.1 Most Powerful Enemy......Page 165
4.2 Static Characterization of NDC......Page 167
4.3 Compositionality......Page 169
5 A General Schema for Security Properties......Page 170
5.2 Non-deducibility on Compositions......Page 171
5.3 The Agreement Property......Page 172
5.4 Message-Oriented Authentication......Page 174
5.5 Secrecy......Page 175
5.6 Non-repudiation......Page 178
5.7 Authentication in the Spi-Calculus......Page 182
6 Some Simple Comparison Results......Page 186
References......Page 189
1 Introduction......Page 193
2 Cryptographic Preliminaries......Page 194
3.1 Simple Authentication of Streams......Page 196
3.2 Non-optimal Solutions for Signing of Streams......Page 197
3.3 An Optimal Solution to Sign Streams......Page 198
4 Authentication in Secure Multicast......Page 201
4.1 Timed Authentication......Page 202
4.2 A MAC-Only Solution......Page 204
5 Secrecy in Secure Multicast......Page 205
5.2 Stateless Receivers......Page 206
6 Tracing Traitors......Page 209
6.1 Tracing Traitors in the Subset Cover Framework......Page 210
6.2 A Public-Key Scheme......Page 211
References......Page 212
1 Introduction......Page 214
2 Mobile Ambients......Page 217
2.1 Syntax and Semantics of Mobile Ambients......Page 218
2.2 A 0CFA Analysis for Mobile Ambients......Page 220
2.3 Crossing Control and Opening Control......Page 230
3 Discretionary Access Control......Page 233
3.1 Syntax and Semantics of Discretionary Ambients......Page 235
3.2 Adapting the 0CFA Analysis to Discretionary Ambients......Page 237
3.3 A Context-Sensitive 1CFA Analysis......Page 240
4.1 Confidentiality: The Bell-LaPadula Model......Page 246
4.2 Integrity: The Biba Model......Page 249
5 Cryptographic Protocols......Page 253
5.1 Syntax and Semantics of Boxed Ambients......Page 254
5.2 Cryptographic Protocols in Boxed Ambients......Page 256
5.3 Adapting the 0CFA Analysis to Deal with Communication......Page 262
5.4 Protocol and Exchange Analysis......Page 266
6 Conclusion......Page 269
References......Page 270