LCC on Friday, August 11th

Session 5: Invited Talk (09:30‑10:30)

09:30‑10:30

John C Mitchell (Computer Science Department, Stanford University) Computationally Sound Formal Logic for Network Security Protocols [ppt] A cryptographically sound formal logic makes it possible to prove security properties of network protocols without explicitly reasoning about probability, asymptotic complexity, or the actions of a malicious attacker. The approach rests on a probabilistic, polynomial-time semantics for a protocol security logic that was originally developed using nondeterministic symbolic semantics. This talk will present the main features of the proof system, its interpretation, and example proofs for known protocols. We will also discuss ways in which the computational semantics leads to different reasoning methods than the coarser symbolic semantics. One significant difference between the symbolic and computational settings stems from the computational difference Between efficiently recognizing and efficiently producing a value. Among our more recent developments are a compositional method for proving cryptographically sound properties of key exchange protocols, and some work on secrecy properties that illustrates the computational interpretation of inductive properties of protocol roles. Joint work with Anupam Datta, Ante Derek, Arnab Roy, Vitaly Shmatikov, Mathieu Turuani, and Bogdan Warinschi.

Break (10:30‑11:00)

Session 6 (11:00‑12:30)

11:00‑11:45

Patrick Baillot (LIPN, CNRS / University Paris 13) Marco Pedicini (IAC, Consiglio Nazionale delle Ricerche) An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus This paper brings together two lines of research: implicit characterization of complexity classes by Linear Logic (LL) on the one hand, and computation over an arbitrary ring in the Blum-Shub-Smale (BSS) model on the other. Given a fixed ring structure K we define an extension of Terui's light affine lambda-calculus typed in LAL (Light Affine Logic) with a basic type for K. We show that this calculus captures the polynomial time function class FP(K): every typed term can be evaluated in polynomial time and conversely every polynomial time BSS machine over K can be simulated in this calculus.

11:45‑12:30

Yevgeniy Makarov (Indiana University) Comparing efficiency of functions provable in classical and constructive logics The relationship between proofs in constructive logic and programs in lambda calculus (for example, modified realizability) is well-known. Therefore, showing that provable functions of some theory based on constructive logic belong to some complexity class is potentially much easier than dealing with the same theory based on classical logic. Of course, classical proofs can be translated into constructive ones using Godel-Gentzen double-negation translation, but this may affect the complexity of induction formulas, which is often a major characteristic of interesting theories leading to useful complexity classes. In this article, we show how to use results about complexity of functions provable in constructive theories with positive induction to prove similar results about classical theories.

Lunch break (12:30‑14:00)

Session 7 (14:00‑14:45)

14:00‑14:45

Johann A. Makowsky (Technion IIT) Logical and Computational Aspects of Graph Polynomials: A Survey We outline a general theory of graph polynomials which covers all the examples we found in the vast literature. We introduce the class of (hyper)graph polynomials definable in second order logic, and outline a research program for their classification in terms of definability and complexity considerations, and various notions of reducibilities.