Seon-Ho Park's Blog (sunoblog) Study on Computer Science, Security, Model

19Jul/100

\mathcal{}

\mathcal{F}, \mathcal{P}, \mathcal{L}_{0}^{'}

\mathcal{F}, \mathcal{P}, \mathcal{L}_{0}^{'}

13Jul/100

Predicate Logic – part I

My second presentation in doctoral seminar presented at lab was about a predicate logic. Predicate logic is one of the important area of the symbolic logic. The predicate logic, also called first-order predicate calculus, is distinguished from propositional logic by its use of predicates and quantifiers. For using predicates and quantifiers, variables are used in predicate logic, and also constants and function symbols can be used.

In this seminar, I presented an overview, description of predicate logic as a formal language, and proof theory of predicate logic. Issues about semantics and undecidability of predicate logic will be presented in next seminar presentation(maybe...7/22~7/23).

My presentation material is attached in this post. It is written using a latex and beamer-class.

[Theory]PredicateLogic_shpark_0.1

13Jul/106

Quantifier Equivalences in Predicate Logic

Theorem for Quantifier Equivalences
  1. \neg \forall x \phi \dashv \vdash \exists x \neg \phi
  2. \neg \exists x \phi \dashv \vdash \forall x \neg \phi
  3. \forall x \phi \wedge \psi \dashv \vdash \forall x (\phi \wedge \psi)
  4. \forall x \phi \vee \psi \dashv \vdash \forall x (\phi \vee \psi)
  5. \exists x \phi \wedge \psi \dashv \vdash \exists x (\phi \wedge \psi)
  6. \exists x \phi \vee \psi \dashv \vdash \exists x (\phi \vee \psi)
  7. \forall x (\psi \rightarrow \phi) \dashv \vdash \psi \rightarrow \forall x \phi
  8. \exists x (\phi \rightarrow \psi) \dashv \vdash \forall x \phi \rightarrow \psi
  9. \forall x(\phi \rightarrow \psi) \dashv \vdash \exists x \phi \rightarrow \psi
  10. \exists x(\psi \rightarrow \phi) \dashv \vdash \psi \rightarrow \exists x \phi
  11. \forall x \phi \wedge \forall x \psi \dashv \vdash \forall x (\phi \wedge \psi)
  12. \exists x \phi \vee \exists x \psi \dashv \vdash \exists x (phi \vee \psi)
  13. \forall x \forall y \phi \dashv \vdash \forall y \forall x \phi
  14. \exists x \exists y \phi \dashv \vdash \exists y \exists x \phi
 Assuming~that~x~is~not~free~in~\psi,~for~theorem3-10.

6Jul/100

[7/6~7/9]To do

In this week, there are a lot of things I must do completely. Paper works, preparing seminar, meeting for LGE project, etc. Followings are that I must do in this week.

  • Paper work

- Related works on context-aware access control
- Scenarios of ubiquitous computing service and security threats

  • Preparing seminar

- Remain parts of the propositional logic and the predicate Logic

  • Meeting

- Preparing LGE meeting (to decide project plans & contract)
- July 8, 5 pm

Filed under: To do No Comments
6Jul/101

Installing Beamer

Today I tried to install the beamer-class to make document for presentation using latex. Until now, I have used MS Power Point application mainly for making presentation document. The power point program is useful and easy for making presentation slides, but it has several difficulties in compatibility and mathematical expression. I suffered these problems in last seminar. So, I decided to try another method though I'm very very busy... I like latex and its mathematical representation, therefore I try to search methods to make presentation using latex. As a result, I found "beamer-class". I downloaded it at once, and tried to install...but it is not easy because I don't know well various functions of the MikTeX. I searched method for install it...and I became known installing beamer-class in MikTex is very simple and easy....

  • After downloading beamer file, just extract that and put it in a so-called texmf tree (c:\texmf in my case)
  • In MikTeX, reflesh FNDB (Setting->General->Refresh FNDB)
  • Installation is just completed.

More details for installation are described "beameruserguide.pdf" in downloaded files. If you are not a MikTeX user, refer to the pdf file.

I'll soon post a result of making my presentation document made using beamer.

Tagged as: , 1 Comment
3Jul/100

Propositional Logic

In lab., doctoral students and Dr. Eom have started doctoral seminar. Computer theories, a probability theory and a graph theory are the subject of seminar. I response a part of computer theory which consists of the logic in computer science, an automata theory, a computability theory and a complexity theory. My first seminar presentation was presented on June 30 in last week. The presentation is about a propositional logic. I attach presentation file on this post.

[Theory]PropositionalLogic_shpark_v1_EngVer

3Jul/100

Role Based Access Control – Frequently Asked Questions


[This material is a contribution of the National Institute of Standards and Technology and is not subject to U.S copyright.]

Ferraiolo and Kuhn (1992) gave a formal definition of roles as sets of permissions, role hierarchies, subject-role activation, subject-object mediation, as well as constraints on user/role membership and role activation.

Nyanchama and Osborn  (1994) developed a role graph model for RBAC, providing efficient algorithms for analyzing role relationships.

Ferraiolo, Kuhn, and colleagues developed a prototype RBAC implementation and a 1995 paper further developing the RBAC model with formal definitions of static and dynamic separation of duty.

Sandhu, Coyne, Feinstein, and Youman  (1996) introduced a framework of RBAC models, breaking down RBAC into four conceptual models that can be combined to provide a variety of RBAC systems.

Sandhu (1996) showed that RBAC could be used to implement traditional multilevel security policies.

Kuhn (1997) provided theorems on necessary and sufficient conditions to ensure separation safety.  These results were extended by Li et al. in 2004.

Osborn (1997) provided a role lemma that must hold in a system supporting both multilevel security and RBAC.

Kuhn (1998) showed that a multilevel-secure system can implement RBAC, when the role hierarchy is a tree rather than a partial order.

Sandhu and Munawer (1998) provided a method of implementing discretionary access control using RBAC.

Tagged as: , No Comments
3Jul/102

Role Based Access Control – Theory and Practice Timeline

Summary of early theoretical results for RBAC models that evolved into RBAC standard

  • 1992 – Ferraiolo and Kuhn paper defining  RBAC model, with access  permitted only through roles. Formally defined role hierarchies and constraints including separation of duty.
  • 1994 – DTOS based RBAC prototype developed by Ferraiolo, Kuhn, Gavrila
  • 1994 – Nyanchama and Osborn paper defined role graph model
  • 1994 – IBM files (in Europe) first patent application in RBAC area, cites Ferraiolo, Kuhn work as “closest prior art”
  • 1995 – Ferraiolo, Cugini, Kuhn publish extended formal model, defined separation of duty forms
  • 1996 – Sandhu, Coyne, Feinstein, Youman  paper defining family of RBAC models
  • 1996 – Sandhu method for implementing MLS/MAC model on RBAC system
  • 1997 – Kuhn paper on separation of duty; necessary and sufficient conditions for separation safety
  • 1997 – Osborn paper on relationship between RBAC and multilevel security mandatory access (MLS/MAC) security policy models; role lemma relating RBAC and multilevel security
  • 1997 – Ferraiolo and Barkley paper on economic advantages of RBAC
  • 1998 – Kuhn method for implementing hierarchical RBAC model on MLS/MAC system
  • 1999 – Prototype RBAC for web servers developed by Barkley, Ferraiolo, Kuhn, Cincotta and distributed as open source
  • 2000 – Sandhu, Ferraiolo, Kuhn define consolidated RBAC model for proposed industry standard
  • 2001 – Research Triangle Institute study on economic impact of RBAC attributes 44% of RBAC impact to NIST research
  • 2004 – American National Standards Institute, International Committee for Information Technology Standards (ANSI/INCITS) adopts Sandhu, Ferraiolo, Kuhn RBAC proposal as an industry consensus standard INCITS 359:2004
Tagged as: 2 Comments
3Jul/100

My first post

My first post at sunoblog which is powerd by wordpress.

I gonna post about my study, schedule, something to do and result, interesting, etc. The post is going to be written by English, though my native language is Korean. My English is not well, so there can be some grammatical error or clumsy expression in my post. I'd like to ask for your understand...^^

Filed under: Uncategorized No Comments