Information Technology Reference
In-Depth Information
Algorithm 1. S-TLC algorithm
Comment: Initialization phase
G← Ø, U F
, U B
S ←{s i | s i Init}
For each s ∈ S
if s Invariant then error, break
if s Constraint then Append ( G, s n , s null ) , Label ( G, s n ) ← s c
if s EvidenceState then Append ( U B , s ) else Append ( U F , s )
Comment: Forward chaining phase
While U F
do
=
s ← tail ( U F )
T ←{t i | (( s, t i ) satisfies the S-TLA + action Next ) ∧ t Constraint}
For each t ∈ T
if t Invariant then error, break
if x
∈G/ t n = x
then Append ( G, t n , t n s n ) , Label ( G, t n ) ← t c
if t EvidenceState then Append ( U B , t ) else Append ( U F , t )
do
if ( ∃ x
∈G/ t n = x ) and t c ⊆ Label ( G, x ) then Join ( G, x s n )
do
if (
x
∈G/ t n = x ) and t c
Label (
G, x )
Label ( G, x ) ← Label ( G, x ) ∪ t c
Delete any superset of hypotheses from Label(
G
, x )
then
if t c ∈ Label ( G, x )
then Join ( G, t n s n )
if t EvidenceState then Append ( U B , t ) else Append ( U F , t )
Comment: Backward chaining phase
While U B
=
t ← tail ( U B )
S ←{s i | (( s i , t ) satisfies the S-TLA + action Next ) ( s i Invariant, Constraint )
( s EvidenceState ) }
For each s ∈ S
if x
∈G/ s n = x
Append ( G, s n , t n
s n )
then
Label ( G, s n ) ← s c
Append ( U B , s )
do
∈G/ s n = x ) and s c ⊆ Label ( G, x ) then Join ( G, x s n )
Append ( U B , s )
do
if ( ∃ x
if ( ∃ x
∈G/ s n = x ) and s c
Label ( G, x )
Label ( G, x ) ← Label ( G, x ) ∪ s c
Delete any superset of hypotheses from Label( G, x )
if s c
then
∈ Label ( G, x ) then Join ( G, t n
s n ) , Append ( U B , s )
- O BrForce : Hypothesizing that the algorithm used to hash the account's
passwords is weak, a user reads the file containing the password hashes and
brute-forces the root password off-line (outside the current system). It suc-
ceeds thus in escalating its privilege.
OffBrforce
=
roothas = “pwdhashcomp”
localpr =2
localpr =1
log = Append ( log,
“root” , “logon”
)
Search WWH ::




Custom Search