There are two additional end-of-semester events taking place in the Computational Logic Seminar, details below.
This Week in Logic at CUNY:
– – – – Thursday, May 26, 2011 – – – –
Computational Logic Seminar
Thursday, May 26, 2011
Room 4421, 2:00 – 4:00 PM, Mind an unusual room!
Speaker: Evan Goris, Graduate Center CUNY (dissertation proposal) Title: Canonical Authentication Proofs
Abstract: Security protocols are vicious little programs that are of vital importance for establishing secure electronic communication within a potentially hostile environment. Their description is usually small though getting them right is hard to accomplish. In Roger Needham’s words: “Cryptographic protocols are three line programs people still manage to get wrong.” Ever since the pioneering BAN paper many formal approaches for analyzing security protocols within the Dolev-Yao model have been developed and remain under active
development for over two decades now. Some of them with main concern a deeper understanding of the formal aspects of such protocols but most of them with primary purpose the verification of security properties, the latter usually using sophisticated automated methods. Especially in the branch that focuses on verification the techniques are so tightly related to the formal model of protocol execution that it is hard to imagine an independent discussion of them. The focus of this research is to loosen this connection. We will investigate a canonical way of proving security properties that is independent of the model of protocol execution. Moreover, the overall structure of such proofs can easily be understood even though the details at the bottom of such verifications are somewhat technical. The generality of the arguments make them suitable for implementation in a theorem prover so that practical applicability is not sacrificed.
Next Week in Logic at CUNY:
– – – – Tuesday, May 31, 2011 – – – –
Computational Logic Seminar
Tuesday, May 31, 2011
Room 3309, 2:00 – 4:00 PM,
Speaker: Giuseppe Primiero (Ghent University)
Title: Making Dependent Evidence explicit in Justification Logic
Abstract: A crucial feature of type theories is their extension to dependently defined terms and types, so as to include a functional structure to interpret the quantificational fragment of FOL. In this talk, I shall explore the extension of the Intuitionistic fragment of JL with a similar notion of dependent evidence. The motivation is double. Firstly, I will show that functional expressions can be entirely reconstructed within the framework of JL, hence enriching the theory of justifications: an appropriate set of axioms including dependent evidence is formulated, along with appropriate rules for equality, application, abstraction and reduction; these schemas can be then generalized to dependency from more than one term. Secondly, I shall show how this extension is useful to the epistemic tasks of JL: I will present a natural deduction calculus which uses dependent evidence with equality to distinguish derivability from valid and from true assumptions. In terms of this latter calculus, crucial structural properties are obtained, including normalization and confluence.