TY - GEN A1 - Klieme, Eric A1 - Tietz, Christian A1 - Meinel, Christoph T1 - Beware of SMOMBIES BT - Verification of Users based on Activities while Walking T2 - The 17th IEEE International Conference on Trust, Security and Privacy in Computing and Communications (IEEE TrustCom 2018)/the 12th IEEE International Conference on Big Data Science and Engineering (IEEE BigDataSE 2018) N2 - Several research evaluated the user's style of walking for the verification of a claimed identity and showed high authentication accuracies in many settings. In this paper we present a system that successfully verifies a user's identity based on many real world smartphone placements and yet not regarded interactions while walking. Our contribution is the distinction of all considered activities into three distinct subsets and a specific one-class Support Vector Machine per subset. Using sensor data of 30 participants collected in a semi-supervised study approach, we prove that unsupervised verification is possible with very low false-acceptance and false-rejection rates. We furthermore show that these subsets can be distinguished with a high accuracy and demonstrate that this system can be deployed on off-the-shelf smartphones. KW - gait KW - authentication KW - smartphone KW - activities KW - verification KW - behavioral KW - continuous Y1 - 2018 SN - 978-1-5386-4387-7 SN - 978-1-5386-4389-1 U6 - https://doi.org/10.1109/TrustCom/BigDataSE.2018.00096 SN - 2324-9013 SP - 651 EP - 660 PB - IEEE CY - New York ER - TY - JOUR A1 - Lorenz, Claas A1 - Clemens, Vera Elisabeth A1 - Schrötter, Max A1 - Schnor, Bettina T1 - Continuous verification of network security compliance JF - IEEE transactions on network and service management N2 - Continuous verification of network security compliance is an accepted need. Especially, the analysis of stateful packet filters plays a central role for network security in practice. But the few existing tools which support the analysis of stateful packet filters are based on general applicable formal methods like Satifiability Modulo Theories (SMT) or theorem prover and show runtimes in the order of minutes to hours making them unsuitable for continuous compliance verification. In this work, we address these challenges and present the concept of state shell interweaving to transform a stateful firewall rule set into a stateless rule set. This allows us to reuse any fast domain specific engine from the field of data plane verification tools leveraging smart, very fast, and domain specialized data structures and algorithms including Header Space Analysis (HSA). First, we introduce the formal language FPL that enables a high-level human-understandable specification of the desired state of network security. Second, we demonstrate the instantiation of a compliance process using a verification framework that analyzes the configuration of complex networks and devices - including stateful firewalls - for compliance with FPL policies. Our evaluation results show the scalability of the presented approach for the well known Internet2 and Stanford benchmarks as well as for large firewall rule sets where it outscales state-of-the-art tools by a factor of over 41. KW - Security KW - Tools KW - Network security KW - Engines KW - Benchmark testing; KW - Analytical models KW - Scalability KW - Network KW - security KW - compliance KW - formal KW - verification Y1 - 2021 U6 - https://doi.org/10.1109/TNSM.2021.3130290 SN - 1932-4537 VL - 19 IS - 2 SP - 1729 EP - 1745 PB - Institute of Electrical and Electronics Engineers CY - New York ER - TY - THES A1 - Decker, Gero T1 - Design and analysis of process choreographies T1 - Design und Analyse von Prozesschoreographien N2 - With the rise of electronic integration between organizations, the need for a precise specification of interaction behavior increases. Information systems, replacing interaction previously carried out by humans via phone, faxes and emails, require a precise specification for handling all possible situations. Such interaction behavior is described in process choreographies. Choreographies enumerate the roles involved, the allowed interactions, the message contents and the behavioral dependencies between interactions. Choreographies serve as interaction contract and are the starting point for adapting existing business processes and systems or for implementing new software components. As a thorough analysis and comparison of choreography modeling languages is missing in the literature, this thesis introduces a requirements framework for choreography languages and uses it for comparing current choreography languages. Language proposals for overcoming the limitations are given for choreography modeling on the conceptual and on the technical level. Using an interconnection modeling style, behavioral dependencies are defined on a per-role basis and different roles are interconnected using message flow. This thesis reveals a number of modeling "anti-patterns" for interconnection modeling, motivating further investigations on choreography languages following the interaction modeling style. Here, interactions are seen as atomic building blocks and the behavioral dependencies between them are defined globally. Two novel language proposals are put forward for this modeling style which have already influenced industrial standardization initiatives. While avoiding many of the pitfalls of interconnection modeling, new anomalies can arise in interaction models. A choreography might not be realizable, i.e. there does not exist a set of interacting roles that collectively realize the specified behavior. This thesis investigates different dimensions of realizability. N2 - Elektronische Integration zwischen Organisationen erfordert eine präzise Spezifikation des Interaktionsverhaltens: Informationssysteme, die Kommunikation per Telefon, Fax und Email ablösen, können nicht so flexibel und selbständig auf Ausnahmesituationen reagieren wie Menschen. Choreographien ermöglichen es, Interaktionsverhalten genau zu spezifizieren. Diese Modelle zählen die beteiligten Rollen, die erlaubten Interaktionen, Nachrichteninhalte und Verhaltensabhängigkeiten auf und dienen somit als Interaktionsvertrag zwischen den Organisationen. Auch als Ausgangspunkt für eine Anpassung existierender Prozesse und Systeme sowie für die Implementierung neuer Softwarekomponenten finden Choreographien Anwendung. Da ein Vergleich von Choreographiemodellierungssprachen in der Literatur bislang fehlt, präsentiert diese Arbeit einen Anforderungskatalog, der als Basis für eine Evaluierung existierender Sprachen angewandt wird. Im Kern führt diese Arbeit Spracherweiterungen ein, um die Schwächen existierender Sprachen zu überwinden. Die vorgestellten Erweiterungen adressieren dabei Modellierung auf konzeptioneller und auf technischer Ebene. Beim Verlinkungsmodellierungsstil werden Verhaltensabhängigkeiten innerhalb der beteiligten Rollen spezifiziert und das Interaktionsverhalten entsteht durch eine Verlinkung der Kommunikationsaktivitäten. Diese Arbeit stellt einige "Anti-Pattern" für die Verlinkungsmodellierung vor, welche wiederum Untersuchungen bzgl. Choreographiesprachen des Interaktionsmodellierungsstils motivieren. Hier werden Interaktionen als atomare Blöcke verstanden und Verhaltensabhängigkeiten werden global definiert. Diese Arbeit führt zwei neue Choreographiesprachen dieses zweiten Modellierungsstils ein, welche bereits in industrielle Standardisierungsinitiativen eingeflossen sind. Während auf der einen Seite zahlreiche Fallstricke der Verlinkungsmodellierung umgangen werden, können in Interaktionsmodellen allerdings neue Anomalien entstehen. Eine Choreographie kann z.B. "unrealisierbar" sein, d.h. es ist nicht möglich interagierende Rollen zu finden, die zusammen genommen das spezifizierte Verhalten abbilden. Dieses Phänomen wird in dieser Arbeit über verschiedene Dimensionen von Realisierbarkeit untersucht. KW - Prozessmodellierung KW - Choreographien KW - Interaktionsmodellierung KW - Verifikation KW - Sprachdesign KW - Process modeling KW - choreographies KW - interaction modeling KW - verification KW - language design Y1 - 2009 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-40761 ER -