Accurate document layout analysis is a key requirement for high-quality PDF document conversion. With the recent availability of public, large ground-truth datasets such as PubLayNet and DocBank, deep-learning models have proven to be very effective at layout detection and segmentation. While these datasets are of adequate size to train such models, they severely lack in layout variability since they are sourced from scientific article repositories such as PubMed and arXiv only. Consequently, the accuracy of the layout segmentation drops significantly when these models are applied on more challenging and diverse layouts. In this paper, we presentDocLayNet, a new, publicly available, document-layout annotation dataset in COCO format. It contains 80863 manually annotated pages from diverse data sources to represent a wide variability in layouts. For each PDF page, the layout annotations provide labelled bounding-boxes with a choice of 11 distinct classes. DocLayNet also provides a subset of double- and triple-annotated pages to determine the inter-annotator agreement. In multiple experiments, we provide baseline accuracy scores (in mAP) for a set of popular object detection models. We also demonstrate that these models fall approximately 10% behind the inter-annotator agreement. Furthermore, we provide evidence that DocLayNet is of sufficient size. Lastly, we compare models trained on PubLayNet, DocBank and DocLayNet, showing that layout predictions of the DocLayNet-trained models are more robust and thus the preferred choice for general-purpose document-layout analysis.

Many enterprises perform data-center transformation, consolidation, and migration in order to improve the efficiency of their IT infrastructures. These transformation projects begin with the discovery of the existing infrastructure, in particular the dependencies between applications. These dependencies are needed in planning, in order to determine how components influence one another, and in relinking, so that the component names and addresses can be updated. Typically, dependency discovery is done by network monitoring and middleware configuration analysis. These existing approaches will often fail to detect dependencies expressed in the application code. In this paper, we present the first method and tool for automatically identifying code-embedded external dependencies in Java Enterprise Edition applications. In addition, our tool can automatically alter the application code to update the dependencies, or externalize them to configuration files. We analyzed over 1000 Java EE applications from three enterprise environments. The results demonstrate the prevalence of code-embedded dependencies that would otherwise have to be identified manually, often causing failures during user-acceptance testing.

Discovering application dependency on data and storage is a key prerequisite for many storage optimization tasks such as data assignment to storage tiers, storage consolidation, virtualization, and handling unused data. However, in the real world these dependencies are rarely known, and discovering them is a challenge because of virtualization at various levels and the need for discovery methods to be non-intrusive. As a result, many optimization tasks are performed, if at all, without the full knowledge of application-to-storage dependencies.This paper presents a non-intrusive application-to-storage discovery method, and while it is built on our prior work, the storage discovery described here is entirely new. We used this discovery method in two production enterprise environments, consisting of about 323 servers, and we show how the discovered data enables three optimization tasks. First, we relate application criticality with storage tiers. Second, we find unused storage devices and we show how this information together with storage consolidation can be used to achieve power savings of up to two orders of magnitude. Third, we identify opportunities for database storage optimization.

We introduce a novel approach to the runtime monitoring of complex system properties. In particular, we present an online algorithm for a safety fragment of metric first-order temporal logic that is considerably more expressive than the logics supported by prior monitoring methods. Our approach, based on automatic structures, allows the unrestricted use of negation, universal and existential quantification over infinite domains, and the arbitrary nesting of both past and bounded future operators. Moreover, we show how to optimize our approach for the common case where structures consist of only finite relations, over possibly infinite domains. Under an additional restriction, we prove that the space consumed by our monitor is polynomially bounded by the cardinality of the data appearing in the processed prefix of the temporal structure being monitored.

Key-dependent message (KDM) security was introduced by Black, Rogaway and Shrimpton to address the case where key cycles occur among encryptions, e.g., a key is encrypted with itself. It was mainly motivated by key cycles in Dolev–Yao models, i.e., symbolic abstractions of cryptography by term alge bras, and a corresponding computational soundness result was later shown by Adão et al. However, both the KDM definition and this soundness result do not allow the general active attacks typical for Dolev–Yao models or for security protocols in general. We extend these definitions to obtain a soundness result under active attacks. We first present a definition AKDM (adaptive KDM) as a KDM equivalent of authenticated symmetric encryption, i.e., it provides chosen-ciphertext security and integrity of ciphertexts for key cycles. However, this is not yet sufficient for the desired computational soundness result and thus we define DKDM (dynamic KDM) that additionally allows limited dynamic revelation of keys. We show that DKDM is sufficient for computational soundness, even in the strong sense of blackbox reactive simulatability (BRSIM)/UC and in cases with joint terms with other operators. We also build on current KDM-secure schemes to construct schemes secure under the new definitions. Moreover, we prove implications or construct separating examples, respectively, for new definitions and existing ones for symmetric encryption.

Key-dependent message security, short KDM security, was introduced by Black, Rogaway and Shrimpton to address the case where key cycles occur among encryptions, e.g., a key is encrypted with itself. It was mainly motivated by key cycles in Dolev-Yao models, i.e., symbolic abstractions of cryptography by term algebras, and a corresponding soundness result was later shown by Adao et al. However, both the KDM definition and this soundness result do not allow the general active attacks typical for Dolev-Yao models and for security protocols in general. We extend these definitions so that we can obtain a soundness result under active attacks.We first present a definition AKDM as a KDM equivalent of authenticated symmetric encryption, i.e., it provides chosen-ciphertext security and integrity of ciphertexts even for key cycles. However, this is not yet sufficient for the desired soundness, and thus we give a definition DKDM that additionally allows limited dynamic revelation of keys.We show that this is sufficient for soundness, even in the strong sense of blackbox reactive simulatability (BRSIM)/UC and including joint terms with other operators. We also present constructions of schemes secure under the new definitions, based on current KDM-secure schemes. Moreover, we explore the relations between the new definitions and existing ones for symmetric encryption in detail, in the sense of implications or separating examples for almost all cases.

We describe a faithful embedding of the Dolev-Yao model of Backes, Pfitzmann, and Waidner (CCS 2003) in the theorem prover Isabelle/HOL. This model is cryptographically sound in the strong sense of blackbox reactive simulatability/UC, which essentially entails the preservation of arbitrary security properties under active attacks and in arbitrary protocol environments. The main challenge in designing a practical formalization of this model is to cope with the complexity of providing such strong soundness guarantees. We reduce this complexity by abstracting the model into a sound, light-weight formalization that enables both concise property specifications and efficient application of our proof strategies and their supporting proof tools. This yields the first tool-supported framework for symbolically verifying security protocols that enjoys the strong cryptographic soundness guarantees provided by reactive simulatability/UC As a proof of concept, we have proved the security of the Needham-Schroeder-Lowe protocol using our framework

Symbolic secrecy of exchanged keys is arguably one of the most important notions of secrecy shown with automated proof tools. It means that an adversary restricted to symbolic operations on terms can never get the entire key into its knowledge set. Cryptographic key secrecy essentially means computational indistinguishability between the real key and a random one, given the view of a much more general adversary. We analyze the cryptographic key secrecy for the strengthened Yahalom protocol, which constitutes one of the most prominent key exchange protocols analyzed symbolically by means of automated proof tools. We show that the strengthened Yahalom protocol does not guarantee cryptographic key secrecy. We further show that cryptographic key secrecy can be proven for a slight simplification of the protocol by exploiting recent results on linking symbolic and cryptographic key secrecy in order to perform a symbolic proof of secrecy for the simplified Yahalom protocol in a specific setting that allows us to derive the desired cryptographic key secrecy from the symbolic proof. The proof holds in the presence of arbitrary active attacks provided that the protocol is relying on standard provably secure cryptographic primitives. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

We investigate the relation between symbolic and cryptographic secrecy properties for cryptographic protocols. Symbolic secrecy of payload messages or exchanged keys is arguably the most important notion of secrecy shown with automated proof tools. It means that an adversary restricted to symbolic operations on terms can never get the entire considered object into its knowledge set. Cryptographic secrecy essentially means computational indistinguishability between the real object and a random one, given the view of a much more general adversary. In spite of recent advances in linking symbolic and computational models of cryptography, no relation for secrecy under active attacks is known yet. For exchanged keys, we show that a certain strict symbolic secrecy definition over a specific Dolev-Yao-style cryptographic library implies cryptographic key secrecy for a real implementation of this cryptographic library. For payload messages, we present the first general cryptographic secrecy definition for a reactive scenario. The main challenge is to separate secrecy violations by the protocol under consideration from secrecy violations by the protocol users in a general way. For this definition we show a general secrecy preservation theorem under reactive simulatability, the cryptographic notion of secure implementation. This theorem is of independent cryptographic interest. We then show that symbolic secrecy implies cryptographic payload secrecy for the same cryptographic library as used in key secrecy. Our results thus enable existing formal proof techniques to establish cryptographically sound proofs of secrecy for payload messages and exchanged keys.

We investigate the relation between symbolic and cryptographic secrecy properties for cryptographic protocols. Symbolic secrecy of payload messages or exchanged keys is arguably the most important notion of secrecy shown with automated proof tools. It means that an adversary restricted to symbolic operations on terms can never get the entire considered object into its knowledge set. Cryptographic secrecy essentially means computational indistinguishability between the real object and a random one, given the view of a much more general adversary. In spite of recent advances in linking symbolic and computational models of cryptography, no relation for secrecy under active attacks is known yet. For exchanged keys, we show that a certain strict symbolic secrecy definition over a specific Dolev-Yao-style cryptographic library implies cryptographic key secrecy for a real implementation of this cryptographic library. For payload messages, we present the first general cryptographic secrecy definition for a reactive scenario. The main challenge is to separate secrecy violations by the protocol under consideration from secrecy violations by the protocol users in a general way. For this definition, we show a general secrecy preservation theorem under reactive simulatability, the cryptographic notion of secure implementation. This theorem is of independent cryptographic interest. We then show that symbolic secrecy implies cryptographic payload secrecy for the same cryptographic library as used in key secrecy. Our results thus enable formal proof techniques to establish cryptographically sound proofs of secrecy for payload messages and exchanged keys.

Important properties of many protocols are liveness or availability, i.e., that something good happens now and then. In asynchronous scenarios, these properties depend on the scheduler, which is usually considered to be fair in this case. The standard definitions of fairness and liveness are based on infinite sequences. Unfortunately, this cannot be applied to most cryptographic protocols since one must restrict the adversary and the runs as a whole to length polynomial in the security parameter. We present the first general definition of polynomial fairness and liveness in asynchronous scenarios which can cope with cryptographic protocols. Furthermore, our definitions provide a link to the common approach of simulatability which is used throughout modern cryptography: We show that polynomial liveness is maintained under simulatability. As an example, we present an abstract specification and a secure implementation of secure message transmission with reliable channels, and prove them to fulfill the desired liveness property, i.e., reliability of messages.

We present a cryptographically sound security proof of the well-known Needham-Schroeder-Lowe public-key protocol for entity authentication. This protocol was previously only proved over unfounded abstractions from cryptography. We show that it is secure against arbitrary active attacks if it is implemented using standard provably secure cryptographic primitives. Nevertheless, our proof does not have to deal with the probabilistic aspects of cryptography and is, hence, in the scope of current automated proof tools. We achieve this by exploiting a recently proposed Dolev-Yao-style cryptographic library with a provably secure cryptographic implementation. Besides establishing the cryptographic security of the Needham-Schroeder-Lowe protocol, our result exemplifies the potential of this cryptographic library and paves the way for the cryptographically sound verification of security protocols by automated proof tools.

We present the first idealized cryptographic library that can be used like the Dolev-Yao model for automated proofs of cryptographic protocols that use nested cryptographic operations, while coming with a cryptographic implementation that is provably secure under active attacks.

Information flow and non-interference have recently become very popular concepts for expressing both integrity and privacy properties. Because of the enormous potential of transmitting information using probabilistic methods of cryptography, interest arose in capturing probabilistic non-interference. We investigate the notion of intransitive probabilistic non-interference in reactive systems, i.e., downgrading of probabilistic information and detection of probabilistic information flow by one or more involved third parties. Based on concrete examples, we derive several definitions that comprise cryptography-related details like error probabilities and computational restrictions. This makes the definitions applicable to systems involving real cryptography. Detection of probabilistic information flow is significantly more complicated to define if several third parties are involved because of the possibilities of secret sharing. We solve this problem by graph-theoretic techniques.

Important properties of many protocols are liveness or availability, i.e. that something good happens now and then. In asynchronous scenarios, these properties obviously depend on the scheduler, which is usually considered to be fair in this case. Unfortunately, the standard definitions of fairness and liveness based on infinite sequences cannot be applied for most cryptographic protocols since one must restrict the adversary and the runs as a whole to polynomial length. We present the first general definition of polynomial fairness and liveness in asynchronous scenarios which is suited to cope with arbitrary cryptographic protocols. Furthermore, our definitions provide a link to the common approach of simulatability which is used throughout modern cryptography, and we show that polynomial liveness is maintained under simulatability. As an example, we present an abstract specification and a secure implementation of secure message transmission with reliable channels, and prove them to fulfill the desired liveness property, i.e., reliability of messages.

We present a rigorous model for secure reactive systems in asynchronous networks with a sound cryptographic semantics, supporting abstract specifications and the composition of secure systems. This enables modular proofs of security, which is essential in bridging the gap between the rigorous proof techniques of cryptography and tool-supported formal proof techniques. The model follows the general simulatability approach of modern cryptography. A variety of network structures and trust models can be described such as static and adaptive adversaries, some examples of this are given. As an example of our specification methodology we provide an abstract and complete specification for Secure Message Transmission, improving on recent results by Lynch (1999), and verify one concrete implementation. Our proof is based on a general theorem on the security of encryption in a reactive multi-user setting, generalizing a recent result by Bellare et. al (2000).

We consider compositional properties of reactive systems that are secure in a cryptographic sense. We follow the well-known simulatability approach, i.e., the specification is an ideal system and a real system should in some sense simulate it. We recently presented the first detailed general definition of this concept for reactive systems that allows abstraction and enables proofs of efficient real-life systems like secure channels or certified mail. We prove two important properties of this definition, preservation of integrity and secure composition: First, a secure real system satis es all integrity requirements (e.g., safety requirements expressed in temporal logic) that are satisfied by the ideal system. Secondly, if a composed system is designed using an ideal subsystem, it will remain secure if a secure real subsystem is used instead. Such a property was so far only known for non-reactive simulatability. Both properties are important for putting formal verification methods for systems u...

A contract is a non-repudiable agreement on a given contract text, i.e., a contract can be used to prove agreement between its signatories to any verifier. A contract signing scheme is used to fairly compute a contract so that, even if one of the signatories misbehaves, either both or none of the signatories obtain a contract. Optimistic contract signing protocols use a third party to ensure fairness, but in such a way that the third party is not actively involved in the fault-less case. Since no satisfactory protocols without any third party exist, this seems to be the best one can hope for. We prove tight lower bounds on the message and round complexity of optimistic contract signing on synchronous and asynchronous networks, and present new and efficient protocols based on digital signatures which achieve provably optimal efficiency. 1 Introduction A contract is a non-repudiable agreement on a given text [4]. A contract signing scheme includes at least three players and two protocol...

We present techniques for efficient anonymous communication with real-time constraints as necessary for services like telephony, where a continuous data stream has to be transmitted. For concreteness, we present the detailed protocols for the narrow-band ISDN (integrated services digital network), although the heart of our techniques-anonymous channels-can also be applied to other networks. For ISDN, we achieve the same data rate as without anonymity, using the same subscriber lines and without any significant modifications to the long-distance network. A precise performance analysis is given. Our techniques are based on mixes, a method for anonymous communication for e-mail-like services introduced by D. Chaum (1981).

We present and compare definitions of "statistically hiding" protocols, and we propose a novel statistically hiding commitment scheme. Informally, a protocol statistically hides a secret if a computationally unlimited adversary who conducts the protocol with the owner of the secret learns almost nothing about it. One definition is based on the L/sub 1/-norm distance between probability distributions, the other on information theory. We prove that the two definitions are essentially equivalent. We also show that statistical counterparts of definitions of computational secrecy are essentially equivalent to our main definitions. Commitment schemes are an important cryptologic primitive. Their purpose is to commit one party to a certain value, while hiding this value from the other party until some later time. We present a statistically hiding commitment scheme allowing commitment to many bits. The commitment and reveal protocols of this scheme are constant-round, and the size of a commitment is independent of the number of bits committed to. This also holds for the total communication complexity, except of course for the bits needed to send the secret when it is revealed. The proof of the hiding property exploits the equivalence of the two definitions.

. Fingerprinting schemes deter people from illegally redistributing digital data by enabling the original merchant of the data to identify the original buyer of a redistributed copy. So-called traitor-tracing schemes have the same goal for keys used to decrypt information that is broadcast in encrypted form. Recently, asymmetric fingerprinting and traitor-tracing schemes were introduced. Here, only the buyer knows the fingerprinted copy after a sale, and if the merchant finds this copy somewhere, he obtains a proof that he found the copy of this particular buyer. This gives both parties security in disputes. First constructions showed the validity of the concept. However, these constructions did not yet achieve much security against collusions, in contrast to known symmetric schemes. This paper presents asymmetric constructions without this restriction. 1 Introduction The main roles in a fingerprinting or traitor tracing scenario are: . merchants, who sell digital data, . buyers, w...

Fail-stop signatures can briefly be characterized as digital signatures that allow the signer to prove that a given forged signature is indeed a forgery. After such a proof has been published, the system can be stopped. This type of security is strictly stronger than that achievable with ordinary digital signatures as introduced by Diffie and Hellman in 1976 and formally defined by Goldwasser, Micali, and Rivest in 1988, which was widely regarded as the strongest possible definition. This paper formally defines fail-stop signatures and shows their relation to ordinary digital signatures. A general construction and actual schemes derived from it follow. They are efficient enough to be used in practice. Next, we prove lower bounds on the efficiency of any fail-stop signature scheme. In particular, we show that the number of secret random bits needed by the signer, the only parameter where the complexity of all our constructions deviates from ordinary digital signatures by more than a small constant factor, cannot be reduced significantly.

Untraceable electronic cash means prepaid digital payment systems, usually with offline payments, that protect user privacy. Such systems have recently been given considerable attention by both theory and development projects. However, in most current schemes, loss of a user device containing electronic cash implies a loss of money, just as with real cash. In comparison with credit schemes, this is considered a serious shortcoming. This article shows how untraceable electronic cash can be made loss tolerant, i.e., how the monetary value of the lost data can be recovered. Security against fraud and preservation of privacy are ensured; strong loss tolerance means that not even denial of recovery is possible. In particular, systems based on electronic coins are treated. We present general design principles and options and their instantiation in one concrete payment system. The measures are practical.

Digital signature schemes are a fundamental tool for secure distributed systems. It is important to have a formal notion of what a secure digital signature scheme is, so that there is a clear interface between designers and users of such schemes. A definition that seemed final was given by Goldwasser, Micali, and Rivest in 1988, and although most signature schemes used in practice cannot be proved secure with respect to it, they are all built so that they hopefully fulfil it, e.g., by the inclusion of hash functions or redundancy to counter active attacks.