 |
| |
|
|
|
Content
|
|
| Title
and Abstracts of Tutorial Lectures |
| |
|
| New
insights into Probabilistically Checkable Proofs (PCPs) |
|
by Eli
Ben-Sasson
(Comput Sci Dept, Technion Inst of Technology, Israel) |
| |
We
revisit the celebrated PCP Theorem in light of recent simplifications
to its proof and discuss new applications to error correcting
codes and sub-linear time proof verification.
Reminder: The celebrated PCP Theorem was proved in the
early 1990's [Arora,Safra;Arora,Lund,Motwani,Sudan,Szegedy].
Informally speaking, it says there is a format of writing proofs
and a probabilistic method of verifying their correctness. In
this method the verifier needs to read only a constant number
of random bits from the proof (independent of the proof length)
to test its validity. Good proofs of true statements are accepted
with probability one, whereas any purported "proof"
of a false statement is rejected with probability of at least
one third. |
|
| Operational
Theories of Sets |
|
by Solomon
Feferman
(Depts of Mathematics and Philosophy, Stanford University, USA) |
| |
In
a kind of extension of von Neumann's axiomatization (VN) of
set theory with functions at the level of classes, the language
of set theory is here augmented by variables for operations
in an untyped partial combinatory algebra over sets. Like the
earlier approach, this language lends itself to a more natural
formulation of standard set-theoretical axioms, such as those
of Replacement and Choice as well as the usual closure conditions
on sets. But the present formalism also has the advantage of
much greater freedom than the VN approach since it permits the
representation of higher order closure conditions. In particular,
operational set theory is applied to obtain unified formulations
of various "small" large cardinal axioms (i.e., those
consistent with V=L), such as Mahlo, weakly compact, etc., in
terms that are abstractly the same whether in usual set theory
with the power-set operation or admissible set theory without
it. The latter replaces analogue formulations in terms of recursive
functions on admissible sets and schematic reflection principles. |
|
| The
expanding notion of algorithm |
|
by Yuri
Gurevich
(Microsoft Research, USA) |
| |
Classical
computation theory, including computational complexity theory,
was a great advance in the study of algorithms but the theory
has severe limitations that make it inadequate for modern engineering.
In particular, the behavior of an algorithm is restricted to
the input/output relation, and inputs are supposed to be string-codable.
Behavioral computation theory, aka the theory of abstract state
machines, overcomes these restrictions. We explain the basics
of behavior computation theory and mention various applications.
For those who want to do a little reading ahead of time, the
best place to start is article #141 at speaker's webpage. For
a broad-brush picture see #164 and #174. For those who have
a greater appetite for reading and who are unafraid of technical
details, there are articles #157, #166, #170, #171, #176. |
|
| Proof
Mining: Applications of Proof Theory to Analysis |
|
by Ulrich
Kohlenbach
(Department of Mathematics, Darmstadt University of Technology,
Germany) |
| |
In
recent years (though influenced by papers of G. Kreisel going
back to the 50's) an applied form of proof theory systematically
evolved with sometimes is called "Proof Mining". This
approach is concerned with the extraction of both new effective
data as well as new qualitative information (independence of
solutions from certain parameters) from typically ineffective
proofs. A particularly fruitful area of applications has been
functional analysis. This 2-part tutorial will give a survey
on the logical background and applications of this approach. |
|
| (tba) |
|
by Thomas
Scanlon
(Mathematics Department, University of California at Berkeley,
USA) |
|
|
|
| Symbolic
Analysis of Computer Network Security Protocols
|
| by
Andre
Scedrov (Department of Mathematics, University
of Pennsylvania, USA) |
| |
While
modern cryptography relies on applications of number theory,
probability theory, and computational complexity, the methods
of symbolic logic are contributing in significant ways to the
wider area of computer security, including network security,
access control, and policy languages. We will explore some of
the applications of the abstract symbolic methods in these areas
and in particular in the analysis of network security protocols.
We will also consider several ways in which abstract symbolic
methods relate to mathematical applications in cryptography.
As an example of this methodology we describe joint work with
I. Cervesato, A.D. Jaggard, J.-K. Tsay, and C. Walstad on a
vulnerability in PKINIT, the public key extension of the widely
deployed Kerberos 5 authentication protocol. The discovery of
this flaw caused an internet standards body IETF to change the
specification of PKINIT and caused Microsoft to release a security
update for a number of Windows operating systems. A Microsoft
Security Bulletin which mentions this work is available on http://www.microsoft.com/technet/security/bulletin/MS05-042.mspx
We discovered this flaw as part of an ongoing symbolic analysis
of the Kerberos protocol suite, and we have verified in the
symbolic model several fixes to PKINIT that prevent our attack.
|
|
|
| Title
and Abstracts of Invited Talks
|
| |
|
| New
insights into Probabilistically Checkable Proofs (PCPs) |
|
by Eli
Ben-Sasson
(Comput Sci Dept, Technion Inst of Technology, Israel) |
| |
We
revisit the celebrated PCP Theorem in light of recent simplifications
to its proof and discuss new applications to error correcting
codes and sub-linear time proof verification.
Reminder: The celebrated PCP Theorem was proved in the
early 1990's [Arora,Safra;Arora,Lund,Motwani,Sudan,Szegedy].
Informally speaking, it says there is a format of writing proofs
and a probabilistic method of verifying their correctness. In
this method the verifier needs to read only a constant number
of random bits from the proof (independent of the proof length)
to test its validity. Good proofs of true statements are accepted
with probability one, whereas any purported "proof"
of a false statement is rejected with probability of at least
one third. |
|
| Operational
Theories of Sets |
|
by Solomon
Feferman
(Depts of Mathematics and Philosophy, Stanford University, USA) |
| |
In
a kind of extension of von Neumann's axiomatization (VN) of
set theory with functions at the level of classes, the language
of set theory is here augmented by variables for operations
in an untyped partial combinatory algebra over sets. Like the
earlier approach, this language lends itself to a more natural
formulation of standard set-theoretical axioms, such as those
of Replacement and Choice as well as the usual closure conditions
on sets. But the present formalism also has the advantage of
much greater freedom than the VN approach since it permits the
representation of higher order closure conditions. In particular,
operational set theory is applied to obtain unified formulations
of various "small" large cardinal axioms (i.e., those
consistent with V=L), such as Mahlo, weakly compact, etc., in
terms that are abstractly the same whether in usual set theory
with the power-set operation or admissible set theory without
it. The latter replaces analogue formulations in terms of recursive
functions on admissible sets and schematic reflection principles. |
|
| The
expanding notion of algorithm |
|
by Yuri
Gurevich
(Microsoft Research, USA) |
| |
The
notion of algorithm is key in computer science. Computer programs
are algorithms. This includes e.g. operating systems. Programming
languages themselves can be viewed as universal algorithms that
treat a particular program as part of input. A foundational
problem arises: What is an algorithm? But the notion of algorithm
expands and deepens as the computer revolution advances. In
addition to classical sequential algorithms, we have now concurrent
algorithms, distributed algorithms, real-time algorithms. Algorithms
grow in size and complexity raising numerous software concerns
like fault tolerance and maintainability. The variety of algorithms
is bewildering. The foundational problem may seem hopeless.
And yet there has been a substantial progress in the area, partially
covered in our WoLLIC 2006 tutorial. Here we concentrate on
issues that are not covered in the tutorial, in particular on
distributed algorithms and on the question what the notion of
algorithm is in its full generality. To what extent one can
anticipate the limit point of the expansion of the notion of
algorithm? |
|
| A
logical uniform boundedness principle for abstract metric and
hyperbolic spaces |
|
by Ulrich
Kohlenbach
(Department of Mathematics, Darmstadt University of Technology,
Germany) |
| |
This
talk will present some of the most recent applications of logical
metatheorems developed in the course of proof mining to functional
analysis. We will also discuss some new proof theoretic results
which were prompted by these applications. This includes a powerful
"nonstandard" uniform boundedness principle for abstract
metric and hyperbolic spaces. |
|
| (tba) |
|
by Thomas
Scanlon
(Mathematics Department, University of California at Berkeley,
USA) |
|
|
|
| Symbolic
Analysis of Computer Network Security Protocols
|
| by
Andre
Scedrov (Department of Mathematics, University
of Pennsylvania, USA) |
| |
While
modern cryptography relies on applications of number theory,
probability theory, and computational complexity, the methods
of symbolic logic are contributing in significant ways to the
wider area of computer security, including network security,
access control, and policy languages. We will explore some of
the applications of the abstract symbolic methods in these areas
and in particular in the analysis of network security protocols.
We will also consider several ways in which abstract symbolic
methods relate to mathematical applications in cryptography.
As an example of this methodology we describe joint work with
I. Cervesato, A.D. Jaggard, J.-K. Tsay, and C. Walstad on a
vulnerability in PKINIT, the public key extension of the widely
deployed Kerberos 5 authentication protocol. The discovery of
this flaw caused an internet standards body IETF to change the
specification of PKINIT and caused Microsoft to release a security
update for a number of Windows operating systems. A Microsoft
Security Bulletin which mentions this work is available on http://www.microsoft.com/technet/security/bulletin/MS05-042.mspx
We discovered this flaw as part of an ongoing symbolic analysis
of the Kerberos protocol suite, and we have verified in the
symbolic model several fixes to PKINIT that prevent our attack.
|
|
|
|
