2  Asymmetric  Encryption (25 marks)

In the following, we describe a simple description of an asymmetric encryption mechanism.  The idea is to represent encryption and decryption with table lookups.  To this end, three types of tables are used:

M1 is just a sequence of N elements and contains a random permutation of all integers between 1 and N.  For example m1 = (4, 3, 2, 5, 1) could be an example for N = 5.  It is used to construct a public key from a private key.  For example, if we assume that our private key is 2, then the corresponding public key, according to our example table m1, is given by m1(2) = 3.

M2 is an N × N matrix such that each row represents a random permutation of all integers between 1 and N. For example, for N = 5 we may have:

3   1   2   5    4

1    4    3   2   5

m2 = 4    5    2    3   1

3    2   1   4   5

2   3   5   1    4

It is used for encryption.   For example,  to encrypt 3 using our table m2 and key 2, we get m2(2, 3) = 3.

M3 is an N×N matrix such that each column represents a random permutation of all integers between 1 and N. It is used for decryption.

The tables must be constructed in a way such that for all k and p, with 1 ≤ k, p ≤ N the following

M3(M2(M1(k), p), k) = p                                                        (1)

2.1 Tasks

T2.1 Construct an example of M1, M2, and M3 for N = 5. Hint: first, randomly create M1 and M2 and then construct M3 such that property Eq. (1) holds.

T2.2 Encrypt the number 3 and then decrypt it again.

T2.3 Is the scheme secure? Explain why/why not.

T2.4 Implement the key generation scheme in Python3.  It should be called myPKE and take one input parameter which represents N.  It should then generate three random tables m1, m2, and m3 which satisfy Eq. 1. For example:

3  Protocol Verification  (25 marks)

Consider the following protocol where X ⟪M⟫ denotes a message M digitally signed by agent X:

The aim of the protocol is to establish authentication between two agents.  In particular, at the end of the protocol, agent B needs to be sure that nonce NA  was indeed send by agent A and also not replayed by someone else.

3.1 Tasks

T3.1 Formalize the protocol in OFMC.

T3.2 State the security property required and formalize it as a goal in OFMC.

T3.3 The protocol does not meet its goal. Provide a counterexample.

T3.4 One simple fix is to encrypt all the messages.  Provide an alternative fix of the protocol and verify in OFMC that the property now holds.

4  Access Control  (25 marks)

For this exercise you should implement a tool in Python3 to validate properties of a given Bell- LaPadula configuration. To this end you should complete the template file blpcheck.py provided on the ELE page.

The system should work for a fixed set of subjects, objects, security levels, and categories:

.  Subjects: Alice (A), Bob (B), Charlie (C)

.  Objects: Document 1 (1), Document 2 (2), Document 3 (3)

.  Security levels: low (l), high (h)

.  Categories: A, B, and C

The objects are assumed to require the following security levels:

.  Document 1: low for categories A and B

.  Document 2: high for category C

.  Document 3: high for category B

Subject-specific configurations are given in text files alice.txt, bob.txt, and charlie.txt. Each file contains the following information for the corresponding subject:

.  The first row contains the access rights for the documents.

.  The second row contains the maximum security level and corresponding categories.

.  The third row contains the current security level and corresponding categories.

For example, a configuration file in which Alice has

. write rights for Document 1, no rights for Document 2, and append rights for Document 3

.  a maximum security level of high for categories A and B

.  a current security level of low for category A

looks as follows:

Listing 1: alice.txt

The currently executed rights are provided as command line parameters.  The tool should output whether the model satisfies the Simple security condition, the star property, and/or the discretionary security property.

Below are a few examples of the input format