Financial Cryptography and Data Security [[electronic resource] ] : 20th International Conference, FC 2016, Christ Church, Barbados, February 22–26, 2016, Revised Selected Papers / / edited by Jens Grossklags, Bart Preneel

• Record Nr.: UNISA996466456503316
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017
• ISBN: 3-662-54970-0
• Edizione: [1st ed. 2017.]
• Descrizione fisica: 1 online resource (XIV, 620 p. 135 illus.)
• Collana: Security and Cryptology ; ; 9603
• Disciplina: 005.82
• Soggetti: Data encryption (Computer science); Computer security; E-commerce; Application software; Computer communication systems; Cryptology; Systems and Data Security; e-Commerce/e-business; Computer Appl. in Administrative Data Processing; Computer Communication Networks
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Includes index.
• Nota di contenuto: Fraud and deception -- Payments, auctions, and e-voting -- Multiparty computation -- Mobile malware -- Social interaction and policy -- Cryptanalysis -- Surveillance and anonymity -- Web security and data privacy -- Bitcoin mining -- Cryptographic protocols -- Payment use and abuse.
• Sommario/riassunto: This book constitutes the thoroughly refereed post-conference proceedings of the 20th International Conference on Financial Cryptography and Data Security, FC 2016, held in Christ church, Barbados, in February 2016. The 27 revised full papers and 9 short papers were carefully selected and reviewed from 137 full papers submissions. The papers are grouped in the following topical sections: ; fraud and deception; payments, auctions, and e-voting; multiparty computation; mobile malware; social interaction and policy; cryptanalysis; surveillance and anonymity; Web security and data privacy; Bitcoin mining; cryptographic protocols; payment use and abuse.

Formal Modeling and Analysis of Timed Systems : 12th International Conference, FORMATS 2014, Florence, Italy, September 8-10, 2014, Proceedings / / edited by Axel Legay, Marius Bozga

• Record Nr.: UNINA9910484397403321
• Pubbl/distr/stampa: Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014
• ISBN: 3-319-10512-4
• Edizione: [1st ed. 2014.]
• Descrizione fisica: 1 online resource (X, 253 p. 74 illus.)
• Collana: Theoretical Computer Science and General Issues, , 2512-2029 ; ; 8711
• Disciplina: 003.3
• Soggetti: Computer science; Software engineering; Application software; Theory of Computation; Computer Science Logic and Foundations of Programming; Software Engineering; Computer and Information Systems Applications
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di contenuto: Intro -- Preface -- Organization -- Table of Contents -- The Modeling and Analysis of Mixed-Criticality Systems -- References -- Modeling Bitcoin Contracts by Timed Automata -- 1 Introduction -- 1.1 A Short Description of Bitcoin -- 2 Modeling the Bitcoin -- 2.1 The Keys, the Secret Strings, and the Signatures -- 2.2 The Transactions -- 2.3 The Parties -- 2.4 The Adversary -- 2.5 The Block Chain and the Notion of Time -- 3 Modeling the Bitcoin-Based Timed Commitment Scheme from [8] -- 3.1 The Results of the Verification -- 3.2 The NewSCS ; Protocol from [8] -- References -- Data-Driven Statistical Learning of Temporal Logic Properties -- 1 Introduction -- 2 Problem Statement and Methodology -- 2.1 Statistical Modelling of Data: Learning and Model Selection -- 2.2 Learning Properties -- 3 Results -- 3.1 Logical Characterisation of a Biological Oscillator -- 3.2 Logical Discrimination of Cardiac Arrhythmias -- 4 Related Work -- 5 Conclusions -- References -- Finding Best and Worst Case Execution Times of Systems Using Difference-Bound Matrices -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 The Zone Approach -- 2.3 The Difference Bound Matrices -- 3 Zone-Based Algorithms For Calculating BCET and WCET -- 3.1 The Zone-Based Algorithms -- 4 Implementation -- 5 Case Studies -- 6 Conclusion -- References -- Delay-Dependent Partial Order Reduction Technique for Time Petri Nets -- 1 Introduction -- 2 Time Petri Nets -- 2.1 Definition and Semantics -- 2.2 Contracted State Class Graph -- 3 Partial Order Reduction Based on POSETs -- 3.1 Partial Order Successors and Reduced State Class Graphs -- 4 RSCG Preserving Non-equivalent Sequences of N -- 4.1 Delay Lower Bound Matrix of N -- 4.2 Computing a Partial Order Generator G -- 4.3 Does G Preserve the Non-equivalent Firing Sequences of N? -- 5 Experimental Results -- 6 Conclusion -- References.; On MITL and Alternating Timed Automata over Infinite Words -- 1 Introduction -- 2 Preliminaries -- 3 The Intervals Semantics for OCATA on Infinite Words -- 4 TOCATA: A Class of OCATA for MITL -- 5 MITL Model-Checking and Satisfiability with TOCATA -- 6 Experimental Results -- References -- Time Petri Nets with Dynamic Firing Dates: Semantics and Applications -- 1 Introduction -- 2 Time Petri Nets and Fickle Transitions -- 2.1 A Semantics for Time Petri Nets Based on Firing Functions -- 2.2 Interesting Classes of DTPN -- 2.3 Interpretation of the Quantized State System Model -- 3 A State Class Abstraction for Dynamic TPN -- 4 Two Application for Dynamic TPN -- 4.1 Scheduling Preemptive Tasks -- 4.2 Verification of Linear Hybrid systems -- 5 Conclusion and Related Work -- References -- Verification and Performance Evaluation of Timed Game Strategies -- 1 Introduction -- 2 Timed Game -- 2.1 Timed Game Automata -- 2.2 A Running Example -- 3 Stochastic Priced Timed Automata -- 3.1 Priced Timed Automata -- 3.2 Stochastic Semantics -- 4 Translating Strategies to Timed Automata -- 4.1 The Method -- 4.2 The Running Example -- 5 MC and SMC under Strategies -- 5.1 Extended Stochastic Semantics -- 5.2 Implementation -- 5.3 The Running Example -- 6 Experiments Results -- 6.1 Case Study 1: Jobshop -- 6.2 Case Study 2: Train-Gate -- 7 Future Work -- References -- The Power of Proofs: New Algorithms for Timed Automata Model Checking -- 1 Introduction -- 2 Background -- 2.1 Timed Automata -- 2.2 Timed Logic Lrel ν,μ and Modal Equation Systems (MES) -- 3 Checking Lrel ,af ν,μ Properties: A Proof-Based Approach -- 3.1 Proof Rules for Laf ν,μ Over Timed Automata -- 3.2 New Proof Rules for the Relativized Operators of Lrel ,af ν,μ -- 4 Optimizing Performance via Derived Proof Rules -- 5 Implementation Details -- 5.1 Addressing Non-convexity: Zone Unions.; 5.2 Addressing Performance: Simpler PES Formulas -- 5.3 Placeholder Implementation Complexities -- 6 Performance Evaluation -- 6.1 Methods: Evaluation Design -- 6.2 Data and Results -- 6.3 Analysis and Discussion -- 7 Conclusion -- References -- Anonymized Reachability of Hybrid Automata Networks -- 1 Introduction -- 2 Hybrid Automata Network Syntax and Semantics -- 2.1 Semantics of Hybrid Automata Networks -- 3 Anonymized State-Space Representation -- 4 Anonymized Reachability of Hybrid Automata ; Networks -- 5 Experimental Results -- 6 Summary -- References -- Combined Global and Local Search for the Falsification of Hybrid Systems -- 1 Introduction -- 2 Problem Formulation -- 3 Algorithm -- 4 Algorithmic Details -- 4.1 Computation of the Path of Minimal Cost -- 4.2 Heuristics -- 4.3 Paths of Minimal Cost -- 5 Local Optimization -- 6 Termination Proof -- 7 Computational Experiments -- 8 Related Work -- 9 Conclusion -- References -- Weak Singular Hybrid Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Singular Hybrid Automata -- 2.2 Reachability, Schedulability, and Model-Checking -- 3 Weak Singular Hybrid Automata -- 3.1 Constant-Rate Multi-mode Systems -- 3.2 Syntax and Semantics -- 4 Undecidable Variants of WSHA -- 5 Conclusion -- References -- Non-convex Invariants and Urgency Conditions on Linear Hybrid Automata -- 1 Introduction -- 2 Linear Hybrid Automata with Non-convex Invariants -- 2.1 Definition and Semantics -- 2.2 Computing the Continuous Post Operator with Nonconvex Invariants -- 2.3 Related Work -- 3 Linear Hybrid Automata with Urgency -- 3.1 Definition and Semantics -- 3.2 Reachability -- 3.3 Computing the Urgent Continuous Post Operator -- 3.4 Related Work -- 4 Example: Batch Reactor -- 5 Conclusions -- References.; Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints -- 1 Introduction -- 2 Preliminaries -- 2.1 Sets and Functions Notations -- 2.2 Transition Systems and Hybrid Automata -- 3 Time-Bounded Reachability -- 3.1 Bounding the Execution Length in Logarithmic Timed Automata -- 3.2 Algorithm for Time-Bounded Reachability -- 4 Time-Bounded Reachability is PSPACE-hard in Initialized Linear Inclusion Automata -- 5 Conclusion -- References -- Virtual Integration of Real-Time Systems Based on Resource Segregation Abstraction -- 1 Introduction and Related Work -- 2 Real-Time Interfaces -- 3 Contracts and Virtual Integration -- 4 Compositional Virtual Integration -- 5 Resource Segregation -- 6 Case Study -- 7 Conclusion -- References -- Timed Pattern Matching -- 1 Introduction -- 2 Timed Regular Expressions over Signals -- 3 Match-Sets and Zones -- 4 Computation -- 4.1 Algorithms and Implementation -- 4.2 A Bound on the Number of Iterations -- 5 Experimentation -- 6 Future Work -- References -- Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets -- 1 Introduction -- 2 Definitions -- 3 Interval Abstractions -- 3.1 Approximation Correctness for Reachability -- 3.2 Approximation Correctness for Liveness -- 4 Trace Validation -- 5 Evaluation -- 6 Conclusion -- References -- Author Index.
• Sommario/riassunto: This book constitutes the refereed proceedings of the 12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014, held in Florence, Italy, in September 2014. The 17 revised full papers presented were carefully reviewed and selected from 36 submissions. The papers cover topics of foundations and semantics; comparison between different models, such as timed automata, timed Petri nets, hybrid automata, timed process algebra, max-plus algebra, probabilistic models; methods and tools for analyzing timed systems and resolving temporal constraints; applications in real-time software, hardware circuits, and problems of scheduling in manufacturing and telecommunication.