• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 135
  • 34
  • 8
  • 6
  • 4
  • 2
  • 2
  • 2
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • Tagged with
  • 247
  • 247
  • 82
  • 50
  • 40
  • 37
  • 36
  • 33
  • 29
  • 29
  • 28
  • 26
  • 24
  • 23
  • 22
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
71

Decompilation of WebAssembly using Datalog / Dekompilering av WebAssembly i Datalog

Brandefelt, Love January 2022 (has links)
With 92% of today’s browsers supporting WebAssembly the need for decompilers to discover malicious code is greater than ever. The introduction of the Datalog to C++ compiler Soufflé, in 2016, enables the implementation of effective Datalog-based decompilers. This thesis investigates if a Datalogbased approach to decompilation can be used to implement a WebAssembly decompiler. Such a decompiler is implemented and then evaluated in terms of decompilability, recompilabilty and semantic equivalence using randomly generated programs of various complexity. Each generated program is first decompiled, then recompiled if the decompilation was successful, and finally executed if the recompilation was successful. The results showed that the implementation can decompile all generated programs and that most of the decompiled programs are recompilable. However, only 70% of the lowest complexity programs maintained the output of the original program. As the complexity increased this percentage fell below 20%, a result of more complex programs being more likely to contain code structures that are not handled correctly. If the similarity of the decompiled programs were instead measured by recompiling the decompiled programs to WebAssembly and observing the number of instructions differing from the original WebAssembly binary the percentages were slightly more satisfying with the percentage of instructions differing ranging from 25% for the lowest complexity programs to 65% for the highest complexity programs. While the results are not distinct enough to draw the conclusion that a Datalog-based approach to decompilation is suitable for implementing a WebAssembly decompiler they instigate the need for further research on the topic, e.g. by supporting more WebAssembly instructions as well as supporting WebAssembly binaries compiled from other languages than C. / Idag stödjer 92% av alla webbläsare WebAssembly och behovet av dekompilatorer för att upptäcka skadlig kod är större än någonsin. Datalog-kompilatorn Soufflé som introducerades 2016 gjorde det möjligt att implementera effektiva Datalog-baserade dekompilatorer. Detta arbete undersöker om en Datalogbaserad dekompilator kan användas för att implementera en WebAssemblydekompilator. Detta genomförs genom att en Datalog-baserad WebAssemblydekompilator implementeras och sedan utvärderas i termer av dekompilerbarhet, återkompilerbarhet och semantisk ekvivalens med hjälp av slumpmässigt genererade program av varierande komplexitet. Varje genererat program dekompileras och kompileras sedan igen för att slutligen exekveras. Resultaten visade att dekompilatorn kunde dekompilera alla genererade program och att de flesta av de dekompilerade programmen var omkompilerbara. Däremot gav endast 70% av programmen med lägst komplexitet samma utdata som respektive ursprungsprogram. När komplexiteten ökade sjönk denna procentsats till under 20%, en följd av att program av en högre komplexitet i högre grad innehåller kodstrukturer som hanteras felaktigt. Om likheten mellan de dekompilerade programmen istället mättes genom att kompilera om de dekompilerade programmen till WebAssembly och titta på antalet instruktioner som skiljer sig från den ursprungliga WebAssembly-binären var resultaten något mer tillfredsställande med endast 25%’s skillnad för programmen med lägst komplexitet upp till 65%’s skillnad för programmen med högst komplexitet. Trots att resultaten inte är tillräckligt tydliga för att dra slutsatsen att en Datalog-baserad dekompilator är lämplig för att implementera en WebAssembly-dekompilator, tydliggör de behovet av vidare forskning på ämnet, t.ex genom att stödja fler WebAssembly-instruktioner samt genom att stödja WebAssembly-binärer kompilerade från andra språk än C.
72

Building an expert system shell for design model synthesis in logic programming

Huang, Yueh-Min, 1960- January 1987 (has links)
This thesis implemented a prototype of an expert system shell for support of engineering design activities in the way of logic programming. The development of the system is based on the theoretical framework for knowledge-based system design and the formal modeling concepts. Under the above methodologies, two knowledge representations, production rule system and system entity structure, are incorporated into the knowledge base for figuring design structures. Here the production system scheme is employed for synthesis of design models represented in the system entity structure. The whole system is coded in Turbo Prolog and a specific domain knowledge, namely a local area network, is currently used as a testbed environment.
73

Using Extended Logic Programs to Formalize Commonsense Reasoning

Horng, Wen-Bing 05 1900 (has links)
In this dissertation, we investigate how commonsense reasoning can be formalized by using extended logic programs. In this investigation, we first use extended logic programs to formalize inheritance hierarchies with exceptions by adopting McCarthy's simple abnormality formalism to express uncertain knowledge. In our representation, not only credulous reasoning can be performed but also the ambiguity-blocking inheritance and the ambiguity-propagating inheritance in skeptical reasoning are simulated. In response to the anomalous extension problem, we explore and discover that the intuition underlying commonsense reasoning is a kind of forward reasoning. The unidirectional nature of this reasoning is applied by many reformulations of the Yale shooting problem to exclude the undesired conclusion. We then identify defeasible conclusions in our representation based on the syntax of extended logic programs. A similar idea is also applied to other formalizations of commonsense reasoning to achieve such a purpose.
74

Apprentissage de problèmes de contraintes / Constraint problems learning

Lopez, Matthieu 08 December 2011 (has links)
La programmation par contraintes permet de modéliser des problèmes et offre des méthodes de résolution efficaces. Cependant, sa complexité augmentant ces dernières années, son utilisation, notamment pour modéliser des problèmes, est devenue limitée à des utilisateurs possédant une bonne expérience dans le domaine. Cette thèse s’inscrit dans un cadre visant à automatiser la modélisation. Les techniques existantes ont montré des résultats encourageants mais certaines exigences rendent leur utilisation encore problématique. Dans une première partie, nous proposons de dépasser une limite existante qui réside dans la nécessité pour l’utilisateur de fournir des solutions du problème qu’il veut modéliser. En remplacement, il nous fournit des solutions de problèmes proches, c’est-à-dire de problèmes dont la sémantique de fond est la même mais dont les variables et leur domaine peuvent changer. Pour exploiter de telles données, nous proposons d’acquérir, grâce à des techniques de programmation logique inductive, un modèle plus abstrait que le réseau de contraintes. Une fois appris, ce modèle est ensuite transformé pour correspondre au problème initial que souhaitait résoudre l’utilisateur. Nous montrons également que la phase d’apprentissage se heurte à des limites pathologiques et qui nous ont contraints à développer un nouvel algorithme pour synthétiser ces modèles abstraits. Dans une seconde partie, nous nous intéressons à la possibilité pour l’utilisateur de ne pas donner d’exemples du tout. En partant d’un CSP sans aucune contrainte, notre méthode consiste à résoudre le problème de l’utilisateur de manière classique. Grâce à un arbre de recherche, nous affectons progressivement des valeurs aux variables. Quand notre outil ne peut décider si l’affectation partielle courante est correcte ou non, nous demandons à l’utilisateur de guider la recherche sous forme de requêtes. Ces requêtes permettent de trouver des contraintes à ajouter aux modèles du CSP et ainsi améliorer la recherche. / Constraint programming allows to model many kind of problems with efficient solving methods. However, its complexity has increased these last years and its use, notably to model problems, has become limited to people with a fair expertise in the domain. This thesis deals with automating the modeling task in constraint programming. Methods already exist, with encouraging results, but many requirements are debatable. In a first part, we propose to avoid the limitation consisting, for the user, in providing solutions of the problem she aims to solve. As a replacement of these solutions, the user has to provide solutions of closed problem, i.e problem with same semantic but where variables and domains can be different. To handle this kind of data, we acquire, thanks to inductive logic programming, a more abstract model than the constraint network. When this model is learned, it is translated in the very constraint network the user aims to model. We show the limitations of learning method to build such a model due to pathological problems and explain the new algorithm we have developed to build these abstract models. In a second part, we are interesting in the possibility to the user to not provide any examples. Starting with a CSP without constraints, our method consists in solving the problem the user wants in a standard way. Thanks to a search tree, we affect to each variable a value. When our tool cannot decide if the current partial affectation is correct or not, we ask to the user, with yes/no queries, to guide the search. These queries allow to find constraints to add to the model and then to improve the quality of the search.
75

Interval linear constraint solving in constraint logic programming.

January 1994 (has links)
by Chong-kan Chiu. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1994. / Includes bibliographical references (leaves 97-103). / Chapter 1 --- Introduction --- p.1 / Chapter 1.1 --- Related Work --- p.2 / Chapter 1.2 --- Organizations of the Dissertation --- p.4 / Chapter 1.3 --- Notations --- p.4 / Chapter 2 --- Overview of ICLP(R) --- p.6 / Chapter 2.1 --- Basics of Interval Arithmetic --- p.6 / Chapter 2.2 --- Relational Interval Arithmetic --- p.8 / Chapter 2.2.1 --- Interval Reduction --- p.8 / Chapter 2.2.2 --- Arithmetic Primitives --- p.10 / Chapter 2.2.3 --- Interval Narrowing and Interval Splitting --- p.13 / Chapter 2.3 --- Syntax and Semantics --- p.16 / Chapter 3 --- Limitations of Interval Narrowing --- p.18 / Chapter 3.1 --- Computation Inefficiency --- p.18 / Chapter 3.2 --- Inability to Detect Inconsistency --- p.23 / Chapter 3.3 --- The Newton Language --- p.27 / Chapter 4 --- Design of CIAL --- p.30 / Chapter 4.1 --- The CIAL Architecture --- p.30 / Chapter 4.2 --- The Inference Engine --- p.31 / Chapter 4.2.1 --- Interval Variables --- p.31 / Chapter 4.2.2 --- Extended Unification Algorithm --- p.33 / Chapter 4.3 --- The Solver Interface and Constraint Decomposition --- p.34 / Chapter 4.4 --- The Linear and the Non-linear Solvers --- p.37 / Chapter 5 --- The Linear Solver --- p.40 / Chapter 5.1 --- An Interval Gaussian Elimination Solver --- p.41 / Chapter 5.1.1 --- Naive Interval Gaussian Elimination --- p.41 / Chapter 5.1.2 --- Generalized Interval Gaussian Elimination --- p.43 / Chapter 5.1.3 --- Incrementality of Generalized Gaussian Elimination --- p.47 / Chapter 5.1.4 --- Solvers Interaction --- p.50 / Chapter 5.2 --- An Interval Gauss-Seidel Solver --- p.52 / Chapter 5.2.1 --- Interval Gauss-Seidel Method --- p.52 / Chapter 5.2.2 --- Preconditioning --- p.55 / Chapter 5.2.3 --- Increment ality of Preconditioned Gauss-Seidel Method --- p.58 / Chapter 5.2.4 --- Solver Interaction --- p.71 / Chapter 5.3 --- Comparisons --- p.72 / Chapter 5.3.1 --- Time Complexity --- p.72 / Chapter 5.3.2 --- Storage Complexity --- p.73 / Chapter 5.3.3 --- Others --- p.74 / Chapter 6 --- Benchmarkings --- p.76 / Chapter 6.1 --- Mortgage --- p.78 / Chapter 6.2 --- Simple Linear Simultaneous Equations --- p.79 / Chapter 6.3 --- Analysis of DC Circuit --- p.80 / Chapter 6.4 --- Inconsistent Simultaneous Equations --- p.82 / Chapter 6.5 --- Collision Problem --- p.82 / Chapter 6.6 --- Wilkinson Polynomial --- p.85 / Chapter 6.7 --- Summary and Discussion --- p.86 / Chapter 6.8 --- Large System of Simultaneous Equations --- p.87 / Chapter 6.9 --- Comparisons Between the Incremental and the Non-Incremental Preconditioning --- p.89 / Chapter 7 --- Concluding Remarks --- p.93 / Chapter 7.1 --- Summary and Contributions --- p.93 / Chapter 7.2 --- Future Work --- p.95 / Bibliography --- p.97
76

Rapid prototyping of software specifications in Z.

January 1993 (has links)
by Wu Chun Pong. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1993. / Includes bibliographical references (leaves 86-[91]). / Chapter 1 --- Introduction --- p.1 / Chapter 1.1 --- Formal Specification Methods --- p.1 / Chapter 1.2 --- The Z notation --- p.2 / Chapter 1.3 --- Overview of Thesis --- p.3 / Chapter 2 --- The Specification Language Z --- p.5 / Chapter 2.1 --- Background --- p.5 / Chapter 2.2 --- Structure and Characteristics --- p.6 / Chapter 2.3 --- Object Orientation in Z --- p.10 / Chapter 2.3.1 --- Hall's style --- p.11 / Chapter 2.3.2 --- Schuman and Pitt's variant --- p.11 / Chapter 2.3.3 --- Object-Z --- p.12 / Chapter 2.4 --- Execution in Z --- p.13 / Chapter 2.5 --- Animation of Z Specifications --- p.15 / Chapter 2.5.1 --- Prolog --- p.15 / Chapter 2.5.2 --- Translation Z into Prolog --- p.18 / Chapter 2.5.3 --- Related Works --- p.19 / Chapter 3 --- Incorporating Real Numbers in Z --- p.22 / Chapter 3.1 --- Dedekind Cut --- p.23 / Chapter 3.2 --- Cantor's definition --- p.23 / Chapter 3.3 --- Practical approach --- p.24 / Chapter 4 --- Constraint Logic Programming and CLP(R) --- p.26 / Chapter 4.1 --- Constraint Logic Programming --- p.26 / Chapter 4.2 --- CLP(R) --- p.27 / Chapter 4.3 --- Example of CLP(R) --- p.29 / Chapter 5 --- The ZCLP(R) Animation System --- p.31 / Chapter 5.1 --- Design Philosophy --- p.31 / Chapter 5.2 --- Implementation Strategy --- p.34 / Chapter 5.3 --- Z editor (ZEDIT) --- p.36 / Chapter 5.4 --- Prolog Library for set operation (ZCLIB) --- p.37 / Chapter 5.4.1 --- Basic needs for the Library --- p.37 / Chapter 5.4.2 --- Rules for the library --- p.38 / Chapter 5.4.3 --- Limitation of the Library --- p.43 / Chapter 5.5 --- Z to CLP(R) Translator (ZCGEN) --- p.44 / Chapter 5.5.1 --- Procedure for translation --- p.45 / Chapter 5.5.2 --- Demonstration --- p.47 / Chapter 5.5.3 --- Rules for translation --- p.48 / Chapter 5.5.4 --- Limitations of the Translator --- p.50 / Chapter 5.6 --- Z to LATEX translator (ZLATEX) --- p.52 / Chapter 6 --- Examples --- p.54 / Chapter 6.1 --- A Simple Banking System --- p.54 / Chapter 6.1.1 --- Bags --- p.54 / Chapter 6.1.2 --- Specifications --- p.56 / Chapter 6.2 --- A Graphics Example --- p.61 / Chapter 6.2.1 --- Defining a Rectangle --- p.62 / Chapter 6.2.2 --- Drawing a Rectangle --- p.63 / Chapter 6.2.3 --- Defining a Circle --- p.63 / Chapter 6.2.4 --- Specifications --- p.64 / Chapter 6.3 --- Specifications Writing Experience --- p.76 / Chapter 7 --- Conclusion --- p.79 / Chapter 7.1 --- Contributions --- p.79 / Chapter 7.2 --- Difficulties --- p.83 / Chapter 7.3 --- Further Works --- p.84 / Bibliography --- p.86
77

Evolutionary program induction directed by logic grammars.

January 1995 (has links)
by Wong Man Leung. / Thesis (Ph.D.)--Chinese University of Hong Kong, 1995. / Includes bibliographical references (leaves 227-236). / List of Figures --- p.iii / List of Tables --- p.vi / Chapter Chapter 1 : --- Introduction --- p.1 / Chapter 1.1. --- Automatic programming and program induction --- p.1 / Chapter 1.2. --- Motivation --- p.6 / Chapter 1.3. --- Contributions of the research --- p.8 / Chapter 1.4. --- Outline of the thesis --- p.11 / Chapter Chapter 2 : --- An Overview of Evolutionary Algorithms --- p.13 / Chapter 2.1. --- Evolutionary algorithms --- p.13 / Chapter 2.2. --- Genetic Algorithms (GAs) --- p.15 / Chapter 2.2.1. --- The canonical genetic algorithm --- p.16 / Chapter 2.2.1.1. --- Selection methods --- p.21 / Chapter 2.2.1.2. --- Recombination methods --- p.24 / Chapter 2.2.1.3. --- Inversion and Reordering --- p.27 / Chapter 2.2.2. --- Implicit parallelism and the building block hypothesis --- p.28 / Chapter 2.2.3. --- Steady state genetic algorithms --- p.32 / Chapter 2.2.4. --- Hybrid algorithms --- p.33 / Chapter 2.3. --- Genetic Programming (GP) --- p.34 / Chapter 2.3.1. --- Introduction to the traditional GP --- p.34 / Chapter 2.3.2. --- Automatic Defined Function (ADF) --- p.41 / Chapter 2.3.3. --- Module Acquisition (MA) --- p.44 / Chapter 2.3.4. --- Strongly Typed Genetic Programming (STGP) --- p.49 / Chapter 2.4. --- Evolution Strategies (ES) --- p.50 / Chapter 2.5. --- Evolutionary Programming (EP) --- p.55 / Chapter Chapter 3 : --- Inductive Logic Programming --- p.59 / Chapter 3.1. --- Inductive concept learning --- p.59 / Chapter 3.2. --- Inductive Logic Programming (ILP) --- p.62 / Chapter 3.2.1. --- Interactive ILP --- p.64 / Chapter 3.2.2. --- Empirical ILP --- p.65 / Chapter 3.3. --- Techniques and methods of ILP --- p.67 / Chapter Chapter 4 : --- Genetic Logic Programming and Applications --- p.74 / Chapter 4.1. --- Introduction --- p.74 / Chapter 4.2. --- Representations of logic programs --- p.76 / Chapter 4.3. --- Crossover of logic programs --- p.81 / Chapter 4.4. --- Genetic Logic Programming System (GLPS) --- p.87 / Chapter 4.5. --- Applications --- p.90 / Chapter 4.5.1. --- The Winston's arch problem --- p.91 / Chapter 4.5.2. --- The modified Quinlan's network reachability problem --- p.92 / Chapter 4.5.3. --- The factorial problem --- p.95 / Chapter Chapter 5 : --- The logic grammars based genetic programming system (LOGENPRO) --- p.100 / Chapter 5.1. --- Logic grammars --- p.101 / Chapter 5.2. --- Representations of programs --- p.103 / Chapter 5.3. --- Crossover of programs --- p.111 / Chapter 5.4. --- Mutation of programs --- p.126 / Chapter 5.5. --- The evolution process of LOGENPRO --- p.130 / Chapter 5.6. --- Discussion --- p.132 / Chapter Chapter 6 : --- Applications of LOGENPRO --- p.134 / Chapter 6.1. --- Learning functional programs --- p.134 / Chapter 6.1.1. --- Learning S-expressions using LOGENPRO --- p.134 / Chapter 6.1.2. --- The DOT PRODUCT problem --- p.137 / Chapter 6.1.2. --- Learning sub-functions using explicit knowledge --- p.143 / Chapter 6.2. --- Learning logic programs --- p.148 / Chapter 6.2.1. --- Learning logic programs using LOGENPRO --- p.148 / Chapter 6.2.2. --- The Winston's arch problem --- p.151 / Chapter 6.2.3. --- The modified Quinlan's network reachability problem --- p.153 / Chapter 6.2.4. --- The factorial problem --- p.154 / Chapter 6.2.5. --- Discussion --- p.155 / Chapter 6.3. --- Learning programs in C --- p.155 / Chapter Chapter 7 : --- Knowledge Discovery in Databases --- p.159 / Chapter 7.1. --- Inducing decision trees using LOGENPRO --- p.160 / Chapter 7.1.1. --- Decision trees --- p.160 / Chapter 7.1.2. --- Representing decision trees as S-expressions --- p.164 / Chapter 7.1.3. --- The credit screening problem --- p.166 / Chapter 7.1.4. --- The experiment --- p.168 / Chapter 7.2. --- Learning logic program from imperfect data --- p.174 / Chapter 7.2.1. --- The chess endgame problem --- p.177 / Chapter 7.2.2. --- The setup of experiments --- p.178 / Chapter 7.2.3. --- Comparison of LOGENPRO with FOIL --- p.180 / Chapter 7.2.4. --- Comparison of LOGENPRO with BEAM-FOIL --- p.182 / Chapter 7.2.5. --- Comparison of LOGENPRO with mFOILl --- p.183 / Chapter 7.2.6. --- Comparison of LOGENPRO with mFOIL2 --- p.184 / Chapter 7.2.7. --- Comparison of LOGENPRO with mFOIL3 --- p.185 / Chapter 7.2.8. --- Comparison of LOGENPRO with mFOIL4 --- p.186 / Chapter 7.2.9. --- Comparison of LOGENPRO with mFOIL5 --- p.187 / Chapter 7.2.10. --- Discussion --- p.188 / Chapter 7.3. --- Learning programs in Fuzzy Prolog --- p.189 / Chapter Chapter 8 : --- An Adaptive Inductive Logic Programming System --- p.192 / Chapter 8.1. --- Adaptive Inductive Logic Programming --- p.192 / Chapter 8.2. --- A generic top-down ILP algorithm --- p.196 / Chapter 8.3. --- Inducing procedural search biases --- p.200 / Chapter 8.3.1. --- The evolution process --- p.201 / Chapter 8.3.2. --- The experimentation setup --- p.202 / Chapter 8.3.3. --- Fitness calculation --- p.203 / Chapter 8.4. --- Experimentation and evaluations --- p.204 / Chapter 8.4.1. --- The member predicate --- p.205 / Chapter 8.4.2. --- The member predicate in a noisy environment --- p.205 / Chapter 8.4.3. --- The multiply predicate --- p.206 / Chapter 8.4.4. --- The uncle predicate --- p.207 / Chapter 8.5. --- Discussion --- p.208 / Chapter Chapter 9 : --- Conclusion and Future Work --- p.210 / Chapter 9.1. --- Conclusion --- p.210 / Chapter 9.2. --- Future work --- p.217 / Chapter 9.2.1. --- Applying LOGENPRO to discover knowledge from databases --- p.217 / Chapter 9.2.2. --- Learning recursive programs --- p.218 / Chapter 9.2.3. --- Applying LOGENPRO in engineering design --- p.220 / Chapter 9.2.4. --- Exploiting parallelism of evolutionary algorithms --- p.222 / Reference --- p.227 / Appendix A --- p.237
78

Superoptimisation : provably optimal code generation using answer set programming

Crick, Thomas January 2009 (has links)
No description available.
79

Needed Narrowing as the Computational Strategy of Evaluable Functions in an Extension of Goedel

Barry, Bobbi J. 12 June 1996 (has links)
A programming language that combines the best aspects of both the functional and logic paradigms with a complete evaluation strategy has been a goal of a Portland State University project team for the last several years. I present the third in a series of modifications to the compiler of the logic programming language Goedel which reaches this goal. This enhancement of Goedel's compiler translates user-defined functions in the form of rewrite rules into code that performs evaluation of these functions by the strategy of needed narrowing. In addition, Goedel's mechanism that evaluates predicates is supplemented so that needed narrowing is still maintained as the evaluation strategy when predicates possess functional arguments.
80

Logic programming based formal representations for authorization and security protocols

Wang, Shujing, University of Western Sydney, College of Health and Science, School of Computing and Mathematics January 2008 (has links)
Logic programming with answer set semantics has been considered appealing rule-based formalism language and applied in information security areas. In this thesis, we investigate the problems of authorization in distributed environments and security protocol verification and update. Authorization decisions are required in large-scale distributed environments, such as electronic commerce, remote resource sharing, etc. We adopt the trust management approach, in which authorization is viewed as a ‘proof of compliance" problem. We develop an authorization language AL with non-monotonic feature as the policy and credential specification language, which can express delegation with depth control, complex subject structures, both positive and negative authorizations, and separation of duty concepts. The theoretical foundation for language AL is the answer set semantics of logic programming. We transform AL to logic programs and the authorization decisions are based on answer sets of the programs. We also explore the tractable subclasses of language AL. We implement a fine grained access control prototype system for XML resources, in which the language AL¤ simplified from AL is the policy and credential specification language. We define XPolicy, the XML format of AL¤, which is a DTD for the XML policy documents. The semantics of the policy is based on the semantics of language AL. The system is implemented using Java programming. We investigate the security protocol verification problem in provable security approach. Based on logic programming with answer set semantics, we develop a unified framework for security protocol verification and update, which integrates protocol specification, verification and update. The update model is defined using forgetting techniques in logic programming. Through a case study protocol, we demonstrate an application of our approach. / Doctor of Philosophy (PhD)

Page generated in 0.1052 seconds