tailieunhanh - Cryptographic Security Architecture: Design and Verification phần 6

Điều này được sử dụng cho thông tin trạng thái khi đối tượng đang trong tình trạng thấp không còn có bất kỳ ý nghĩa khi nó đã được di chuyển vào tình trạng cao, ví dụ, các chi tiết của một khóa là cần thiết để di chuyển đối tượng vào cao nhà nước. Read-only truy cập trong trạng thái cao, không có quyền truy cập trong trạng thái thấp. | 142 4 Verification Techniques particular order. This problem arose due to the particular Weltanschauung of the formal specification language rather than any error in the specification or implementation itself. In the analysis of the Needham-Schroeder public-key protocol mentioned earlier the NRL protocol analyser was able to locate problems that had not been found by the FDR model checker because the model checker took a CSP specification and worked forwards while the NRL analyser took a specification of state transitions and worked backwards and because the model checker couldn t verify any properties that involved an unbounded number of executions of the protocol whereas the analyser could. This allowed it to detect odd boundary conditions such as one where the two participants in the protocol were one and the same 114 . The use of FDR to find weaknesses in a protocol that was previously thought to be secure triggered a wave of other analyses. These included the use of the Isabelle theorem prover 120 the Brutus model checker with the same properties and limitations as FDR but using various reduction techniques to try to combat the state-space explosion that is experienced by model checkers 121 the Murọ model checker and typography stress tester 122 and the Athena model checker combined with a new modelling technique called the strand space model which attempts to work around the state space explosion problem and restrictions on the number of principals although not the number of protocol runs that beset traditional model checkers 123 124 125 some of the other model checkers run out of steam once three or four principals participate . These further analyses that confirmed the findings of the initial work are an example of the analysis technique being a social process that serves to increase our confidence in the object being examined something that is examined in more detail in the next section. Credibility of Formal Methods From a mathematical point of view