International Journal Articles

Fatih Turkmen, Jerry den Hartog, Silvio Ranise, and Nicola Zannone. Formal analysis of XACML policies using SMT. Computers & Security, 66:185-203, May 2017. (link, abstract, bib-entry)

Abstract:

The eXtensible Access Control Markup Language (XACML) has attracted significant attention from both industry and academia, and has become the de facto standard for the specification of access control policies. However, its XML-based verbose syntax and rich set of constructs make the authoring of XACML policies difficult and error-prone. Several automated tools have been proposed to analyze XACML policies before their actual deployment. However, most of the existing tools either cannot efficiently reason about non-Boolean attributes, which often appear in XACML policies, or restrict the analysis to a small set of properties. This work presents a policy analysis framework for the verification of XACML policies based on SAT modulo theories (SMT).We show how XACML policies can be encoded into SMT formulas, along with a query language able to express a variety of well-known security properties, for policy analysis. By being able to reason over non-Boolean attributes, our SMT-based policy analysis framework allows a fine-grained policy analysis while relieving policy authors of the burden of defining an appropriate level of granularity of the analysis. An evaluation of the framework shows that it is computationally efficient and requires less memory compared to existing approaches.

E Costante, J den Hartog, Milan Petkovic, S Etalle, and M Pechenizkiy. A white-box anomaly-based framework for database leakage detection. Journal of Information Security and Applications, 2016. (link, abstract, bib-entry)

Abstract:

Data leakage is at the heart most of the privacy breaches worldwide. In this paper we present a white-box approach to detect potential data leakage by spotting anomalies in database transactions. We refer to our solution as white-box because it builds self explanatory profiles that are easy to understand and update, as opposite to black-box systems which create profiles hard to interpret and maintain (e.g., neural networks). In this paper we introduce our approach and we demonstrate that it is a major leap forward w.r.t. previous work on the topic in several aspects: (i) it significantly decreases the number of false positives, which is orders of magnitude lower than in state-of-the-art comparable approaches (we demonstrate this using an experimental dataset consisting of millions of real enterprise transactions); (ii) it creates profiles that are easy to understand and update, and therefore it provides an explanation of the origins of an anomaly; (iii) it allows the introduction of a feedback mechanism that makes possible for the system to improve based on its own mistakes; and (iv) feature aggregation and transaction flow analysis allow the system to detect threats which span over multiple features and multiple transactions.

S.P. Kaluvuri, A.I. Egner, J.I. den Hartog, and N. Zannone. SAFAX-an extensible authorization service for cloud environments. Frontiers in ICT, 2:9, 2015. (link, abstract, bib-entry)

Abstract:

Cloud storage services have become increasingly popular in recent years. Users are often registered to multiple cloud storage services that suit different needs. However, the ad hoc manner in which data sharing between users is implemented lead to issues for these users. For instance, users are required to define different access control policies for each cloud service that they use and are responsible for synchronizing their policies across different cloud providers. Users do not have access to a uniform and expressive method to deal with authorization. Current authorization solutions cannot be applied as-is, since they cannot cope with challenges specific to cloud environments. In this paper, we analyze the challenges of data sharing in multi-cloud environments and propose SAFAX, an XACML-based authorization service designed to address these challenges. SAFAX’s architecture allows users to deploy their access control policies in a standard format, in a single location, and augment policy evaluation with information from user selectable external trust services. We describe the architecture of SAFAX, a prototype implementation based on this architecture, illustrate the extensibility through external trust services and discuss the benefits of using SAFAX from both the user’s and cloud provider’s perspectives.

E. Costante, J.I. den Hartog, and M. Petkovic. Understanding perceived trust to reduce regret. Computational Intelligence, 31(2):327-347, May 2015. (link, abstract, bib-entry)

Abstract:

Trust is fundamental for promoting the use of online services, such as e-commerce or e-health. Understanding how users perceive trust online is a precondition to create trustworthy marketplaces. In this article, we present a domain-independent general trust perception model that helps us to understand how users make online trust decisions and how we can help them in making the right decisions, which minimize future regret. We also present the results of a user study describing the weight that different factors in the model (e.g., security, look&feel, and privacy) have on perceived trust. The study identifies the existence of a positive correlation between the user's knowledge and the importance placed on factors such as security and privacy. This indicates that the impact factors as security and privacy have on perceived trust is higher in users with higher knowledge.

L. Bauer, S. Etalle, J.I. den Hartog, and L. Viganó. Preface of special issue on "computer security: Foundations and automated reasoning". Journal of Automated Reasoning, 46 (3-4):223-224, April 2011. (link, abstract, bib-entry)

K. Böhm, S. Etalle, J. I. den Hartog, C. Hütter, S. Trabelsi, D. Trivellato, and N. Zannone. A flexible architecture for privacy-aware trust management. Journal of Theoretical and Applied Electronic Commerce Research, 5(2):77-96, August 2010. ISSN 0718-1876. (link, abstract, bib-entry)

Abstract:

In service-oriented systems a constellation of services cooperate, sharing potentially sensitive information and responsibilities. Cooperation is only possible if the different participants trust each other. As trust may depend on many different factors, in a flexible framework for Trust Management (TM) trust must be computed by combining different types of information. In this paper we describe the TAS3 TM framework which integrates independent TM systems into a single trust decision point. The TM framework supports intricate combinations whilst still remaining easily extensible. It also provides a unified trust evaluation interface to the (authorization framework of the) services. We demonstrate the flexibility of the approach by integrating three distinct TM paradigms: reputation-based TM, credential-based TM, and Key Performance Indicator TM. Finally, we discuss privacy concerns in TM systems and the directions to be taken for the definition of a privacy-friendly TM architecture.

J.I. den Hartog. Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic hoare style logic. Science of Computer Programming, 74(1-2):52-63, 2008. (link, abstract, bib-entry)

J. G. Cederquist, R. J. Corin, M. A. C. Dekker, S. Etalle, J. I. den Hartog, and G. Lenzini. Audit-based compliance control. International Journal of Information Security, 6(2-3):133-151, 2007. ISSN 1615-5262. (link, abstract, bib-entry)

Abstract:

In this paper we introduce a new framework for controlling compliance to discretionary access control policies [Cederquist et al. in Proceedings of the International Workshop on Policies for Distributed Systems and Networks (POLICY), 2005; Corin et al. in Proceedings of the IFIP Workshop on Formal Aspects in Security and Trust (FAST), 2004]. The framework consists of a simple policy language, modeling ownership of data and administrative policies. Users can create documents, and authorize others to process the documents. To control compliance to the document policies, we define a formal audit procedure by which users may be audited and asked to justify that an action was in compliance with a policy. In this paper we focus on the implementation of our framework.We present a formal proof system, which was only informally described in earlier work. We derive an important tractability result (a cut-elimination theorem), and we use this result to implement a proof-finder, a key component in this framework. We argue that in a number of settings, such as collaborative work environments, where a small group of users create and manage document in a decentralized way, our framework is a more flexible approach for controlling the compliance to policies.

J.I. den Hartog and E.P. de Vink. Verifying probabilistic programs using a Hoare like logic. International Journal of Foundations of Computer Science, 13(3):315-340, 2002. (link, abstract, bib-entry)

Abstract:

Probability, be it inherent or explicitly introduced, has become an important issue in the verification of many programs. We study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify properties of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates are introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be correct and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.

J. I. den Hartog, E. P. de Vink, and J. W. de Bakker. Full abstractness of a metric semantics for action refinement. Fundamenta Informaticae, 40:335-382, 1999. ISSN 0169-2968. (link, abstract, bib-entry)

Abstract:

For a process language with action refinement and synchronization both an operational and a denotational semantics are given. The operational semantics is based on an SOS-style transition system specification involving syntactical refinement sequences. The denotational semantics is an interleaving model which uses semantical refinement `environments'. It identifies those statements which are equal under all refinements. The denotational model is shown to be fully abstract with respect to the operational one. The underlying metric machinery is exploited to obtain this full abstractness result. Usually, action refinement is treated either in a model with some form of true concurrency, or, when an interleaving model is applied, by assuming that the refining statements are atomized. We argue that an interleaving model without such atomization is attractive as well.

International Conference and Workshop Publications

Ömer Yüksel, Jerry den Hartog, and Sandro Etalle. Towards useful anomaly detection for back office networks. In Proceedings twelfth International Conference on Information Systems Security (ICISS-2016), LNCS. (link, abstract, bib-entry)

Abstract:

In this paper we present a protocol-aware anomaly detection framework specifically designed for back office networks together with a new automatic method for feature selection that allows to dramatically reduce the false positive rate (FPR) without compromising the detection rate (DR). The system monitors SMB and MS-RPC (the main protocols in back office networks) and takes into consideration specific features of SMB such as the presence of file paths, which are noisy, yet contain information necessary to detect some attacks. As a part of the framework we introduce a new method to cut the FPR by carefully building and selecting the right set of features to be monitored. In back office networks this is a challenging task where manual selection requires carefully exploring the network traffic to choose from numerous potential features. Also features need to be resilient to irregularities in the traffic caused by human involvement. Our framework automates selection utilizing two new metrics to determine the ‘quality’ of a feature: stability, i.e. its robustness to false alarms and granularity, i.e. the relative amount of information contained. Our experiments show a significant improvement in FPR-DR trade-off when our framework is used to select features in detection of network-based exploits and malicious file accesses.

J.I. den Hartog and N. Zannone. Collaborative access decisions: Why has my decision not been enforced? In Proceedings twelfth International Conference on Information Systems Security (ICISS-2016), LNCS. (link, abstract, bib-entry)

Abstract:

With the increasing popularity of collaborative systems like social networks, the risk of data misuse has become even more critical for users. As a consequence, there is a growing demand for solutions to properly protect data created and used within these systems. Enabling collaborative specification of permissions, while ensuring an appropriate levels of control to the different parties involved, inherently leads to decisions of some users being overruled by the policies of other users. Users need to be aware that this is happening and why, otherwise they may lose trust in the system, which can impact their willingness to collaborate. Enhancing user awareness requires that users know about and understand the conflicts that occurred. In this paper, we propose an approach to compute a justification for a decision in cases where conflicts occur and, based on this, generate feedback that explains users why their decision was not enforced.

Stefan Thaler, Jerry den Hartog, and Milan Petkovic. Towards creating believable decoy project folders for detecting data theft. In IFIP Annual Conference on Data and Applications Security and Privacy, pages 161-169. Springer International Publishing, 2016. (link, abstract, bib-entry)

Abstract:

Digital data theft is difficult to detect and typically it also takes a long time to discover that data has been stolen. This paper introduces a data-driven approach based on Markov chains to create believable decoy project folders which can assist in detecting potentially ongoing attacks. This can be done by deploying these intrinsically valueless folders between real project folders and by monitoring interactions with them. We present our approach and results from a user study demonstrating the believability of the generated decoy folders.

Rauf Mahumudlu, J.I. den Hartog, and N. Zannone. Data governance & transparency for collaborative systems. In IFIP Annual Conference on Data and Applications Security and Privacy, pages 199-216. Springer International Publishing, 2016. (link, abstract, bib-entry)

Abstract:

As social networks, shared editing platforms and other collaborative systems are becoming increasingly popular, the demands for proper protection of the data created and used within these systems grows. Yet, existing access control mechanisms are not suited for the challenges imposed by collaborative systems. Two main challenges should be addressed: collaborative specification of permissions, while ensuring an appropriate levels of control to the different parties involved, and enabling transparency in decision making in cases where the access requirements of these different parties are in conflict. In this paper we propose a data governance model for collaborative systems, which allows the integration of access requirements specified by different users based on their relation with a data object. We also study the practical feasibility of enabling transparency by comparing different deployment options for transparency in XACML.

E. Costante, S Etalle, D. Fauri, J.I. den Hartog, and N. Zannone. A hybrid framework for data loss prevention and detection. In Proceedings of the Workshop on Research for Insider Threats (WRIT 2016), pages 324-333. IEEE, 2016. ISBN 978-1-5090-3690-5. workshop at IEEE Symposium on Security and Privacy. (link, abstract, bib-entry)

Abstract:

Data loss, i.e. the unauthorized/unwanted disclosure of data, is a major threat for modern organizations. Data Loss Protection (DLP) solutions in use nowadays, either employ patterns of known attacks (signature-based) or try to find deviations from normal behavior (anomaly-based). While signature-based solutions provide accurate identification of known attacks and, thus, are suitable for the prevention of these attacks, they cannot cope with unknown attacks, nor with attackers who follow unusual paths (like those known only to insiders) to carry out their attack. On the other hand, anomaly-based solutions can find unknown attacks but typically have a high false positive rate, limiting their applicability to the detection of suspicious activities. In this paper, we propose a hybrid DLP framework that combines signature-based and anomaly-based solutions, enabling both detection and prevention. The framework uses an anomaly-based engine that automatically learns a model of normal user behavior, allowing it to flag when insiders carry out anomalous transactions. Typically, anomaly-based solutions stop at this stage. Our framework goes further in that it exploits an operator's feedback on alerts to automatically build and update signatures of attacks that are used to timely block undesired transactions before they can cause any damage.

Ömer Yüksel, Jerry den Hartog, and Sandro Etalle. Reading between the fields: Practical, effective intrusion detection for industrial control systems. In Proceedings 31st ACM/SIGAPP Symposium on Applied Computing (SAC 2016), volume 1, pages 2063-2070, New York, NY, USA, April 2016. ACM. (link, abstract, bib-entry)

Abstract:

Detection of previously unknown attacks and malicious messages is a challenging problem faced by modern network intrusion detection systems. Anomaly-based solutions, despite being able to detect unknown attacks, have not been used often in practice due to their high false positive rate, and because they provide little actionable information to the security officer in case of an alert. In this paper we focus on intrusion detection in industrial control systems networks and we propose an innovative, practical and semantics-aware framework for anomaly detection. The network communication model and alerts generated by our framework are userunderstandable, making them much easier to manage. At the same time the framework exhibits an excellent tradeoff between detection rate and false positive rate, which we show by comparing it with two existing payload-based anomaly detection methods on several ICS datasets.

J.I. den Hartog and N. Zannone. A policy framework for data fusion and derived data control. In Proceedings of the 2016 ACM International Workshop on Attribute Based Access Control, pages 47-57, 2016. ISBN 978-1-4503-4079-3. Codaspy workshop. (link, abstract, bib-entry)

Abstract:

Recent years have seen an exponential growth of the collection and processing of data from heterogeneous sources for a variety of purposes. Several methods and techniques have been proposed to transform and fuse data into "useful" information. However, the security aspects concerning the fusion of sensitive data are often overlooked. This paper investigates the problem of data fusion and derived data control. In particular, we identify the requirements for regulating the fusion process and eliciting restrictions on the access and usage of derived data. Based on these requirements, we propose an attribute-based policy framework to control the fusion of data from different information sources and under the control of different authorities. The framework comprises two types of policies: access control policies, which define the authorizations governing the resources used in the fusion process, and fusion policies, which define constraints on allowed fusion processes. We also discuss how such policies can be obtained for derived data.

A.I. Egner, D Luu, J.I. den Hartog, and N. Zannone. An authorization service for collaborative situation awareness. In Proceedings of the 6th ACM Conference on Data and Application Security and Privacy (CODASPY 2016), pages 136-138, 2016. ISBN 978-1-4503-3935-3. (link, abstract, bib-entry)

Abstract:

In international military coalitions, situation awareness is achieved by gathering critical intel from different authorities. Authorities want to retain control over their data, as they are sensitive by nature, and, thus, usually employ their own authorization solutions to regulate access to them. In this paper, we highlight that harmonizing authorization solutions at the coalition level raises many challenges. We demonstrate how we address authorization challenges in the context of a scenario defined by military experts using a prototype implementation of SAFAX, an XACML-based architectural framework tailored to the development of authorization services for distributed systems.

E. Costante, D. Fauri, S Etalle, J.I. den Hartog, and N. Zannone. Poster: Combining data loss prevention and detection. In IEEE Symposium on Security and Privacy, 2016. http://www.ieee-security.org/TC/SP2016/poster-abstracts/58-poster_abstract.pdf. (link, abstract, bib-entry)

Abstract:

In this paper, we propose a hybrid Data Loss Protection framework that combines signature-based and anomaly-based solutions, enabling both detection and prevention of unauthorized disclosures of data. The framework uses an anomaly-based engine that automatically learns a model of normal user behavior, allowing it to flag when insiders carry out anomalous transactions. Typically, anomaly-based solutions stop at this stage. Our framework goes further in that it exploits an operator’s feedback on alerts to automatically build and update signatures of attacks which are used to timely block undesired transactions before they can cause any damage.

F. Turkmen, J.I. den Hartog, S. Ranise, and N. Zannone. Analysis of xacml policies with smt. In 4th Conference on Principles of Security and Trust (POST 2015), 2015. (link, abstract, bib-entry)

Abstract:

The eXtensible Access Control Markup Language (XACML) is an extensible and flexible XML language for the specification of access control policies. However, the richness and flexibility of the language (along with the verbose syntax of XML) come with a price: errors are easy to make and difficult to detect when policies grow in size. If these errors are not detected and rectified, they can result in serious data leakage and/or privacy violations leading to significant legal and financial consequences. To assist policy authors in the analysis of their policies, several policy analysis tools have been proposed based on different underlying formalisms. However, most of these tools either abstract away functions over non-Boolean domains (hence they cannot provide information about them) or produce very large encodings which hinder the performance. In this paper, we present a generic policy analysis framework that employs SMT as the underlying reasoning mechanism. The use of SMT does not only allow more fine-grained analysis of policies but also improves the performance. We demonstrate that a wide range of security properties proposed in the literature can be easily modeled within the framework. A prototype implementation and its evaluation are also provided.

S. Thaler, J. den Hartog, D. Ayed, D. Sommer, and M.l. Hitchens. Attribute-based authentication and authorization for collaborative services. In Proc. of the 10th International Conference on Availability, Reliability and Security (ARES), Workshop AU2EU, 2015. (link, abstract, bib-entry)

Abstract:

Authentication and authorisation has been a basic and necessary service for internet transactions. With the evolution of e-commerce, traditional mechanisms for data security and access control are becoming outdated. Several new standards have emerged which allow dynamic access control based on exchanging user attributes. Unfortunately, while providing highly secure and flexible access mechanisms is a very demanding task, it cannot be considered a core competency for most e-commerce corporations. Therefore, a need to outsource or at least share such services with other entities arises. Authen-tication and Authorisation Infrastructures (AAIs) can provide such integrated federations of security services. They could, in particular, provide attribute-based access control (ABAC) mechanisms and mediate customers’ demand for privacy and vendors’ needs for information. We propose an AAI reference model that includes ABAC functionality based on the XACML standard and lessons learned from various existing AAIs. AAIs analysed are AKENTI, CARDEA, CAS, GridShib, Liberty ID-FF, Microsoft .NET Passport, PAPI, PERMIS, Shibboleth and VOMS.

U.S. Sher, J.I. den Hartog, S. Etalle, and N. Zannone. Auditing with incomplete logs. In Proceedings of the 3rd Workshop on Hot Issues in Security Principles and Trust, pages 1-23, 2015. (link, abstract, bib-entry)

Abstract:

The protection of sensitive information is of utmost importance for organizations. The complexity and dynamism of modern businesses are forcing a re-think of traditional protection mechanisms. In particular, a priori policy enforcement mechanisms are often complemented with auditing mechanisms that rely on an a posteriori analysis of logs recording users’ activities to prove conformity to policies and detect policy violations when a valid explanation of conformity does not exist. However, existing auditing solutions require that the information necessary to assess policy compliance is available for the analysis. This assumption is not realistic. Indeed, a good deal of users’ activities may not be under the control of the IT system and thus they cannot be logged. In this paper we tackle the problem of accessing policy compliance in presence of incomplete logs. In particular, we present an auditing framework to assist analysts in finding a valid explanation for the events recorded in the logs and to pinpoint policy violations if such an explanation does not exist, when logs are incomplete. We also introduce two strategies for the refinement of plausible explanations of conformity to drive analysts along the auditing process. Our framework has been implemented on top of CIFF, an abductive proof procedure, and the efficiency and effectiveness of the refinement strategies evaluated. Keywords: Abduction, Policy Compliance, Abductive Reasoning

Michael N. Johnstone, Matthew Peacock, and J.I. den Hartog. Timing attack detection on BACNET via a machine learning approach. In 13th Australian Information Security Management Conference, 2015. (link, abstract, bib-entry)

Abstract:

Building Automation Systems (BAS), alternatively known as Building Management Systems (BMS), which centralise the management of building services, are often connected to corporate networks and are routinely accessed remotely for operational management and emergency purposes. The protocols used in BAS, in particular BACnet, were not designed with security as a primary requirement, thus the majority of systems operate with sub-standard or non-existent security implementations. As intrusion is thus likely easy to achieve, intrusion detection systems should be put in place to ensure they can be detected and mitigated. Existing intrusion detection systems typically deal only with known threats (signature-based approaches) or suffer from a high false positive rate (anomaly-based approaches). In this paper we present an overview of the problem space with respect to BAS, and suggest that state aware machine learning techniques could be used to discover threats that comprise a collection of legitimate commands. We provide a first step showing that the concept can be used to detect an attack where legitimate write commands being sent in rapid succession may cause system failure. We capture the state as a ‘time since last write’ event and use a basic artificial neural network classifier to detect attacks.

J.I. den Hartog and I. Matteucci. Introducing probabilities in controller strategies. In Joaquin Garcia-Alfaro, Jordi Herrera-Joancomartí, Emil Lupu, Joachim Posegga, Alessandro Aldini, Fabio Martinelli, and Neeraj Suri, editors, Post-conference Proceedings 3rd international workshop on Quantitative Aspects in Security Assurance (QASA 2014), LNCS 8872, pages 233-249. Springer International Publishing, 2015. ISBN 978-3-319-17015-2. (link, abstract, bib-entry)

Abstract:

In this paper we propose a basic framework to merge security controllers with probabilistic concepts. This framework provides a first step towards quantitative security achieved by probabilistic controllers. It extends the framework for specification, analysis, and automatic generation of security controllers provided in [21, 23] by considering probabilistic aspects of the behaviour of both the target process and the controller. Controllers may actively try to influence the choice of action of the target system or only passively react to actions the target system tried to perform. In a non-probabilistic setting both active and passive controllers can be expressed by the same model. In a probabilistic setting, however, these two types of controllers can differ. We respectively use the notions of generative and reactive processes to capture this distinction and discuss the different behaviours obtaining in the different settings.

D. Ayed, P. Bichsel, J. Camenisch, and J.I. den Hartog. Integration of data-minimising authentication into authorisation systems. In Thorsten Holz and Sotiris Ioannidis, editors, Proceedings of 7th International Conference on Trust and Trustworthy Computing (Trust 2014), volume LNCS 8564, pages 179-187. Springer International Publishing, 2014. ISBN 978-3-319-08592-0. (link, abstract, bib-entry)

E. Costante, J.I. den Hartog, M Petkovic, S. Etalle, and M. Pechenizkiy. Hunting the unknown - white-box database leakage detection. In Proceedings of 28th IFIP WG 11.3 Conference on Data and Applications Security and Privacy (DBSEC2014), volume 8566 of LNCS, pages 243-259, 2014. (link, abstract, bib-entry)

Abstract:

Data leakage causes significant losses and privacy breaches worldwide. In this paper we present a white-box data leakage detection system to spot anomalies in database transactions. We argue that our approach represents a major leap forward w.r.t. previous work because: i) it significantly decreases the False Positive Rate (FPR) while keeping the Detection Rate (DR) high; on our experimental dataset, consisting of millions of real enterprise transactions, we measure a FPR that is orders of magnitude lower than in state-of-the-art comparable approaches; and ii) the white-box approach allows the creation of self-explanatory and easy to update profiles able to explain why a given query is anomalous, which further boosts the practical applicability of the system.

S. Damen, J.I. den Hartog, and N. Zannone. Collac: Collaborative access control. In Proceedings of Conference on Collaboration Technologies and Systems (CTS 2014), 2014. (link, abstract, bib-entry)

F. Turkmen, J.I. den Hartog, and N. Zannone. Poster: Analyzing access control policies with smt. In Proceedings of the 21st ACM Conference on Computer and Communications Security (CCS 2014). ACM, 2014. (link, abstract, bib-entry)

Abstract:

The exibility and expressiveness of eXtensible Access Control Markup Language (XACML) allows the specification of a wide range of policies in different access control models. However, XACML policies are often verbose and, thus, prone to errors. Several tools have been developed to assist policy authors for the verification and analysis of policies, but most of them are limited in the types of analysis they can perform. In particular, they are not able to reason about predicates of non-boolean variables and, even if they do, they do it inefficiently. In this paper, we present the X2S framework, a formal framework for the analysis of XACML policies that employs Satisfiability Modulo Theories (SMT) as the underlying reasoning mechanism. The use of SMT not only allows more fine-grained analysis of policies, but it also improves the performance of policy analysis significantly.

M. Veeningen, M. Bruso, J.I. den Hartog, and N. Zannone. Triplex: Verifying data minimisation in communication systems. In Proceedings of the 20th ACM SIGSAC Conference on Computer and Communication Security (CCS'13, Berlin, Germany, November 4-8, 2013), pages 1415-1418. ACM, 2013. (link, abstract, bib-entry)

Abstract:

Systems dealing with personal information are legally required to satisfy the principle of data minimisation. Privacy-enhancing protocols use cryptographic primitives to minimise the amount of personal information exposed by communication. However, the complexity of these primitives and their interplay makes it hard for non-cryptography experts to understand the privacy implications of their use. In this paper, we present TRIPLEX, a framework for the analysis of data minimisation in privacy-enhancing protocols. Keywords: Data minimisation; Coalition Graphs; Detectability; Linkability

E. Costante, Y. Sun, M. Petkovic, and J.I. den Hartog. A machine learning solution to assess privacy policy completeness. In Proceedings of the 2012 ACM Workshop on Privacy in the Electronic Society (WPES co-located with CCS 2012), pages 91-96. ACM, 2012. (link, abstract, bib-entry)

Abstract:

A privacy policy is a legal document, used by websites to communicate how the personal data that they collect will be managed. By accepting it, the user agrees to release his data under the conditions stated by the policy. Privacy policies should provide enough information to enable users to make informed decisions. Privacy regulations support this by specifying what kind of information has to be provided. As privacy policies can be long and difficult to understand, users tend not to read them. Because of this, users generally agree with a policy without knowing what it states and whether aspects important to him are covered at all. In this paper we present a solution to assist the user by providing a structured way to browse the policy content and by automatically assessing the completeness of a policy, i.e. the degree of coverage of privacy categories important to the user. The privacy categories are extracted from privacy regulations, while text categorization and machine learning techniques are used to verify which categories are covered by a policy. The results show the feasibility of our approach; an automatic classifier, able to associate the right category to paragraphs of a policy with an accuracy approximating that obtainable by a human judge, can be effectively created.

M. Bruso, K. Chatzikokolakis, S. Etalle, and J.I. den Hartog. Linking unlinkability. In C. Palamidessi and M.D. Ryan, editors, Proceedings of the 7th International Symposium on Trustworthy Global Computing (TGC 2012). Revised Selected Papers., volume LNCS 8191, pages 129-144. Springer-Verlag, 2012. (link, abstract, bib-entry)

Abstract:

Unlinkability is a privacy property of crucial importance for several systems (such as RFID or voting systems). Informally, unlinkability states that, given two events/items in a system, an attacker is not able to infer whether they are related to each other. However, in the literature we find several definitions for this notion, which are apparently unrelated and shows a potentially problematic lack of agreement. This paper sheds new light on unlinkability by comparing different ways of defining it and showing that in many practical situations the various definitions coincide. It does so by (a) expressing in a unifying framework four definitions of unlinkability from the literature (b) demonstrating how these definitions are different yet related to each other and to their dual notion of “inseparability” and (c) by identifying conditions under which all these definitions become equivalent. We argue that the conditions are reasonable to expect in identification systems, and we prove that they hold for a generic class of protocols.

E. Costante, J.I. den Hartog, and M. Petkovic. What websites know about you - privacy policy analysis using information extraction. In R. Di Pietro, J. Herranz, E. Damiani, and R. State, editors, Proceedings of the 7th DPM International Workshop on Data Privacy Management and Autonomous Spontaneous Security. (Revised Selected Papers), volume LNCS 7731, pages 146-159. Springer-Verlag, 2012. (link, abstract, bib-entry)

Abstract:

The need for privacy protection on the Internet is well recognized. Everyday users are asked to release personal information in order to use online services and applications. Service providers do not always need all the data they gather to be able to offer a service. Thus users should be aware of what data is collected by a provider to judge whether this is too much for the services offered. Providers are obliged to describe how they treat personal data in privacy policies. By reading the policy users could discover, amongst others, what personal data they agree to give away when choosing to use a service. Unfortunately, privacy policies are long legal documents that users notoriously refuse to read. In this paper we propose a solution which automatically analyzes privacy policy text and shows what personal information is collected. Our solution is based on the use of Information Extraction techniques and represents a step towards the more ambitious aim of automated grading of privacy policies.

E. Costante, J.den Hartog, and M. Petkovic. On-line trust perception: What really matters. In Proceedings of the 1st Workshop on Socio-Technical Aspects in Security and Trust (STAST'11), pages 52-59. IEEE Computer Society, 2011. (link, abstract, bib-entry)

D.W. Chadwick, S.F. Lievens, J.I. den Hartog, A. Pashalidis, and J. Alhadeff. My private cloud overview : a trust, privacy and security infrastructure for the cloud. In Proceedings of the 4th IEEE International Conference on Cloud Computing (CLOUD 2011), pages 752-753. IEEE Computer Society, 2011. (link, abstract, bib-entry)

J. Pan, J.G.J. van Woudenberg, J.I. den Hartog, and M.F. Witteman. Improving dpa by peak distribution analysis. In A. Biryukov, G. Gong, and D.R. Stinson, editors, Selected Areas in Cryptography (17th international workshop, SAC 2010, Revised Selected Papers), LNCS 6544, pages 241-261, Waterloo, Ontario, Canada, 2011. Springer-Verlag. (link, abstract, bib-entry)

B. Pontes Soares Rocha, S. Bandhakavi, J. I. den Hartog, W. H. Winsborough, and S. Etalle. Towards static flow-based declassification for legacy and untrusted programs. In IEEE Symposium on Security and Privacy, Oakland, California, pages 93-108, USA, May 2010. IEEE Society press. (link, abstract, bib-entry)

Abstract:

Simple non-interference is too restrictive for specifying and enforcing information flow policies in most programs. Exceptions to non-interference are provided using declassification policies. Several approaches for enforcing declassification have been proposed in the literature. In most of these approaches, the declassification policies are embedded in the program itself or heavily tied to the variables in the program being analyzed, thereby providing little separation between the code and the policy. Consequently, the previous approaches essentially require that the code be trusted, since to trust that the correct policy is being enforced, we need to trust the source code. In this paper, we propose a novel framework in which declassification policies are related to the source code being analyzed via its I/O channels. The framework supports many of the of declassification policies identified in the literature. Based on flow-based static analysis, it represents a first step towards a new approach that can be applied to untrusted and legacy source code to automatically verify that the analyzed program complies with the specified declassification policies. The analysis works by constructing a conservative approximation of expressions over input channel values that could be output by the program, and by determining whether all such expressions satisfy the declassification requirements stated in the policy. We introduce a representation of such expressions that resembles tree automata. We prove that if a program is considered safe according to our analysis then it satisfies a property we call Policy Controlled Release, which formalizes information-flow correctness according to our notion of declassification policy. We demonstrate, through examples, that our approach works for several interesting and useful declassification policies, including one involving declassification of the average of several confidential values.

M. Bruso, K. Chatzikokolakis, and J.I. den Hartog. Formal verification of privacy for rfid systems. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10, Edinburgh, UK, July 17-19, 2010), pages 75-88. IEEE Computer Society, 2010. (no link available, abstract, bib-entry)

J. Lu, J. Pan, and J. den Hartog. Principles on the security of aes against first and second-order differential power analysis. In Jianying Zhou and Moti Yung, editors, Proceedings of the 8th International Conference on Applied Cryptography and Network Security (ACNS'10), volume 6123 of Lecture Notes in Computer Science, pages 168-185. Springer-Verlag, 2010. (link, abstract, bib-entry)

A.O.D. Spiessens, J.I. den Hartog, and S. Etalle. Know what you trust: Analyzing and designing trust policies with scoll. In P. Degano, J. Guttma, and F. Martinelli, editors, Formal Aspects in Security and Trust 2008. Revised Selected Papers, LNCS 5491, pages 129-142. Springer-Verlag, 2009. (link, abstract, bib-entry)

J. Pan, J. Lu, and J.I. den Hartog. You cannot hide behind the mask: Power analysis on a provably secure s-box implementation. In H.Y. Youm and M. Yung, editors, Information Security Applications (10th International Workshop, WISA 2009, Busan, Korea, August 25-27, 2009, Revised Selected Papers ), Lecture Notes in Computer Science, Vol. 5932, pages 178-192. Springer, 2009. (link, abstract, bib-entry)

J. Pan, J.I. den Hartog, and E.P. de Vink. An operation-based metric for dpa resistance. In Proc. IFIP 23rd International Information Security Conferenfce (SEC08), IFIP Conference Proceedings, Vol. 278, pages 429-443. Springer-Verlag, 2008. (link, abstract, bib-entry)

S. Etalle, J. I. den Hartog, and S. Marsh. Trust and punishment (invited paper). In Proceedings of the 1st International Conference on Autonomic Computing and Communication Systems, Autonomics, Rome, Italy, number 302 in ACM International Conference Proceeding Series. ACM: Association for Computing Machinery, December 2007. (link, abstract, bib-entry)

Abstract:

In recent years we have witnessed a great increase in the interest in Trust Management (TM) techniques both from the industrial and the academic sectors. The booming research has also determined a duality in the very definition of TM system which can lead to confusion. In one of the two categories of TM systems a great deal of work has yet to be done in advancing the inherently adaptive nature of trust. This position paper examines reasons for the success of TM, the two broad TM categories, and, for reputation-based TM, issues of ?Regret Management' and accountability that are necessary enhancements on the road leading to much more sophisticated TM architectures.

R. J. Corin and J. I. den Hartog. A probabilistic hoare-style logic for game-based cryptographic proofs. In M. Bugliesi, B. Preneel, and V. Sassone, editors, ICALP 2006 track C, Venice, Italy, volume 4052 of Lecture Notes in Computer Science, pages 252-263, Berlin, July 2006. Springer-Verlag. ISBN 3-540-35907-9. (link, abstract, bib-entry)

J. G. Cederquist, R. J. Corin, M. A. C. Dekker, S. Etalle, and J. I. den Hartog. An audit logic for accountability. In A. Sahai and W. H. Winsborough, editors, 6th Int. Workshop on Policies for Distributed Systems & Networks (POLICY), Stockholm, Sweden, pages 34-43, Los Alamitos, California, June 2005. IEEE Computer Society. ISBN 0-7695-2265-3. (link, abstract, bib-entry)

Abstract:

We describe and implement a policy language. In our system, agents can distribute data along with usage policies in a decentralized architecture. Our language supports the specification of conditions and obligations, and also the possibility to refine policies. In our framework, the compliance with usage policies is not actively enforced. However, agents are accountable for their actions, and may be audited by an authority requiring justifications.

M. Czenko, H. Tran, J.M. Doumen, S. Etalle, P.H. Hartel, and J.I. den Hartog. Nonmonotonic trust management for p2p applications. In S. Mauw, V. Isarny, and C. Cremers, editors, Proceedings of the First International Workshop on Security and Trust Management (STM'05), Milan, Italy, volume Vol. 157(3) of Electronic Notes in Theoretical Computer Science, pages 113-130. Elsevier Science, 2005. (link, abstract, bib-entry)

V. Sundramoorthy, C. Tan, P. H. Hartel, J. I. den Hartog, and J. Scholten. Functional principles of registry-based service discovery. In 30th Annual IEEE Conf. on Local Computer Networks (LCN), Sydney, Australia, pages 209-217, Los Alamitos, California, November 2005. IEEE Computer Society. ISBN 0-7695-2421-4. (link, abstract, bib-entry)

Y. W. Law, P. H. Hartel, J. I. den Hartog, and P. J. M. Havinga. Link-layer jamming attacks on s-mac. In 2nd European Workshop on Wireless Sensor Networks (EWSN), Istanbul, Turkey, pages 217-225, Los Alamitos, California, January 2005. IEEE Computer Society. ISBN 0-7803-8801-1. (link, abstract, bib-entry)

Abstract:

We argue that among denial-of-service (DoS) attacks, link-layer jamming is a more attractive option to attackers than radio jamming is. By exploiting the semantics of the link-layer protocol (aka MAC protocol), an attacker can achieve better efficiency than blindly jamming the radio signals alone. We investigate some jamming attacks of S-MAC, what level of effectiveness and efficiency the attack can potentially achieve, and what countermeasures can be implemented against these attacks.

R. J. Corin, S. Etalle, J. I. den Hartog, G. Lenzini, and I. S. Staicu. A logic for auditing accountability in decentralized systems. In T. Dimitrakos and F. Martinelli, editors, 2nd Int. Workshop on Formal Aspect of Security and Trust (FAST), Toulouse, France, volume IFIP 173, pages 187-201, Berlin, August 2004. Springer-Verlag. ISBN 0-387-24050-0. (link, abstract, bib-entry)

Abstract:

We propose a language that allows agents to distribute data with usage policies in a decentralized architecture. In our framework, the compliance with usage policies is not enforced. However, agents may be audited by an authority at an arbitrary moment in time. We design a logic that allows audited agents to prove their actions, and to prove their authorization to posses particular data. Accountability is defined in several flavors, including agent accountability and data accountability. Finally, we show the soundness of the logic.

J. I. den Hartog and E. P. de Vink. Virtual analysis and reduction of side-channel vulnerabilities of smartcards. In T. Dimitrakos and F. Martinelli, editors, 2nd Int. Workshop on Formal Aspect of Security and Trust (FAST), Toulouse, France, volume IFIP 173, pages 85-98, Boston, Massachusetts, August 2004. Kluwer Academic Publishers. ISBN 0-387-24050-0. (link, abstract, bib-entry)

Abstract:

This paper focuses on the usability of the PINPAS tool. The PINPAS tool is an instruction-level interpreter for smartcard assembler languages, augmented with facilities to study side-channel vulnerabilities. The tool can simulate side-channel leakage and has a suite of utilities to analyze this. The usage of the tool, for the analysis of a cryptographic algorithm is illustrated using the standard AES and RSA. Vulnerabilities of the implementations are identified and protective measures added. It is argued, that the tool can be instrumental for the design and realization of secure smartcard implementations in a systematic way.

J. I. den Hartog, J. Verschuren, E. P. de Vink, J. Vos, and W. Wiersma. Pinpas: A tool for power analysis of smartcards. In D. Gritzalis, S. De Capitani di Vimercati, P. Samarati, and S. K. Katsikas, editors, 18th IFIP TC11 Int. Conf. on Information Security and Privacy in the Age of Uncertainty (SEC), Athens, Greece, pages 453-457, Boston, Massachusetts, 2003. Kluwer Academic Publishers. ISBN 1-4020-7449-2. (link, abstract, bib-entry)

Abstract:

This paper describes the PINPAS tool, a tool for the simulation of power analysis and other side-channel attacks on smartcards. The PINPAS tool supports the testing of algorithms for vulnerability to SPA, DPA, etc. at the software level. Exploitation of the PINPAS tool allows for the identification of weaknesses in the implementation in an early stage of development. A toy algorithm is discussed to illustrate the usage of the tool.

J. I. den Hartog, E. P. de Vink, and J. W. de Bakker. Metric semantics and full abstractness for action refinement and probabilistic choice. In T. Hurley, M. Mac an Airchinnigh, M. Schellekens, and A. Seda, editors, MFCSIT2000, The First Irish Conference on the Mathematical Foundations of Computer Science and Information, Cork, Ireland, volume 40 of Electronic Notes in Theoretical Computer Science, pages 72-99, Amsterdam, March 2001. Elsevier. (link, abstract, bib-entry)

Abstract:

This paper provides a case-study in the field of metric semantics for probabilistic programming. Both an operational and a denotational semantics are presented for an abstract process language L_pr, which features action refinement and probabilistic choice. The two models are constructed in the setting of complete ultrametric spaces, here based on probability measures of compact support over sequences of actions. It is shown that the standard toolkit for metric semantics works well in the probabilistic context of L_pr, e.g. in establishing the correctness of the denotational semantics with respect to the operational one. In addition, it is shown how the method of proving full abstraction --as proposed recently by the authors for a nondeterministic language with action refinement-- can be adapted to deal with the probabilistic language L_pr as well.

J.I. den Hartog. Verifying probabilistic programs using a Hoare like logic. In P.S. Thiagarajan and R. Yap, editors, LNCS 1742 (ASIAN'99), pages 113-125. Springer, 1999. (link, abstract, bib-entry)

J. I. den Hartog and E. P. de Vink. Mixing up nondeterminism and probability: A preliminary report. In PROBMIV'98, First International Workshop on Probabilistic Methods in Verification, Indianapolis, Indiana, volume 22 of Electronic Notes in Theoretical Computer Science, pages 88-110, Amsterdam, June 1998. Elsevier. (link, abstract, bib-entry)

Abstract:

For a process language with both nondeterministic and probabilistic choice, and a form of failure a transition system is given from which, in a modular way, various operational models corresponding to various interpretations of nondeterminism and probability can be obtained. The effect of failure of one component for the system as a whole is treated differently in each interpretation. The same approach is followed for an extension of the language with a parallel operator. The adopted concurrency model is of a distributed nature and assumes that progress is guaranteed if nonfailing components exist. To this end the notion of a take-over of a failing component is incorporated in the transition system. It is shown that the modular way in which the transition system can yield different semantical models applies to this setting as well.

E. Todoran, J. I. den Hartog, E. P. de Vink, and J. Maluszynski. Comparative metric semantics for commit in or-parallel logic programming. In Int. Symp. on Logic Programming (ILPS), Long Island, New York, pages 101-115, Boston, Massachusetts, October 1997. The MIT Press. ISBN 0-262-63180-6. (no link available, abstract, bib-entry)

Abstract:

For the control flow kernel of or-parallel Prolog with commit an operational and a denotational model are constructed and related using techniques from metric semantics. By maintaining explicit scope information a compositional handling of the commit for the denotational model is established. By application of an abstraction function, which deletes this extra information the operational semantics is recovered.

PhD Thesis

J.I. den Hartog. Probabilistic Extensions of Semantical Models. PhD thesis, Vrije Universiteit Amsterdam, 2002. (link, abstract, bib-entry)

Book Chapters

E. Costante, J.I. den Hartog, and M. Petkovic. Trust management and user's trust perception in e-business (chapter 14). In E. Kajan, F.D. Dorloff, and I. Bedini, editors, Handbook of research on e-business standards and protocols : documents, data and advanced web technologies, pages 321-341. IGI Global, 2012. (link, abstract, bib-entry)

Abstract:

Trust is essential in the e-business world: to allow the cooperation needed in this setting, independent service providers have to trust each other and, also, end-users have to trust service providers. Trust Management, i.e. the process of establishing trust amongst the parties involved in a transaction, can be carried out using different approaches, methods and technologies. The end-user is an important party involved in this process. Trust Perception models attempt to understand the end-user’s point of view and the pattern he adopts to trust a service over the Internet. In this chapter the authors provide a state of the art for Trust Management in e-business. They review the most important Trust Management technologies and concepts including credentials and PKI, reputation, authorization and access control, trust policies, and trust languages. A conceptual map is presented clarifying the meaning and the links between different elements of a Trust Management system. Moreover, the authors discuss the end-user’s Trust Perception. The chapter presents a literature study on Trust Perception models and introduces the new model, able to list the trust signals the end-user considers to make trust decision. Examples of such signals can be the reputation of a website, the use of security protocols, the privacy policies adopted, and the look and feel of its user interface. Finally, the directions of future work are presented, and conclusions are drawn.

M. A. C. Dekker, S. Etalle, and J. I. den Hartog. Privacy policies. In M. Petkovic and W. Jonker, editors, Security, Privacy and Trust in Modern Data Management, volume XVIII of Data-Centric Systems and Applications, pages 383-397. Springer Verlag, Berlin, 2007. (link, abstract, bib-entry)

Abstract:

Privacy is a prime concern in today's information society. To protect the privacy of individuals, enterprises must follow certain privacy practices, while collecting or processing personal data. In this chapter we look at the setting where an enterprise collects private data on its website, processes it inside the enterprise and shares it with partner enterprises. In particular, we analyse three different privacy systems that can be used in the different stages of this lifecycle. One of them is the Audit Logic, recently introduced, which can be used to keep data private when it travels across enterprise boundaries. We conclude with an analysis of the features and shortcomings of these systems.

Other publications

J.I. den Hartog, C. Hütter, and S. Trabelsi. Combined trust managemeent architecture (extended abstract). http://www.eife-l.org/publications/eportfolio/proceedings2/lfl2010/lfl2010proceedings.pdf, 2010. (link, abstract, bib-entry)

M. A. C. Dekker, J. I. den Hartog, and S. Etalle. Audit-based compliance control (ac2) for ehr systems. Technical Report TR-CTIT-07-46, Centre for Telematics and Information Technology University of Twente, Enschede, 2007. (link, abstract, bib-entry)

Abstract:

Traditionally, medical data is stored and processed using paper-based files. Recently, medical facilities have started to store, access and exchange medical data in digital form. The drivers for this change are mainly demands for cost reduction, and higher quality of health care. The main concerns when dealing with medical data are availability and confidentiality. Unavailability (even temporary) of medical data is expensive. Physicians may not be able to diagnose patients correctly, or they may have to repeat exams, adding to the overall costs of health care. In extreme cases availability of medical data can even be a matter of life or death. On the other hand, confidentiality of medical data is also important. Legislation requires medical facilities to observe the privacy of the patients, and states that patients have a final say on whether or not their medical data can be processed or not. Moreover, if physicians, or their EHR systems, are not trusted by the patients, for instance because of frequent privacy breaches, then patients may refuse to submit (correct) information, complicating the work of the physicians greatly.
In traditional data protection systems, confidentiality and availability are conflicting requirements. The more data protection methods are applied to shield data from outsiders the more likely it becomes that authorized persons will not get access to the data in time. Consider for example, a password verification service that is temporarily not available, an access pass that someone forgot to bring, and so on. In this report we discuss a novel approach to data protection, Audit-based Compliance Control (AC2), and we argue that it is particularly suited for application in EHR systems. In AC2, a-priori access control is minimized to the mere authentication of users and objects, and their basic authorizations. More complex security procedures, such as checking user compliance to policies, are performed a-posteriori by using a formal and automated auditing mechanism. To support our claim we discuss legislation concerning the processing of health records, and we formalize a scenario involving medical personnel and a basic EHR system to show how AC2 can be used in practice.
This report is based on previous work (Dekker & Etalle 2006) where we assessed the applicability of a-posteriori access control in a health care scenario. A more technically detailed article about AC2 recently appeared in the IJIS journal, where we focussed however on collaborative work environments (Cederquist, Corin, Dekker, Etalle, & Hartog, 2007). In this report we first provide background and related work before explaining the principal components of the AC2 framework. Moreover we model a detailed EHR case study to show its operation in practice. We conclude by discussing how this framework meets current trends in healthcare and by highlighting the main advantages and drawbacks of using an a-posteriori access control mechanism as opposed to more traditional access control mechanisms.

J. G. Cederquist, R. J. Corin, M. A. C. Dekker, S. Etalle, J. I. den Hartog, and G. Lenzini. The audit logic: Policy compliance in distributed systems. Technical Report TR-CTIT-06-33, Centre for Telematics and Information Technology University of Twente, Enschede, 2006. (link, abstract, bib-entry)

Abstract:

We present a distributed framework where agents can share data along with usage policies. We use an expressive policy language including conditions, obligations and delegation. Our framework also supports the possibility to refine policies. Policies are not enforced a-priori. Instead policy compliance is checked using an a-posteriri auditing approach. Policy compliance is shown by a (logical) proof that the authority can systematically check for validity. Tools for automatically checking and generating proofs are also part of the framework.

M. A. C. Dekker, S. Etalle, and J. I. den Hartog. Privacy in an ambient world. Technical Report TR-CTIT-06-16, Centre for Telematics and Information Technology University of Twente, Enschede, April 2006. (link, abstract, bib-entry)

Abstract:

W. Mostowski, J. Pan, S. Akkiraju, E.P. de Vink, E. Poll, and J.I. den Hartog. A comparison of java cards : state-of-affairs 2006. Technical Report CSR 07-06, Eindhoven University of Technology, Eindhoven, 2006. (link, abstract, bib-entry)

G. Hollestelle, W. Burgers, and J. I. den Hartog. Power analysis on smartcard algorithms using simulation. Technical report CSR 04-22, Eindhoven University of Technology, Eindhoven, 2004. (link, abstract, bib-entry)

Abstract:

This paper presents the results from a power analysis of the AES and RSA algorithms by simulation using the PINPAS tool. The PINPAS tool is capable of simulating the power consumption of assembler programs implemented in, amongst others, Hitachi H8/300 assembler. The Hitachi H8/300 is a popular CPU for smartcards. Using the PINPAS tool, the vulnerability for power analysis attacks of straightforward AES and RSA implementations is examined. In case a vulnerability is found countermeasures are added to the implementation that attempt to counter power analysis attacks. After these modifications the analysis is performed again and the new results are compared to the original results.

J.I. den Hartog and E.P. de Vink. Building metric structures with the maes-factor. In F.S. de Boer, M. van der Heijden, and P. Klint, editors, Liber amicorum Jaco de Bakker, pages 93-107. CWI, Amsterdam, 2002. (no link available, abstract, bib-entry)

J. I. den Hartog. Comparative semantics for a process language with probabilistic choice and non-determinism. Technical Report IR-445, Vrije Universiteit, Amsterdam, 1998. (link, abstract, bib-entry)

Abstract:

A comparative semantics is given for a language Lprob containing probabilistic and non-deterministic choice. The effects of interpreting these operators as local or global are investigated. For three of the possible combinations an operational model and a denotational model are given and compared. First models for local probabilistic choice and local non-deterministic choice are given using a generative approach. By adjusting these models slightly models for global probability and local non-determinism are obtained. Finally models for local probability and global non-determinism are presented using a stratified approach. For use with the denotational models a construction of a complete ultra-metric space of finite multisets is given.