Overview on Real Quantifier Elimination

Real quantifier elimination problem arises in numerous areas in logic, mathematics, science and engineering: to name a few, geometric theorem proving, topological analysis of curves and surfaces, verification/analysis/synthesis of algorithms, robot motion planning, design of robust control systems, analysis of bio-chemical reactions, statistical model evaluation, and many others. Due to its importance, extensive research has been done and is still being actively carried out. This talk will provide a brief overview on general ideas and various special methods for particular application domains.

Proving and Inferring Invariants

Program analysis consists in automatically proving properties of computer programs. This is in general an undecidable problem. Yet, there exist methods that work for many programs, enough to be of industrial significance. Analysis of programs with loops or recursive functions relies on the notion of invariants; while certain methods require these invariants to be input by the user, others attempt to infer them. Certain invariant inference problems can be recast as optimization or numerical constraint problems; we'll describe a few methods for solving these.

Learning through Deterministic Assignment of Hidden Parameters

Supervised learning boils down to determining hidden and bright parameters in a parameterized hypothesis space based on a finite number of input-output pairs. The hidden parameters are those parameters that determine the hidden predictors or nonlinear mechanism of an estimator, while the bright parameters are those characterizing how the hidden predictors are linearly combined or the linear mechanism. In traditional learning paradigms, the hidden and bright parameters are not distinguished and trained simultaneously in one learning process (or saying, in one-stage). Such an one-stage learning (OSL) brings a benefit of theoretical analysis but suffers severely from the very high computation burden. To overcome this difficulty, the two-stage learning scheme (TSL), that could be named as the learning through random assignment of hidden parameters (LRHP), was developed in past years, which assigns randomly the hidden parameters in the first stage and determines the bright parameters by solving a linear least squares problem in the second stage. LRHP works well in many applications but suffers from the uncertainty problem: Its performance can be guaranteed only in a certain statistical expectation sense.

In this talk, we report a new scheme of TSL: The learning through deterministic assignment of hidden parameters (LDHP). Motivated from the study on the classical hard sphere problem in mathematics, we propose to deterministically take the hidden parameters as the tensor product of the minimal Riesz energy points on sphere and the best packing points in an interval. We theoretically show that with such deterministic assignment of hidden parameters, LDHP shares the same generalization performance with that of OSL, i.e., does not degrade the generalization capability of OSL. Thus LDHP provides an effective way of overcoming both the very high computation burden in OSL and the uncertainty difficulty in LRHP. We present a series of simulation and application examples to support this advantage and the outperformance of LDHP, as compared with a typical one-stage algorithm – Support Vector Regression (SVR) and a typical LRHP algorithm – Extreme Learning Machine (ELM). The study reported here paves a new road to simply and more efficiently solve any supervised learning problem.

Isabelle/HOL – Interaction and Automation

Isabelle/HOL is a popular proof assistant based on higher-order logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on automatic theorem provers for its proof search, and the counterexample generator Nitpick relies on SAT solvers. Together with the Isar structured proof format and a new asynchronous user interface, these tools have radically transformed the Isabelle user experience. Recently, Isabelle has been used to verify the seL4 microkernel, to formalize the Java and C++ memory models, and even to formalize a proof of God's existence.

Link-Based Similarity Measures in Scientific Literature Data: Methods, Performance, and Applications

As the number of people who use scientific literature databases such as google scholar, citeSeer, and Microsoft academic search grows, the demand for literature retrieval services has been steadily increasing. One of the most popular retrieval services is to find a set of papers similar to a paper under consideration, which requires a measure that computes similarity between papers. Scientific literature databases exhibit two interesting characteristics that are different from general databases. First, the papers cited by old papers are often not included in the database due to technical and economic reasons. Second, a few papers cite recently-published papers. These two characteristics cause existing similarity measures to fail in at least one of the following cases: (1) measuring the similarity between old, but similar papers, (2) measuring the similarity between recent, but similar papers, and (3) measuring the similarity between two similar papers: one old and the other recent. In this talk, we address link-based similarity measures that take into account the characteristics of scientific literature databases. The talk consists of the following parts: (1) Previous and our methods for computing link-based similarity, (2) performance comparisons of link-based similarity measures, and (3) some other interesting applications to which link-based similarity measures can be applied.

The Interplay between Privacy, Cryptography and Law

The talk illustrates the relation between privacy, cryptography, and law, and shows that an interdisciplinary perspective on these concepts leads to relevant research questions.

Privacy and law

Privacy has been defined by Westin [7] as "the claim of individuals, groups, or institutions to determine for themselves when, how, and to what extent information about them is communicated to others". Law defines, among others, the rights of individuals in their interactions with other individuals and institutions, including companies and the state. This includes the right to privacy: Law defines to what extent individuals' privacy has to be protected. Privacy (or "data protection") legislation can also require the use of technical, including cryptographic, measures to achieve privacy protection.

Privacy and cryptography

We can derive some aspects of the relation between privacy and cryptography from Westin's definition:

• Cryptography can be applied to ensure confidentiality of information (about "individuals, groups, or institutions"). Encryption functions directly serve this purpose; other cryptographic functions, such as authentication protocols, are also related to this goal as they help making sure that no unauthorized party gets access to information.
• Cryptographic research can reduce the amount of information disclosed by cryptographic protocols themselves. For example, anonymous credential schemes [1] enable proof of an authorization without revelation of the prover's identity. This way, while information is revealed, it is no longer information about a specific individual.

In case the application of cryptographic schemes or other technical measures is not already required by law, it can be seen as a complementary measure: in case legal protection is considered insufficient, individuals can protect themselves (e.g. by using anonymization networks like Tor [2]).

Cryptography and Law

Cryptographic schemes are used for a large number of business and e-government transactions. Electronic signatures are a prime example. The term is used (in the legal context, like in the European Directive 1999/93/EC on Electronic Signatures) to designate data that are used to sign, or authenticate, a document. In principle, even a scanned handwritten signature or a typed name can constitute an electronic signature. For electronic signatures to be secure in a technical sense, (cryptographic) digital signature schemes have to be used. In that case, courts have to decide, among others, whether a digital signature is authentic or not. The security of cryptographic schemes themselves is not sufficient for this decision, as the mapping of public keys to persons, and the secure storage of private keys, are not part of typical digital signature scheme definitions. These gaps have to be filled, and the precise requirements for digital signatures to become acceptable as evidence to be defined, by law.

The approaches of the European Union and the United States are vastly different in this respect. The stricter and more detailed regulation in the European Union may help to increase confidence in electronic signatures, but may also be considered as an obstacle to their acceptance. The legal classification of identity-based signatures [4] serves as an example to illustrate the relation between cryptography and law. As it turns out, legal requirements can pose interesting challenges for the development of new identity-based signature schemes.

Privacy, Cryptography, and Law

Cryptographic and legal research in the field of privacy may benefit from each other at least in two ways:

• Trends in regulation lead to new challenges for cryptography. For example, privacy implications of smart metering systems were discussed in the legal community, and these discussions prompted the development of technical schemes (beyond the establishment of secure transport channels) to reduce the disclosure of personal data (e.g.[6]).
• Both research communities try to find suitable definitions (or measurements) for anonymity and privacy. One example is the question under which circumstances the use of pseudonyms constitutes a sufficient protection of privacy – as, in a number of cases, the use of pseudonyms has been proven insufficient [3,5].

References

1. Jan Camenisch and Anna Lysyanskaya. An efficient system for non-transferable anonymous credentials with optional anonymity revocation. In Birgit Pfitzmann, editor, Advances in Cryptology – EUROCRYPT 2001, volume 2045 of Lecture Notes in Computer Science, pages 93-118. Springer Berlin Heidelberg, 2001.
2. Roger Dingledine, Nick Mathewson, and Paul Syverson. Tor: The second-generation onion router. In Proceedings of the 13th Conference on USENIX Security Symposium - Volume 13, SSYM'04, pages 21-21, Berkeley, CA, USA, 2004. USENIX Association.
3. Frank McSherry and Ilya Mironov. Differentially private recommender systems: Building privacy into the net. In Proceedings of the 15th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD '09, pages 627-636, New York, NY, USA, 2009. ACM.
4. Christoph Sorge. The legal classification of identity-based signatures. Cryptology ePrint Archive, Report 2013/271, 2013. http://eprint.iacr.org/.
5. Latanya Sweeney. K-anonymity: A model for protecting privacy. Int. J. Uncertain. Fuzziness Knowl.-Based Syst., 10(5):557-570, October 2002.
6. Benjamin Vetter, Osman Ugus, Dirk Westhoff, and Christoph Sorge. Homomorphic primitives for a privacy-friendly smart metering architecture. In Proceedings of the International Conference on Security and Cryptography (SECRYPT 2012), 2012.
7. Alan F. Westin. Privacy and Freedom. Atheneum, New York, 1967.