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”
)