11Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Using Formal Methodsto Analyze Encryption Protocols2Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009A secure network with encryption uses• Encryption algorithms• Encryption protocols3Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Encryption algorithmconverts clear text into cipher text or cipher text into clear textEncryption protocolA set of rules or procedures for using an encryption algorithm to send and receive messages in a secure manner over a network4Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009ApproachFormally specify – components of the facility– cryptographic operationsExpress desired properties of the protocol as state invariantsVerification system automatically generates the necessary proof obligations to guarantee that the desired properties are preserved5Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Nothing is proved about the encryption algorithms being used6Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Formal SpecificationUsed Ina JoSystem modeled as a state machine– components are state variables and constants– operations are state transitions (transforms in Ina Jo)– Desirable properties are state invariants (criterion in Ina Jo)27Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Example SystemBased on IBM’s System Network Architecture (SNA), which supports session-level cryptographySingle-domain communication system using dynamically generated primary keys and two secret master keys8Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Example SystemSession Keys– One per terminal– Dynamically generated by the host for each session– Primary communication key9Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Variablesession_key(terminal):key10Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Example SystemSession Keys– One per terminal– Dynamically generated by the host for each session– Primary communication keyTerminal Keys– One per terminal– Permanent– Used to distribute new sessions keys11Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Variablesession_key(terminal):keyConstantterminal_key(terminal):key12Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Example SystemSession Keys– One per terminal– Dynamically generated by the host for each session– Primary communication keyTerminal Keys– One per terminal– Permanent– Used to distribute new sessions keysTwo Master KeysKMH0, KMH1313Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Variablesession_key(terminal):keyConstantterminal_key(terminal):key,KMH0, KMH1:key14Analysis of Encryption ProtocolsGCMPSC 266 March 13, 200915Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Terminal keys are stored in the terminal’s cryptographic facilityHost keys are stored in the host’s cryptographic facilityTerminal keys and session keys are stored in the host in encrypted form16Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Terminal keys are stored in the terminal’s cryptographic facilityHost keys are stored in the host’s cryptographic facilityTerminal keys and session keys are stored in the host in encrypted formSession Key Table - current session keys encrypted using KMH0Terminal Key Table - terminal keys encrypted using KMH117Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Session Key Table - current session keys encrypted using KMH0EKMH0(session_key(i))Terminal Key Table - terminal keys encrypted using KMH1EKMH1(terminal_key(i))18Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Operations ProvidedEncipher Data (ECPH)Decipher Data (DCPH)Reencipher From Master Key (RFMK)419Analysis of Encryption ProtocolsGCMPSC 266 March 13, 200920Analysis of Encryption ProtocolsGCMPSC 266 March 13, 200921Analysis of Encryption ProtocolsGCMPSC 266 March 13, 200922Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Generate Session Key OperationNot part of the cryptographic facilityCan use pseudo-random number generator to generate a value interpreted as encrypted version of new session key EKMH0(session_key(j))Meyer-Matayas 198023Analysis of Encryption ProtocolsGCMPSC 266 March 13, 200924Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Variablesession_key(terminal):key,intruder_info:information,keys_used:information525Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Variablesession_key(terminal):key,intruder_info:information,keys_used:informationTransform ECPH(K:key,T:text)EffectN”intruder_info =intruder_info U{Encrypt(Decrypt(KMH0,K),T))}26Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Properties to be assumed about the encryption algorithms are represented as axioms in Ina Jo27Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Properties to be assumed about the encryption algorithms are represented as axioms in Ina JoFor example the commutativity of the encryption and decryption functions would be represented as:Axiom ∀ T:Text, K1,K2:key ( Encrypt(K1,Decrypt(K2,T))= Decrypt(K2,Encrypt(K1,T)) )28Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Analysis TechniqueWrite the formal specificationGenerate the necessary proof obligations to guarantee preservation of the desirable propertiesIf the proof obligations can be proved and the encryption algorithms satisfy the specified axioms, then the system will satisfy its critical requirements29Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Analysis TechniqueWrite the formal specificationGenerate the necessary proof obligations to guarantee preservation of the desirable propertiesIf the proof obligations can be proved and the encryption algorithms satisfy the specified axioms, then the system will satisfy its critical requirementsIf the proofs fail, then the unproved parts of the proof obligations often indicate weaknesses in the protocol or incompleteness in the specification30Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Cryptoanalytic Assumptions• What does the intruder know about the system• What does the intruder observe• What can the intruder do631Analysis of Encryption ProtocolsGCMPSC 266 March 13, 2009Assume the intruder can• Obtain any information communicated between the host and the terminals• Masquerade as an authorized user• Invoke operations of the host’s cryptographic facilities32Analysis of Encryption ProtocolsGCMPSC 266 March