This　paper　introduces　a　new　methodology　that　uses　knowledge　structures,　a　specific　form　of　Kripke　semantics　for　epistemic　logic,　to　analyze　communication　protocols　over　hostile　networks.　The　paper　particularly　focuses　on　automatic　verification　of　authentication　protocols.　Our　approach　is　based　on　the　actual　definitions　of　a　protocol,　not　on　some　difficult-to-establish　justifications.　The　proposed　methodology　is　different　from　many　previous　approaches　to　automatic　verification　of　security　protocols　in　that　it　is　justification-oriented　instead　of　falsification-oriented,　i.e.,　finding　bugs　in　a　protocol.　The　main　idea　is　based　on　observations:　separating　a　principal　executing　a　run　of　protocol　from　the　role　in　the　protocol,　and　inferring　a　principal＇s　knowledge　from　the　local　observations　of　the　principal.　And　we　show　analytically　and　empirically　that　this　model　can　be　easily　reduced　to　Satisfiability　(SAT)　problem　and　efficiently　implemented　by　a　modern　SAT　solver.