Formal Specification and Verification of Control Software for
`Cryptographic Equipment
`
`D. Richard Kuhn and James F. Dray
`
`National Computer Systems Laboratory
`National Institute of Standards and Technology
`Gaithersburg, Md. 20899
`
`ABSTRACT
`
`This paper describes the application of
`formal specification and verification methods to
`two
`microprocessor-based
`cryptographic
`devices: a "smart token" system that controls
`access to a network of work.stations, and a
`message authentication device implementing the
`ANSI X9.9 message authentication standard.
`Formal specification and verification were found
`to be practical, cost-effective tools for detecting
`potential security weaknesses, and helped to
`significantly strengthen the security of the access
`control system.
`
`1. Introduction
`increasingly
`systems are
`Microprocessor-based
`1be
`improved
`security.
`being used
`to provide
`improvements in security are often accomplished at the
`cost of increased complexity, as when a smart card
`microprocessor replaces a simple password system for
`network access control. Formal methods are recognized
`as an effective means of assuring the security of systems,
`and have been used
`in several military security
`applications over the past 15 years [Neumann et al., 1974;
`Tagney et al., 1977; Feiertag et al., 1977; Neuman et al.,
`1980; Young et al., 1986; Levin et al., 1989]. This paper
`reports on the application of formal methods to two
`civilian security-critical systems: the NIST Token-Based
`Access Control System (TBACS), a "smart token" 1
`system that controls access to a network of work.stations,
`and a message authentication device implementing the
`
`U.S. Government work.
`Not protected by U.S. copyright.
`
`ANSI X9.9 message authentication standard [ANSI,
`1986]. A state-based specification was prepared for the
`smart token system. The message authentication device
`specification used the notation of the Vienna Development
`Method.
`The projects were undertaken primarily as exercises
`in preparation for a larger project that is planned, but the
`results surpassed the initial goal of gaining familiarity
`with verification tools. It is noteworthy that no funding
`was available for formal methods work in either case. A
`verification
`tool, Unisys'
`Formal Development
`Methodology (FDM) [Eggert et al., 1988], was obtained at
`no cost and the formal methods work was done as time
`permitted. Even with limited time available, we found the
`effort worthwhile.
`In the smart token access control
`system, several inconsistencies were found that led to
`improved security.
`In addition, a subtle error was
`discovered that could have compromised the security of
`TBACS, had it been released A breakdown of hours and
`resources used in the access control system verification is
`given in section 2.8. The most interesting result of this
`work, beyond
`the
`increased assurance
`for TBACS
`security, is that it gives additional evidence that formal
`methods can be successfully applied to ''real world''
`problems. Formal methods are rarely used today and are
`often rejected out-of-hand as being too difficult or
`expensive. Our experience has convinced us that, at least
`for small projects, or for small portions of large systems,
`formal methods are a practical and cost-effective adjunct
`to traditional software engineering methods.
`
`2. The Token Based Access Control System
`
`2.1. System Desaiption
`The Token Based Access Control System (TBACS)
`was developed as an experimental system to replace
`traditional password based systems. Based on the TBACS
`proof-of-concept, a Smart card based Access Control
`System (SACS) that incorporates the TBACS design and
`
`I Strictly speaking, a smart token is different from a smart card, although the two terms arc often used interchangably.
`Both arc hand-carried devices containing microprocessors and memory, but there is an ISO standard for smart cards. A
`smart token is typically larger than a smart card.
`
`TH0351-7/90/0000/0032$01.00©1990 IEEE
`
`32
`
`IPR2017-00430
`UNIFIED EX1023
`
`

`
`code is now under development TBACS uses a portable
`device called a smart token to control access to the
`resources of networked computer systems. 1be TBACS
`smart token performs cryptographic authentication to
`identify the user and up to 100 computers which the user
`wishes to access.
`1be system configuration for TBACS consists of a
`of workstations
`and
`host
`computers
`number
`interconnected by a communications network. Each
`workstation on the network is connected to a reader/writer
`device, which provides the electrical interface between the
`TBACS token and the workstation. When the user inserts
`a token into the reader/writer, a program running on the
`workstation manages the authentication process by issuing
`a sequence of commands to the token and receiving the
`token's responses to these commands.
`
`2.1.1. Hardware
`1be smart token consists of a plastic carrier
`containing a microprocessor and non-volatile memory.
`The carrier has the same major dimensions as a standard
`credit card, with six recessed metallic contacts along one
`edge. 1be reader/writer connects
`to the workstation
`through a standard asynchronous serial communications
`port, eliminating the need for a custom communications
`interface.
`
`2.1.2. Software
`1be TBACS
`to a set of 17
`token responds
`commands (see Table 1), which are implemented in
`firmware stored in the token's non-volatile memory. The
`firmware code is approximately 2,600 lines of C. 1be
`sequence in which these commands are executed is
`controlled by a set of flags which are checked at the first
`step of each command. If the flags are not set correctly,
`the given command will not be executed and the token
`will return an error code.
`
`1be commands are grouped into three general
`classes: security officer (SO) commands, user/workstation
`authentication
`commands,
`and
`user/remote
`host
`authentication commands. The SO commands provide for
`the initialization of new tokens by loading host IDs,
`cryptographic keys, and PINs. The token is ready to be
`issued to the user after the SO has completed this
`The
`remaunng
`commands
`initialization
`process.
`implement the authentications required by TBACS to
`control the login process.
`
`Table 1. TBACS Commands
`Command
`Verified
`no
`yes
`yes
`yes
`yes
`yes
`yes
`yes
`yes
`yes
`no
`yes
`no
`no
`no
`no
`no
`
`Reset
`Enter SO PIN
`Authenticate SO
`Enter User PIN
`Load Key
`Authenticate Token
`Generate Challenge
`Authenticate User
`Change Token PIN
`Workstation Verify and Respond
`Output ID Table
`Host Verify and Respond
`Read Zone
`Write Zone
`Append Zone
`Call DES
`Test
`
`2.2. Authentication Processes
`For a user to gain access to computing resources on
`a network using TBACS, a series of authentications
`between the smart token, the user, and various host
`computers must be performed. TBACS selectively
`controls access to all computers on the network, including
`the user's local workstation. By taking advantage of the
`processing capabilities of the smart token, the login
`process can proceed transparently to the user while
`providing a high level of authentication. The DES
`algorithm, operating firmware, and critical data are stored
`internally on the smart token, providing a higher level of
`security than systems which use tokens only as data
`storage devices.
`
`2.2.1. User/Token Authentications
`When a user begins
`the
`login process on a
`workstation, he or she should have some means of
`determining the identity of the token. A program called
`the ''login manager'' is executed on the workstation when
`the user initiates a login, and is responsible for mediating
`the required series of authentications between the user, the
`token, and the workstation. First, the user must prove his
`or her identity to the token. The next step performed by
`the login manager is to request the token identification
`number from the token and display it on the user's screen
`for visual verification. The user can choose to either
`
`33
`
`

`
`At this point, the local rlogin manager acts primarily as a
`communications path between the token and the remote
`rlogin server. The token is provided with the host ID,
`which it uses to select the proper key for subsequent
`cryptographic operations. The steps of the three-way
`handshake are repeated between the token and the rlogin
`server on the remote host, and finally the rlogin server
`terminates and the standard rlogin process connects the
`user to the remote host.
`
`2.3. Token Deactivation
`In addition to sequence control, the TBACS token is
`capable of deactivating itself after three failed login
`attempts or when the token expiration date is reached.
`Deactivation is accomplished by deleting the internal
`token identification number, after which none of the
`authentication steps required for user login will execute.
`A token is reactivated when a security officer installs a
`new token identification number.
`
`2.4. Key Management
`When a user first enrolls on a TBACS computer
`system, the user must contact the appropriate security
`officer for that computer. The SO initializes a blank token
`by loading the following:
`the security officer's ID,
`encrypted under the security officer's PIN; the user's ID,
`encrypted under an initial user PIN; a token identification
`number; and the token expiration date.
`The SO next generates a DES key which is loaded
`onto the token. The random number generation capability
`of the security officer's token can be used to generate
`these keys. The token encrypts this key using the user's
`PIN and stores it in the key table along with the
`computer's host identification number. The host computer
`can generate this key from the user's PIN and the host
`master key as required during future login processes. As
`the DES key could be stored in the
`an alternative,
`computer's key database indexed by the user's identity.
`After receiving the token from the SO, the user may
`change the token identification number and the user PIN
`by entering the current values.
`
`The user may now enroll on another TBACS
`computer by contacting
`that computer's SO, who
`generates another DES key which is stored on the token
`and the host computer as previously described. The
`
`continue the login process or abort by simply pressing a
`key. The login manager prompts the user for his or her
`PIN/password, which is then encrypted and transmitted to
`the token along with the user ID. The token decrypts the
`user PIN and uses it as the key to encrypt the user ID. The
`result is then compared to the value stored on the token,
`and if these values match the token accepts the identity of
`the user. From this point on, TBACS uses the token to
`:remaining
`the
`represent
`the user's
`identity
`for
`authentications.
`
`2.2.2. Three-Way Handshake Protocol
`Once the previous steps have been completed, the
`token and the workstation must authenticate to each other.
`This is accomplished through a three-way handshake
`protocol which allows each party to prove that it posesses
`the same cryptographic key as the other party, without
`having to physically exchange keys [NIST, 1988]. This
`protocol worlcs as follows:
`
`1
`
`2
`
`3
`
`4
`
`Party A generates a 64-bit random number and
`transmits it to party B.
`Party B encrypts the random number using its secret
`key, generates a second random number, and
`transmits both values to party A.
`Party A decrypts the first number and verifies the
`result. Party A then encrypts the second random
`number and transmits it to party B.
`Party B decrypts and verifies the second random
`number. At this point, each party is satisfied that the
`other party posesses the same secret key.
`
`2.2.3. User/Workstation Authentications
`After the user and token authenticate to each other,
`to the workstation. To
`the token must authenticate
`perform the authentications between the workstation and
`the token, the login manager requests a random number
`from the token. The three-way handshake then proceeds
`with the token acting as party A and the workstation as
`party B. If this handshake is completed successfully, the
`login manager tenninates and the user is logged in to the
`system.
`
`2.2.4. User/Remote Bost Authentications
`At some point during a session, the user may decide
`to connect to a remote host via the network. The user
`activates an rlogin manager, which requests a table of the
`allowed TBACS hosts for this user from the token and
`displays this table in a menu format. After the user selects
`the desired remote host from this menu, the rlogin
`manager connects to an rlogin server on the remote host
`
`34
`
`

`
`TBACS token is designed so that only the SO who first
`initialized the token can delete token keys. Other security
`officers can only append keys to the token key table. 2
`In order to activate the token during a login, the user
`must supply the correct user PIN. Once activated, the
`token can be used to authenticate the user to the user's
`workstation and then to other host computers by means of
`the three-way handshake previously described.
`
`2.S. Development
`is a small but reasonably complex
`TBACS
`embedded system containing custom hardware. It was
`developed at NIST primarily as a proof-of-concept for the
`Smart card based Access Control System. Initially, a
`software simulation of TBACS was written to serve as a
`prototype. Experimentation with the prototype resulted in
`several design changes that were later incorporated into
`TBACS. 1be prototype also served as a specification for
`TBACS functions. Because of hardware requirements,
`most of the simulation code could not be used in the
`TBACS
`implementation.
`SACS,
`however,
`does
`incorporate almost all of the TBACS code. For this
`reason, the formal specification was based on the design as
`reflected in the TBACS code.
`The formal specification and verification were done
`the TBACS hardware and software had been
`after
`implemented because, as noted earlier, formal verification
`was not
`initially part of the development plan.
`Fortunately however, we were able to complete the
`verification before the implementation of the Smart card
`based Access Control System, allowing a problem
`detected in the formal verification to be corrected in the
`SACS implementation.
`
`2.6. Security Policy
`Generally accepted practice for developing trusted
`systems requires the statement of a security policy that
`describes the security properties of the system [NSA,
`1985; Tavilla, 1986; Bell, 1988]. A formal model defining
`the meaning of the security policy
`in
`terms of
`
`mathematical logic can then be constructed. Confidence is
`gained in the security of the system by showing that it
`implements the requirements of the model. When a
`formal top-level specification of the system is prepared, its
`consistency with the model can be shown by rigorous
`mathematical
`argument. Proofs of
`lower
`level
`specifications and of the code may be formal or informal,
`depending on the complexity of the system and the
`resources available. Showing the consistency of the
`model with the policy statement is necessarily an informal
`process.
`toward a
`formal model must be oriented
`A
`particular class of systems [Nessett, 1986]. For example, a
`model prepared for an operating system is not appropriate
`for expressing the security requirements for a network.
`Significant work has been done on the definition of formal
`models for multi-level secure operating systems [Bell and
`LaPadula, 1976; Feiertag et al., 1977], and for trusted
`networks [Gove, 1985; Freeman et al., 1988;]. Integrity
`models, such as those of Biba [1977], Lipner [1982], and
`Clark and Wtlson [1987) are more directly related to
`TBACS verification requirements, but even these are not
`completely appropriate, so we developed a model that is
`particular to the requirements of TBACS.
`Figure 1 summarizes the rules of operation that
`were originally defined as the security policy for TBACS,
`detailed in Dray et al. [1989] and Smid et al. [1989). 1be
`original security policy was developed informally. The
`formal specification effort was started later. Initially we
`derived mathematical statements of the assertions given in
`
`Figure 1. However, it was not immediately clear that the
`conjunction of these assertions would guarantee
`the
`security of TBACS. For a greater degree of assurance, a
`more rigorously developed model of the security policy
`was required. The goal of this model development was to
`prepare a formal statement, P , of the security policy at a
`sufficiently abstract level that its security would be clear.
`Detailed assertions, A 1, ••• , An , such as those in Figure 1,
`could then be stated and the model of TBACS functions
`shown correct with respect to these detailed assertions
`provided that A 1 & A 2 & ... & An => P . This model and
`its derivation are documented in the next section.
`
`2 Anyone can in fact append keys to the key table. This somewhat suprising feature was determined to be a reasonable
`design lradcoff. Security officers maintain control over the keys for their systems, and a user must have a valid key to ac(cid:173)
`cess a particular host. A user can append a key, but it will be of no use unless it is the conect one that is controlled by the
`security officer. An alternative to this design would be to have each security officer store an encrypted secret key on the
`token, but this would require the token to be initialized by up to l 00 security officers, since it is not known in advance
`which hosts a user will eventually need access to. Another alternative would be to have a "master key" that could be used
`by any security officer. But such a key would add little security, since a key known to over 100 people would likely be
`leaked in a short time in a civilian environment, where there arc no criminal penalties for disclosure of confidential infor(cid:173)
`mation.
`
`35
`
`

`
`1: Token commands may only be executed in legal se(cid:173)
`quences: user authorization; token authorization; works(cid:173)
`tation authorization; remote host authorization.
`2: A token deactivates itself when its expiration date is
`reached.
`3: A user must enter correct ID and PIN to be authorized:
`4: A token deactivates itself after three failed login at(cid:173)
`tempts
`5: A deactivated token will not permit login.
`6: A token allows a user access only to hosts whose ID and
`key are stored on the token.
`7: The user cannot open the token if fail limit exceeded or
`token expired.
`8: The user cannot get SO privileges.
`9: An SO must enter correct ID and PIN to be authorized:
`10: Only an SO may initialize a blank token.
`11: A PIN for a particular token may be changed only by
`an SO or by the owner of that token.
`12: After an SO has initialized a token, only this SO can
`enter the user PIN.
`13: After an SO has initialized a token, only this SO can
`reactivate the token after it has been deactivated.
`14: After an SO has initialized a token, only this SO can
`delete a key from the token.
`15: Only the SO can change the expiration date.
`
`Figure 1. Security Assertions
`
`2.7. Security Model
`1bis section describes the derivation of the formal
`statement of security policy. In summary, TBACS security
`is defined as the conjunction of the following conditions:
`1.
`Access control: Access to the network is granted
`only if the user posesses the correct PIN and a valid
`token. Ensuring
`this condition holds requires
`condition 2.
`Change control: An invalid token cannot be made
`valid by the user, only by the security officer.
`Ensuring this condition holds requires condition 3.
`
`2.
`
`3.
`
`Privilege control: A user cannot gain security
`officer privileges through manipulation of TBACS
`functions. 3
`
`2.7 .1. Terms
`The primitive terms shown in Table 2 are used. In
`the remainder of the paper, the symbols &, I . --,, =>
`represent and, or, not, implies, respectively. The notation
`x' indicates the value of variable x after a state ttansition.
`The universal quantifier is denoted by A and the
`existential quantifier by E.
`
`2.7.2. Formal Statement of Model
`
`2.7 .2.1. Access Control
`Access to the network is permitted only if the user
`possesses a PIN which encrypts the user ID to the value
`stored on the token, and the token is valid. That is,
`
`(1) access=> Epin_in(id_in)=user_pin & token_valid
`where EK(!) represents the encryption of I with key K.
`Access
`is defined as authorization of remote host,
`workstation, token, or user. 'The token is valid when the
`token has not expired and is active, the failure limit has
`not been reached, and the workstation ID is in the token's
`host table. Substituting terms for these conditions into
`
`'
`
`invariant (1) gives
`(2)
`remote_host_autbd I ws_authd I token_authd I user_authd
`=> E pin_in(id _in) = user_pin &
`today < exp_date &
`fail_log < 3 &
`token_pin '# null &
`ws_id E host_ids
`
`2.7.2.2. Change Control
`Invariant (2) must be maintained across state
`ttansitions. If the user could change the variables that
`determine if the token is valid, an invalid token could be
`made valid illegitimately. Thus for each variable in the
`definition of token_ valid, we must define the conditions
`under which its value can change: 4
`
`3 Note that this refers only to user actions within the system, and does not deal with actions that arc beyond the con1r0l
`ofTBACS, such as the user observing the security officer's PIN being entered, which is a separate concern.
`
`4 ~ th~t no ~stricti?'1 is placed on the addition of keys to the host table, as explained in Key Management, Section
`2.4. Secunty m this case 1S external to TBACS and relies on the security officers for the different hosts maintaining
`confidentiality of keys.
`
`36
`
`

`
`exp_date
`fail log
`remote_host_authd
`ws_authd
`token authd
`user_authd
`so_authd
`today
`user_pin
`ws_id
`host_ids
`token_pin
`user_pin
`
`Table 2. Primitive Tenns
`Token expiration date.
`Count of failed login attempts.
`'IIue iff remote host is authorized.
`'IIue iff wotkstation is authorized.
`True iff token is authorized.
`True iff user is authorized.
`True iff security officer is authorized.
`Today's date.
`User PIN stored on token (encrypted).
`Wotkstation ID of the wotkstation to which token is connected.
`Host IDs to which the token may be used to gain access.
`Token PIN.
`User PIN.
`
`The initial value for the user PIN can only be entered by
`the SO:
`(user_pin =null & user_pin' '#null => so_authd)
`A user PIN may be changed only by an SO or by the owner
`of that token:
`(user_pin' '# user_pin => so_authd I user_authd)
`Only the SO can change the expiration date:
`(exp_date' * exp_date => so_authd)
`The failure log is reset only after a successful login.
`(fail_log' = 0 & fail_log > 0 & fail_log < 3 =>
`user_authd)
`
`A PIN for a particular token may be changed only by an
`SO or by the owner of that token:
`
`(toke°'-pin' * token_pin
`
`user_authd)
`
`=>
`
`so_authd
`
`Only the SO can reactivate the token after it has been
`deactivated:
`(token_pin = null &
`so_authd)
`
`:t:. null =>
`
`token_pin'
`
`2.7.2.3. Privilege Control
`If it can be shown also that the user cannot obtain
`security officer privileges, the system is considered secure.
`The user cannot get SO privileges:
`user_authd =>-, so_authd
`
`2.7.3. Security Assertions
`
`More detailed assertions were developed from the
`design description. Many of these are directly derivable
`from the formal policy statement given above. Others
`
`37
`
`reflect design considerations, such as the sequencing
`requirement, assertion 1. The security model assertions
`are shown below. The FDM system notation has been
`replaced by standard first order logic notation to enhance
`readability.
`
`State Assertions
`These assertions must be true in all states.
`1: Token commands may only be executed in the sequence:
`user authorization;
`token authorization; workstation
`authorization; remote host authorization:
`(remote_host_authd => ws_authd) & (ws_authd =>
`token_authd) & (token_authd => user_autbd)
`2: A user must enter correct ID and PIN to be authorized:
`(user_authd => E pin_in(id _in) = user_pin)
`3: A token deactivates itself when its expiration date is
`reached:
`(today ~ exp_date & -, so_authd => token_pin =
`null)
`4: A token deactivates itself after three failed login
`attempts
`(fail_log ~ 3 => token_pin =null)
`5: A deactivated token will not permit login:
`(token_pin =null => -, user_authd)
`6: A token allows a user access only to hosts whose ID and
`key are stored on the token:
`(user_authd => ws_id E host_ids)
`7: The user cannot open the token if fail limit exceeded or
`token expired:
`(user_authd => fail_log < 3 & today< exp_date)
`
`

`
`8: The user cannot get SO privileges:
`(user_authd => --. so_authd)
`9: A security officer must enter correct ID and PIN to be
`authorized:
`(so_authd => E pin_in(id _in)= so_pin)
`10: Only an SO may initialize a blank token:
`/*relies on external conditions, cannot be proven*/
`
`Transition Assertions
`These assertions must be true of all transitions
`between states.
`
`11: The initial value for the user PIN can only be entered
`by the SO:
`(user__pin =null & user__pin' -::F- null => so_authd)
`12: A PIN for a particular token may be changed only by
`an SO or by the owner of that token:
`(token__pin'
`token__pin
`-:#
`user_authd)
`
`so_authd
`
`=>
`
`13: Only the SO can change the expiration date:
`(exp_date'-:# exp_ date => so_authd)
`14: A PIN for a particular token may be changed only by
`an SO or by the owner of that token:
`(token_pin'
`token__pin
`-:#
`user_authd)
`
`so_authd
`
`=>
`
`15: The failure log is reset only after a successful login.
`(fail_log' = 0 & fail_log > 0 & fail_log < 3 =>
`user_authd)
`
`16: Only the SO can reactivate the token after it has been
`deactivated:
`token__pin' * null =>
`(token__pin = null &
`so_authd)
`
`17: After an SO has initialized a token, only this SO can
`delete a key from the token:
`((E h:host_id_t (-, (h E host_ids') & h E host_ids))
`=> so_authd)
`
`2.8. Verification
`
`When the verification was started, IBACS had
`already been prototyped and built. The SACS system,
`based on IBACS, was undergoing critical design review
`during the verification effort. The verification thus served
`as an additional check on the soundness of the SACS
`design beyond the experimentation done with IBACS.
`
`level
`top
`The secmity assertions and formal
`specification (FTLS) were specified using Unisys' Formal
`Development Methodology (FDM) [Eggert et al., 1988].
`
`38
`
`FDM provides a formal language called Inajo [Scheid and
`Holtsberg, 1988] that is derived from first order logic.
`Inajo is used to represent the system as a state machine,
`specifying system states, state transitions, and security
`criteria. An interactive theorem proving tool [Schone et
`al., 1988] assists the user in showing that all transforms of
`the abstract machine meet the safety criteria. The ten
`critical functions that implement the three-way handshake
`and control functions were modeled with 297 lines (not
`including comments) oflnajo.
`The verification resulted in some cases where the
`FI'LS for a command could not be proven consistent with
`the security requirements. Such cases where the proof
`failed were the most interesting part of the verification.
`They prompted the discovery of some subtle discrepancies
`between the security requirements and the FI'LS. With
`the discrepancies would not have
`one exception,
`compromised the security of the system, although they did
`expose design changes that could strengthen system
`security. The verification effort thus served to increase
`our confidence in the security of IBACS. This section
`discusses some of the anomalies that were discovered
`
`The security officer authentication procedure had no
`check that the input date parameter is greater than today's
`date, so assertion 2 could not be shown for this procedure:
`token deactivates itself when its expiration date is
`reached:
`(today~ exp_date => token__pin =null)
`
`The SO could enter an expiration date that invalidated this
`requirement, although the user would still not be able to
`gain access in this case.
`
`A more interesting condition occurred with the
`procedure for entering the user PIN. The following
`assertion could not be satisfied:
`
`After an SO has initialized a token, only this SO can enter
`the user PIN:
`(user_pin =null & user_pin'-:# null=> so_authd)
`Proving this condition would have required assuming that
`no combination of key and data encrypted to null, i.e.:
`
`A i:id, p:pin EP (i)-:# null)
`
`which, although highly improbable, is not strictly valid.
`
`This was because a user PIN initialized to 0 could match
`the encryption of the entered user ID with the user PIN if
`Ep;n(id) = 0. The user PIN can be changed if either (the
`SO opened the token) or (the user opened the token and
`
`

`
`E Pll/JD) = stored encryption of user ID). If E p;,.(id) = 0
`and the stored encryption of user ID is 0, then the user PIN
`could be changed by user rather than just the SO.
`
`However, the checks for token expiration and deactivation
`remained in the authenticate token procedure, so only the
`following assertions could be shown:
`
`Similarly, the system was designed to deactivate a token
`by setting its token PIN to null. Since the token PIN is an
`encrypted value,
`there was a small, but non-zero,
`probability that two values would be found that encrypt to
`null. In the implementation, special flags were used to
`indicate the conditions described above, rather than using
`null values.
`
`1be user authentication procedure allowed the
`failure counter to be bumped to 3 without clearing the
`token pin after it becomes equal to 3, so the assertion
`below could not be proven for this procedure.
`
`A token deactivates itself after three failed login attempts:
`(fail_log ;;;:: 3 => token_pin = null)
`
`This occurred because the failure log was specified to be
`tested initially in the user authentication procedure but
`was not tested again after it was incremented when the
`user failed to authenticate. The token would of course be
`deactivated when the user attempted to log in again.
`
`When the SO opened
`the
`the token entering
`procedure to change the token PIN, it was possible for the
`token to be expired but still active. The requirement that
`could not be satisfied is:
`
`A token deactivates itself when its expiration date is
`reached:
`(today;;;:: exp_date => token_pin =null)
`
`The initial design called for the token authentication
`to be perfonned before the user authentication. By the
`time the fonnal specification was prepared, this had been
`changed to perfonn the user authentication first. The
`security requirements thus had assertions that the user
`could not be authenticated if the token was expired or
`deactivated:
`
`A deactivated token will not permit login:
`(token_pin =null => -, user_authd)
`
`user cannot open token if fail limit exceeded or token
`expired:
`(user_authd => fail_log < 3 & today< exp_date)
`
`(token_pin =null => --, token_authd)
`(token_authd => fail_log < 3 & today< exp_date)
`
`The design was changed to do the validation in the user
`authentication procedure.
`that could have
`One error was discovered
`If a
`compromised
`the security of TBACS.
`token
`deactivates itself because it expires or because there were
`too many unsuccessful login attempts, only the security
`officer should be able to reactivate it:
`
`After an SO has initialized a token, only this SO can
`reactivate the token after it has been deactivated:
`(token_pin = null &
`token_pin'
`f:. null =>
`so_authd)
`An error in the token PIN change procedure allowed a
`user to reactivate a token that had been deactivated as a
`result of expiration. 1be token pin change procedure
`checked that either the user or security officer bad been
`authenticated, without checking to see if the token was
`deactivated. In the original design this would have been
`acceptable, because the token was authenticated first, then
`the user. The token authentication procedure checked for
`a deactivated token and the sequence would have been
`this procedure. With
`stowed by
`the change
`to
`authenticate the user first, the token PIN change procedure
`could be invoked before the token had been authenticated.
`
`2.9. Discussion
`This section discusses the impact of the fonnal
`verification on the design and construction of TBA CS.
`
`2.9.1. Assurance/Confidence Gained
`The most significant problem discovered was the
`possibility that a user could reactivate a token after it had
`deactivated itself because the expiration date was reached
`or for other reasons. Preventing this error from being
`incorporated into a relea