Invariant Negation (I - Q)
The attack changes the state name: state-name ? S0
“Request” buffer overflow: buffer-size(request) > maximum-buffer-size
Denial of Service Attack: used > 7 or used ɟ --> not-grant or number-of(grant) > used + number-of(release)
Faking a release: number(release) > number-of(grant)