Trustworthy Global Computing: Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers (Lecture Notes in Computer Science, 4912)

"This book constitutes the thoroughly refereed post-conference proceedings of the Third Symposium on Trustworthy Global Computing, TGC 2007; it moreover contains tutorials from the adjacent Workshop on the Interplay of Programming Languages and Cryptography, both held in Sophia-Antipolis, France, in November 2007." "The 19 revised papers presented together with 3 invited papers were carefully selected from 48 submissions during two rounds of reviewing and improvement. The TGC 2007 symposium papers focus on providing tools and frameworks for constructing well-behaved applications and for reasoning about their behavior and properties in models of computation that incorporate code and data mobility over distributed networks with highly dynamic topologies and heterogeneous devices. The volume concludes with 3 tutorial papers, presented at the co-located Workshop on the Interplay of Programming Languages and Cryptography."--Jacket Title Page Preface Organization Table of Contents Elimination of Ghost Variables in Program Logics Introduction Ghost Variables and Their Use Ghost Variables in Internal Assertions Expressing Extra-Functional Code Properties Problems with Ghost Variables Semantics of Ghost Variables Modelling Extra-Functional Properties Contributions of This Paper Elimination of Ghost Variables Extension to Extra-Functional Properties Language and Program Logic Simple Programming Language Logic for a Simple Language Introducing Ghost Variables Relation between Ghost and Standard Logic Ghost Variables for Extra-Functional Properties Program Logic for Trace Properties and Ghost Variables Example Application Ghost Variables for Object Invariants Conclusion and Further Work Functional Behaviours Big Step Operational Semantics for a Simple Language Logic for Partial Correctness Syntax of Language with Ghost Variables Extra-Functional Behaviours with Traces Semantics of Terminating Executions in the Presence of Traces Semantics of Reachable States in the Presence of Traces Logic for Partial Correctness in the Presence of Traces for the Extended Language Logic for Trace Properties for the Extended Language Logic for Dealing with Invariants Combining a Verification Condition Generator for a Bytecode Language with Static Analyses Introduction Preliminaries Reducing Proof Obligations Preliminary Definitions Combining a Static Analysis with the VCgen Combining Static Analyses and Specifications Certificate Generation and Checking Related Work Conclusions and Future Work Extracting Control from Data: User Interfaces of MIDP Applications Introduction MIDP Application Frameworks A Java Variant for Mobile Phones MIDP User Interface An Axiomatized Semantics of MIDP User Interface Navigation Graphs Use of Navigation Graphs MIDP Security Principles Other Uses Extraction of a Navigation Graph Pointer Analysis Relational Algebra Notations Compound Dependencies Path Selection Algorithm Adding Critical Actions Implementation and Assessment Conclusion Extending Operational Semantics of the Java Bytecode Introduction Preliminaries Bicolano Architecture The Horizontal Extension Framework How to Use the Framework? The Realisation of the Framework The Vertical Extension Framework How to Use the Framework? The Realisation of the Framework The Frameworks Compared Conclusions Relational Analysis for Delivery of Services Introduction The Accident Service The p$\phi$-Calculus Syntax Semantics Relational Analysis Analysis Domains The Relational Analysis Properties of the Analysis Correctness Implementation Complexity Conclusion Analysability and Subject Reduction Logical Networks: Towards Foundations for Programmable Overlay Networks and Overlay Computing Systems Introduction Virtual Organizations User Application Independence, Parametricity, Universality Functional Units and Protocols in Arigatoni Functional Units The Resource Discovery Protocol (RDP) Inside Routing Tables for Resource Discovery The Virtual Intermittent Protocol (VIP) Inside Routing Tables for Intermittent Participation Social Model, Security, Trust and Implementation Issues The Social Model Underneath Arigatoni Trust, Security, and Implementation Issues Related Work, Applications, and Conclusions Discussion on Overlay Topologies Discussion on Closest Technologies Challenges Conclusions and Future Work Type-Safe Distributed Programming with ML5 Introduction Modal Logic IS5 ML5 Validity Polymorphism and Type Inference Web Features Implementation Compiler Runtime Theory Related and Future Work Transactional Service Level Agreement Introduction Constrained-Based SLA Negotations Compensating Transactions From Cjoin to committed pi Committed cc-pi Syntax Operational Semantics Example: A Transactional SLA Big-Step Operational Semantics Concluding Remarks On the Complexity of Termination Inference for Processes Introduction Processes and Type Systems Type Inference for Deng and Sangiorgi's Type Systems Inference for Systems S1 and S2 Is in P Hardness of Systems S3 and S4 Summing the Levels Assigned to Names Exploiting Partial Orders on Names System S4': Definition and Properties Type Inference for S4' Conclusion A Practical Approach for Establishing Trust Relationships between Remote Platforms Using Trusted Computing Introduction Related Work Outline of the Paper The Proof of Concept Architecture The Attestation Proxy The Trusted Software Stack The Trusted Java Virtual Machine Trusted PKI Support Conclusion Access Control Based on Code Identity for Open Distributed Systems Introduction The Language A Calculus of Compound Principals Syntax Operational Semantics Examples Example: A Trusted Software Stack Example: Secure E-Commerce A Type System for Certified Processes Related Work Conclusions Service Oriented Architectural Design Introduction Architectural Design Rewriting Design of SRML Diagrams Architectural Elements of SRML Design Productions for SRML Reconfiguration of SRML Diagrams Conclusion Reconfiguration Rule for Module Composition Replicating Web Services for Scalability Introduction Related Work The SOCK Calculus Modelling Behaviour with SOCK Model in SOCK The PEPA Stochastic Process Algebra Relating Markov Chains and ODEs Modelling Performance with PEPA Commentary on the Results Software Tools Conclusions Location-Aware Quality of ServiceMeasurements for Service-Level Agreements Introduction Stochastic Probes Location-Aware Stochastic Probes Impact on Aggregation Communicating Stochastic Probes Worked Example: Wireless Sensor Network Location Probe Measurements Design Immediate Actions and SM-PEPA Immediate Actions and Probes Implementation Conclusions Multipoint Session Types for a Distributed Calculus Introduction Syntax and Operational Semantics Syntax Operational Semantics Type System Subject Reduction and Safety Related Work Conclusions On Progress for Structured Communications Introduction A Calculus for Structured Communications Process Syntax Operational Semantics Typing System for Progress Communication Types Motivating the Design of the Type System Typing Judgements Type System Justifying Examples Subject Reduction and Progress Subject Reduction Progress Conclusion and Future Works A Protocol Compiler for Secure Sessions in ML Sessions for Distributed Programming Specifying Sessions A Language for Sessions Example A: Remote Procedure Call Example B: A Conference Management System Programming with Sessions Programming an RPC Session Session Programming and CMS Example Session Security Compiling Sessions to Modules Concrete Implementation and Benchmarks Conclusions References Application of Dependency Graphs to Security Protocol Analysis Introduction Related Work Dependency Graphs Security Definition Dependency Graphs with Replication Transformations Dead Code Removal The Replacement of Encryptions The Movement of Multiplexers Other Transformations Proving Integrity Properties Results Achieved Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols Introduction Background Proof System Diffie-Hellman Axioms Secretive Protocols Joint Security of Multiple Encryption Schemes Kerberos with DHINIT Modelling the Protocol Security Properties and Proofs IKEv2 Conclusion Anonymity Protocol with Identity Escrow and Analysis in the Applied π-Calculus Introduction Preliminaries Notation The Protocol Model in the Applied Signature and Equations The Protocol Process Analysis of Anonymity Property Auxiliary Results Proof of the Anonymity Property Conclusions Formal Approaches to Information-Hiding Introduction The Possibilistic Approaches The Dining Cryptographers' Problem Nondeterministic Version of the Dining Cryptographers The Probabilistic Approaches Comparison Information Theory Hypothesis Testing Computing the Matrix Associated to a Protocol Computational Soundness of Equational Theories Introduction Preliminaries The Abadi-Rogaway Result Formal Expressions and Equivalence Computational Messages and Indistinguishability Interpretation of Formal Expressions and Soundness Result Extensions Abstract and Computational Algebras Abstract Algebras Deducibility and Static Equivalence Concrete Semantics Relating Abstract and Computational Algebras Soundness and Faithfulness Examples Exclusive OR Modular Exponentiation Ciphers and Lists A Theory for Guessing Attacks Adaptive Soundness Adaptively Sound Theories Symmetric Encryption Modular Exponentiation Composing Encryption with Exponentiation Composing Encryption with XOR Conclusion Adversaries and Information Leaks Introduction Secure Information Flow for a Language with Encryption Termination Leaks in Probabilistic Programs Foundations for Quantitative Information Flow Author Index

This book constitutes the thoroughly refereed post-conference proceedings of the Third Symposium on Trustworthy Global Computing, TGC 2007; it moreover contains tutorials from the adjacent Workshop on the Interplay of Programming Languages and Cryptography, both held in Sophia-Antipolis, France, in November 2007.

The 19 revised papers presented together with 3 invited papers were carefully selected from 48 submissions during two rounds of reviewing and improvement. The TGC 2007 symposium papers focus on providing tools and frameworks for constructing well-behaved applications and for reasoning about their behavior and properties in models of computation that incorporate code and data mobility over distributed networks with highly dynamic topologies and heterogeneous devices. The volume concludes with 3 tutorial papers, presented at the co-located Workshop on the Interplay of Programming Languages and Cryptography.

This Book Constitutes The Thoroughly Refereed Post-conference Proceedings Of The Third Symposium On Trustworthy Global Computing, Tgc 2007; It Also Contains Tutorials From The Adjacent Workshop On The Interplay Of Programming Languages And Cryptography.