Research on formal description and verification of automated trust negotiation

First, a unified ATN formal framework was presented, into which typical negotiation strategies could be reduced. Second, the formal verification of ATN was defined based on the formal framework. The objectives and procedures of the formal verification of ATN were described. Third, several typical negotiation strategies were discussed, and the computational complexity of the corresponding verification problems was shown, several conclusions had been obtained. Last, the formal verification of ATN was implemented by using logic programming and model checking methods. The experimental results show that the number of rules is a crucial factor in determining the runtime. Both logic programming and model checking are efficient when the number of transition rules is small, and logic programming does not scale as well as model checking.