Home

Welcome to the DESwiz wiki! Find specifications for how input should be formatted, as well as other documentation, in the right-hand sidebar.

General Layout of DESwiz

The DESwiz command-line interface is designed to easily import JSON files of finite state automata (labelled transition systems) and perform operations on them. There are a few main tasks you can perform using the program:

• Open an automaton already saved as a JSON file.
• List all automata already read into the program.
• Perform operations on automata already opened.
• Save automata which have been created.
• Close automata no longer needed.
• Visualize automata opened in the program.
• Change settings, including visualization settings.

Most time spent in the application is done in the operations section.

Operations for Automata

By default, the result of any operation is visualized after it is computed and given a name. Subsequently, the resulting automaton is available as a separate automaton for use in the program. It is not saved automatically; use the save function to store the results.

Any operations that require an observable alphabet to perform the operation, such as performing the determinization with respect to an attacker's alphabet, requests the alphabet's index from the user. The 0th index is the global controller's observable alphabet and remaining are the individual agents' observable alphabets, as specified in the input JSON file provided by the user.

• Determinization: This operation takes in a single automaton which will be determinized. It also takes the index of the observer's alphabet to determinize with. That is, any event not in the observer's alphabet is treated as a silent transition. The resulting automaton has the same language as the original, projected onto the alphabet selected, and it is deterministic.
• Check current state opacity: This operation checks if a single automaton is current state opaque with respect to an observable alphabet. It does this by determinizing the system with respect to the alphabet and checking if any states are a subset of the marked states with respect to another agent. That is, opacity might hold if there are states that are a subset of the observer's secret state set (if we chose alphabet index 0, then this is the index 0 marked state set). However, it will not hold if there is a state that is a subset of any other agent's secret state set (such as the index 1 or 2 marked state set).
  • Note that marked states are assumed to indicate secret states, not final states, with this operation, as with all other operations in this program.
• Union: This is an operation sometimes called the synchronous product or parallel composition of at least two automata. The result synchronizes on pairwise shared events between input automata and interleaves private transitions which are not shared.
• Product: Also called the intersection, this operations composes a system from at least two automata. It synchronizes on shared events; an event is only permitted if it is allowed in all input automata. Private events are always disabled.
• Accessible: This operation prunes off all states which are not accessible from the initial state. That is, it parses through the input automaton and keeps only portions which have a string originating from the initial state.
• Coaccessible: This operation creates an automaton which only retains states that ultimately lead to a marked state. The accessible operation is implicitly called in a call to this operation to avoid having a large number of inaccessible states. This is useful for building leakage automata.
• Leakage automaton: This generates an automaton that only keeps paths which violate opacity of agent 2's secret from the perspective of agent 1. This is done by determinizing the automaton with respect to agent 1's alphabet, identifying states that are a subset of the secret states of agent 2, and performing the coaccessible operation on the result. Both agent 1 and agent 2 must be provided to perform the operation, and they should both be specified in the input text file.

Operations for Leaking Secrets (2019 paper)

These operations are implementations of algorithms in Leaking Secrets.

• Build arena: This creates a game-theory style arena as specified in the paper. There are two types of states. The first is a state where the system controller can make a control decision, with edges representing valid control decisions which are possible. The second is a state where the system performs one of the allowed actions (these states are augmented with the control decision taken as a part of the state). States in the system are tuples including:
  • The current state of the system
  • The current state estimate of the global controller
  • The current state estimate of each agent
  • The control decision taken (if it is a type-2 state, described above)
• Build attractor: This marks more states as bad by declaring type-1 states as bad if all control actions lead to a bad state and type-2 states as bad if they have a transition to a bad state.
• Build pruned arena: This gets the arena with the supremal controllable sublanguage that avoids all bad states. That is, any transition going to a bad state is disabled.
  • This assumes that the arena's attractor is being used! You should not directly give an arena to this algorithm, as it will not give the correct result. The attractor must be built beforehand.