ApplicationsofLogicinComputerSecurity逻辑在计算机安全中的应用

《ApplicationsofLogicinComputerSecurity逻辑在计算机安全中的应用》由会员分享，可在线阅读，更多相关《ApplicationsofLogicinComputerSecurity逻辑在计算机安全中的应用（21页珍藏版）》请在装配图网上搜索。

1、Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,Applications of Logic in Computer Security,Jonathan Millen,SRI International,Areas of Application,Multilevel Operating System Security,“Orange Book,Commercial Trusted Product Evaluat

2、ion,A1-level,Emphasis on secrecy,security/clearance levels,Access Control Policies,Discretionary or role-based policies,Emphasis on application-specific policies,integrity,Public-Key Infrastructure and Trust Management,Network and distributed system security,Digitally signed certificates for identit

3、y and privileges,Cryptographic Authentication Protocols,For network communication confidentiality and authentication,Other areas:databases,firewalls/routers,intrusion detection,Computer Security,Network Security,Contributions of Logic,Undecidability Results,Safety problem for discretionary access co

4、ntrol,Cryptographic protocol analysis,Theorem Proving Environments,Verifying correctness of formal OS specifications,Inductive proofs of cryptographic protocols,Logic Programming,Prolog programs for cryptographic protocol analysis,trust management,Model Checking,For cryptographic protocol analysis,S

5、pecialized Logics,For cryptographic protocol analysis,trust management,Multilevel Operating System Security,Motivated by protection of classified information in shared systems,High-assurance(A1)systems may protect Secret data from uncleared users,Architecture:trusted OS kernel,hardware support,Abstr

6、act system model of access control:Bell-LaPadula(ca.1975),Structured state-transition system:subject-object access matrix,levels,Security invariants and transition rules(for OS functions),“Formal Top-Level Specification(FTLS),More detailed state-transition system,Formal Proofs:,Model transitions sat

7、isfy invariants,FTLS is an interpretation of the system model,Carried out in environments like Gypsy,FDM,HDM,Some FTLS errors reflected in code were discovered,Of Historical Interest,Access Control Policies,Safety Problem,Subject-object-rights matrix,“rights were arbitrary,representing different kin

8、ds of access,Operations:create/delete subjects,objects;enter/remove rights,System of conditional rules to apply operations,Harrison-Ruzzo-Ullman Undecidability Result,Whether S can ever receive right r to object O,Comm.ACM 19(8),1976,Decidable if number of subjects is bounded,Historical Impact,Led t

9、o interest in efficiently decidable systems,Take-Grant,DAC,RBAC,O,j,S,i,r,Public-Key Certificates,Based on asymmetric encryption,Key pair KA,KA-1:one made public,one kept secret,Text block encrypted with KA can be decrypted only with KA-1.,Impractical to compute secret key from public key,Digital si

10、gnature,Text string T,Apply one-way(hash)function,Encrypt with secret key,Verify by decrypting with signers public key,compare hash result,Public Key Certificate,Binds name to public key,signed by trusted party,Logical Equivalent,“A says(KB is the public key of B),provided that KA is the public key

11、of A,T,h(T),h(T)K,A,-1,B,K,B,h(B,K,B,)K,A,-1,Logic of Distributed Authentication,Origination:,“Authentication in distributed systems:theory and practice,by Lampson,Abadi,Burrows,and Wobber,ACM Trans.Comp.Sys.,10(4),1992,Theory of says and speaks for(relation),(A B)(A says s)(B says s)(P8),(A says(B

12、A)(B A)(P10),Application to distributed systems,A and B are principals:users or keys(can say something),A says s means:A authorizes command(operation,access)s,A B means:B delegates authority to A,Certificate T,T KA-1 means KA says T,Public key certificate means KA A,Credentials sent from one network

13、 node to another to authorize resources,Implemented in Taos operating system,“credentials,Trust Management,Policymaker,“Decentralized trust management,Blaze,Feigenbaum,Lacy,1996 IEEE Symposium on Security and Privacy,Identified trust management as a distinct problem,Purpose:to define and implement p

14、olicy using credentials to process queries,Delegation Logic,“A logic-based knowledge representation for Authorization with Delegation,Li,Feigenbaum,Grosof,1999 Computer Security Foundations Workshop,Language to express policies,Primitives include says,delegates(speaks for with object),Access permiss

15、ion is decidable,Logic program implementation(in Datalog),Cryptographic Protocols,Cryptographic protocol,an exchange of messages over an insecure communication medium,using cryptographic transformations to ensure authentication and secrecy of data and keying material.,Applications,military communica

16、tions,business communications,electronic commerce,privacy,Examples,Kerberos:MIT protocol for unitary login to network services,SSL(Secure Socket Layer,used in Web browsers),IPSec:standard suite of Internet protocols due to the IETF,SET(Secure Electronic Transaction)protocol,PGP(Pretty Good Privacy),A Popular Example,The Needham-Schroeder public-key handshake,R.M.Needham and M.D.Schroeder,“Using Encryption for Authentication in Large Networks of Computers,Comm.ACM,Dec.,1978,A B:A,NaKb,B A:Na,NbKa