Intrusion　tolerance　is　an　emerging　network　security　technique,　which　enables　the　victim　server　systems　to　continue　offering　services　(or　degraded　services)　after　being　attacked.　A　state　transition　model　has　been　presented　to　describe　the　dynamic　behaviors　of　intrusion　tolerant　systems.　In　this　paper,　we　build　an　attack　finite　state　system　based　on　the　recent　network　attacks,　and　use　SMV,　a　model　checking　tool,　to　analyze　the　intrusion　tolerant　systems　by　the　interaction　of　the　system　model　and　the　attack　model.　The　analysis　results　demonstrate　that　not　all　types　of　attacks　can　be　mapped　to　the　system　model.　We　improve　this　state　transition　model,　whose　correctness　is　proved　by　SMV.　In　addition,　we　give　two　attack　instances　mapped　to　our　improved　model.　©　Springer-Verlag　Berlin　Heidelberg　2005.