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 (Removed) Was already used in HW 5

    20 

    21 \item 

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

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

    24 \begin{center}

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

    26 \end{center}

    27 

    28 (a) Modify the formula

    29 \begin{center}

    30 \begin{tabular}{l}

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

    32 \end{tabular}

    33 \end{center}

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

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

    36 from the {\it Biba} access policy.

    37 

    38 (b)Modify the formula

    39 \begin{center}

    40 \begin{tabular}{l}

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

    42 \end{tabular}

    43 \end{center}

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

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

    46 from the {\it Biba} access policy.

    47 

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

    49 Assume further the substitution rules

    50 \begin{center}

    51 \begin{tabular}{c}

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

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

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

    55 \end{tabular}

    56 \end{center}

    57 

    58 \begin{center}

    59 \begin{tabular}{c}

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

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

    62 \end{tabular}

    63 \end{center}

    64 

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

    66 \begin{center}

    67 \begin{tabular}{l}

    68 \\

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

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

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

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

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

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

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

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

    77 \\

    78 \end{tabular}

    79 \end{center}

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

    81 give proofs for the two judgements

    82 \begin{center}

    83 \begin{tabular}{l}

    84 $\Gamma \vdash

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

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

    87 $\Gamma \vdash

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

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

    90 \end{tabular}

    91 \end{center}

    92 

    93 \end{enumerate}

    94 \end{document}

    95 

    96 %%% Local Variables: 

    97 %%% mode: latex

    98 %%% TeX-master: t

    99 %%% End: