Formal Model, AVT, Alice and Bob

Question 1

What is the goal of a formal model?

Answer 1

The goal of a formal model is to enable the use of a formal language so that a formal proof can be conducted
to ensure that system requirements meet desired security properties.

Question 2

What is an Automated Verification Tool?

Answer 2

An AVT is a tool that takes in a protocol and security properties, and analyses the protocol to establish
whether it satisfies the security properties.

Question 3

Why are AVT’s initially undecidable?

Answer 3

They are undecidable due to inifinite state space of the protocol. Essentially, we can’t test the protocol against
all the infinite possibilities.

Question 4

Define the Halting Problem…

Answer 4

The Halting Problem is the problem that a program that takes a program and input as arguments is not computable since it’s impossible to write a program that decides termination for all other programs.

Question 5

How can we make an Automated Verification Tool semi-decidable? Why is this needed?

Answer 5

AVT can be made semi-decidable by ensuring that we implement finite testing boundaries for all protocols that are input into the tool. Essentially, selecting a subset of the infinite state space for testing.

Question 6

What two things can we assume if our protocol passes the AVT analysis?

Answer 6

If our protocol passes the AVT. We assume it’s sufficient, or the tool is not intelligent enough to identify
flaws.

Question 7

What is OFMC?

Answer 7

OFMC is a semi-decidable AVT.

Question 8

What are the 5 components of Alice and Bob Syntax?

Answer 8

Protocol Name, Types, Knowledge, Actions, Goals.

Question 9

How can we formalise Alice and Bob Syntax?

Answer 9

By separating roles into isolated sub-components.