Predicate encryption with various properties

Predicate encryption (PE) is a new primitive which supports exible control over access to encrypted data. In PE schemes, users' decryption keys are associated with predicates f and ciphertexts encode attributes a that are specified during the encryption procedure. A user can successfully decrypt if and only if f(a) = 1. In this thesis, we will investigate several properties that are crucial to PE. We focus on expressiveness of PE, Revocable PE and Hierarchical PE (HPE) with forward security. For all proposed systems, we provide a security model and analysis using the widely accepted computational complexity approach. Our first contribution is to explore the expressiveness of PE. Existing PE supports a wide class of predicates such as conjunctions of equality, comparison and subset queries, disjunctions of equality queries, and more generally, arbitrary combinations of conjunctive and disjunctive equality queries. We advance PE to evaluate more expressive predicates, e.g., disjunctive comparison or disjunctive subset queries. Such expressiveness is achieved at the cost of computational and space overhead. To improve the performance, we appropriately revise the PE to reduce the computational and space cost. Furthermore, we propose a heuristic method to reduce disjunctions in the predicates. Our schemes are proved in the standard model. We then introduce the concept of Revocable Predicate Encryption (RPE), which extends the previous PE setting with revocation support: private keys can be used to decrypt an RPE ciphertext only if they match the decryption policy (defined via attributes encoded into the ciphertext and predicates associated with private keys) and were not revoked by the time the ciphertext was created. We propose two RPE schemes. Our first scheme, termed Attribute- Hiding RPE (AH-RPE), offers attribute-hiding, which is the standard PE property. Our second scheme, termed Full-Hiding RPE (FH-RPE), offers even stronger privacy guarantees, i.e., apart from possessing the Attribute-Hiding property, the scheme also ensures that no information about revoked users is leaked from a given ciphertext. The proposed schemes are also proved to be secure under well established assumptions in the standard model. Secrecy of decryption keys is an important pre-requisite for security of (H)PE and compromised private keys must be immediately replaced. The notion of Forward Security (FS) reduces damage from compromised keys by guaranteeing confidentiality of messages that were encrypted prior to the compromise event. We present the first Forward-Secure Hierarchical Predicate Encryption (FS-HPE) that is proved secure in the standard model. Our FS-HPE scheme offers some desirable properties: time-independent delegation of predicates (to support dynamic behavior for delegation of decrypting rights to new users), local update for users' private keys (i.e., no master authority needs to be contacted), forward security, and the scheme's encryption process does not require knowledge of predicates at any level including when those predicates join the hierarchy.

Predicate encryption for multi-inner-products

Predicate encryption is a new primitive that supports flexible control over access to encrypted data. We study predicate encryption systems, evaluating a wide class of predicates. Our systems are more expressive than the existing attribute-hiding systems in the sense that the proposed constructions support not only all existing predicate evaluations but also arbitrary conjunctions and disjunctions of comparison and subset queries. Toward our goal, we propose encryption schemes supporting multi-inner-product predicate and provide formal security analysis. We show how to apply the proposed schemes to achieve all those predicate evaluations.

Vagueness and software engineering

We do not commonly associate software engineering with philosophical debate. Indeed, software engineers ought to be concerned with building software systems and not settling philosophical questions. I attempt to show that software engineers do, in fact, take philosophical sides when designing software applications. In particular, I look at how the problem of vagueness arises in software engineering and argue that when software engineers solve it, they commit to philosophical views that they are seldom aware of. In the second part of the paper, I suggest a way of dealing with vague predicates without having to confront the problem of vagueness itself. The purpose of my paper is to highlight the currently prevalent disconnect between philosophy and software engineering. I claim that a better knowledge of the philosophical debate is important as it can have ramifications for crucial software design decisions. Better awareness of philosophical issues not only produces better software engineers, it also produces better engineered products.

Permissions in Deontic Event-Calculus

Permissions are special case of deontic effects and play important role compliance. Essentially they are used to determine the obligations or prohibitions to contrary. A formal language e.g., temporal logic, event-calculus et., not able to represent permissions is doomed to be unable to represent most of the real-life legal norms. In this paper we address this issue and extend deontic-event-calculus (DEC) with new predicates for modelling permissions enabling it to elegantly capture the intuition of real-life cases of permissions.

Truth, Proof and Gödelian Arguments : A Defence of Tarskian Truth in Mathematics

One of the most fundamental questions in the philosophy of mathematics concerns the relation between truth and formal proof. The position according to which the two concepts are the same is called deflationism, and the opposing viewpoint substantialism. In an important result of mathematical logic, Kurt Gödel proved in his first incompleteness theorem that all consistent formal systems containing arithmetic include sentences that can neither be proved nor disproved within that system. However, such undecidable Gödel sentences can be established to be true once we expand the formal system with Alfred Tarski s semantical theory of truth, as shown by Stewart Shapiro and Jeffrey Ketland in their semantical arguments for the substantiality of truth. According to them, in Gödel sentences we have an explicit case of true but unprovable sentences, and hence deflationism is refuted. Against that, Neil Tennant has shown that instead of Tarskian truth we can expand the formal system with a soundness principle, according to which all provable sentences are assertable, and the assertability of Gödel sentences follows. This way, the relevant question is not whether we can establish the truth of Gödel sentences, but whether Tarskian truth is a more plausible expansion than a soundness principle. In this work I will argue that this problem is best approached once we think of mathematics as the full human phenomenon, and not just consisting of formal systems. When pre-formal mathematical thinking is included in our account, we see that Tarskian truth is in fact not an expansion at all. I claim that what proof is to formal mathematics, truth is to pre-formal thinking, and the Tarskian account of semantical truth mirrors this relation accurately. However, the introduction of pre-formal mathematics is vulnerable to the deflationist counterargument that while existing in practice, pre-formal thinking could still be philosophically superfluous if it does not refer to anything objective. Against this, I argue that all truly deflationist philosophical theories lead to arbitrariness of mathematics. In all other philosophical accounts of mathematics there is room for a reference of the pre-formal mathematics, and the expansion of Tarkian truth can be made naturally. Hence, if we reject the arbitrariness of mathematics, I argue in this work, we must accept the substantiality of truth. Related subjects such as neo-Fregeanism will also be covered, and shown not to change the need for Tarskian truth. The only remaining route for the deflationist is to change the underlying logic so that our formal languages can include their own truth predicates, which Tarski showed to be impossible for classical first-order languages. With such logics we would have no need to expand the formal systems, and the above argument would fail. From the alternative approaches, in this work I focus mostly on the Independence Friendly (IF) logic of Jaakko Hintikka and Gabriel Sandu. Hintikka has claimed that an IF language can include its own adequate truth predicate. I argue that while this is indeed the case, we cannot recognize the truth predicate as such within the same IF language, and the need for Tarskian truth remains. In addition to IF logic, also second-order logic and Saul Kripke s approach using Kleenean logic will be shown to fail in a similar fashion.

Nonverbal predication in Erzya : Studies on morphosyntactic variation and part of speech distinctions

This dissertation consists of four articles and an introduction. The five parts address the same topic, nonverbal predication in Erzya, from different perspectives. The work is at the same time linguistic typology and Uralic studies. The findings based on a large corpus of empirical Erzya data, which was collected using several different methods and included recordings of the spoken language, made it possible for the present study to apply, then test and finally discuss the previous theories based on cross-linguistic data. Erzya makes use of multiple predication patterns which vary from totally analytic to the morphologically very complex. Nonverbal predicate clause types are classified on the basis of propositional acts in clauses denoting class-membership, identity, property and location. The predicates of these clauses are nouns, adjectives and locational expressions, respectively. The following three predication strategies in Erzya nonverbal predication can be identified: i. the zero-copula construction, ii. the predicative suffix construction and iii. the copula construction. It has been suggested that verbs and nouns cannot be clearly distinguished on morphological grounds when functioning as predicates in Erzya. This study shows that even though predicativity must not be considered a sufficient tool for defining parts of speech in any language, the Erzya lexical classes of adjective, noun and verb can be distinguished from each other also in predicate position. The relative frequency and degree of obligation for using the predicative suffix construction decreases when moving left to right on the scale verb adjective/locative noun ( identificational statement). The predicative suffix is the main pattern in the present tense over the whole domain of nonverbal predication in Standard Erzya, but if it is replaced it is most likely to be with a zero-copula construction in a nominal predication. This study exploits the theory of (a)symmetry for the first time in order to describe verbal vs. nonverbal predication. It is shown that the asymmetry of paradigms and constructions differentiates the lexical classes. Asymmetrical structures are motivated by functional level asymmetry. Variation in predication as such adds to the complexity of the grammar. When symmetric structures are employed, the functional complexity of grammar decreases, even though morphological complexity increases. The genre affects the employment of predication strategies in Erzya. There are differences in the relative frequency of the patterns, and some patterns are totally lacking from some of the data. The clearest difference is that the past tense predicative suffix construction occurs relatively frequently in Standard Erzya, while it occurs infrequently in the other data. Also, the predicative suffixes of the present tense are used more regularly in written Standard Erzya than in any other genre. The genre also affects the incidence of the translative in uľ(ń)ems copula constructions. In translations from Russian to Erzya the translative case is employed relatively frequently in comparison to other data. This study reveals differences between the two Mordvinic languages Erzya and Moksha. The predicative suffixes (bound person markers) of the present tense are used more regularly in Moksha in all kinds of nonverbal predicate clauses compared to Erzya. It should further be observed that identificational statements are encoded with a predicative suffix in Moksha, but seldom in Erzya. Erzya clauses are more frequently encoded using zero-constructions, displaying agreement in number only.

Fast in-memory XPath search using compressed indexes

A large fraction of an XML document typically consists of text data. The XPath query language allows text search via the equal, contains, and starts-with predicates. Such predicates can be efficiently implemented using a compressed self-index of the document's text nodes. Most queries, however, contain some parts querying the text of the document, plus some parts querying the tree structure. It is therefore a challenge to choose an appropriate evaluation order for a given query, which optimally leverages the execution speeds of the text and tree indexes. Here the SXSI system is introduced. It stores the tree structure of an XML document using a bit array of opening and closing brackets plus a sequence of labels, and stores the text nodes of the document using a global compressed self-index. On top of these indexes sits an XPath query engine that is based on tree automata. The engine uses fast counting queries of the text index in order to dynamically determine whether to evaluate top-down or bottom-up with respect to the tree structure. The resulting system has several advantages over existing systems: (1) on pure tree queries (without text search) such as the XPathMark queries, the SXSI system performs on par or better than the fastest known systems MonetDB and Qizx, (2) on queries that use text search, SXSI outperforms the existing systems by 1-3 orders of magnitude (depending on the size of the result set), and (3) with respect to memory consumption, SXSI outperforms all other systems for counting-only queries.

Una gramática descriptiva del chabacano de Ternate

This dissertation is a descriptive grammar of Ternate Chabacano, a Spanish-lexifier Creole spoken by 3.000 people in the town of Ternate, Philippines. The dissertation offers an analysis of the phonological, morphological, and syntactic system of the language. It includes an overview of the historical background, the current situation of the speech community and a collection of annotated texts. Ternate Chabacano shares many characteristics with its main adstrate language Tagalog as well as the dialectal varieties of Spanish. At present, English also exerts an influence, nevertheless mainly affecting its lexicon. The description offered is based on fieldwork conducted in Ternate. Spoken language collected through thematic interviews forms the main type of the material analysed. Information regarding the informants and text types is included in the examples. Ternate Chabacano has a five-vowel system and 17 consonant phonemes. The morphology of the language is largely isolating. Clitics are used extensively for expressing adverbial relations. The verbal system is based on the preverbal markers that express the category of tense, modality and aspect, among which aspect is the main dimension. Complex predicates and verbal chains are used in order to further distinguish aspect and modality, as well as changes of voice and valency. Intransitive verbs express motion, states, and reflexive actions, even though the majority of verbs can occur in both intransitive and transitive clauses. Ternate Chabacano is a nominative-accusative type language but the typological configuration of the Philippine languages influences the marking of its constituents. A case in point is constituted by the nominal determination system. The basic constituent order in a clause is VSO. Equative and attibutive clauses are formed by juxtaposition while the locative clauses feature a copula. Indefinite terms are expressed through existential constructions. The negation of existential clauses differs from standard negation but both are intensified in the same way. In spoken discourse, tag-questions are common. Pragmatic elements and social formulas reflect largely the corresponding Tagalog expressions. Coordination and subordination occur typically without overt markers but a variety of markers exists for expressing different relations, especially those made explicit by adverbial clauses. Verbal chains form a continuum from serial verbs to complementation and ultimately to coordination.

On the Decidability of Model-Checking Information Flow Properties

Current standard security practices do not provide substantial assurance about information flow security: the end-to-end behavior of a computing system. Noninterference is the basic semantical condition used to account for information flow security. In the literature, there are many definitions of noninterference: Non-inference, Separability and so on. Mantel presented a framework of Basic Security Predicates (BSPs) for characterizing the definitions of noninterference in the literature. Model-checking these BSPs for finite state systems was shown to be decidable in [8]. In this paper, we show that verifying these BSPs for the more expressive system model of pushdown systems is undecidable. We also give an example of a simple security property which is undecidable even for finite-state systems: the property is a weak form of non-inference called WNI, which is not expressible in Mantel’s BSP framework.

Aquisição da factividade: complementação infinitiva e extração-QU no português brasileiro

O fenômeno da factividade, no âmbito da linguística, em sentido amplo, está relacionado à propriedade que certos itens lexicais ou determinados predicadores gramaticais possuem de introduzir um pressuposto, que pode estar implícito ou explícito. No domínio verbal, Kiparsky e Kiparsky (1971) remetem a um conjunto de verbos, os quais admitem uma sentença como complemento e cujo uso pressupõe a veracidade da proposição aí expressa. Em termos aquisicionais, não há consenso acerca da idade em que factividade estaria dominada. Hopmann e Maratsos (1977), por exemplo, propuseram que seu domínio se daria a partir dos 6 anos. Para Abbeduto e Rosenberg (1985), no entanto, isso ocorreria mais cedo, por volta dos 4 anos de idade. Já Schulz (2002; 2003), defende uma aquisição gradual, que se daria por estágios e se estenderia até os 7;0 anos de idade. Léger (2007), por sua vez, afirma que o domínio da factividade, especificamente dos semifactivos, só se daria após os 11 anos. Scoville e Gordon (1979), por fim, propõem que só por volta dos 14 anos a criança seria capaz de dominar a factividade em todos os seus aspectos. Essa falta de consenso corrobora a ideia de uma aquisição gradual, uma vez que esse fenômeno envolve vários aspectos: identificação de uma subclasse de verbos, uma interpretação semântica específica, uma subcategorização sintática variável entre as línguas e um comportamento característico no que diz respeito ao movimento-QU. Esta dissertação tem como objetivo geral contribuir para os estudos sobre aquisição da factividade, particularmente no que diz respeito ao português, debruçando-se mais especificamente sobre dois aspectos pouco explorados na literatura da área: uma questão de variação translinguística, que diz respeito à possibilidade de se admitirem complementos não-finitos factivos em português, e a questão da interpretação de interrogativas-QU em contextos factivos, com propriedades características de ilha fraca. O quadro obtido é discutido frente às análises linguísticas propostas para os verbos/ predicados factivos, que têm considerado uma distinção sintática (KIPARSKY E KIPARSKY, 1971; MELVOLD, 1991; SCHULZ, 2003; AUGUSTO, 2003; LIMA, 2007), com repercussões de ordem lógico/ semântica (LEROUX E SCHULZ, 1999; SCHULZ, 2002; 2003)

O etos de Akihito: uma análise discursiva de alocuções do Imperador do Japão

Após a Segunda Guerra Mundial, o Imperador do Japão perdeu sua soberania e passou a ser símbolo da nação e da união do povo japonês, de acordo com a Constituição promulgada em 1947, sendo suas funções basicamente cerimoniais e diplomáticas. Pensando nesse Imperador enquanto símbolo e no futuro da instituição imperial no Japão, a presente dissertação objetivou principalmente analisar que imagem o Imperador Akihito cria de si por meio de suas alocuções. Tais alocuções se encontram disponíveis no sítio eletrônico da Agência da Casa Imperial, tanto no original em japonês quanto em inglês. Dessa forma, considerando que a disponibilidade dos textos em japonês pressupõe coenunciadores nipônicos e a dos textos em inglês pressupõe a comunidade internacional como coenunciadores, analisaram-se as imagens criadas nos dois casos, buscando indícios de possíveis diferenças na criação do etos de Akihito em cada uma das versões de suas alocuções. Além disso, buscou-se também pensar as relações de poder, segundo Foucault (1995, 2010), no córpus de pesquisa. Como arcabouço teórico, utilizaram-se conceitos da Análise do Discurso de base enunciativa, mais precisamente o conceito de etos na leitura de Maingueneau (1997, 2001b). O material de análise coletado abrange conferências de imprensa realizadas por ocasião da comemoração de dez e vinte anos de reinado de Akihito, nos anos de 1999 e 2009, respectivamente. A metodologia de pesquisa, por sua vez, consistiu em se analisar de forma comparativa os textos em japonês com aqueles em inglês, tendo como foco as ocorrências do verbo japonês omou, que expressa sentimento e julgamento, recorrente nas alocuções do Imperador. Analisaram-se também as ocorrências de modalidades deônticas em ambas as versões do texto, acreditando-se que a pouca ocorrência dessas também contribui para se pensar a imagem do Imperador. Como resultado, verificaram-se diferenças significativas entre as duas versões das alocuções. O etos de Akihito nas alocuções em japonês sugere um Imperador amigo e próximo do povo, de tom moderado e amenizado, criando identificação entre ele e o povo. O etos apreendido na versão em inglês, por sua vez, sugere um Imperador mais firme em suas convicções, ora enfatizando mais seus sentimentos e opiniões, ora menos, conferindo-se certa ocidentalização de sua imagem. Pensando-se em termos de relação de poder, que caracteriza controle e divulgação, também se concluiu que, sendo o Japão o maior aliado capitalista no Oriente e seu Imperador, representante simbólico desse país, parece pertinente que suas alocuções estejam disponíveis de forma tal que possibilite um controle constante por parte da comunidade internacional, garantindo a ordem capitalista

青藏高原东部电性结构特征及地球动力学意义

As the largest and highest plateau on the Earth, the Tibetan Plateau has been a key location for understanding the processes of mountain building and plateau formation during India-Asia continent-continent collision. As the front-end of the collision, the geological structure of eastern Tibetan Plateau is very complex. It is ideal as a natural laboratory for investigating the formation and evolution of the Tibetan Plateau. Institute of Geophysics, Chinese Academy of Sciences (CAS) carried out MT survey from XiaZayii to Qingshuihe in the east part of the plateau in 1998. After error analysis and distortion analysis, the Non-linear Conjugate Gradient inversion(NLCG), Rapid Relaxation Inversin (RRI) and 2D OCCAM Inversion algorithms were used to invert the data. The three models obtained from 3 algorithms provided similar electrical structure and the NLCG model fit the observed data better than the other two models. According to the analysis of skin depth, the exploration depth of MT in Tibet is much more shallow than in stable continent. For example, the Schmucker depth at period 100s is less than 50km in Tibet, but more than 100km in Canadian Shield. There is a high conductivity layer at the depth of several kilometers beneath middle Qiangtang terrane, and almost 30 kilometers beneath northern Qiangtang terrane. The sensitivity analysis of the data predicates that the depth and resistivity of the crustal high conductivity layer are reliable. The MT results provide a high conductivity layer at 20~40km depth, where the seismic data show a low velocity zone. The experiments show that the rock will dehydrate and partially melt in the relative temperature and pressure. Fluids originated from dehydration and partial melting will seriously change rheological characteristics of rock. Therefore, This layer with low velocity and high conductivity layer in the crust is a weak layer. There is a low velocity path at the depth of 90-110 km beneath southeastern Tibetan Plateau and adjacent areas from seismology results. The analysis on the temperature and rheological property of the lithosphere show that the low velocity path is also weak. GPS measurements and the numerical simulation of the crust-mantle deformation show that the movement rate is different for different terranes. The regional strike derived from decomposition analysis for different frequency band and seismic anisotropy indicate that the crust and upper mantle move separately instead of as a whole. There are material flow in the eastern and southeastern Tibetan Plateau. Therefore, the faults, the crustal and upper mantle weak layers are three different boundaries for relatively movement. Those results support the "two layer wedge plates" geodynamic model on Tibetan formation and evolution.

Program Improvement by Automatic Redistribution of Intermediate Results

Introducing function sharing into designs allows eliminating costly structure by adapting existing structure to perform its function. This can eliminate many inefficiencies of reusing general componentssin specific contexts. "Redistribution of intermediate results'' focuses on instances where adaptation requires only addition/deletion of data flow and unused code removal. I show that this approach unifies and extends several well-known optimization classes. The system performs search and screening by deriving, using a novel explanation-based generalization technique, operational filtering predicates from input teleological information. The key advantage is to focus the system's effort on optimizations that are easier to prove safe.

Justified Generalization: Acquiring Procedures from Examples

This thesis describes an implemented system called NODDY for acquiring procedures from examples presented by a teacher. Acquiring procedures form examples involves several different generalization tasks. Generalization is an underconstrained task, and the main issue of machine learning is how to deal with this underconstraint. The thesis presents two principles for constraining generalization on which NODDY is based. The first principle is to exploit domain based constraints. NODDY demonstrated how such constraints can be used both to reduce the space of possible generalizations to manageable size, and how to generate negative examples out of positive examples to further constrain the generalization. The second principle is to avoid spurious generalizations by requiring justification before adopting a generalization. NODDY demonstrates several different ways of justifying a generalization and proposes a way of ordering and searching a space of candidate generalizations based on how much evidence would be required to justify each generalization. Acquiring procedures also involves three types of constructive generalizations: inferring loops (a kind of group), inferring complex relations and state variables, and inferring predicates. NODDY demonstrates three constructive generalization methods for these kinds of generalization.

An Empirical Study of the Use of Relevance Information in Inductive Logic Programming

Srinivasan, A., King, R. D. and Bain, M.E. (2003) An Empirical Study of the Use of Relevance Information in Inductive Logic Programming. Journal of Machine Learning Research. 4(Jul):369-383