With the development of science and technology, computers have brought many changes to our life. For artistic design creation, the use of computer aided design can not only break through the traditional form of expression, more importantly, it can liberate our design thinking. Computer in visual communication, environmental design, animation and industrial modeling and other fields, has become an indispensable performance tool. Computer aided design as a new design tool, it broke the original design form, compared with the traditional technique of expression to its visual effect is distinct, picture abound change simple, accurate and fast operation, easy to modify and so on a series of advantages are obvious, that is why by computer-generated performance figure has a wide range of generally accepted by people in the area, in cultivating talents of higher learning design, computer aided design course has become an important part of art design teaching course system, for art design major students to master relevant professional auxiliary software has become an essential skill.3DS MAX aided design can provide powerful real-time 3 d modeling, rendering and animation design, and other functions, it has been widely used in film and television, games, multimedia production, advertising, architecture, industrial design and engineering visual field, as a design student engaged in film and television media, advertising design and architectural design in the future, etc. At the same time, industrial design, architectural design, environmental art design, animation design and other art design related majors in colleges and universities have listed “computer Aided Design - 3DS MAX” as a compulsory course, and its teaching reform is attracting more and more attention.

Protocol security in a composition protocol environment has always been an open problem in the field of formal analysis and verification of security protocols. As a well-known tool to analyze and verify the logical consistency of concurrent systems, SPIN (Simple Promela Interpreter) has been widely used in the analysis and verification of the security of a single protocol. There is no special research on the verification of protocol security in a composition protocol environment. To solve this problem, firstly, a formal analysis method for composition protocol based on SPIN is proposed, and a formal description of protocol operation semantics is given. Then the attacker model is formalized, and a message specification method based on field detection and component recognition is presented to alleviate the state explosion problem. Finally, the NSB protocol and the NSL protocol are used as examples for compositional analysis. It is demonstrated that the proposed method can effectively verify the security of the protocol in a composition protocol environment and enhance the efficiency of composition protocol verification.

Ultralightweight mutual authentication protocols (UMAP) of Radio frequency identification (RFID) systems have attracted much attention from researchers. Many studies reveal that most of UMAP suffer malicious attack. To improve security of UMAP, formal analysis is performed with Simple promela interpreter (SPIN). Two typical UMAPs, which are RCIA and RAPP, are selected as our case study. A protocol abstract modeling method is presented to make UMAP can be formalized simply. Using SPIN, verification results show that RCIA and RAPP are both vulnerable against desynchronization attack. A Generalized model of UMAP (G-UMAP) and a general patching scheme are presented for resisting the attack. To validate the patching scheme, formal verification is then performed for the improved protocol. SPIN verification shows that the improved RCIA and RAPP both gain higher security. The above proposed modeling method has great significance for similar UMAP analyzing, and the proposed patching scheme is proved to be practical and reliable.

The verification of security protocols is an important basis for network security. Now, some security protocols add timestamps to messages to defend against replay attacks by network intruders. Therefore, verifying the security properties of protocols with timestamps is of great significance to ensure network security. However, previous formal analysis method of such protocols often extracted timestamps into random numbers in order to simplify the model before modeling and verification, which probably cause time-dependent security properties that are ignored. To solve this problem, a method for verifying security protocols with timestamps using model checking technique is proposed in this paper. To preserve the time-dependent properties of the protocol, Promela (process meta language) is utilized to define global clock representing the protocol system time, timer representing message transmission time, and the clock function representing the passage of time; in addition, a mechanism for checking timestamps in messages is built using Promela. To mitigate state space explosion in model checking, we propose a vulnerable channel priority method of using Promela to build intruder model. We take the famous WMF protocol as an example by modeling it with Promela and verifying it with model checker SPIN (Simple Promela Interpreter), and we have successfully found two attacks in the protocol. The results of our work can make some security schemes based on WMF protocol used in the Internet of things or other fields get security alerts. The results also show that our method is effective, and it can provide a direction for the analysis of other security protocols with timestamp in many fields.

Nowadays, more and more new cryptographic protocols are emerging, and the security analysis of emerging cryptographic protocols is increasingly important. Logic of events is an axiomatic method based on theorem proving, it is designed around a message automation with actions for possible protocol steps, it figured out types of information transmitted in the protocols and also presented novel proof rules and mechanism. However, with the emergence of various cryptographic protocols, logic of events lacks corresponding axioms and rules in the process of proving certain cryptographic protocols, so it needs further extension. Based on the logical framework of protocol composition logic, this paper presents a refined theory of logic of events called LoET-E, in which the novel rules about the freshness of nonces, the event attributes of messages and the states of predicate is presented, the concepts of Fresh, Gen and FirstSend is introduced, the definition of has and the honesty axiom of LoET is extended. The refined theory can guarantee the correctness, integrity and validity of the original axioms, ensure the consistency of event classes and basic sequences in the proof process, reduce the complexity and redundancy in the protocol analysis process, and, most importantly, extend the provable range of cryptographic protocols.