In this paper, we present a prenex form theorem for a version of Independence Friendly logic, a logic with imperfect information. Lifting classical results to such logics turns out not to be straightforward, because independence conditions make the formulas sensitive to signalling phenomena. In particular, nested quantification over the same variable is shown to cause problems. For instance, renaming of bound variables may change the interpretations of a formula, there are only restricted quantifier extraction theorems, and slashed connectives cannot be (...) so easily removed. Thus we correct some claims from Hintikka [8], Caicedo & Krynicki [3] and Hodges [11]. We refine definitions, in particular the notion of equivalence, and sharpen preconditions, allowing us to restore those claims, including the prenex form theorem of Caicedo & Krynicki [3], and, as a side result, we obtain an application to Skolem forms of classical formulas. It is a known fact that a complete calculus for IF-logic is impossible, but with our results we establish several quantifier rules that form a partial calculus of equivalence for a general version of IF-logic reflecting general properties of information flow in games. (shrink)

Security properties naturally combine temporal aspects of protocols with aspects of knowledge of the agents. Since BAN-logic, there have been several initiatives and attempts to incorpórate epistemics into the analysis of security protocols. In this paper, we give an overview of work in the field and present it in a unified perspective, with comparisons on technical subtleties that have been employed in different approaches. Also, we study to which degree the use of epistemics is essential for the analysis of security (...) protocols. We look for formal conditions under which knowledge modalities can bring extra expressive power to pure temporal languages. On the other hand, we discuss the cost of the epistemic operators in terms of model checking complexity. (shrink)

Conceiving new technologies as social experiments is a means to discuss responsible deployment of technologies that may have unknown and potentially harmful side-effects. Thus far, the uncertain outcomes addressed in the paradigm of new technologies as social experiments have been mostly safety-related, meaning that potential harm is caused by the design plus accidental events in the environment. In some domains, such as cyberspace, adversarial agents may be at least as important when it comes to undesirable effects of deployed technologies. In (...) such cases, conditions for responsible experimentation may need to be implemented differently, as attackers behave strategically rather than probabilistically. In this contribution, we outline how adversarial aspects are already taken into account in technology deployment in the field of cyber security, and what the paradigm of new technologies as social experiments can learn from this. In particular, we show the importance of adversarial roles in social experiments with new technologies. (shrink)

In this paper we study connections between game theoretical concepts and results, and features of IF-predicate logic, extending observations from J. van Benthem (2001) for IF-propositional logic. We highlight how both characteristics of perfect recall can fail in the semantic games for IF-formulas, and we discuss the four Thompson transformations in relation with IF-logic. Many (strong) equivalence schemes for IF-logic correspond to one or more of the transformations. However, we also find one equivalence that does not fit in this picture, (...) by the type of imperfect recall involved. We point out that the connection between the transformations and logical equivalence schemes is less direct in IF-first order logic than in the propositional case. The transformations do not generate a reduced normal form for IF-logic, because the IF-language is not flexible enough. (shrink)

We give a procedure to obtain falsity conditions for IF-sentences, using Skolemization. The expressive power of an IF-sentence can then be strongly captured by a pair of Σ11-sentences. A result from [Burgess 2003] shows that, conversely, any pair of incompatible Σ11-sentences corresponds with an IF-sentence.In the second part, we reflect on the influence of the order of the steps (inside-out versus outside-in) in the Skolemization procedures for IF-logic. We also reflect on the nature of game theoretical negation.

We give a procedure to obtain falsity conditions for IF-sentences, using Skolemization. The expressive power of an IF-sentence can then be strongly captured by a pair of Σ11-sentences. A result from [Burgess 2003] shows that, conversely, any pair of incompatible Σ11-sentences corresponds with an IF-sentence.In the second part, we reflect on the influence of the order of the steps (inside-out versus outside-in) in the Skolemization procedures for IF-logic. We also reflect on the nature of game theoretical negation.

Information technology is widely used to fulfill societal goals such as safety and security. These application areas put ever changing demands on the functionality of the technology. Designing technological appliances to be reconfigurable, thereby keeping them open to functionalities yet to be determined, will possibly allow the technology to fulfill these changing demands in an efficient way. In this paper we present a first exploration of potential societal and moral issues of reconfigurable sensors developed for application in the safety and (...) security domain, in the context of a large scale R&D-project in the Netherlands. We discuss the subtle distinction between the relevant notions of reconfigurability, function creep, and unrestricted or unforeseen technological affordances. We argue that the feature of reconfigurability makes context of use the central issue in the assessment of the societal and moral impact of the technology. It follows that the design of good policies for new application contexts has to be central in a value sensitive design approach to reconfigurable technology. (shrink)

We use the example of the introduction of the anti-smoking legislation to model the relationship between the cultural make-up, in terms of values, of societies and the acceptance of and compliance with norms. We present two agent-based simulations and discuss the challenge of modeling sanctions and their relation to values and culture.