Modeling and Testing of Radius Protocol Base on TLA
Wan Liang · International Conference on Mechanic Automation and Control Engineering · 2012
Formal methods use mathematic and logic method to describe and validate the system. Leslie Lamport proposed the theory of Temporal Logic of Action (TLA), which can express model program and logical formulas in one page at the same time. AAA protocol refers to Authentication, Authorization, Accounting, Using various types of network resources needs the management of AAA protocol, and Radius protocol is the most widely used AAA protocol. So the security of it is very essential. To detect loopholes of the protocol based on TLA we take the following method. Created the roles for it, especially including intruder, then specified the actions of the roles. And set the environment parameters for it, then wrote the program for it, which included the model of the protocol and the detected properties of it, and then repeatedly checking and modifying the program. The results show the security loopholes of the protocol and the method is effective.