1 \documentclass{article}

     2 \usepackage{charter}

     3 \usepackage{hyperref}

     4 \usepackage{amssymb}

     5 

     6 \begin{document}

     7 

     8 \section*{Homework 6}

     9 

    10 \begin{enumerate}

    11 \item Access-control logic includes formulas of the form

    12 \begin{center}

    13 $P\;\textit{says}\;F$

    14 \end{center}

    15 

    16 where $P$ is a principal and $F$ a formula. Give two inference rules

    17 of access-control logic involving $\textit{says}$.

    18 

    19 \item

    20 The informal meaning of the formula $P\;\textit{controls}\;F$ is `$P$ is entitled

    21 to do $F$'. Give a definition for this formula in terms of $\textit{says}$. 

    22 

    23 \item 

    24 Assume an access control logic with security levels, say top secret ({\it TS}),

    25 secret ({\it S}) and public ({\it P}), with

    26 \begin{center}

    27 $slev(\textit{P}) < slev(\textit{S}) < slev(\textit{TS})$

    28 \end{center}

    29 

    30 (a) Modify the formula

    31 \begin{center}

    32 \begin{tabular}{l}

    33 $P\;\textit{controls}\;\textit{Permitted}(O, \textit{write})$\\

    34 \end{tabular}

    35 \end{center}

    36 using security levels so that it satisfies the {\it write rule} from the {\it

    37 Bell-LaPadula} access policy. Do the same again, but satisfy the {\it write rule}

    38 from the {\it Biba} access policy.

    39 

    40 (b)Modify the formula

    41 \begin{center}

    42 \begin{tabular}{l}

    43 $P\;\textit{controls}\;\textit{Permitted}(O, \textit{read})$\\

    44 \end{tabular}

    45 \end{center}

    46 using security levels so that it satisfies the {\it read rule} from the {\it

    47 Bell-LaPadula} access policy. Do the same again, but satisfy the {\it read rule}

    48 from the {\it Biba} access policy.

    49 

    50 \item Assume two security levels $\textit{S}$ and $\textit{TS}$, which are ordered so that $slev(\textit{S}) < slev(\textit{TS})$. 

    51 Assume further the substitution rules

    52 \begin{center}

    53 \begin{tabular}{c}

    54 $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$

    55 \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline

    56 $\Gamma \vdash slev(P) < slev(Q)$

    57 \end{tabular}

    58 \end{center}

    59 

    60 \begin{center}

    61 \begin{tabular}{c}

    62 $\Gamma \vdash slev(P) = l$ \hspace{4mm} $\Gamma \vdash slev(Q) = l$\\\hline

    63 $\Gamma \vdash slev(P) = slev(Q)$

    64 \end{tabular}

    65 \end{center}

    66 

    67 Let $\Gamma$ be the set containing the following six formulas

    68 \begin{center}

    69 \begin{tabular}{l}

    70 \\

    71 $slev(\textit{S}) < slev(\textit{TS})$\smallskip\\

    72 $slev(\textit{Agent}) = \textit{TS}$\smallskip\\

    73 $slev(\textit{File}_1) = \textit{S}$\smallskip\\

    74 $slev(\textit{File}_2) = \textit{TS}$\smallskip\\

    75 $\forall O.\;slev(O) < slev(\textit{Agent}) \Rightarrow 

    76 (\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\smallskip\\

    77 $\forall O.\;slev(O) = slev(\textit{Agent}) \Rightarrow 

    78 (\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\\

    79 \\

    80 \end{tabular}

    81 \end{center}

    82 Using the inference rules of access-control logic and the substitution rules shown above,

    83 give proofs for the two judgements

    84 \begin{center}

    85 \begin{tabular}{l}

    86 $\Gamma \vdash

    87 (\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_1,

    88 \textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_1, \textit{read})$\smallskip\\

    89 $\Gamma \vdash

    90 (\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_2,

    91 \textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_2, \textit{read})$\\

    92 \end{tabular}

    93 \end{center}

    94 

    95 \end{enumerate}

    96 \end{document}

    97 

    98 %%% Local Variables: 

    99 %%% mode: latex

   100 %%% TeX-master: t

   101 %%% End: