6 \begin{document} |
6 \begin{document} |
7 |
7 |
8 \section*{Homework 6} |
8 \section*{Homework 6} |
9 |
9 |
10 \begin{enumerate} |
10 \begin{enumerate} |
11 \item Access-control logic includes formulas of the form |
11 \item Zero-knowledge protocols depend on three main properties called |
12 \begin{center} |
12 completeness, soundness and zero-knowledge. Explain what they mean? |
13 $P\;\textit{says}\;F$ |
|
14 \end{center} |
|
15 |
13 |
16 where $P$ is a principal and $F$ a formula. Give two inference rules |
14 \item Why do zero-knowledge protocols require an NP-problem as building |
17 of access-control logic involving $\textit{says}$. |
15 block? |
18 |
16 |
19 \item |
17 \item Why is it a good choice in a ZKP to flip a coin when requesting a |
20 Assume an access control logic with security levels, say top secret ({\it TS}), |
18 proof from the person who knows the secret? |
21 secret ({\it S}) and public ({\it P}), with |
19 \end{enumerate} |
22 \begin{center} |
|
23 $slev(\textit{P}) < slev(\textit{S}) < slev(\textit{TS})$ |
|
24 \end{center} |
|
25 |
20 |
26 (a) Modify the formula |
|
27 \begin{center} |
|
28 \begin{tabular}{l} |
|
29 $P\;\textit{controls}\;\textit{Permitted}(O, \textit{write})$\\ |
|
30 \end{tabular} |
|
31 \end{center} |
|
32 using security levels so that it satisfies the {\it write rule} from the {\it |
|
33 Bell-LaPadula} access policy. Do the same again, but satisfy the {\it write rule} |
|
34 from the {\it Biba} access policy. |
|
35 |
|
36 (b)Modify the formula |
|
37 \begin{center} |
|
38 \begin{tabular}{l} |
|
39 $P\;\textit{controls}\;\textit{Permitted}(O, \textit{read})$\\ |
|
40 \end{tabular} |
|
41 \end{center} |
|
42 using security levels so that it satisfies the {\it read rule} from the {\it |
|
43 Bell-LaPadula} access policy. Do the same again, but satisfy the {\it read rule} |
|
44 from the {\it Biba} access policy. |
|
45 |
|
46 \item Assume two security levels $\textit{S}$ and $\textit{TS}$, which are ordered so that $slev(\textit{S}) < slev(\textit{TS})$. |
|
47 Assume further the substitution rules |
|
48 \begin{center} |
|
49 \begin{tabular}{c} |
|
50 $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$ |
|
51 \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline |
|
52 $\Gamma \vdash slev(P) < slev(Q)$ |
|
53 \end{tabular} |
|
54 \end{center} |
|
55 |
|
56 \begin{center} |
|
57 \begin{tabular}{c} |
|
58 $\Gamma \vdash slev(P) = l$ \hspace{4mm} $\Gamma \vdash slev(Q) = l$\\\hline |
|
59 $\Gamma \vdash slev(P) = slev(Q)$ |
|
60 \end{tabular} |
|
61 \end{center} |
|
62 |
|
63 Let $\Gamma$ be the set containing the following six formulas |
|
64 \begin{center} |
|
65 \begin{tabular}{l} |
|
66 \\ |
|
67 $slev(\textit{S}) < slev(\textit{TS})$\smallskip\\ |
|
68 $slev(\textit{Agent}) = slev(\textit{TS})$\smallskip\\ |
|
69 $slev(\textit{File}_1) = slev(\textit{S})$\smallskip\\ |
|
70 $slev(\textit{File}_2) = slev(\textit{TS})$\smallskip\\ |
|
71 $\forall O.\;slev(O) < slev(\textit{Agent}) \Rightarrow |
|
72 (\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\smallskip\\ |
|
73 $\forall O.\;slev(O) = slev(\textit{Agent}) \Rightarrow |
|
74 (\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\\ |
|
75 \\ |
|
76 \end{tabular} |
|
77 \end{center} |
|
78 Using the inference rules of access-control logic and the substitution rules shown above, |
|
79 give proofs for the two judgements |
|
80 \begin{center} |
|
81 \begin{tabular}{l} |
|
82 $\Gamma \vdash |
|
83 (\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_1, |
|
84 \textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_1, \textit{read})$\smallskip\\ |
|
85 $\Gamma \vdash |
|
86 (\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_2, |
|
87 \textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_2, \textit{read})$\\ |
|
88 \end{tabular} |
|
89 \end{center} |
|
90 |
|
91 \end{enumerate} |
|
92 \end{document} |
21 \end{document} |
93 |
22 |
94 %%% Local Variables: |
23 %%% Local Variables: |
95 %%% mode: latex |
24 %%% mode: latex |
96 %%% TeX-master: t |
25 %%% TeX-master: t |