The　Wide-Mouth　Frog　protocol　is　a　computer　network　authentication　protocol　commonly　used　over　insecure　networks.　It　facilitates　communication　between　parties　over　the　network　to　verify　each　other＇s　identity,　aiding　in　the　prevention　of　replay　attacks　or　eavesdropping,　and　offering　detection　of　any　alterations　while　preventing　any　unauthorized　readings.　To　ensure　the　secure　exchange　of　session　keys　by　a　trusted　third　party　among　communication　participants,　the　article　executes　a　formal　theoretical　verification　of　this　communication　process.　Through　an　abstraction　analysis　of　the　random　session　key　distribution　mechanism　based　on　a　trusted　platform,　an　abstract　model　is　established,　detailing　the　states　of　each　participating　entity　within　the　model　and　the　operational　semantics　of　state　transitions.　By　constructing　a　structured　operational　semantics　parallel　computation　model　of　the　Wide-Mouth　Frog　protocol　and　employing　the　APTC　axiomatic　system　for　the　formal　verification　of　the　protocol＇s　state　transitions,　rigorous　theoretical　deductions　indicate　that　the　protocol　exhibits　the　expected　external　behavior,　providing　theoretical　support　for　the　effectiveness　of　the　Wide-Mouth　Frog　protocol.