(Downloads - 0)
For more info about our services contact : help@bestpfe.com
Table of contents
1 Introduction
1.1 Anonymity
1.1.1 The relevance of anonymity nowadays
1.1.2 Anonymizing technologies nowadays
1.1.3 Anonymizing technologies: a bit of history
1.1.4 Anonymity and computer science
1.2 Formal methods
1.2.1 The need of formal verification
1.2.2 Formal verication
1.3 Background
1.4 Contribution and plan of the thesis
1.5 Origins of the Chapters and Credits
2 Conditional Probabilities over Probabilistic and Nondeterministic Systems
2.1 Introduction
2.2 Markov Decision Processes
2.3 Conditional Probabilities over MDPs
2.4 Conditional Probabilistic Temporal Logic
2.4.1 Expressiveness
2.5 Semi History-Independent and Deterministic Schedulers
2.5.1 Semi History-Independent Schedulers
2.5.2 Deterministic Schedulers
2.6 Model Checking cpCTL
2.6.1 Model Checking Pa[j ]
2.6.2 Complexity
2.7 Counterexamples for cpCTL
3 Computing the Leakage of Information Hiding Systems
3.1 Introduction
3.2 Preliminaries
3.2.1 Probabilistic automata
3.2.2 Noisy Channels
3.2.3 Information leakage
3.3 Information Hiding Systems
3.4 Reachability analysis approach
3.4.1 Complexity Analysis
3.5 The Iterative Approach
3.5.1 Partial matrices
3.5.2 On the computation of partial matrices
3.5.3 Identifying high-leakage sources
3.6 Information Hiding Systems with Variable a Priori
3.7 Interactive Information Hiding Systems
3.8 Related Work
4 Information Hiding in Probabilistic Concurrent Systems
4.1 Introduction
4.1.1 Contribution
4.2 Preliminaries
4.2.1 Probabilistic automata
4.2.2 Noisy Channels
4.2.3 Information leakage
4.2.4 Dining Cryptographers
4.3 Systems
4.3.1 Tagged Probabilistic Automata
4.3.2 Components
4.3.3 Systems
4.4 Admissible Schedulers
4.4.1 The screens intuition
4.4.2 The formalization
4.5 Information-hiding properties in presence of nondeterminism
4.5.1 Adversaries
4.5.2 Information leakage
4.5.3 Strong anonymity (revised)
4.6 Verifying strong anonymity: a proof technique based on automorphisms
4.6.1 The proof technique
4.6.2 An Application: Dining Cryptographers
4.7 Related Work
5 Signicant Diagnostic Counterexample Generation
5.1 Introduction
5.2 Preliminaries
5.2.1 Markov Decision Processes
5.2.2 Schedulers
5.2.3 Markov Chains
5.2.4 Linear Temporal Logic
5.3 Counterexamples
5.4 Representative Counterexamples, Partitions and Witnesses
5.5 Rails and Torrents
5.6 Signicant Diagnostic Counterexamples
5.7 Computing Counterexamples
5.7.1 Maximizing Schedulers
5.7.2 Computing most indicative torrent-counterexamples
5.7.3 Debugging issues
5.8 Related Work
6 Interactive Systems and Equivalences for Security
6.1 Interactive Information Flow
6.1.1 Applications
6.2 Nondeterminism and Information Flow
7 Conclusion
7.1 Contributions
7.2 Further directions
Bibliography
