TAOS
UCL Course COMP0133: Distributed Systems and Security LEC-15
Motivations
Design a more general and flexible authentication system
Drawbacks of Simple Authentication Model
which uses digitial signatures based on public key encryption scheme
-
Slow
Public key encryption scheme are expensive and slow
-
Rigid
The \( 2^{nd} \) Machine Problem
If one user wants to SSH into the \( 2^{nd} \) machine, the \( 2^{nd} \) machine also needs to sign its RPCs to server
The \( 2^{nd} \) machine may need to send messages back to the \( 1^{st} \) machine for signing
since only the \( 1^{st} \) machine has the private key (not want the \( 2^{nd} \) machine to store)
Outline
-
Each machine has an identity: \( (K,K^{-1}) \)
-
Alice logs into machine \( X \) will sign certificate: Alice says \( X \) speaks for Alice
English Language
Alice claims that the machine \( X \) is doing execution of code on behalf of Alice
such that others should view things machine \( X \) does as being done by Alice
Security Relationship
Alice signs “\( X \) speaks for Alice” with \( K_{Alice} \)
(using public key \( K_{Alice} \) for shorthand 速记, actually using private key \( K_{Alice}^{-1} \))
such that machine \( X \) does not need to have private key of Alice
Solve the \( 2^{nd} \) Machine Problem
-
I’m \( Y \) —– The \( 2^{nd} \) Machine
-
\( X \) says \( Y \) speaks for Alice
-
Alice says \( X \) speaks for Alice
Drawbacks of SSL/TLS
Although SSL/TLS improve efficiency using symmetric key ciphers for session data
-
Rigid
The \( 2^{nd} \) Machine Problem
SSL/TLS are exactly for two principals (client principal and server principal) tied to channels
If \( X \) says something to \( Y \), \( Y \) can’t prove anything to \( Z \)
If \( X \) closes its connection to \( Y \), \( Y \) can’t verify anything after closing
Only support distributed systems with 2 parties
Advantages of TAOS
-
Certificates are independent of channels
-
Certificates can be stored, passed to other parties
-
Certificates can be used to prove transitive trust relationships (not pairwise trust relationships)
Axioms in TAOS Logic
speaks for Axiom
IF
(\( A \) speaks for \( B \)) AND (\( A \) says \( S \))
THEN
\( B \) says \( S \)
Handoff Axiom
IF
\( A \) says (\( B \) speaks for \( A \))
THEN
(\( B \) speaks for \( A \))
Delegation Axiom (precise type of Handoff Axiom)
IF
\( A \) says ((\( B \) | \( A \)) speaks for (\( B \) for \( A \)))
THEN
(\( B \) | \( A \)) speaks for (\( B \) for \( A \))
Combine Together
Combine speaks for and Handoff Together
IF
(\( A \) says (\( B \) speaks for \( A \))) AND (\( B \) says \( S \))
THEN
(\( B \) speaks for \( A \)) AND (\( B \) says \( S \))
THEN
\( A \) says \( S \)
Combine speaks for and Delegation Together
IF
(\( A \) says (\( B \) | \( A \)) speaks for (\( B \) for \( A \))) AND (\( B \) says \( A \) says \( S \))
THEN
((\( B \) | \( A \)) speaks for (\( B \) for \( A \))) AND (\( B \) says \( A \) says \( S \))
THEN
(\( B \) for \( A \)) says \( S \)
Compare two combination: Delegation is more specific than Handoff
since Delegation involves both delegator \( A \) and delegate \( B \) (while Handoff only involves delegator \( A \))
which is helpful and important for auditing
Example
Scenario
-
User Bob logs into workstation WS
-
TAOS logic used to authenticate requests from Bob’s login session to a remote file server FS
Principals
-
Workstation firmware 固件
-
OS
-
Bob
-
Channel
Keep track
-
who knows private keys
-
who knows signed certificates
-
who knows channel keys
State Before Bob Logs in
-
Workstation firmware knows \( K_{vax4} \)
-
User knows \( K_{Bob} \)’s private “half”
-
File server has \( K_{Bob} \)’s public “half” in an ACL
Workstation Boot Time
-
Workstation firmware generates fresh public/private key \( K_{ws} \)
Why not use \( K_{vax4} \) directly?
Don’t want it to be stolen
Don’t want statements (i.e., certificates generated for login sessions) to survive reboot (temporary identity)
-
Workstation firmware signs
\( K_{vax4} \) says (\( K_{ws} \) speaks for \( K_{vax4} \)) —– Handoff
such that \( K_{vax4} \) will nerver be used again until reboot
Why preserve \( K_{vax4} \) identity?
Want workstation identity to survive reboot (long-term identity)
-
In assigned paper
(\( K_{vax4} \) as OS) says (\( K_{ws} \) speaks for (\( K_{vax4} \) as OS)) —– Handoff
Why use (\( K_{vax4} \) as OS)?
User might not trust some versions of OS, or some OS
Want to allow OS type/version to be visible in ACLs
Assuming a role amounts to reducing access rights
Keep Tracking: Now vax4’s authentication agent knows
-
\( K_{ws} \) (but forgets \( K_{vax4} \))
-
(\( K_{vax4} \) as OS) says (\( K_{ws} \) speaks for (\( K_{vax4} \) as OS))
User Login
Treat login as a specialized form of delegation
such that the machine vax4 can be delegated by user Bob (who does not want vax4 to know his private key)
therefore, the machine vax4 needs an identity in this authentication
-
When Bob logs in
\( K_{Bob} \) says ((\( K_{ws} \) | \( K_{Bob} \)) speaks for (\( K_{ws} \) for \( K_{Bob} \))) —– Delegation
such that \( K_{Bob} \) will nerver be used again until his next login
Why here not use Handoff : \( K_{Bob} \) says (\( K_{ws} \) speaks for \( K_{Bob} \)) ?
If the following statements signed by \( K_{ws} \) are ambiguous, it may be usable out of context (misused in some way)
Note
-
\( A \) | \( B \) is \( A \) quoting\( B \) which means A is claiming (no proof yet) that \( A \) is speaking for \( B \): if \( A \) says \( B \) says \( S \), then (\( A \) | \( B \)) says S
-
\( A \) for \( B \) is stronger than \( A \) | \( B \) which means it is the logical conclusion that A is allowed to speak for \( B \):
if \( A \) says \( B \) says \( S \) and \( A \) is authorized to act as \( B \)’s delegate, then (\( A \) for \( B \)) says S
which is usually used in \( A \) | \( B \) with delegation
-
Keep Tracking: Now vax4’s authentication agent knows
-
\( K_{ws} \)
-
(\( K_{vax4} \) as OS) says (\( K_{ws} \) speaks for (\( K_{vax4} \) as OS))
-
\( K_{Bob} \) says ((\( K_{ws} \) | \( K_{Bob} \)) speaks for (\( K_{ws} \) for \( K_{Bob} \)))
Request from Login Session to File server
A channel \( C_{Bob} \) exists to issue the request
-
TAOS uses symmetric-key ciphers to encrypt channels between hosts
-
Channels named by their symmetric key
-
\( C_{Bob} \) doesn’t imply anything about Bob
which is only a mnemonic 助记符 used by authors to indicate intent that \( C_{Bob} \) carries messages from Bob
System must establish proof that this is case
Keep Tracking: File server knows
-
\( C_{Bob} \) says \( RQ \)
where \( RQ \) is a file server request
which means the received request from someone who knows key \( C_{Bob} \)
Channel Certificate
-
Workstation firmware signs channel certificate
when channel between workstation firmware and file server first created
(\( K_{ws} \) | \( K_{Bob} \)) says (\( C_{Bob} \) speaks for (\( K_{ws} \) for \( K_{Bob} \))) —— Delegation
Aim: Link \( RQ \) encrypted with \( C_{Bob} \) to user Bob
Why not \( K_{Bob} \) says (\( C_{Bob} \) speaks for \( K_{Bob} \))?
This is what SSL/TLS client-side certificates do
But in TAOS, authentication agent doesn’t hold \( K_{Bob} \)’s private half
Why not \( K_{ws} \) says (\( C_{Bob} \) speaks for \( K_{ws} \))?
\( C_{Bob} \) doesn’t speak for \( K_{ws} \) in general and only for \( K_{Bob} \)
Authentication Proof
After workstation firmware sends all certificates to file server
Keep Tracking: file server knows
-
(\( K_{vax4} \) as OS) says (\( K_{ws} \) speaks for (\( K_{vax4} \) as OS)) —– (1)
-
\( K_{Bob} \) says ((\( K_{ws} \) | \( K_{Bob} \)) speaks for (\( K_{ws} \) for \( K_{Bob} \))) —– (2)
-
(\( K_{ws} \) | \( K_{Bob} \)) says (\( C_{Bob} \) speaks for (\( K_{ws} \) for \( K_{Bob} \))) —– (3)
-
\( C_{Bob} \) says \( RQ \) —– (4)
Proof
Delegation Axiom
IF (2)
\( K_{Bob} \) says ((\( K_{ws} \) | \( K_{Bob} \)) speaks for (\( K_{ws} \) for \( K_{Bob} \)))
THEN
(\( K_{ws} \) | \( K_{Bob} \)) speaks for (\( K_{ws} \) for \( K_{Bob} \)) —– (5)
speaks for Axiom
IF (3)
(\( K_{ws} \) | \( K_{Bob} \)) says (\( C_{Bob} \) speaks for (\( K_{ws} \) for \( K_{Bob} \)))
AND (5)
(\( K_{ws} \) | \( K_{Bob} \)) speaks for (\( K_{ws} \) for \( K_{Bob} \))
THEN
(\( K_{ws} \) for \( K_{Bob} \)) says (\( C_{Bob} \) speaks for (\( K_{ws} \) for \( K_{Bob} \))) —– (6)
Handoff Axiom
IF (6)
(\( K_{ws} \) for \( K_{Bob} \)) says (\( C_{Bob} \) speaks for (\( K_{ws} \) for \( K_{Bob} \)))
THEN
\( C_{Bob} \) speaks for (\( K_{ws} \) for \( K_{Bob} \)) —– (7)
speaks for Axiom
IF (4)
\( C_{Bob} \) says \( RQ \)
AND (7)
\( C_{Bob} \) speaks for (\( K_{ws} \) for \( K_{Bob} \))
THEN
(\( K_{ws} \) for \( K_{Bob} \)) says \( RQ \) —– (8)