No description available.

This diploma thesis is focused on the analysis of security tools, which are commonly used for automatic verification of security protocols mainly. These security protocols are used for creation of private communication channells in insecured networks. Security will never be perfect, so finding of weaknesses in security protocols is always necessary and we need to improve these protocols. In this diploma thesis I have focused on looking for various verification tools on Internet. Subsequently, I have described each tool in this thesis, in way that each reader can easily find out, which tool is for him useful and which is not. I have summarized main benefits and drawbacks of each tool at the end of his description.

The aim of the master's thesis "Analysis of Selected Payment Protocols" is overview of used payment. The first part is concentrated on data security, the second is dedicated to payment protocols, their characteristics, used technology and security elements. The third part is dedicated to verification and simulation tools. Comparison of particular payment protocols and of particular verification tools is part of this work too. Experimental part of the thesis is focused on formalization and verification of the payment protocol Visa 3-D Secure, of the protocol NetBill and on formalization of two subprotocols of SET.

Over the past ten years, the architecture community has witnessed the end of single-threaded performance scaling and a subsequent shift in focus toward multicore and manycore processing. While this is an exciting time for architects, with many new opportunities and design spaces to explore, this brings with it some new challenges. One area that is especially impacted is the memory subsystem. Specifically, the design, verification, and evaluation of cache coherence protocols becomes very challenging as cores become more numerous and more diverse. This dissertation examines these issues and presents Manager-Client Pairing as a solution to the challenges facing next-generation coherence protocol design. By defining a standardized coherence communication interface and permissions checking algorithm, Manager-Client Pairing enables coherence hierarchies to be constructed and evaluated quickly without the high design-cost previously associated with hierarchical composition. Further, Manager-Client Pairing also allows for verification composition, even in the presence of protocol heterogeneity. As a result, this rapid development of diverse protocols is ensured to be bug-free, enabling architects to focus on performance optimization, rather than debugging and correctness concerns, while comparing diverse coherence configurations for use in future heterogeneous systems.

Unreliable communication channels are a practical reality. They add to the complexity of protocol design and verification. In this work, we consider noisy channels which can corrupt messages. We present an approach to model and verify protocols which combine error detection and error control to provide reliable communication over noisy channels. We call these protocols retransmission protocols as they achieve reliable communication through repeated retransmissions of messages. These protocols typically use cyclic redundancy checks and sliding window protocols for error detection and control respectively. We propose models of these protocols as regular transducers operating on bit strings. Deterministic streaming string transducers provide a natural way of modeling these protocols and formalizing correctness requirements. The verification problem is posed as functional equivalence between the protocol transducer and the specification transducer. Functional equivalence checking is decidable for this class of transducers and this makes the transducer models amenable to algorithmic verification. In our transducer models, message lengths and retransmission rounds are unbounded. We present case studies based on TinyOS serial communication and the HDLC retransmission protocol. We further extend our protocol models to capture the effects of a noisy channel with non-determinism. We present two non-deterministic yet decidable extensions of transducer models of retransmission protocols. For one of our models, we achieve decidable verification by bounding the retransmission rounds, whereas for the other, even retransmission rounds are unbounded.

<div>Comprehensive networking security is a goal to achieve for enterprise networks. In forensics, the traffic analysis, causality dependence in intricate program network flows is needed in flow-based attribution techniques. The provenance, the connection between stealthy advanced persistent threats (APTs) and the execution of loadable modules is stripped because loading a module does not guarantee an execution. The reports of common vulnerabilities and exposures (CVE) demonstrate that lots of vulnerabilities have been introduced in protocol engineering process, especially for the emerging Internet-of-Things (IoT) applications. A code generation framework targeting secure protocol implementations can substantially enhance security.</div><div>A novel automaton-based technique, NetCrop, to infer fine-grained program behavior by analyzing network traffic is proposed in this thesis. Based on network flow causality, it constructs automata that describe both the network behavior and the end-host behavior of a whole program to attribute individual packets to their belonging programs and fingerprint the high-level program behavior. A novel provenance-oriented library tracing system, Lprov, which enforces library tracing on top of existing syscall logging based provenance tracking approaches is investigated. With the dynamic library call stack, the provenance of implicit library function execution is revealed and correlated to system events, facilitating the locating and defense of malicious libraries. The thesis presents ProFactory, in which a protocol is modeled, checked and securely generated, averting common vulnerabilities residing in protocol implementations.</div>

Security protocols are ubiquitously used in various applications with the intention to ensure secure and private communication. To achieve this goal, a mechanism offering reliable and systematic protocol verification is needed. Accordingly, a major interest in academic research on formal methods for protocol analysis has been apparent for the last two decades. Such methods formalize the operational semantics of a protocol, laying the base for protocol verification with automatic model checking tools. So far, little work in this field has focused on protocol standardization. Within this thesis a security analysis of a novel Authenticated Key-Exchange (AKE) protocol for secure association handover between two Long-Term Evolution (LTE) base stations (which support dual-connectivity) is carried out by applying two state-of-the-art tools for automated model checking (Scyther and Tamarin Prover). In the course of this a formal protocol model and tool input models are developed. Finally, the suitability of the used tools for LTE protocol analysis is evaluated. The major outcome is that none of the two applied tools is capable to accurately model and verify the dual-connectivity protocol in such detail that it would make them particularly useful in the considered setting. The reason for this are restrictions in the syntax of Scyther and a degraded performance of Tamarin when using complex protocol input models. However, the use of formal methods in protocol standardization can be highly beneficial, since it implies a careful consideration of a protocol’s fundamentals. Hence, formal methods are helpful to improve and structure a protocol’s design process when applied in conjunction to current practices. / Säkerhetsprotokoll används i många typer av applikationer för att säkerställa säkerhet och integritet för kommunikation. För att uppnå detta mål behövs en behövs mekanismer som tillhandahåller pålitlig och systematisk verifiering av protokollen. Därför har det visats stort akademiskt intresse för forskning inom formell verifiering av säkerhetsprotokoll de senaste två decennierna. Sådana metoder formaliserar protokollsemantiken, vilket lägger grunden till automatiserad verifiering med modellverifieringsverktyg. Än så la¨nge har det inte varit stort focus på praktiska tilla¨mpningar, som t.ex. hur väl metoderna fungerar för de problem som dyker upp under en standardiseringsprocess. I detta examensarbete konstrueras en formell modell för ett säkerhetsprotokoll som etablerar en säkerhetsassociation mellan en terminal och två Long-Term Evolution (LTE) basstationer i ett delsystem kallat Dual Connectivity. Detta delsystem standardiseras för närvarande i 3GPP. Den formella modellen verifieras sedan med bästa tillgängliga verktyg för automatiserad modellverifiering (Scyther och Tamarin Prover). För att åstadkomma detta har den formella modellen implementerats i inmatningsspråken för de två verktygen.  Slutligen ha de två verktygen evaluerats. Huvudslutsatsen är att inget av de två verktygen tillräckligt väl kan modellera de koncept där maskinstödd verifiering som mest behövs. Skälen till detta är Scythers begränsade syntax, och Tamarins begränsade prestanda och möjlighet att terminera för komplexa protokollmodeller. Trots detta är formella metoder andvändbara i standardiseringsprocessen eftersom de tvingar fram väldigt noggrann granskning av protokollens fundamentala delar. Därför kan formella metoder bidra till att förbättra strukturen på protokollkonstruktionsprocessen om det kombineras med nuvarande metoder.