Enhancing Authorization in Alpaca: A Decade-old Approach Revisited

 
Extensible proof-carrying
authorization in 
Alpaca
 
October 31, 2007
ACM CCS – Alexandria, VA
 
Chris Lesniewski-Laas
, Bryan Ford, Jacob Strauss,
Robert Morris, and M. Frans Kaashoek
MIT
Authorization proliferation
 
 
“Peggy”
Carol
 
Carol
 
Peggy
 
Authorization proliferation
 
“Peggy”
Carol
 
Victor
 
 
“MIT”
put(
)
?
Peggy
 
Authorization proliferation
 
“Peggy”
Carol
 
Victor
 
“MIT”
put(
)
“Peggy@MIT”
 
put(
)
Peggy
 
Authorization proliferation
 
“Peggy”
Carol
 
Victor
 
“MIT”
?
MIT!
put(
)
put(
)
Peggy
 
Solution approach
 
“Peggy”
Carol
 
Victor
 
“MIT”
put(
)
?
DSA for
Dummies
Peggy
@MIT!
 
How do we build this?
Peggy
 
Our system: Alpaca
 
Logic-based authentication framework
Bridges the gaps between PKIs
Verifier doesn’t know details of prover’s PKI
 
Carol
 
Victor
 
put(
)
Peggy
DSA for
Dummies
put(
x
)
put(
x
)
put(
)
Proof-carrying authorization
Appel, Felten. 
PCA
. In CCS 1999
Requests are logical formulas
Credentials are proofs of logical formulas
flexible certificates, delegation policy
 
Victor
 
request:
 formula 
[Peggy 
says
 put(
)]
Peggy
(says 
Peggy
 (apply ‘put
 bytes
))
credential:
 
proof of 
[Peggy 
says
 put(
)]
(speaks-for-elim (axiom 
p
.K
ca
p
) (…) )
(axiom 
p
.K
ca
p
)
speaks-for-elim
Alpaca’s new techniques
“Dynamic” principals defined by logical rules
Signatures built from more elementary primitives
Enables Victor’s Alpaca PKI to check foreign
signatures and credentials
 
Victor
 
request:
 formula 
[Peggy 
says
 put(
)]
Peggy
(says 
Peggy
 (apply ‘put
 bytes
))
credential:
 
proof of 
[Peggy 
says
 put(
)]
(speaks-for-elim (axiom 
p
.K
ca
p
) (…) )
Peggy
P
rincipals
 are name chains A/N/M
 
Built-in “authorities”
emit statements defined by axiom schema
e.g., 
math
 authority: emit 1+1=2, 2
3
 mod 7 = 1, …
 
 
Name (role) connective A/N
A
 is a principal, 
N
 is a name (“Peggy”, 0x96, tuple)
Proof checker rule: A 
speaks for
 A/N
A controls all principals A/N/M/… (A’s “sandbox”)
math
 
Bootstrap familiar principals
 
Built-in “authorities”
Name (role) connective A/B
Bootstrap other principal types
Public key 
K
a
 (emits statements signed by K
a
)
User name (“Peggy”)
Compound names (“localname@domain.com”, “Dad’s
dentist”, …)
others (see paper)
 
Key principals defined by 
rsa
 authority
 
Goal:
if
 K
n,e
 is an RSA key,
and
 K
n,e
-1
 signs repr[
𝜑
],
then
 can construct proof of [K
n,e
 
says
 
𝜑
].
Key principals defined by 
rsa
 authority
 
Goal: 
if
 K
n,e
 is an RSA key, 
and
 K
n,e
-1
 signs repr[
𝜑
],
then
 can prove [K
n,e
 
says
 
𝜑
].
Principal K
n,e
 
 expression 
rsa
/n,e
(/ ‘rsa (cons 0x8f1f… 0x10001))
rsa
 authority contains one axiom
*
:
rsa 
says
(
σ
e
 = 
𝜑
 (mod n))   
   
rsa
/n,e 
says
 
𝜑
 
uses [
rsa
 
 
rsa
/n,e]
σ
e
 = 
𝜑
 (mod n)
rsa
/n,e 
says
 
𝜑
 
iff RSA-Verify(
𝜑
, K
n,e
, 
σ
)
 
Goal
Credential = signature + proof tree
 
Peggy
Victor
 
K
p
 
says
 put(
)
proof of 
[K
p
 
says
 put(
)]
Compose proof tree:
axiom [
math
 
says
 
σ
e
 
 
𝜑
 (mod n)]
+ axiom [
rsa 
says
(
σ
e
 
 
𝜑
 (mod n)) 
 
rsa
/n,e 
says
 
𝜑
]
+ 
substitute
 
𝜑
 
= repr [
 put(
) 
]
+ 
implies-eliminate
, …
= proof of:                                    [
rsa
/n,e 
says
 put(
)]
Compute:
𝜑
 
= repr [
 put(
) 
]
σ
 
= 
𝜑
1/e
 mod n
Checks axioms
and
proof steps
 
Not everyone uses RSA signatures
Victor doesn’t want all algorithms in TCB
rsa
/n,e: could be K
carol
 or anyone else
Bootstrap from one-time-pad authenticator
Victor starts with just OTP
Signed statement:
“meta-credential”
Built-in
authority
Bootstrap other crypto from RSA
rsa
/n,e 
 
dsa
Certificates and CAs
 
Goal: bind “Peggy” to K
p
 (attested by K
ca
)
Using K
ca
-1
, sign formula [K
p
 
 K
ca
/“Peggy”]
“K
p
 
speaks for
 K
ca
’s name 
Peggy
Proof is a certificate!
Nothing special about K
ca
users or apps choose namespaces to use by, e.g.,
adopting axioms 
x
. K
ca
/
x
 
 K
user
/
x
Credential = signature + certificate +
proof tree
 
Peggy
Victor
 
K
ca
/“Peggy” 
says
 put(
)
proof of 
[K
ca
/“Peggy” 
says
 put(
)]
Compose proof tree:
Incorporate RSA signature proof…
subproof of: [K
p
 
says
 
K
ca
/“Peggy” 
says 
put(
)
]
+ subproof of: [
K
p
 
 K
ca
/“Peggy”]
+ 
speaks-for-rule
, …
= proof of:                  [
K
ca
/“Peggy” 
says
 put(
)]
Compute:
𝜑
 
= repr [
K
ca
/“Peggy” 
says 
put(
)
]
σ
 
= 
𝜑
1/e
 mod n
Checks axioms
and
proof steps
Carol
 
 
Policy in the logic: authorization
 
Can roll access control into logic
ACL entries could be
( K
ca
/“Peggy” 
says
 put(
x
) ) 
 put(
x
)
 
Requires Peggy to prove [put(
)]:
First prove [K
ca
/“Peggy” 
says
 put(
)]
Then combine with ACL (or other policy logic) to
get [put(
)]
 
See, e.g., DCC [Abadi 2006] for variations
Credential = signature + certificate +
policy + proof tree
 
Peggy
Victor
 
put(
)
proof of 
[put(
)]
Compose proof tree:
Blah blah blah…
[proof from some credential]
+ [maybe some axioms
]
+ 
deductive rules
, …
= proof of:                          [
put(
)]
Compute:
𝜑
 
= repr [
K
ca
/“Peggy” 
says 
put(
)
]
σ
 
= 
𝜑
1/e
 mod n
Checks axioms
and
proof steps
Foreign credentials
 
Carol
 
Victor
 
 
Alpaca: [K
ca
“MIT”]
put(
)
Peggy@MIT
says to
put(
)
!
 
X
.
5
0
9
 
f
o
r
D
u
m
m
i
e
s
Peggy
 
Alpaca can use foreign credentials
 
Carol publishes X.509 meta-credential:
 
 
 
 
 
 
Now Peggy can present X.509 cert to Victor
What if MIT uses DSA certificates?
K
ca
 
says
 
 x509 : 
str
.
 
signed
( K
ca
, x509 ) 
 
(n,e) = RSAPK(x509) 
 
name = CN(x509) 
  
rsa
/n,e 
 
K
ca
/name
Alpaca can use foreign credentials
 
Carol publishes X.509 meta-credential:
 
 
 
 
+ DSA meta-credential:
 
Now Peggy can present X.509 cert to Victor
using DSA private key to sign requests
K
ca
 
says
 
 x509 : 
str
.
 
signed
( K
ca
, x509 ) 
 
(p,q,g,y) = DSAPK(x509) 
 
name = CN(x509) 
  
K
ca
/
dsa
/p,q,g,y 
 
K
ca
/name
K
ca
 
says 
(r = g
𝜑
/s
y
r/s
 (mod p)) 
 
K
ca
/
dsa
/p,q,g,y 
says
 
𝜑
 
not built-in
authority
 
Other cool things Alpaca can do
 
Policy
restricted delegation
conjunctive/disjunctive
 principals
flexible quota assignment policies
PKI namespace structures (SPKI, hash-IDs, …)
Enabling incremental improvements
encoding (padding, batching, hash chains, …)
vanilla
 
SHA,
 
RSA
 
 wizzbang
 new crypto (IBE, …)
secure
 root of trust for updates: one-time MAC
 
Implementation features (in paper)
 
Python library and API
3500 non-blank LOC (TCB: 800 LOC)
Proof construction language
Efficient sandboxed computations
Hashing as fast as native evaluation
Replay protection (nonces)
Integrated with UIA name system
 
Future directions
 
What’s nice about Alpaca right now?
Apps 
can
 say new things with logic
Flexibly specify 
who
 holds credential and delimit
what
 they can do with it
What’s still to do?
Meta-credentials n
eed to be self-describing
How
 to use this credential?
Why
 is this credential valid?
 
Related work
 
Proof-carrying (authorization|code)
Logic of authorization (BAN, TAOS, ABLP, DCC)
Decentralized PKI (SPKI/SDSI)
Mobile code (Active certificates)
P
olicy languages
 (SecPAL, Binder, Daisy, SD3,
RT, …)
 
Summary
 
Alpaca: a logic-based authorization framework
introduces “dynamic” principals
decentralizes definition of authorization rules
extensible PKI, signatures, hashes, credentials
flexible delegation and access control policy
 
Make logic an explicit part of wire protocols
request :: formula, credential :: proof
enables incremental improvement of PKI
 
http://pdos.csail.mit.edu/alpaca/
Slide Note
Embed
Share

The research led by Chris Lesniewski-Laas et al. in 2007 proposed extensible proof-carrying authorization in Alpaca, addressing the challenges of authorization proliferation and introducing innovative solutions in logic-based authentication, bridging PKI gaps, and dynamic principals in PKI systems. The study explores PCA, logical formulas for requests, and Alpaca's techniques for checking foreign signatures and credentials. It highlights the advancements in proof-carrying authorization and its relevance in modern PKI frameworks.


Uploaded on Sep 02, 2024 | 0 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

E N D

Presentation Transcript


  1. Extensible proof-carrying authorization in Alpaca October 31, 2007 ACM CCS Alexandria, VA Chris Lesniewski-Laas, Bryan Ford, Jacob Strauss, Robert Morris, and M. Frans Kaashoek MIT

  2. Authorization proliferation Carol Peggy Peggy

  3. Authorization proliferation MIT Carol Victor ? Peggy Peggy put( )

  4. Authorization proliferation MIT Carol Victor Peggy@MIT Peggy Peggy put( ) put( )

  5. Authorization proliferation MIT Carol Victor ? put( ) MIT! Peggy Peggy put( )

  6. Solution approach MIT Carol Victor ? DSA for Dummies Peggy @MIT! Peggy How do we build this? Peggy put( )

  7. Our system: Alpaca Logic-based authentication framework Bridges the gaps between PKIs Verifier doesn t know details of prover s PKI Carol Victor put( ) DSA for Dummies put(x) put(x) DSA for Dummies put(x) put(x) put( ) Peggy put( ) put( )

  8. Proof-carrying authorization Appel, Felten. PCA. In CCS 1999 Requests are logical formulas Credentials are proofs of logical formulas flexible certificates, delegation policy Peggy Victor request: formula [Peggy says put( )] (says Peggy(apply put bytes )) credential: proof of [Peggy says put( )] (speaks-for-elim (axiom p.Kca p) ( ) ) (axiom p.Kca p) speaks-for-elim

  9. Alpacas new techniques Dynamic principals defined by logical rules Signatures built from more elementary primitives Enables Victor s Alpaca PKI to check foreign signatures and credentials Peggy Victor request: formula [Peggy says put( )] (says Peggy(apply put bytes )) Peggy credential: proof of [Peggy says put( )] (speaks-for-elim (axiom p.Kca p) ( ) )

  10. Principals are name chains A/N/M Built-in authorities emit statements defined by axiom schema e.g., math authority: emit 1+1=2, 23mod 7 = 1, math mathsays 1+1=2 (axiom math (= (+ 1 1) 2)) Name (role) connective A/N A is a principal, Nis a name ( Peggy , 0x96, tuple) Proof checker rule: A speaks for A/N A controls all principals A/N/M/ (A s sandbox )

  11. Bootstrap familiar principals Built-in authorities Name (role) connective A/B Bootstrap other principal types Public key Ka (emits statements signed by Ka) User name ( Peggy ) Compound names ( localname@domain.com , Dad s dentist , ) others (see paper)

  12. Key principals defined by rsa authority Goal: if Kn,e is an RSA key, and Kn,e-1 signs repr[?], then can construct proof of [Kn,esays?].

  13. Key principals defined by rsa authority Goal: if Kn,e is an RSA key, and Kn,e-1 signs repr[?], then can prove [Kn,esays?]. Principal Kn,e expression rsa/n,e (/ rsa (cons 0x8f1f 0x10001)) rsa authority contains one axiom*: e = ? (mod n) iff RSA-Verify(?, Kn,e, ) uses [rsa rsa/n,e] rsa says ( e = ? (mod n)) rsa/n,e says? Goal rsa/n,e says?

  14. Credential = signature + proof tree Peggy Victor Kpsays put( ) proof of [Kpsays put( )] Compute: ? = repr [ put( ) ] = ?1/e mod n Compose proof tree: axiom [mathsays e ? (mod n)] + axiom [rsa says( e ? (mod n)) rsa/n,e says?] + substitute? = repr [ put( ) ] + implies-eliminate, = proof of: [rsa/n,e says put( )] Checks axioms and proof steps [rsa/n,e says put( )]

  15. Bootstrap other crypto from RSA Built-in authority (?e = ? (mod n)) says? rsa says rsa/n,e says (r = g?/syr/s (mod p)) dsa/p,q,g,y says? dsa rsa/n,e says (r = g?/syr/s (mod p)) rsa/n,e/p,q,g,y says? Signed statement: meta-credential rsa/n,e dsa Not everyone uses RSA signatures Victor doesn t want all algorithms in TCB rsa/n,e: could be Kcarol or anyone else Bootstrap from one-time-pad authenticator Victor starts with just OTP

  16. Certificates and CAs Goal: bind Peggy to Kp (attested by Kca) Using Kca-1, sign formula [Kp Kca/ Peggy ] Kpspeaks for Kca s name Peggy Proof is a certificate! Nothing special about Kca users or apps choose namespaces to use by, e.g., adopting axioms x. Kca/x Kuser/x

  17. Credential = signature + certificate + proof tree Peggy Carol Victor Kca/ Peggy says put( ) proof of [Kca/ Peggy says put( )] Compute: ? = repr [Kca/ Peggy says put( )] = ?1/e mod n Compose proof tree: Incorporate RSA signature proof subproof of: [Kpsays Kca/ Peggy says put( )] + subproof of: [Kp Kca/ Peggy ] + speaks-for-rule, = proof of: [Kca/ Peggy says put( )] [rsa/n,eca/ Peggy says put( )] Checks axioms and proof steps

  18. Policy in the logic: authorization Can roll access control into logic ACL entries could be ( Kca/ Peggy says put(x) ) put(x) Requires Peggy to prove [put( )]: First prove [Kca/ Peggy says put( )] Then combine with ACL (or other policy logic) to get [put( )] See, e.g., DCC [Abadi 2006] for variations

  19. Credential = signature + certificate + policy + proof tree Peggy Victor put( ) proof of [put( )] Compute: ? = repr [Kca/ Peggy says put( )] = ?1/e mod n Compose proof tree: Blah blah blah [proof from some credential] + [maybe some axioms] + deductive rules, = proof of: [put( )] Checks axioms and proof steps [put( )]

  20. Foreign credentials Alpaca: [Kca MIT ] Carol Victor X.509 for Dummies Peggy@MIT says to put( )! X.509 cert { CN= Peggy , RSAPK=(n,e) }Kca Peggy put( )

  21. Alpaca can use foreign credentials Carol publishes X.509 meta-credential: Kcasays x509 : str. signed( Kca, x509 ) (n,e) = RSAPK(x509) name = CN(x509) rsa/n,e Kca/name Now Peggy can present X.509 cert to Victor What if MIT uses DSA certificates?

  22. Alpaca can use foreign credentials Carol publishes X.509 meta-credential: Kcasays x509 : str. signed( Kca, x509 ) (p,q,g,y) = DSAPK(x509) name = CN(x509) Kca/dsa/p,q,g,y Kca/name not built-in authority + DSA meta-credential: Kcasays (r = g?/syr/s (mod p)) Kca/dsa/p,q,g,y says? Now Peggy can present X.509 cert to Victor using DSA private key to sign requests

  23. Other cool things Alpaca can do Policy restricted delegation conjunctive/disjunctive principals flexible quota assignment policies PKI namespace structures (SPKI, hash-IDs, ) Enabling incremental improvements encoding (padding, batching, hash chains, ) vanilla SHA, RSA wizzbang new crypto (IBE, ) secure root of trust for updates: one-time MAC

  24. Implementation features (in paper) Python library and API 3500 non-blank LOC (TCB: 800 LOC) Proof construction language Efficient sandboxed computations Hashing as fast as native evaluation Replay protection (nonces) Integrated with UIA name system

  25. Future directions What s nice about Alpaca right now? Apps can say new things with logic Flexibly specify who holds credential and delimit what they can do with it What s still to do? Meta-credentials need to be self-describing How to use this credential? Why is this credential valid?

  26. Related work Proof-carrying (authorization|code) Logic of authorization (BAN, TAOS, ABLP, DCC) Decentralized PKI (SPKI/SDSI) Mobile code (Active certificates) Policy languages (SecPAL, Binder, Daisy, SD3, RT, )

  27. Summary Alpaca: a logic-based authorization framework introduces dynamic principals decentralizes definition of authorization rules extensible PKI, signatures, hashes, credentials flexible delegation and access control policy Make logic an explicit part of wire protocols request :: formula, credential :: proof enables incremental improvement of PKI http://pdos.csail.mit.edu/alpaca/

Related


More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#