What, if anything, can be done in linear time?
Yuri Gurevich Microsoft Research - USA
The answer to the title question seems to be "Not much." Even sorting n items takes n.log(n) swaps. It turns out, however, that quite a bit can be done in linear time. We start with a brief discussion of the importance of linear time in the age of big data and with illustration of linear-time techniques. Then we sketch a linear-time decision algorithm for propositional primal infon logic (PPIL). Finally we mention some extensions of PPIL with linear-time decidable derivability problem.
Formal Methods for the Security of the Internet of Services
Luca Viganò
Dipartimento di Informatica, Università di Verona, Italy
In the Internet of Services (IoS), systems and applications are no longer the result of programming components in the traditional meaning but are built by composing services that are distributed over the network and reconfigured and consumed dynamically in a demand-driven, flexible way. However, composing services leads to new, subtle and dangerous, vulnerabilities due to interference between component services and policies, the shared communication layer, and application functionality.
I will present the AVANTSSAR Platform [1] and the SPaCIoS Tool [6], two integrated toolsets for the formal specification and automated validation of trust and security of applications in the IoS at design time and run time, respectively. (Both have been developed in the context of FP7 projects that I have been coordinating.) I will focus on two particular results.
First, I will discuss a compositionality result [5] that formalizes conditions for vertical composition of security protocols, i.e., when an application protocol (e.g., a banking service) runs over a channel established by another protocol (e.g., a secure channel provided by TLS). This is interesting and useful as protocol composition can lead to attacks even when the individual protocols are all secure in isolation.
Second, I will discuss how although computer security typically revolves around threats, attacks and defenses, the sub-field of security protocol analysis has so far focused almost exclusively on the notion of attack. I will motivate that there is room for a fruitful notion of defense for vulnerable protocols and that the conceptual bridge lies in the notion of multiple non-collaborating attackers and interference between simultaneous attack procedures [2,3,4].
References
1. A. Armando, W. Arsac, T. Avanesov, M. Barletta, A. Calvi, A. Cappai, R. Carbone, Y. Chevalier, L. Compagna, J. Cuéllar, G. Erzse, S. Frau, M. Minea, S. Mödersheim, D. von Oheimb, G. Pellegrino, S. E. Ponta, M. Rocchetto, M. Rusinowitch, M. Torabi Dashti, M. Turuani, and L. Viganò. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In TACAS 2012, LNCS 7214, pages 267--282. Springer, 2012.
2. M.-C. Fiazza, M. Peroli, L. Viganò. Attack Interference in Non-Collaborative Scenarios for Security Protocol Analysis. In SECRYPT 2011, pages 144--156. SciTePress, 2011.
3. M.-C. Fiazza, M. Peroli, L. Viganò. Security Protocols as Environments: a Lesson from Non-collaboration.
In CollaborateCom 2011, pages 479--486. IEEE Computer Society Press, 2011.
4. M.-C. Fiazza, M. Peroli, L. Viganò. An Environmental Paradigm for Defending Security Protocols.
In CTS 2012, pages 427--438, IEEE Computer Society Press, 2012.
5. S. Mödersheim and L. Viganò. Secure Pseudonymous Channels. In Proceedings of Esorics'09, LNCS 5789, pages 337--354. Springer, 2009.
6. L. Viganò. Towards the Secure Provision and Consumption in the Internet of Services. In TrustBus 2012, LNCS 7449, pages 214--215, Springer, 2012.
Disambiguating bi-intuitionism
Gianluigi Bellin
Dipartimento di Informatica, Università di Verona, Italy
Bi-intuitionistic logic, as defined by C.Rauszer 1974, 1977 and others, lacks the ``rich proof-theory'' which is characteristic of intuitionism: its categorical (and topological) models are degenerate, in the sense that they reduce to partial orders. But already for co-intuitionistic logic categorical models do not exist in the category Set, since the coproduct is disjoint union and the co-exponent of two non-empty sets cannot be defined, as shown by T.Crolard 2001. Such problems vanish if we ``polarise''` bi-intuitionistic expressions as either ``assertive'' or ``hypothetical''; namely, if intuitionism is a logic of assertions, as M.Dummett held, then co- intuitionism is a logic of hypotheses; if ``conclusive evidence'' for a proposition p justifies the assertion that p, then a ``scintilla of evidence'' for p justifies the hypothesis that p. Strong intuitionistic and weak co-intuitionistic negation (``doubt'') are mutually inverse and relate the dual sides: thus a ``scintilla of evidence'' against an assertion justifies a doubt, but only ``conclusive evidence'' against a hypothesis justifies its refutation. Moreover co-intuitionistic disjunction is similar to Girard's par rather than to intuitionistic disjunction. In fact by "linearizing" co- intuitionism one can produce categorical models of co-intuitionistic logic by dualizing the construction by Benton, Bierman, Hyland and de Paiva 1993 and also Benton 1995; here the term assignment to co-intuitionstic proofs is based on T.Crolard's calculus of ``safe coroutines'' (2004). Finally, using strong and weak negations one can define intuitionistic modalities that change the side. If we also define a ``conjecture'' as the ``possibility of an assertion'' and an ``expectation'' as the ``necessity of a hypothesis'', then Parigot's lambda-mu-calculus can be typed in an intuitionistic ``logic of expectations'', an intermediate logic where the law of double negation holds but the law of excluded middle does not.
Our ``disambiguated'' version of bi-intuitionism is translated into classical S4, extending Godel, McKinsey and Tarski's modal interpretation, rather than into Rauszer's ``tensed S4'', as shown by Bellin and Biasi (2004). The classical S4 translation of our ``logic of expectations'' is the ``Diamond Box'' interpretation of classical logic (see Smullyan and Fitting 1996). One expects that using bi-modal S4 a similar treatment can be given of Fairtlough and Mendler's Lax Logic (1997) and Alechina, Mender, DePaiva and Ritter's Constructive S4 (2001) in our bi- intuitionistic setting.
An algebraic axiomatization of IKt system
Aldo V. Figallo and Gustavo Pelaitay
Universidad Nacional de San Juan, Argentina and Universidad Nacional del Sur Bahía Blanca, Argentina
Ewald in [1] considered tense operators G (it will always be the case), H (it has always been the case), F (it will be the case) and P (it was the case) on intuitionistic propositional calculus and constructed an intuitionistic tense logic system called IKt. The aim of this paper is to show an algebraic version of the IKt system. It is worth mentioning that our axiomatization is different from Chajda’s in [2], for tense intuitionistic logic.
References
1. W. B. Ewald, “Intuitionistic tense and modal logic”, J. Symbolic Logic 51(1986), 1, 166–179.
2. I.Chajda, “Algebraic axiomatization of tense intuitionistic logic”, Cent. Eur. J. Math. 9 (2011), 5, 1185–1191.
Logic of Negation-Complete Interactive Proofs
Simon Kramer
University of Luxembourg, Luxenbourg
We produce a decidable classical normal modal logic of internalized negation-complete or disjunctive non-monotonic interactive proofs (LDiiP) from an existing logical counterpart of non-monotonic or instant interactive proofs (LiiP). LDiiP internalizes agent-centric proof theories that are negation-complete (maximal) and consistent (and hence strictly weaker than, for example, Peano Arithmetic) and enjoy the disjunction property (like Intuitionistic Logic). In other words, internalized proof theories are ultrafilters and all internalized proof goals are definite in the sense of being either provable or disprovable to an agent by means of disjunctive internalized proofs (thus also called epistemic deciders). Still, LDiiP itself is classical (monotonic, non-constructive), negation-incomplete, and does not have the disjunction property. The price to pay for the nega- tion completeness of our interactive proofs is their non-monotonicity and non-communality (for singleton agent communities only). As a normal modal logic, LDiiP enjoys a standard Kripke-semantics, which we justify by invoking the Axiom of Choice on LiiP’s and then construct in terms of a concrete oracle-computable function. Our agent-centric notion of proof is also a negation-complete disjunctive explicit refinement of standard KD45-belief, and yields a disjunctive but negation-incomplete explicit refinement of standard S5-knowledge.
A typed lambda calculus for Intuitionistic Justification Logic
Konstantinos Pouliasis and Giuseppe Primiero
The Graduate Center at City University of New York NY, USA and FWO - Research Foundation Flanders Center for Logic and Philosophy of Science Ghent University, Belgium
In this paper we offer a system J-Calc that can be regarded as a typed λ- calculus for the {→, ⊥} fragment of Intuitionistic Justification Logic. We offer different interpretations of J-Calc, in particular, as a two phase proof system in which we proof check the validity of deductions of a theory T based on deductions from a stronger theory T′. We establish some first metatheoretic results.
Intuitionistic Hypothetical Logic of Proofs
Gabriela Steren and Eduardo Bonelli
UBA, Argentina and UNQ and CONICET, Argentina
We study a term assignment for an intuitonistic fragment of the Logic of Proofs (LP). LP is a refinement of modal logic S4 in which the assertion box A is replaced by [[s]]A whose intended reading is “s is a proof of A”. We first introduce a natural deduction presentation based on hypothetical judgements and then its term assignment, which yields a confluent and strongly normalising typed lambda calculus λIHLP . This work is part of an ongoing effort towards reformulating LP in terms of hypothetical reasoning in order to explore its applications in programming languages.
A graph calculus for proving intuitionistic relation algebraic equations
Renata de Freitas and Petrucio Viana
Universidade Federal Fluminense, Niteroi, Brazil
We introduce a diagrammatic system in which diagrams based on graphs represent binary relations and reasoning on binary relations is performed by transformations on diagrams. We prove that if a diagram D1 is transformed into a diagram D2 using the rules of our system, under a set Γ of hypotheses, then “it is intuitionistically true that the relation defined by diagram D1 is a subrelation of the one defined by diagram D2, under the hypotheses in Γ”. We present the system formally, prove its soundness, and left the question of its completeness for further investigation.
If, not when
Richard Crouch and Valeria de Paiva
Nuance Communications, USA
We present a logic of verified and unverified assertions and prove it sound and complete with respect to its possible-worlds semantics. The logic, a constructive modal logic, is motivated by considerations of the interpretation of conditionals in natural language semantics, but, we claim, is of independent interest.
A rich language for negative modalities
Adriano Dodó and João Marcos
UFRN, Natal-RN, Brazil
The paper studies a modal language for negative operators– an intuitionistic- like negation and its independent dual–added to (bounded) distributive lattices. For each negation an extra operator is added to describe the models in which it behaves classically. The minimal normal logic with these operators is characterized. Statements of all important results are provided and proofs of main propositions are sketched.