We give the adversary the power to mount a chosen message attack, namely the attacker can request the signature on any message of his choice. Even with such power, the adversary should not be able to create an existential forgery, namely the attacker cannot output a valid message-signature pair \((m, \omega)\) for some new message \(m\).
Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:
The challenger runs \((pk, sk) \leftarrow \mathcal{G}()\) (private signing key, public verifying key) and sends \(pk\) to \(\mathcal{A}\).
Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:
\(\mathcal{A}\) queries the challenger several times. For \(i = 1, 2, \dots\), the \(i^{th}\) signing query is a message \(m_i \in \mathcal{M}\). Given \(m_i\), the challenger computes \(\sigma_i \leftarrow \mathcal{S}(sk, m_i)\), and then gives \(\sigma_i\) to \(\mathcal{A}\).
Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:
Eventually \(\mathcal{A}\) outputs a candidate forgery pair \((m, \sigma) \in \mathcal{M} \times \Sigma\).
Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:
We say that the adversary wins the game if the following two conditions hold:
\[
\mathcal{V}(pk, m, \sigma) = \text{accept}
\]
Techniques
Define the scope and depth of analysis.
Gain a visual understanding of what you’re threat modeling.
The traffic light property is the set of all sequences over precisely the states {"GREEN_", "YELLOW", "RED___"} such that the only state succeeding "GREEN_" is "YELLOW" and the only state succeeding "YELLOW" is "RED___" and the only state succeeding "RED___" is "GREEN_".
Today
✓ Threat and Threat Models
✓ (Trace) Properties
Kripke Structures
Linear Temporal Logic
Büchi Automata
DFAs
Safety & Liveness
CIA Triad
Model Checking
A Kripke Structure is a tuple that models a state machine.
Recall:
A state machine is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time.
Exactly one!
Model Checking
A Kripke Structure is a tuple {S, …} that models a state machine.
S is a finite set of states
Kripke structures only work for finite state machines
For the sake of this class, we can imagine infinite states if needed.
Model Checking
A Kripke Structure is a tuple {S, …} that models a state machine.
For a traffic light, S is: {"GREEN_", "YELLOW", "RED___"}
For a Bitcoin, it is perhaps the current owner.
Many possible, but finite, number of owners.
Model Checking
A Kripke Structure is a tuple {S, I, …} that models a state machine.
I is a subset of S, we denote this I ⊂ S
Any state in I must be a state in S
There may be states in S that are not in I
These are the possible initial states of the state machine.
Model Checking
A Kripke Structure is a tuple {S, I, …} that models a state machine.
For a traffic light, I = S{"GREEN_", "YELLOW", "RED___"}
For a Bitcoin, the initial state is Satoshi Nakamoto’s public key.
Model Checking
A Kripke Structure is a tuple {S, I, …} that models a state machine.
S is a finite set of states
I ⊂ S is the set of initial states.
Model Checking
A Kripke Structure is a tuple {S, I, R, …} that models a state machine.
R is a transition relation over S, we denote this R ⊂ S × S
This just means R says whether one state may be transitioned to from another.
Same as graph edges (if we take S to be nodes)
Model Checking
BONUS/CHALLENGE:R is left-total.
Note
A binary relation R ⊂ S × S is left-total if for all elements s of S there exists some ordered pair in R such that the first element of the ordered pair is s.
R ⊂ S × S is left-total ≔ ∀ s1 ∈ S, ∃ s2 ∈ S such that (s1,s2) ∈ R
Model Checking
A Kripke Structure is a tuple {S, I, R, …} that models a state machine.
A formal characterization for safety prop- erties and liveness properties is given in terms of the structure of the Buchi automaton that specifies the property. The characterizations permit a prop- erty to be decomposed into a safety property and a liveness property whose conjunction is the original.
Traffic Light
Büchi traffic light (traffic lights don’t have to stop someday, so not DFAs)
Safety
“Bad thing won’t happen”
If a Büchi Automata is a safety property…
If the bad things happens, the system is unrecoverable.
Therefore, any failures result from “falling off” the diagram.
Therefore, all states are accepting states (no failures based on ending).
Safety
The unsafe thing is “green to red”
Accepting States
These should, properly, be denoted with double circles (as they accept)
Closure
The closure of Büchi Automaton given by A ≔ {Q, Σ, δ, q0, F } is cl(A) ≔ {Q, Σ, δ, q0, Q }.
That is, cl(A) is equivalent to A if the set of accepting states F is expanded to include all of the states of A
That is, all circles are double circles.
Safety
A safety property is a property given by a Büchi Automaton A ≔ {Q, Σ, δ, q0, F } such that all traces accepted by A are also accepted by its cl(A) ≔ {Q, Σ, δ, q0, Q }.
We do not require that Q = F, just that the accepted traces are the same.
Safety
This means, we can develop safety properties from arrows (edges), or from δ
Traffic lights must not allow \(R\) immediately after \(G\)?
No problem, make a state “last was \(G\)”
Have no defined outgoing edges labeled \(R\)
Wait…
LTL
That’s just LTL
GXred\(\implies \neg\)green
G\(\neg\)green\(\lor\)\(\neg\)Xred
LTL and Büchi automata are equivalent
Proof left as an exercise to the student.
Possibly the most interest proof of all time.
Liveness
“Good thing eventually” e.g. F_good_
If a Büchi Automata is a liveness property…
No matter what happens, the system is recoverable.
Therefore, any failures result from not reaching accepting states.
Therefore, all states should have outgoing edges covering all letters of the trace alphabet.
Liveness
I’d argue a light must be green eventually.
Liveness
The closure of Büchi Automaton given by A ≔ {Q, Σ, δ, q0, F } is cl(A) ≔ {Q, Σ, δ, q0, Q }.
That is, cl(A) is equivalent to A if the set of accepting states F is expanded to include all of the states of A
Liveness
A liveness property is a property given by a Büchi Automaton A ≔ {Q, Σ, δ, q0, F } such that cl(A) ≔ {Q, Σ, δ, q0, Q } accepts all possible traces in Σω.
Liveness
This means, we can study liveness properties by adding a self-loop with negation of all other outgoing edges to each automaton state.
This isn’t great.
It is more common to add a “trap state” which captures these transitions but does not accept.
Intersection
We recall set theoretic intersection… \[
\forall e : e \in A \lor e \in B \implies e \in A \cup B
\]
What are these automata accepting again?
Note
A trace property is a set of traces.
Claim
Given a Buchi automaton m, it is not difficult to construct Buchi automata Safe(m) and Live(m) such that Safe(m) specifies a safety property, Live(m) specifies a liveness property, and the property specified by m is the intersection of those specified by Safe(m) and Live(m).
Example
Consider the following Büchi automata over the alphabet of lower case letters:
The intersection represents elements in both Safe(m) and Live(m)…
Safe()
We recall the definition of safety.
Safe(m) excludes the “bad thing” for a Buchi automaton, which is attempting an undefined transition, because if such a “bad thing” happens at any point in the trace, the Buchi automaton will not accept that trace.
Safe()
A core “nicety” of Büchi Automata is that the safety property is the closure.
Safe(m) = cl(m)
Live()
We recall the definition of liveness.
Live(m) requires the “good thing” for a Buchi automaton, which is entering an accepting state infinitely often, because we require this “good thing” to happen for trace to be accepted.
Live()
“Consider the following Büchi automata over the alphabet of lower case letters”
Live()
While safety is mostly about F, the accepting states or the double circles, liveness is mostly about Σ = {a, b, ?}, the alphabet or the possible states of the trace (NOT the states of the automata) that form the labels on arrows.
Live()
Define liveness relative to Σ.
There most be no undefined transitions (that would be safety)
So we require that any letter in Σ has a defined transition at any point in time.
