Arena—Leaking Secrets (2019)

This page outlines how input and output works specifically for the arena used in Leaking Secrets (Ricker, Marchand, & Keroglou, 2019).

Input Specification

In order to create an arena as specified in Leaking Secrets, the default automaton input is necessary (click here for details). Note the following:

• "controllable" should be a list of three empty lists (it will be ignored for the output, because ultimately, the controller can choose a control policy which is any subset of the events)
• "observable" should have three arrays inside of it, representing the controller's, first agent's, and second agent's view, respectively. The controller's view must be a superset of the agents' views.

"observable": [
    ["a", "b", "c", "d"],
    ["a", "b", "c"],
    ["a", "b", "d"]
]

• "attacker" is the observable alphabet for the controller that will be working with the system. This is a misnomer, but it makes the definition different from other possible inputs.
• "marked" should have three arrays inside of it, representing the controller's, first, and second agent's secrets, respectively. The controller has no secret in this paper, so this should be an empty list. Note that the first agent would be looking to identify when the system is in a subset of the final array and the second agent would be looking to identify when the system is in a subset of the second array.

"marked": [
    [],
    ["q1", "q2", "q3"],
    ["q4", "q5"]
]

Example Input

{
    "states": {
        "all": ["q1", "q2", "q3", "q4"],
        "initial": ["q1"],
        "marked": [
            [],
            ["q2"],
            ["q3", "q4"]
        ],
        "bad": []
    },
    "events": {
        "all": ["a", "b"],
        "controllable": [
            ["a", "b"],
            ["a"],
            ["b"]
        ],
        "observable": [
            ["a", "b"],
            ["a"],
            ["b"]
        ]
    },
    "transitions": {
        "all": {
            "q1->a": ["q2"],
            "q1->b": ["q3"],
            "q3->a": ["q4"]
        },
        "bad": {}
    }
}

Arena Output Format

In addition to the regular pieces in the input format for an automaton, there is also a section within states for v1 and v2, which are the two state sets of the arena (states held in either of them are also present in all). This is not part of the input format; it is simply extra output information.

Furthermore, the transitions section also has v1 and v2 sections for the transitions from states in the two state sets, respectively (transitions held in either of them are also present in all).

All bad states will be in the list bad.

Example Output

{
    "states": {
        "all": [],
        "v1": [],
        "v2": [],
        "initial": [],
        "marked": [
            []
        ],
        "bad": []
    },
    "events": {
        "all": [],
        "controllable": [
            []
        ],
        "observable": [
            []
        ]
    },
    "transitions": {
        "all": {},
        "v1": {},
        "v2": {},
        "bad": {}
    }
}