Logic and Computation Day

Steklov Mathematical Institute
June 7, 2013

Program

Friday, June 7, Room 530

9:45–10:00

Coffee

10:00–11:00

Andre Scedrov (University of Pennsylvania)

Bounded Memory Protocols and the Unbounded Adversary [slides]

The Dolev-Yao adversary is a non-deterministic adversary which can act as the network, intercept, send, compose and decompose messages, and remember as much information as it needs. That is, its memory is unbounded. We recently proposed a weaker Dolev-Yao like adversary, which can also act as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev-Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where there is only a bounded number of concurrent sessions and the honest participants of the protocol cannot generate an unbounded number of facts nor an unbounded number of nonces. This led us to the question of whether it is possible to infer a computable upper bound on the memory required by the standard, unbounded Dolev-Yao adversary to carry out a protocol anomaly from the memory restrictions of the bounded protocol. We answer this question negatively. This is joint work with Max Kanovich, Tajana Ban Kirigin, and Vivek Nigam.

11:00–11:45

Nikolai Vereshchagin (Moscow State University).

High Entropy Random Selection Protocols

We study the two party problem of randomly selecting a string among all the strings of length n. We want the protocol to have the property that the output distribution has high entropy, even when one of the two parties is dishonest and deviates from the protocol. We develop protocols that achieve high, close to n, entropy. In the literature the randomness guarantee is usually expressed as being close to the uniform distribution or in terms of resiliency. The notion of entropy is not directly comparable to that of resiliency, but we establish a connection between the two that allows us to compare our protocols with the existing ones. We construct an explicit protocol that yields entropy n - O(1) and has 4 log* n rounds, improving over the protocol of Goldwasser et.al. that also achieves this entropy but needs O(n) rounds. Both these protocols need O(n²) bits of communication. Next we reduce the communication in our protocols. We show the existence, non-explicitly, of a protocol that has 6-rounds, 2n + 8log n bits of communication and yields entropy n- O(log n) and min-entropy n/2 - O(log n). Our protocol achieves the same entropy bound as the recent, also non-explicit, protocol of Gradwohl et.al., however achieves much higher min-entropy: n/2 - O(log n) versus O(log n). Finally we exhibit very simple explicit protocols. We connect the security parameter of these geometric protocols with the well studied Kakeya problem motivated by harmonic analysis and analytical number theory. We are only able to prove that these protocols have entropy (3/4)n but still n/2 - O(log n) min-entropy. Therefor they do not perform as well with respect to the explicit constructions of Gradwohl et.al. entropy-wise, but still have much better min-entropy. We conjecture that these simple protocols achieve n - o(n) entropy. Our geometric construction and its relation to the Kakeya problem follows a new and different approach to the random selection problem than any of the previously known protocols. Based on joint paper with Harry Buhrman, Matthias Christandl, Michal Koucky, Zvi Lotker, Boaz Patt-Shamir.

11:45–12:15

Coffee

12:15–13:00

Daniyar Shamkanov (Steklov Mathematical Institute).

Circular proofs for provability logic [slides]

We present a circular proof system for the Gödel-Löb provability logic GL. In contrast to the ordinary proofs, a circular proof can be formed from an ordinary derivation tree by identifying each open assumption with an identical interior sequent. We prove that the circular proof-system is sound and complete with respect to the standard sequent-style formulation of GL, that it is contraction-free and cut-free, and that its logical rules are invertible. As an application, we give a syntactic proof of Lyndon interpolation for GL.

13:00–14:30

Lunch

14:30–15:15

Vladimir Krupski (Moscow State University).

Primal implication as encryption [slides]

We propose a "cryptographic" interpretation for the propositional connectives of primal infon logic introduced by Y. Gurevich and I. Neeman and prove the corresponding soundness and completeness results. Primal implication φ→ψ corresponds to the encryption of ψ with a secret key φ, primal disjunction is a group key and ⊥ reflects some backdoor constructions such as full superuser permissions or a universal decryption key. For the logic of ⊥ as a universal key (it was never considered before) we prove that the derivability problem has linear time complexity. We also show that the universal key can be emulated using primal disjunction.

15:15–15:30

Coffee

15:30–16:15

Andrei Romashchenko (IITP, Moscow and LIRMM, Montpellier).

Fixed-point tile sets and their applications [slides]

An aperiodic tile set was first constructed by R. Berger while proving the undecidability of the domino problem. It turned out that aperiodic tile sets appear in many topics ranging from logic (Entscheidungsproblem) to physics (quasicrystals). We present a construction of an aperiodic tile set that is based on Kleene's fixed-point construction instead of traditional geometric arguments. This construction it very flexible, and it can be used in embed many supplementary features in a tiling: it is suitable to give a new proof for the undecidability of the domino problem, to enforce high Kolmogorov complexity of a tiling, to characterize effectively closed 1D subshift it terms of 2D shifts of finite type, to construct a robust aperiodic tile set that does not have periodic (or close to periodic) tilings even if we allow sparse tiling errors, etc. Joint work with Bruno Durand and Alexander Shen.

16:15–17:00

Ilya Shapirovsky (IITP, Moscow).

Hamming metrics and products of modal logics [slides]

With a set S of words in an alphabet A we associate the frame (S,H), where sHt iff s and t are words of the same length and h(s,t) = 1 for the Hamming distance h, and investigate unimodal logics of such frames. These logics are closely related to many-dimensional modal logics: if we consider the n-th power of the inequality frame over a given alphabet A, then the Hamming box-operator on words of length n acts as the conjunction of all box-operators of the product; on the other hand, we show that all modalities of the logic of the n-th power of A with the universal relation can be expressed in the unimodal language with the Hamming box-operator. We present results on (un)decidability, complexity, (non-)finite axiomatizability, and completeness for these logics. Joint work with Andrey Kudinov and Valentin Shehtman.

17:00

Coffee