Example: Connection Spoofing

concept Connection_Spoofing

requires

Trusted_Partner: TP

Network_DOS: ND

SeqNumProbe: SNP

SpoofedPacketSend: SPS

where

ND.hosts includes TP.host

SPS.source is SPS.target

active(ND) while active(SPS)

not ND.hosts includes SPS.true_src

not ND.hosts includes SPS.target

report

assert Connection_Spoofing

(dest <- SPS.target)

(source <- SPS.source)

(true_src <- SPS.true_src)

(start_time <- SPS.time)

(end_time <- SPS.time)

end.